From 62a80fcd2fdfc3046493b468242ec77f48924a7b Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Tue, 4 Feb 2025 14:36:05 +0100
Subject: [PATCH] morphism base: store vec of seq-types

---
 src/morphism.rs      | 61 +++++++++++++++++++++++++-------------------
 src/test/morphism.rs |  8 +++---
 2 files changed, 39 insertions(+), 30 deletions(-)

diff --git a/src/morphism.rs b/src/morphism.rs
index a433bdc..ba7cc23 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -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
     }
 
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index 309d881..ae3775f 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -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());