unification: reject non-identity loops & add test cases

- introduce `MorphismInstantiation` which instantiates a
  morphism-template using a type-substitution and a halo type.
- find_morphism_path returns list of `MorphismInstatiation`.

src/morphism.rs

@@ -1,9 +1,10 @@
 use {
     crate::{
-        TypeTerm, TypeID,
-        unification::UnificationProblem,
+        unification::UnificationProblem, TypeDict, TypeID, TypeTerm,
+        pretty::*,
+        sugar::SugaredTypeTerm,
     },
-    std::collections::HashMap
+    std::{collections::HashMap, u64}
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -14,6 +15,17 @@ pub struct MorphismType {
     pub dst_type: TypeTerm,
 }
 
+impl MorphismType {
+    pub fn normalize(self) -> Self {
+        MorphismType {
+            src_type: self.src_type.normalize().param_normalize(),
+            dst_type: self.dst_type.normalize().param_normalize()
+        }
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
 pub trait Morphism : Sized {
     fn get_type(&self) -> MorphismType;
     fn map_morphism(&self, seq_type: TypeTerm) -> Option< Self >;
@@ -23,25 +35,50 @@ pub trait Morphism : Sized {
     }
 }
 
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, Debug, PartialEq)]
+pub struct MorphismInstance<M: Morphism + Clone> {
+    pub halo: TypeTerm,
+    pub m: M,
+    pub σ: HashMap<TypeID, TypeTerm>
+}
+
+impl<M: Morphism + Clone> MorphismInstance<M> {
+    pub fn get_type(&self) -> MorphismType {
+        MorphismType {
+            src_type: TypeTerm::Ladder(vec![
+                self.halo.clone(),
+                self.m.get_type().src_type.clone()
+            ]).apply_substitution(&|k| self.σ.get(k).cloned())
+            .clone(),
+
+            dst_type: TypeTerm::Ladder(vec![
+                self.halo.clone(),
+                self.m.get_type().dst_type.clone()
+            ]).apply_substitution(&|k| self.σ.get(k).cloned())
+            .clone()
+        }.normalize()
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct MorphismPath<M: Morphism + Clone> {
+    pub weight: u64,
+    pub cur_type: TypeTerm,
+    pub morphisms: Vec< MorphismInstance<M> >
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
 #[derive(Clone)]
 pub struct MorphismBase<M: Morphism + Clone> {
     morphisms: Vec< M >,
     seq_types: Vec< TypeTerm >
 }
 
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-impl MorphismType {
-    pub fn normalize(self) -> Self {
-        MorphismType {
-            src_type: self.src_type.normalize(),
-            dst_type: self.dst_type.normalize()
-        }
-    }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
 impl<M: Morphism + Clone> MorphismBase<M> {
     pub fn new(seq_types: Vec<TypeTerm>) -> Self {
         MorphismBase {
@@ -54,176 +91,196 @@ impl<M: Morphism + Clone> MorphismBase<M> {
         self.morphisms.push( m );
     }
 
-    pub fn enum_morphisms(&self, src_type: &TypeTerm)
-    -> Vec< (HashMap<TypeID, TypeTerm>, TypeTerm) >
+    pub fn enum_direct_morphisms(&self, src_type: &TypeTerm)
+    -> Vec< MorphismInstance<M> >
     {
         let mut dst_types = Vec::new();
-
-        // first enumerate all "direct" morphisms,
         for m in self.morphisms.iter() {
-            if let Ok(σ) = crate::unification::unify(
-                &m.get_type().src_type,
-                &src_type.clone().normalize()
+            if let Ok((halo, σ)) = crate::unification::subtype_unify(
+                &src_type.clone().param_normalize(),
+                &m.get_type().src_type.param_normalize(),
             ) {
-                let dst_type =
-                    m.get_type().dst_type.clone()
-                    .apply_substitution( &|x| σ.get(x).cloned() )
-                    .clone();
-
-                dst_types.push( (σ, dst_type) );
+                dst_types.push(MorphismInstance{ halo, m: m.clone(), σ });
             }
         }
+        dst_types
+    }
+
+    pub fn enum_map_morphisms(&self, src_type: &TypeTerm)
+    -> Vec< MorphismInstance<M> > {
+        let src_type = src_type.clone().param_normalize();
+        let mut dst_types = Vec::new();
 
-        // ..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);
+        let item_variable = TypeID::Var(800);
 
         for seq_type in self.seq_types.iter() {
-        if let Ok(σ) = crate::unification::unify(
-            &TypeTerm::App(vec![
-                seq_type.clone(),
-                TypeTerm::TypeID(item_variable)
-            ]),
-            &src_type.clone().param_normalize(),
-        ) {
-            let src_item_type = σ.get(&item_variable).unwrap().clone();
+            if let Ok((halo, σ)) = crate::unification::subtype_unify(
+                &src_type,
+                &TypeTerm::App(vec![
+                    seq_type.clone(),
+                    TypeTerm::TypeID(item_variable)
+                ])
+            ) {
+                let src_item_type = σ.get(&item_variable).expect("var not in unificator").clone();
+                for item_morph_inst in self.enum_morphisms( &src_item_type ) {
 
-            for (γ, dst_item_type) in self.enum_morphisms( &src_item_type ) {
-                let dst_type =
-                        TypeTerm::App(vec![
-                            seq_type.clone(),
-                            dst_item_type.clone()
-                                .apply_substitution(
-                                    &|x| γ.get(x).cloned()
-                                ).clone()
-                        ]).normalize();
+                    let mut dst_halo_ladder = vec![ halo.clone() ];
+                    if item_morph_inst.halo != TypeTerm::unit() {
+                        dst_halo_ladder.push(
+                            TypeTerm::App(vec![
+                                seq_type.clone().get_lnf_vec().first().unwrap().clone(),
+                                item_morph_inst.halo.clone()
+                            ]));
+                    }
 
-                dst_types.push( (γ.clone(), dst_type) );
+                    dst_types.push(
+                        MorphismInstance {
+                            halo: TypeTerm::Ladder(dst_halo_ladder).normalize(),
+                            m: item_morph_inst.m.map_morphism(seq_type.clone()).expect("couldnt get map morphism"),
+                            σ: item_morph_inst.σ
+                        }
+                    );
+                }
             }
         }
-        }
 
         dst_types
     }
 
-    pub fn enum_morphisms_with_subtyping(
-        &self,
-        src_type: &TypeTerm,
-    ) -> Vec<(TypeTerm, TypeTerm, HashMap<TypeID, TypeTerm>)> {
-        let mut src_lnf = src_type.clone().get_lnf_vec();
-        let mut halo_lnf = vec![];
+    pub fn enum_morphisms(&self, src_type: &TypeTerm) -> Vec< MorphismInstance<M> > {
         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.append(&mut self.enum_direct_morphisms(src_type));
+        dst_types.append(&mut self.enum_map_morphisms(src_type));
         dst_types
     }
 
     /* try to find shortest morphism-path for a given type
      */
-    pub fn find_morphism_path(&self, ty: MorphismType)
-    -> Option< Vec<TypeTerm> >
+    pub fn find_morphism_path(&self, ty: MorphismType
+        /*, type_dict: &mut impl TypeDict*/
+    )
+    -> Option< Vec<MorphismInstance<M>> >
     {
         let ty = ty.normalize();
-
         let mut queue = vec![
-            (0, vec![ ty.src_type.clone().normalize() ])
+            MorphismPath { weight: 0, cur_type: ty.src_type.clone(), morphisms: vec![] }
         ];
 
         while ! queue.is_empty() {
-            queue.sort_by( |&(w1,_),&(w2,_)| w2.cmp(&w1));
+            queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
 
-            if let Some((current_weight, current_path)) = queue.pop() {
-                let current_type = current_path.last().unwrap();
-                for (h, t, σp) in self.enum_morphisms_with_subtyping(&current_type) {
-                    let tt = TypeTerm::Ladder(vec![h, t]).normalize();
-
-                    if !current_path.contains(&tt) {
-                        let unification_result = crate::unification::unify(&tt, &ty.dst_type);
-                        let morphism_weight = 1;
-                        /*self.find_morphism( &tt ).unwrap().0.get_weight()*/
-
-                        let new_weight = current_weight + morphism_weight;
-                        let mut new_path = current_path.clone();
-
-                        new_path.push(tt);
-
-                        for n in new_path.iter_mut() {
-                            n.apply_substitution(&|x| σp.get(x).cloned());
+            if let Some(mut cur_path) = queue.pop() {
+                if let Ok((halo, σ)) = crate::unification::subtype_unify( &cur_path.cur_type, &ty.dst_type ) {
+                    // found path
+                    for n in cur_path.morphisms.iter_mut() {
+                        let mut new_σ = HashMap::new();
+                        for (k,v) in σ.iter() {
+                            new_σ.insert(
+                                k.clone(),
+                                v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone()
+                            );
+                        }
+                        for (k,v) in n.σ.iter() {
+                            new_σ.insert(
+                                k.clone(),
+                                v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone()
+                            );
                         }
 
-                        if let Ok(σ) = unification_result {
-                            for n in new_path.iter_mut() {
-                                n.apply_substitution(&|x| σ.get(x).cloned());
-                            }
-                            return Some(new_path);
-                        } else {
-                            queue.push((new_weight, new_path));
+                        n.σ = new_σ;
+                    }
+
+                    return Some(cur_path.morphisms);
+                }
+
+                //eprintln!("cur path (w ={}) : @ {}", cur_path.weight, cur_path.cur_type.clone().sugar(type_dict).pretty(type_dict, 0) );
+                for next_morph_inst in self.enum_morphisms(&cur_path.cur_type) {
+                    let dst_type = next_morph_inst.get_type().dst_type;
+
+                    let mut creates_loop = false;
+
+                    let mut new_path = cur_path.clone();
+                    for n in new_path.morphisms.iter_mut() {
+                        let mut new_σ = HashMap::new();
+                        for (k,v) in n.σ.iter() {
+                            new_σ.insert(
+                                k.clone(),
+                                v.clone().apply_substitution(&|k| next_morph_inst.σ.get(k).cloned()).clone()
+                            );
                         }
+                        for (k,v) in next_morph_inst.σ.iter() {
+                            new_σ.insert(
+                                k.clone(),
+                                v.clone().apply_substitution(&|k| next_morph_inst.σ.get(k).cloned()).clone()
+                            );
+                        }
+                        n.σ = new_σ;
+                    }
+
+                    for m in new_path.morphisms.iter() {
+                        if m.get_type().src_type == dst_type {
+                            creates_loop = true;
+                            //eprintln!("creates loop..");
+                            break;
+                        }
+                    }
+
+                    if ! creates_loop {
+                        /*eprintln!("next morph ? \n    {}\n--> {} ",
+                            next_morph_inst.get_type().src_type.sugar(type_dict).pretty(type_dict, 0),
+                            next_morph_inst.get_type().dst_type.sugar(type_dict).pretty(type_dict, 0)
+                        );
+                        eprintln!("....take!\n  :: halo = {}\n  :: σ = {:?}", next_morph_inst.halo.clone().sugar(type_dict).pretty(type_dict, 0), next_morph_inst.σ);
+                        */
+                        new_path.weight += next_morph_inst.m.weight();
+                        new_path.cur_type = dst_type;
+                        new_path.morphisms.push(next_morph_inst);
+                        queue.push(new_path);
                     }
                 }
             }
         }
-
         None
     }
 
-    /// finde a morphism that matches the given morphism type
-    pub fn find_morphism(&self, ty: &MorphismType)
-    -> Option< ( M, HashMap<TypeID, TypeTerm> ) > {
-
-        // try to find primitive morphism
+/*
+    pub fn find_direct_morphism(&self, ty: &MorphismType) -> Option< (M, HashMap<TypeID, TypeTerm>) > {
         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() )
+                    ( ty.src_type.clone(), m.get_type().src_type.clone() ),
+                    ( m.get_type().dst_type.clone(), ty.dst_type.clone() )
                 ]
             );
 
-            let unification_result = unification_problem.solve();
-            if let Ok(σ) = unification_result {
+            let unification_result = unification_problem.solve_subtype();
+            if let Ok((halo, σ)) = unification_result {
                 return Some((m.clone(), σ));
             }
         }
+        None
+    }
 
-        // try list-map morphism
+    pub fn find_map_morphism(&self, ty: &MorphismType) -> Option< (M, HashMap<TypeID, TypeTerm>) > {
         for seq_type in self.seq_types.iter() {
             eprintln!("try seq type {:?}", seq_type);
 
-            eprintln!("");
-
-            if let Ok(σ) = UnificationProblem::new(vec![
+            if let Ok((halo, σ)) = 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() {
+
+                (TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(101)) ]),
+                    ty.dst_type.clone().param_normalize()),
+            ]).solve_subtype() {
                 // 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();
 
+                //eprintln!("Map Morph: try to find item-morph with type {:?}", item_morph_type);
                 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, σ) );
@@ -235,33 +292,17 @@ impl<M: Morphism + Clone> MorphismBase<M> {
         None
     }
 
-    pub fn find_morphism_with_subtyping(&self, ty: &MorphismType)
-    -> Option<( M, TypeTerm, HashMap<TypeID, TypeTerm> )> {
-        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![];
-
-        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())
-            }) {
-                halo.push(src_lnf.get(0).unwrap().clone());
-                return Some((m,
-                    TypeTerm::Ladder(halo).apply_substitution(&|x| σ.get(x).cloned()).clone(),
-                    σ));
-            } else {
-                if src_lnf[0] == dst_lnf[0] {
-                    src_lnf.remove(0);
-                    halo.push(dst_lnf.remove(0));
-                } else {
-                    return None;
-                }
-            }
+    pub fn find_morphism(&self, ty: &MorphismType)
+    -> Option< ( M, HashMap<TypeID, TypeTerm> ) > {
+        if let Some((m,σ)) = self.find_direct_morphism(ty) {
+            return Some((m,σ));
+        }
+        if let Some((m,σ)) = self.find_map_morphism(ty) {
+            return Some((m, σ));
         }
-
         None
     }
+    */
 }
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/pretty.rs

@@ -1,5 +1,5 @@
 use {
-    crate::TypeDict,
+    crate::{TypeDict, dict::TypeID},
     crate::sugar::SugaredTypeTerm,
     tiny_ansi::TinyAnsi
 };
@@ -9,11 +9,18 @@ impl SugaredTypeTerm {
         let indent_width = 4;
         match self {
             SugaredTypeTerm::TypeID(id) => {
-                format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).bright_blue()
+                match id {
+                    TypeID::Var(varid) => {
+                        format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).bright_magenta()
+                    },
+                    TypeID::Fun(funid) => {
+                        format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).blue().bold()
+                    }
+                }
             },
 
             SugaredTypeTerm::Num(n) => {
-                format!("{}", n).bright_cyan()
+                format!("{}", n).green().bold()
             }
 
             SugaredTypeTerm::Char(c) => {
@@ -34,7 +41,7 @@ impl SugaredTypeTerm {
 
             SugaredTypeTerm::Spec(args) => {
                 let mut s = String::new();
-                s.push_str(&"<".yellow().bold());
+                s.push_str(&"<".yellow());
                 for i in 0..args.len() {
                     let arg = &args[i];
                     if i > 0 {
@@ -42,7 +49,7 @@ impl SugaredTypeTerm {
                     }
                     s.push_str( &arg.pretty(dict,indent+1) );
                 }
-                s.push_str(&">".yellow().bold());
+                s.push_str(&">".yellow());
                 s
             }
 

src/steiner_tree.rs

@@ -108,28 +108,24 @@ impl PathApproxSteinerTreeSolver {
 
                 // check all existing nodes..
 
-                if new_path_iter.peek().unwrap() == &src_type {
+                if new_path_iter.peek().unwrap().get_type().src_type == src_type {
                     new_path_iter.next();
                 }
 
                 for mt in tree.iter() {
                     //assert!( mt.src_type == &src_type );
                     if let Some(t) = new_path_iter.peek() {
-                        if &mt.dst_type == t {
+                        if &mt.dst_type == &t.get_type().src_type {
                             // eliminate this node from new path
-                            src_type = new_path_iter.next().unwrap().clone();
+                            src_type = new_path_iter.next().unwrap().get_type().src_type;
                         }
                     } else {
                         break;
                     }
                 }
 
-                for dst_type in new_path_iter {
-                    tree.push(MorphismType {
-                        src_type: src_type.clone(),
-                        dst_type: dst_type.clone()
-                    });
-                    src_type = dst_type;
+                for m in new_path_iter {
+                    tree.push(m.get_type());
                 }
             } else {
                 eprintln!("could not find path\nfrom {:?}\nto {:?}", &self.root, &goal);
@@ -223,8 +219,9 @@ impl SteinerTreeProblem {
 
             // extend the tree by one edge and add it to the queue
             for src_type in current_nodes {
-                for (dst_halo, dst_ty, σ) in morphisms.enum_morphisms_with_subtyping(&src_type) {
-                    let dst_type = TypeTerm::Ladder(vec![dst_halo, dst_ty]).normalize();
+                for next_morph_inst in morphisms.enum_morphisms(&src_type) {
+                    //let dst_type = TypeTerm::Ladder(vec![dst_halo, dst_ty]).normalize();
+                    let dst_type = next_morph_inst.get_type().dst_type;
 
                     if current_tree.contains( &dst_type ).is_none() {
                         let mut new_tree = current_tree.clone();

src/term.rs

@@ -76,6 +76,22 @@ impl TypeTerm {
         self.arg(TypeTerm::Char(c))
     }
 
+    pub fn contains_var(&self, var_id: u64) -> bool {
+        match self {
+            TypeTerm::TypeID(TypeID::Var(v)) => (&var_id == v),
+            TypeTerm::App(args) |
+            TypeTerm::Ladder(args) => {
+                for a in args.iter() {
+                    if a.contains_var(var_id) {
+                        return true;
+                    }
+                }
+                false
+            }
+            _ => false
+        }
+    }
+
     /// recursively apply substitution to all subterms,
     /// which will replace all occurences of variables which map
     /// some type-term in `subst`

src/test/morphism.rs

@@ -1,5 +1,5 @@
 use {
-    crate::{dict::*, parser::*, unparser::*, morphism::*, steiner_tree::*, TypeTerm}
+    crate::{dict::*, parser::*, unparser::*, morphism::*, TypeTerm}
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -73,23 +73,105 @@ fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
 fn test_morphism_path() {
     let (mut dict, mut base) = morphism_test_setup();
 
+    let path = base.find_morphism_path(MorphismType {
+        src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+        dst_type: dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap(),
+    });
+
+    fn print_subst(m: &std::collections::HashMap<TypeID, TypeTerm>, dict: &mut impl TypeDict) {
+        eprintln!("{{");
+
+        for (k,v) in m.iter() {
+            eprintln!("    {} --> {}",
+                dict.get_typename(k).unwrap(),
+                dict.unparse(v)
+            );
+        }
+
+        eprintln!("}}");
+    }
+
+    if let Some(path) = path.as_ref() {
+        for n in path.iter() {
+            eprintln!("
+ψ = {}
+morph {}
+  --> {}
+with
+            ",
+            n.halo.clone().sugar(&mut dict).pretty(&mut dict, 0),
+            n.m.get_type().src_type.sugar(&mut dict).pretty(&mut dict, 0),
+            n.m.get_type().dst_type.sugar(&mut dict).pretty(&mut dict, 0),
+            );
+            print_subst(&n.σ, &mut dict)
+        }
+    }
+
     assert_eq!(
-        base.find_morphism_path(MorphismType {
-            src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
-            dst_type: dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
-        }),
+        path,
         Some(
             vec![
-                dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().normalize(),
-                dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().normalize(),
+                MorphismInstance {
+                    σ: vec![
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16))
+                    ].into_iter().collect(),
+                    halo: dict.parse("ℕ ~ <PosInt 10 BigEndian>").unwrap(),
+                    m: DummyMorphism(MorphismType {
+                        src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
+                        dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+                    }),
+                },
+                MorphismInstance {
+                    σ: vec![
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16))
+                    ].into_iter().collect(),
+                    halo: TypeTerm::unit(),
+                    m: DummyMorphism(MorphismType{
+                        src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+                        dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+                    }),
+                },
+                MorphismInstance {
+                    σ: vec![
+                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
+                    ].into_iter().collect(),
+                    halo: TypeTerm::unit(),
+                    m: DummyMorphism(MorphismType{
+                        src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+                        dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+                    }),
+                },
+                MorphismInstance {
+                    σ: vec![
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
+                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16))
+                    ].into_iter().collect(),
+                    halo: TypeTerm::unit(),
+                    m: DummyMorphism(MorphismType{
+                        src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+                        dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+                    }),
+                },
+                MorphismInstance {
+                    σ: vec![
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16))
+                    ].into_iter().collect(),
+                    halo: dict.parse("ℕ ~ <PosInt Radix BigEndian>").unwrap(),
+                    m: DummyMorphism(MorphismType{
+                        src_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+                        dst_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap()
+                    })
+                }
             ]
         )
     );
-
+/*
     assert_eq!(
         base.find_morphism_path(MorphismType {
             src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
@@ -106,7 +188,10 @@ fn test_morphism_path() {
             ]
         )
     );
+    */
 
+
+/*
     assert_eq!(
         base.find_morphism_with_subtyping(
             &MorphismType {
@@ -129,8 +214,9 @@ fn test_morphism_path() {
                 ].into_iter().collect::<std::collections::HashMap<TypeID, TypeTerm>>()
         ))
     );
+    */
 }
-
+/*
 #[test]
 fn test_steiner_tree() {
     let (mut dict, mut base) = morphism_test_setup();
@@ -158,3 +244,4 @@ fn test_steiner_tree() {
         eprintln!("no solution");
     }
 }
+*/

src/test/unification.rs

@@ -61,6 +61,19 @@ fn test_unification_error() {
             t2: dict.parse("B").unwrap()
         })
     );
+
+    assert_eq!(
+        crate::unify(
+            &dict.parse("T").unwrap(),
+            &dict.parse("<Seq T>").unwrap()
+        ),
+
+        Err(UnificationError {
+            addr: vec![],
+            t1: dict.parse("T").unwrap(),
+            t2: dict.parse("<Seq T>").unwrap()
+        })
+    );
 }
 
 #[test]
@@ -115,3 +128,64 @@ fn test_unification() {
         )
     );
 }
+
+#[test]
+fn test_subtype_unification() {
+    let mut dict = BimapTypeDict::new();
+    dict.add_varname(String::from("T"));
+    dict.add_varname(String::from("U"));
+    dict.add_varname(String::from("V"));
+    dict.add_varname(String::from("W"));
+
+    assert_eq!(
+        UnificationProblem::new(vec![
+            (dict.parse("<Seq~T <Digit 10> ~ Char>").unwrap(),
+                dict.parse("<Seq~<LengthPrefix x86.UInt64> Char ~ Ascii>").unwrap()),
+        ]).solve_subtype(),
+        Ok((
+            dict.parse("<Seq <Digit 10>>").unwrap(),
+            vec![
+                // T
+                (TypeID::Var(0), dict.parse("<LengthPrefix x86.UInt64>").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+
+    assert_eq!(
+        UnificationProblem::new(vec![
+            (dict.parse("U").unwrap(), dict.parse("<Seq Char>").unwrap()),
+            (dict.parse("T").unwrap(), dict.parse("<Seq U>").unwrap()),
+        ]).solve_subtype(),
+        Ok((
+            TypeTerm::unit(),
+            vec![
+                // T
+                (TypeID::Var(0), dict.parse("<Seq <Seq Char>>").unwrap()),
+
+                // U
+                (TypeID::Var(1), dict.parse("<Seq Char>").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+
+    assert_eq!(
+        UnificationProblem::new(vec![
+            (dict.parse("<Seq T>").unwrap(),
+                dict.parse("<Seq W~<Seq Char>>").unwrap()),
+            (dict.parse("<Seq ℕ~<PosInt 10 BigEndian>>").unwrap(),
+                dict.parse("<Seq~<LengthPrefix x86.UInt64> W>").unwrap()),
+        ]).solve_subtype(),
+        Ok((
+            dict.parse("
+                <Seq~<LengthPrefix x86.UInt64> ℕ~<PosInt 10 BigEndian>>
+            ").unwrap(),
+            vec![
+                // W
+                (TypeID::Var(3), dict.parse("ℕ~<PosInt 10 BigEndian>").unwrap()),
+
+                // T
+                (TypeID::Var(0), dict.parse("ℕ~<PosInt 10 BigEndian>~<Seq Char>").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+}

src/unification.rs

@@ -25,22 +25,140 @@ impl UnificationProblem {
         }
     }
 
+    pub fn reapply_subst(&mut self) {
+        // update all values in substitution
+        let mut new_σ = HashMap::new();
+        for (v, tt) in self.σ.iter() {
+            let mut tt = tt.clone().normalize();
+            tt.apply_substitution(&|v| self.σ.get(v).cloned());
+            tt = tt.normalize();
+            //eprintln!("update σ : {:?} --> {:?}", v, tt);
+            new_σ.insert(v.clone(), tt);
+        }
+        self.σ = new_σ;
+    }
+
+    pub fn eval_subtype(&mut self, lhs: TypeTerm, rhs: TypeTerm, addr: Vec<usize>) -> Result<Vec<TypeTerm>, UnificationError> {
+        match (lhs.clone(), rhs.clone()) {
+            (TypeTerm::TypeID(TypeID::Var(varid)), t) |
+            (t, TypeTerm::TypeID(TypeID::Var(varid))) => {
+
+                if ! t.contains_var( varid ) {
+                    self.σ.insert(TypeID::Var(varid), t.clone());
+                    self.reapply_subst();
+                    Ok(vec![])
+                } else if t == TypeTerm::TypeID(TypeID::Var(varid)) {
+                    Ok(vec![])
+                } else {
+                    Err(UnificationError{ addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t })
+                }
+            }
+
+            (TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
+                if a1 == a2 { Ok(vec![]) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
+            }
+            (TypeTerm::Num(n1), TypeTerm::Num(n2)) => {
+                if n1 == n2 { Ok(vec![]) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
+            }
+            (TypeTerm::Char(c1), TypeTerm::Char(c2)) => {
+                if c1 == c2 { Ok(vec![]) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
+            }
+
+            (TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) => {
+                let mut halo = Vec::new();
+                for i in 0..a1.len() {
+                    if let Ok((r_halo, σ)) = subtype_unify( &a1[i], &a2[0] ) {
+                        //eprintln!("unified ladders at {}, r_halo = {:?}", i, r_halo);
+                        for (k,v) in σ.iter() {
+                            self.σ.insert(k.clone(),v.clone());
+                        }
+
+                        for j in 0..a2.len() {
+                            if i+j < a1.len() {
+                                let mut new_addr = addr.clone();
+                                new_addr.push(i+j);
+                                self.eqs.push((a1[i+j].clone().apply_substitution(&|k| σ.get(k).cloned()).clone(),
+                                    a2[j].clone().apply_substitution(&|k| σ.get(k).cloned()).clone(),
+                                    new_addr));
+                            }
+                        }
+                        return Ok(halo)
+                    } else {
+                        halo.push(a1[i].clone());
+                        //eprintln!("could not unify ladders");
+                    }
+                }
+
+                Err(UnificationError{ addr, t1: lhs, t2: rhs })
+            },
+
+            (t, TypeTerm::Ladder(mut a1)) => {
+                if let Ok(mut halo) = self.eval_subtype( t.clone(), a1.first().unwrap().clone(), addr.clone() ) {
+                    a1.append(&mut halo);
+                    Ok(a1)
+                } else {
+                    Err(UnificationError{ addr, t1: t, t2: TypeTerm::Ladder(a1) })
+                }
+            }
+
+            (TypeTerm::Ladder(mut a1), t) => {
+                if let Ok(mut halo) = self.eval_subtype( a1.pop().unwrap(), t.clone(), addr.clone() ) {
+                    a1.append(&mut halo);
+                    Ok(a1)
+                } else {
+                    Err(UnificationError{ addr, t1: TypeTerm::Ladder(a1), t2: t })
+                }
+            }
+
+            (TypeTerm::App(a1), TypeTerm::App(a2)) => {
+                if a1.len() == a2.len() {
+                    let mut halo_args = Vec::new();
+                    let mut halo_required = false;
+
+                    for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
+                        let mut new_addr = addr.clone();
+                        new_addr.push(i);
+                        //self.eqs.push((x, y, new_addr));
+
+                        if let Ok(halo) = self.eval_subtype( x.clone(), y.clone(), new_addr ) {
+                            if halo.len() == 0 {
+                                halo_args.push(y.get_lnf_vec().first().unwrap().clone());
+                            } else {
+                                halo_args.push(TypeTerm::Ladder(halo));
+                                halo_required = true;
+                            }
+                        } else {
+                            return Err(UnificationError{ addr, t1: x, t2: y })
+                        }
+                    }
+
+                    if halo_required {
+                        Ok(vec![ TypeTerm::App(halo_args) ])
+                    } else {
+                        Ok(vec![])
+                    }
+                } else {
+                    Err(UnificationError{ addr, t1: lhs, t2: rhs })
+                }
+            }
+
+            _ => Err(UnificationError{ addr, t1: lhs, t2: rhs})
+        }
+    }
+
     pub fn eval_equation(&mut self, lhs: TypeTerm, rhs: TypeTerm, addr: Vec<usize>) -> Result<(), UnificationError> {
         match (lhs.clone(), rhs.clone()) {
             (TypeTerm::TypeID(TypeID::Var(varid)), t) |
             (t, TypeTerm::TypeID(TypeID::Var(varid))) => {
-                self.σ.insert(TypeID::Var(varid), t.clone());
-
-                // update all values in substitution
-                let mut new_σ = HashMap::new();
-                for (v, tt) in self.σ.iter() {
-                    let mut tt = tt.clone();
-                    tt.apply_substitution(&|v| self.σ.get(v).cloned());
-                    new_σ.insert(v.clone(), tt);
+                if ! t.contains_var( varid ) {
+                    self.σ.insert(TypeID::Var(varid), t.clone());
+                    self.reapply_subst();
+                    Ok(())
+                } else if t == TypeTerm::TypeID(TypeID::Var(varid)) {
+                    Ok(())
+                } else {
+                    Err(UnificationError{ addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t })
                 }
-                self.σ = new_σ;
-
-                Ok(())
             }
 
             (TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
@@ -56,7 +174,7 @@ impl UnificationProblem {
             (TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) |
             (TypeTerm::App(a1), TypeTerm::App(a2)) => {
                 if a1.len() == a2.len() {
-                    for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
+                    for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate().rev() {
                         let mut new_addr = addr.clone();
                         new_addr.push(i);
                         self.eqs.push((x, y, new_addr));
@@ -67,24 +185,75 @@ impl UnificationProblem {
                 }
             }
 
-            (TypeTerm::Ladder(l1), TypeTerm::Ladder(l2)) => {
-                Err(UnificationError{ addr, t1: lhs, t2: rhs })
-            }
-
             _ => Err(UnificationError{ addr, t1: lhs, t2: rhs})
         }
     }
 
     pub fn solve(mut self) -> Result<HashMap<TypeID, TypeTerm>, UnificationError> {
-        while self.eqs.len() > 0 {
-            while let Some( (mut lhs,mut rhs,addr) ) = self.eqs.pop() {
-                lhs.apply_substitution(&|v| self.σ.get(v).cloned());
-                rhs.apply_substitution(&|v| self.σ.get(v).cloned());
-                self.eval_equation(lhs, rhs, addr)?;
+        while let Some( (mut lhs,mut rhs,addr) ) = self.eqs.pop() {
+            lhs.apply_substitution(&|v| self.σ.get(v).cloned());
+            rhs.apply_substitution(&|v| self.σ.get(v).cloned());
+            self.eval_equation(lhs, rhs, addr)?;
+        }
+        Ok(self.σ)
+    }
+
+    pub fn solve_subtype(mut self) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), UnificationError> {
+
+        pub fn insert_halo_at(
+            t: &mut TypeTerm,
+            mut addr: Vec<usize>,
+            halo_type: TypeTerm
+        ) {
+            match t {
+                TypeTerm::Ladder(rungs) => {
+                    if let Some(idx) = addr.pop() {
+                        for i in rungs.len()..idx+1 {
+                            rungs.push(TypeTerm::unit());
+                        }
+                        insert_halo_at( &mut rungs[idx], addr, halo_type );
+                    } else {
+                        rungs.push(halo_type);
+                    }
+                },
+
+                TypeTerm::App(args) => {
+                    if let Some(idx) = addr.pop() {
+                        insert_halo_at( &mut args[idx], addr, halo_type );
+                    } else {
+                        *t = TypeTerm::Ladder(vec![
+                            halo_type,
+                            t.clone()
+                        ]);
+                    }
+                }
+
+                atomic => {
+
+                }
             }
         }
 
-        Ok(self.σ)
+        //let mut halo_type = TypeTerm::unit();
+        let mut halo_rungs = Vec::new();
+
+        while let Some( (mut lhs, mut rhs, mut addr) ) = self.eqs.pop() {
+            lhs.apply_substitution(&|v| self.σ.get(v).cloned());
+            rhs.apply_substitution(&|v| self.σ.get(v).cloned());
+            //eprintln!("eval subtype\n\tLHS={:?}\n\tRHS={:?}\n", lhs, rhs);
+            let mut new_halo = self.eval_subtype(lhs, rhs, addr.clone())?;
+            if new_halo.len() > 0 {
+                //insert_halo_at( &mut halo_type, addr, TypeTerm::Ladder(new_halo) );
+                if addr.len() == 0 {
+                    halo_rungs.push(TypeTerm::Ladder(new_halo))
+                }
+            }
+        }
+
+        let mut halo_type = TypeTerm::Ladder(halo_rungs);
+        halo_type = halo_type.normalize();
+        halo_type = halo_type.apply_substitution(&|k| self.σ.get(k).cloned()).clone();
+        Ok((halo_type.param_normalize(), self.σ))
     }
 }
 
@@ -96,5 +265,12 @@ pub fn unify(
     unification.solve()
 }
 
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+pub fn subtype_unify(
+    t1: &TypeTerm,
+    t2: &TypeTerm
+) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), UnificationError> {
+    let mut unification = UnificationProblem::new(vec![ (t1.clone(), t2.clone()) ]);
+    unification.solve_subtype()
+}
 
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\