From b835cddcf1129920608cebafbad2f9a94b8064f7 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Sun, 4 Aug 2024 23:23:20 +0200 Subject: [PATCH] initial MorphismBase with DFS to find morphism paths --- src/lib.rs | 1 + src/morphism.rs | 204 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 205 insertions(+) create mode 100644 src/morphism.rs diff --git a/src/lib.rs b/src/lib.rs index 970c555..00821d4 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -10,6 +10,7 @@ pub mod lnf; pub mod pnf; pub mod subtype; pub mod unification; +pub mod morphism; #[cfg(test)] mod test; diff --git a/src/morphism.rs b/src/morphism.rs new file mode 100644 index 0000000..31a8e31 --- /dev/null +++ b/src/morphism.rs @@ -0,0 +1,204 @@ +use { + crate::{ + TypeTerm, TypeID, + unification::UnificationProblem, + }, + std::collections::HashMap +}; + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ + +pub struct MorphismType { + pub src_type: TypeTerm, + pub dst_type: TypeTerm, +} + +pub struct MorphismBase { + morphisms: Vec< (MorphismType, Morphism) >, + list_typeid: TypeID +} + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ + +impl MorphismType { + fn normalize(self) -> Self { + MorphismType { + src_type: self.src_type.normalize(), + dst_type: self.dst_type.normalize() + } + } +} + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ + +impl MorphismBase { + pub fn new() -> Self { + MorphismBase { + morphisms: Vec::new(), + + // FIXME: magic number + list_typeid: TypeID::Fun(10) + } + } + + pub fn add_morphism(&mut self, morph_type: MorphismType, morphism: Morphism) { + self.morphisms.push( (morph_type.normalize(), morphism) ); + } + + pub fn enum_morphisms(&self, src_type: &TypeTerm) + -> Vec< (HashMap, TypeTerm) > + { + let mut dst_types = Vec::new(); + + // first enumerate all "direct" morphisms, + for (ty,m) in self.morphisms.iter() { + if let Ok(σ) = crate::unification::unify( + &ty.src_type, + &src_type.clone().normalize() + ) { + let dst_type = + ty.dst_type.clone() + .apply_substitution( + &|x| σ.get(x).cloned() + ) + .clone(); + + dst_types.push( (σ, dst_type) ); + } + } + + // ..then all "list-map" morphisms. + // Check if we have a List type, and if so, see what the Item type is + + // TODO: function for generating fresh variables + let item_variable = TypeID::Var(100); + + if let Ok(σ) = crate::unification::unify( + &TypeTerm::App(vec![ + TypeTerm::TypeID(self.list_typeid), + TypeTerm::TypeID(item_variable) + ]), + &src_type.clone().param_normalize(), + ) { + let src_item_type = σ.get(&item_variable).unwrap().clone(); + + for (γ, dst_item_type) in self.enum_morphisms( &src_item_type ) { + let dst_type = + TypeTerm::App(vec![ + TypeTerm::TypeID(self.list_typeid), + dst_item_type.clone() + .apply_substitution( + &|x| γ.get(x).cloned() + ).clone() + ]).normalize(); + + dst_types.push( (γ.clone(), dst_type) ); + } + } + + dst_types + } + + pub fn enum_morphisms_with_subtyping(&self, src_type: &TypeTerm) + -> Vec< (TypeTerm, TypeTerm) > + { + let mut src_lnf = src_type.clone().get_lnf_vec(); + let mut halo_lnf = vec![]; + let mut dst_types = Vec::new(); + + while src_lnf.len() > 0 { + let src_type = TypeTerm::Ladder( src_lnf.clone() ); + let halo_type = TypeTerm::Ladder( halo_lnf.clone() ); + + for (σ, t) in self.enum_morphisms( &src_type ) { + dst_types.push( + (halo_type.clone() + .apply_substitution( + &|x| σ.get(x).cloned() + ).clone(), + t.clone() + .apply_substitution( + &|x| σ.get(x).cloned() + ).clone() + ) + ); + } + + // continue with next supertype + halo_lnf.push(src_lnf.remove(0)); + } + + dst_types + } + + /* performs DFS to find a morphism-path for a given type + * will return the first matching path, not the shortest + */ + pub fn find_morphism_path(&self, ty: MorphismType) + -> Option< Vec > + { + let ty = ty.normalize(); + let mut visited = Vec::new(); + let mut queue = vec![ + vec![ ty.src_type.clone().normalize() ] + ]; + + while let Some(current_path) = queue.pop() { + let current_type = current_path.last().unwrap(); + + if ! visited.contains( current_type ) { + visited.push( current_type.clone() ); + + for (h, t) in self.enum_morphisms_with_subtyping(¤t_type) { + let tt = TypeTerm::Ladder( vec![ h, t ] ).normalize(); + + if ! visited.contains( &tt ) { + let unification_result = crate::unification::unify(&tt, &ty.dst_type); + let mut new_path = current_path.clone(); + + new_path.push( tt ); + + if let Ok(σ) = unification_result { + new_path = new_path.into_iter().map( + |mut t: TypeTerm| t.apply_substitution(&|x| σ.get(x).cloned()).clone() + ).collect::>(); + + return Some(new_path); + } else { + queue.push( new_path ); + } + } + } + } + } + + None + } + + pub fn find_morphism(&self, ty: &MorphismType) + -> Option< Morphism > { + + // TODO + + None + } + + pub fn find_list_map_morphism(&self, item_ty: &MorphismType) + -> Option< Morphism > { + + // TODO + + None + } + + pub fn find_morphism_with_subtyping(&self, ty: &MorphismType) + -> Option<( Morphism, TypeTerm, HashMap )> { + + // TODO + + None + } +} + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ +