syntaxAlchemist/lib-laddertypes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

morphism base: store vec of seq-types

Browse source
This commit is contained in:
Michael Sippel 2025-02-04 14:36:05 +01:00
parent 75aaf096eb
commit 62a80fcd2f
Signed by: senvas
GPG key ID: F96CF119C34B64A6
2 changed files with 39 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
src/morphism.rs
View file

@ -16,7 +16,7 @@ pub struct MorphismType {
pub trait Morphism : Sized {
fn get_type(&self) -> MorphismType;
fn list_map_morphism(&self, list_typeid: TypeID) -> Option< Self >;
fn map_morphism(&self, seq_type: TypeTerm) -> Option< Self >;
fn weight(&self) -> u64 {
1
@ -26,7 +26,7 @@ pub trait Morphism : Sized {
#[derive(Clone)]
pub struct MorphismBase<M: Morphism + Clone> {
morphisms: Vec< M >,
list_typeid: TypeID
seq_types: Vec< TypeTerm >
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@ -43,10 +43,10 @@ impl MorphismType {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl<M: Morphism + Clone> MorphismBase<M> {
pub fn new(list_typeid: TypeID) -> Self {
pub fn new(seq_types: Vec<TypeTerm>) -> Self {
MorphismBase {
morphisms: Vec::new(),
list_typeid
seq_types
}
}
@ -80,9 +80,10 @@ impl<M: Morphism + Clone> MorphismBase<M> {
// TODO: function for generating fresh variables
let item_variable = TypeID::Var(100);
for seq_type in self.seq_types.iter() {
if let Ok(σ) = crate::unification::unify(
&TypeTerm::App(vec![
TypeTerm::TypeID(self.list_typeid),
seq_type.clone(),
TypeTerm::TypeID(item_variable)
]),
&src_type.clone().param_normalize(),
@ -92,7 +93,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
for (γ, dst_item_type) in self.enum_morphisms( &src_item_type ) {
let dst_type =
TypeTerm::App(vec![
TypeTerm::TypeID(self.list_typeid),
seq_type.clone(),
dst_item_type.clone()
.apply_substitution(
&|x| γ.get(x).cloned()
@ -102,6 +103,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
dst_types.push( (γ.clone(), dst_type) );
}
}
}
dst_types
}
@ -189,26 +191,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
pub fn find_morphism(&self, ty: &MorphismType)
-> Option< ( M, HashMap<TypeID, TypeTerm> ) > {
// 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() {
// 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();
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, σ) );
}
}
}
// otherwise
// try to find primitive morphism
for m in self.morphisms.iter() {
let unification_problem = UnificationProblem::new(
vec![
@ -223,6 +206,32 @@ impl<M: Morphism + Clone> MorphismBase<M> {
}
}
// try list-map morphism
for seq_type in self.seq_types.iter() {
eprintln!("try seq type {:?}", seq_type);
eprintln!("");
if let Ok(σ) = UnificationProblem::new(vec![
(ty.src_type.clone().param_normalize(),
TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(100)) ])),
(ty.dst_type.clone().param_normalize(),
TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(101)) ])),
]).solve() {
// 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();
if let Some((m, σ)) = self.find_morphism( &item_morph_type ) {
if let Some(list_morph) = m.map_morphism( seq_type.clone() ) {
return Some( (list_morph, σ) );
}
}
}
}
None
}

8
src/test/morphism.rs
View file

@ -12,15 +12,15 @@ impl Morphism for DummyMorphism {
self.0.clone().normalize()
}
fn list_map_morphism(&self, list_typeid: TypeID) -> Option<DummyMorphism> {
fn map_morphism(&self, seq_type: TypeTerm) -> Option<DummyMorphism> {
Some(DummyMorphism(MorphismType {
src_type: TypeTerm::App(vec![
TypeTerm::TypeID( list_typeid ),
seq_type.clone(),
self.0.src_type.clone()
]),
dst_type: TypeTerm::App(vec![
TypeTerm::TypeID( list_typeid ),
seq_type.clone(),
self.0.dst_type.clone()
])
}))
@ -29,7 +29,7 @@ impl Morphism for DummyMorphism {
fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
let mut dict = BimapTypeDict::new();
let mut base = MorphismBase::<DummyMorphism>::new( dict.add_typename("Seq".into()) );
let mut base = MorphismBase::<DummyMorphism>::new( vec![ dict.parse("Seq").expect("") ] );
dict.add_varname("Radix".into());
dict.add_varname("SrcRadix".into());