From 811adde1b9a095801056b9898cb1f99708484c2d Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Mon, 5 Aug 2024 02:54:35 +0200 Subject: [PATCH] turn Morphism into trait and add find_morphism() function --- src/lib.rs | 3 +- src/morphism.rs | 91 +++++++++++++++++++++++++++++++++----------- src/test/morphism.rs | 53 +++++++++++++++++--------- 3 files changed, 106 insertions(+), 41 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 00821d4..bf775b4 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -18,6 +18,7 @@ mod test; pub use { dict::*, term::*, - unification::* + unification::*, + morphism::* }; diff --git a/src/morphism.rs b/src/morphism.rs index 6b921bf..3211651 100644 --- a/src/morphism.rs +++ b/src/morphism.rs @@ -8,20 +8,27 @@ use { //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ +#[derive(Clone, PartialEq, Eq, Debug)] pub struct MorphismType { pub src_type: TypeTerm, pub dst_type: TypeTerm, } -pub struct MorphismBase { - morphisms: Vec< (MorphismType, Morphism) >, +pub trait Morphism : Sized { + fn get_type(&self) -> MorphismType; + fn list_map_morphism(&self, list_typeid: TypeID) -> Option< Self >; +} + +#[derive(Clone)] +pub struct MorphismBase { + morphisms: Vec< M >, list_typeid: TypeID } //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ impl MorphismType { - fn normalize(self) -> Self { + pub fn normalize(self) -> Self { MorphismType { src_type: self.src_type.normalize(), dst_type: self.dst_type.normalize() @@ -31,7 +38,7 @@ impl MorphismType { //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ -impl MorphismBase { +impl MorphismBase { pub fn new(list_typeid: TypeID) -> Self { MorphismBase { morphisms: Vec::new(), @@ -39,8 +46,8 @@ impl MorphismBase { } } - pub fn add_morphism(&mut self, morph_type: MorphismType, morphism: Morphism) { - self.morphisms.push( (morph_type.normalize(), morphism) ); + pub fn add_morphism(&mut self, m: M) { + self.morphisms.push( m ); } pub fn enum_morphisms(&self, src_type: &TypeTerm) @@ -49,17 +56,15 @@ impl MorphismBase { let mut dst_types = Vec::new(); // first enumerate all "direct" morphisms, - for (ty,m) in self.morphisms.iter() { + for m in self.morphisms.iter() { if let Ok(σ) = crate::unification::unify( - &ty.src_type, + &m.get_type().src_type, &src_type.clone().normalize() ) { let dst_type = - ty.dst_type.clone() - .apply_substitution( - &|x| σ.get(x).cloned() - ) - .clone(); + m.get_type().dst_type.clone() + .apply_substitution( &|x| σ.get(x).cloned() ) + .clone(); dst_types.push( (σ, dst_type) ); } @@ -173,26 +178,68 @@ impl MorphismBase { None } + pub fn find_morphism(&self, ty: &MorphismType) - -> Option< Morphism > { + -> Option< ( M, HashMap ) > { - // TODO + // try list-map morphism + if let Ok(σ) = UnificationProblem::new(vec![ + (ty.src_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(self.list_typeid), TypeTerm::TypeID(TypeID::Var(100)) ])), + (ty.dst_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(self.list_typeid), TypeTerm::TypeID(TypeID::Var(101)) ])), + ]).solve() { - None - } + // TODO: use real fresh variable names + let item_morph_type = MorphismType { + src_type: σ.get(&TypeID::Var(100)).unwrap().clone(), + dst_type: σ.get(&TypeID::Var(101)).unwrap().clone(), + }.normalize(); - pub fn find_list_map_morphism(&self, item_ty: &MorphismType) - -> Option< Morphism > { + if let Some((m, σ)) = self.find_morphism( &item_morph_type ) { + if let Some(list_morph) = m.list_map_morphism( self.list_typeid ) { + return Some( (list_morph, σ) ); + } + } + } - // TODO + // otherwise + for m in self.morphisms.iter() { + let unification_problem = UnificationProblem::new( + vec![ + ( ty.src_type.clone().normalize(), m.get_type().src_type.clone() ), + ( ty.dst_type.clone().normalize(), m.get_type().dst_type.clone() ) + ] + ); + + let unification_result = unification_problem.solve(); + if let Ok(σ) = unification_result { + return Some((m.clone(), σ)); + } + } None } pub fn find_morphism_with_subtyping(&self, ty: &MorphismType) - -> Option<( Morphism, TypeTerm, HashMap )> { + -> Option<( M, TypeTerm, HashMap )> { + let mut src_lnf = ty.src_type.clone().get_lnf_vec(); + let mut dst_lnf = ty.dst_type.clone().get_lnf_vec(); + let mut halo = vec![]; - // TODO + while src_lnf.len() > 0 && dst_lnf.len() > 0 { + if let Some((m, σ)) = self.find_morphism(&MorphismType{ + src_type: TypeTerm::Ladder(src_lnf.clone()), + dst_type: TypeTerm::Ladder(dst_lnf.clone()) + }) { + return Some((m, TypeTerm::Ladder(halo), σ)); + } else { + if src_lnf[0] == dst_lnf[0] { + src_lnf.remove(0); + halo.push(dst_lnf.remove(0)); + } else { + return None; + } + } + } None } diff --git a/src/test/morphism.rs b/src/test/morphism.rs index d2328d7..fa4b492 100644 --- a/src/test/morphism.rs +++ b/src/test/morphism.rs @@ -1,55 +1,72 @@ use { - crate::{dict::*, morphism::*} + crate::{dict::*, morphism::*, TypeTerm} }; //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ +#[derive(Clone)] +struct DummyMorphism(MorphismType); + +impl Morphism for DummyMorphism { + fn get_type(&self) -> MorphismType { + self.0.clone().normalize() + } + + fn list_map_morphism(&self, list_typeid: TypeID) -> Option { + Some(DummyMorphism(MorphismType { + src_type: TypeTerm::App(vec![ + TypeTerm::TypeID( list_typeid ), + self.0.src_type.clone() + ]), + + dst_type: TypeTerm::App(vec![ + TypeTerm::TypeID( list_typeid ), + self.0.dst_type.clone() + ]) + })) + } +} + #[test] fn test_morphism_path() { let mut dict = TypeDict::new(); - let mut base = MorphismBase::::new( dict.add_typename("Seq".into()) ); + let mut base = MorphismBase::::new( dict.add_typename("Seq".into()) ); dict.add_varname("Radix".into()); dict.add_varname("SrcRadix".into()); dict.add_varname("DstRadix".into()); base.add_morphism( - MorphismType{ + DummyMorphism(MorphismType{ src_type: dict.parse(" ~ Char").unwrap(), dst_type: dict.parse(" ~ ℤ_2^64 ~ machine.UInt64").unwrap() - }, - 11 + }) ); base.add_morphism( - MorphismType{ + DummyMorphism(MorphismType{ src_type: dict.parse(" ~ ℤ_2^64 ~ machine.UInt64").unwrap(), dst_type: dict.parse(" ~ Char").unwrap() - }, - 22 + }) ); base.add_morphism( - MorphismType{ + DummyMorphism(MorphismType{ src_type: dict.parse("ℕ ~ ~ ~ℤ_2^64~machine.UInt64>").unwrap(), dst_type: dict.parse("ℕ ~ ~ ~ℤ_2^64~machine.UInt64>").unwrap() - }, - 333 + }) ); base.add_morphism( - MorphismType{ + DummyMorphism(MorphismType{ src_type: dict.parse("ℕ ~ ~ ~ℤ_2^64~machine.UInt64>").unwrap(), dst_type: dict.parse("ℕ ~ ~ ~ℤ_2^64~machine.UInt64>").unwrap() - }, - 444 + }) ); base.add_morphism( - MorphismType{ + DummyMorphism(MorphismType{ src_type: dict.parse("ℕ ~ ~ ~ℤ_2^64~machine.UInt64>").unwrap(), dst_type: dict.parse("ℕ ~ ~ ~ℤ_2^64~machine.UInt64>").unwrap() - }, - 555 + }) ); - assert_eq!( base.find_morphism_path(MorphismType { src_type: dict.parse("ℕ ~ ~ ~ Char>").unwrap(),