fix unification test

src/lib.rs

@@ -27,3 +27,70 @@ pub use {
     unification::*,
     morphism::*
 };
+
+
+pub fn common_halo(
+    a: &TypeTerm,
+    b: &TypeTerm
+) -> Option< TypeTerm > {
+    match (a,b) {
+        (TypeTerm::Ladder(rs1), TypeTerm::Ladder(rs2)) => {
+            let mut halo_rungs = Vec::new();
+
+            for (r1, r2) in rs1.iter().zip(rs2.iter()) {
+                if let Some(h) = common_halo(r1, r2) {
+                    halo_rungs.push(h);
+                } else {
+                    return Some(TypeTerm::Ladder(halo_rungs).normalize());
+                }
+            }
+
+            if halo_rungs.len() == 0 {
+                None
+            } else {
+                Some(TypeTerm::Ladder(halo_rungs).normalize())
+            }
+        }
+
+        (TypeTerm::App(a1), TypeTerm::App(a2)) => {
+            let mut halo_args = Vec::new();
+
+            for (r1, r2) in a1.iter().zip(a2.iter()) {
+                if let Some(h) = common_halo(r1, r2) {
+                    halo_args.push(h);
+                } else {
+                    return Some(TypeTerm::Ladder(halo_args).normalize());
+                }
+            }
+
+            if halo_args.len() == 0 {
+                None
+            } else {
+                Some(TypeTerm::App(halo_args).normalize())
+            }
+        }
+
+        (TypeTerm::Ladder(rsl), r) => {
+            if rsl.first().unwrap() == r {
+                Some(r.clone())
+            } else {
+                None
+            }
+        }
+        (l, TypeTerm::Ladder(rsr)) => {
+            if rsr.first().unwrap() == l {
+                Some(l.clone())
+            } else {
+                None
+            }
+        }
+
+        (a1, a2) => {
+            if a1 == a2 {
+                Some(a1.clone())
+            } else {
+                None
+            }
+        }
+    }
+}

src/morphism.rs

@@ -1,8 +1,6 @@
 use {
     crate::{
-        unification::UnificationProblem, TypeDict, TypeID, TypeTerm,
-        pretty::*,
-        sugar::SugaredTypeTerm,
+        subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm
     },
     std::{collections::HashMap, u64}
 };
@@ -135,13 +133,17 @@ impl<M: Morphism + Clone> MorphismBase<M> {
                             ]));
                     }
 
-                    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.σ
-                        }
-                    );
+                    if let Some( map_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
+                        dst_types.push(
+                            MorphismInstance {
+                                halo: TypeTerm::Ladder(dst_halo_ladder).normalize(),
+                                m: map_morph,
+                                σ: item_morph_inst.σ
+                            }
+                        );
+                    } else {
+                        eprintln!("could not get map morphism");
+                    }
                 }
             }
         }
@@ -245,28 +247,54 @@ impl<M: Morphism + Clone> MorphismBase<M> {
         None
     }
 
-/*
-    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(), m.get_type().src_type.clone() ),
-                    ( m.get_type().dst_type.clone(), ty.dst_type.clone() )
-                ]
-            );
 
-            let unification_result = unification_problem.solve_subtype();
-            if let Ok((halo, σ)) = unification_result {
-                return Some((m.clone(), σ));
+    pub fn find_direct_morphism(&self,
+        ty: &MorphismType,
+        dict: &mut impl TypeDict
+    ) -> Option< MorphismInstance<M> > {
+        eprintln!("find direct morph");
+        for m in self.morphisms.iter() {
+            let ty = ty.clone().normalize();
+            let morph_type = m.get_type().normalize();
+
+            eprintln!("find direct morph:\n   {}  <=   {}",
+                            dict.unparse(&ty.src_type), dict.unparse(&morph_type.src_type),
+                        );
+
+            if let Ok((halo, σ)) = subtype_unify(&ty.src_type, &morph_type.src_type) {
+                eprintln!("halo: {}", dict.unparse(&halo));
+
+                let dst_type = TypeTerm::Ladder(vec![
+                    halo.clone(),
+                    morph_type.dst_type.clone()
+                ]);
+                eprintln!("----------->   {}  <=   {}",
+                    dict.unparse(&dst_type), dict.unparse(&ty.dst_type)
+                );
+
+                /*
+                let unification_problem = UnificationProblem::new(
+                                vec![
+                                    ( ty.src_type, morph_type.src_type ),
+                                    ( morph_type.dst_type, ty.dst_type )
+                                ]
+                            );*/
+
+                if let Ok((halo2, σ2)) = subtype_unify(&dst_type, &ty.dst_type) {
+                    eprintln!("match. halo2 = {}", dict.unparse(&halo2));
+                    return Some(MorphismInstance {
+                        m: m.clone(),
+                        halo: halo2,
+                        σ,
+                    });
+                }
             }
         }
         None
     }
 
-    pub fn find_map_morphism(&self, ty: &MorphismType) -> Option< (M, HashMap<TypeID, TypeTerm>) > {
+    pub fn find_map_morphism(&self, ty: &MorphismType, dict: &mut impl TypeDict) -> Option< MorphismInstance<M> > {
         for seq_type in self.seq_types.iter() {
-            eprintln!("try seq type {:?}", seq_type);
-
             if let Ok((halo, σ)) = UnificationProblem::new(vec![
                 (ty.src_type.clone().param_normalize(),
                     TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(100)) ])),
@@ -281,9 +309,13 @@ impl<M: Morphism + Clone> MorphismBase<M> {
                 }.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, σ) );
+                if let Some(item_morph_inst) = self.find_morphism( &item_morph_type, dict ) {
+                    if let Some( list_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
+                        return Some( MorphismInstance {
+                            m: list_morph,
+                            σ,
+                            halo
+                        } );
                     }
                 }
             }
@@ -292,17 +324,18 @@ impl<M: Morphism + Clone> MorphismBase<M> {
         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,σ));
+    pub fn find_morphism(&self, ty: &MorphismType,
+        dict: &mut impl TypeDict
+    )
+    -> Option< MorphismInstance<M> > {
+        if let Some(m) = self.find_direct_morphism(ty, dict) {
+            return Some(m);
         }
-        if let Some((m,σ)) = self.find_map_morphism(ty) {
-            return Some((m, σ));
+        if let Some(m) = self.find_map_morphism(ty, dict) {
+            return Some(m);
         }
         None
     }
-    */
 }
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/steiner_tree.rs

@@ -1,14 +1,9 @@
 use {
-    std::collections::HashMap,
     crate::{
-        TypeID,
-        TypeTerm,
         morphism::{
-            MorphismType,
-            Morphism,
-            MorphismBase
-        }
-    }
+            Morphism, MorphismBase, MorphismType
+        }, MorphismInstance, TypeID, TypeTerm
+    }, std::collections::HashMap
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -91,10 +86,11 @@ impl PathApproxSteinerTreeSolver {
         }
     }
 
-    pub fn solve<M: Morphism + Clone>(self, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
-        let mut tree = Vec::<MorphismType>::new();
+    pub fn solve<M: Morphism + Clone + PartialEq>(self, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
+        let mut edges = Vec::<MorphismType>::new();
 
         for goal in self.leaves {
+            eprintln!("solve steiner tree: find path to goal {:?}", goal);
             // try to find shortest path from root to current leaf
             if let Some(new_path) = morphisms.find_morphism_path(
                 MorphismType {
@@ -102,6 +98,15 @@ impl PathApproxSteinerTreeSolver {
                     dst_type: goal.clone()
                 }
             ) {
+                eprintln!("path to {:?} has len {}", goal.clone(), new_path.len());
+                for morph_inst in new_path {
+                    let t = morph_inst.get_type();
+                    if ! edges.contains(&t) {
+                        eprintln!("add edge {:?}", t);
+                        edges.push(t);
+                    }
+                }
+/*
                 // reduce new path so that it does not collide with any existing path
                 let mut src_type = self.root.clone();
                 let mut new_path_iter = new_path.into_iter().peekable();
@@ -109,12 +114,14 @@ impl PathApproxSteinerTreeSolver {
                 // check all existing nodes..
 
                 if new_path_iter.peek().unwrap().get_type().src_type == src_type {
+                    eprintln!("skip initial node..");
                     new_path_iter.next();
                 }
 
                 for mt in tree.iter() {
                     //assert!( mt.src_type == &src_type );
                     if let Some(t) = new_path_iter.peek() {
+                        eprintln!("");
                         if &mt.dst_type == &t.get_type().src_type {
                             // eliminate this node from new path
                             src_type = new_path_iter.next().unwrap().get_type().src_type;
@@ -127,6 +134,7 @@ impl PathApproxSteinerTreeSolver {
                 for m in new_path_iter {
                     tree.push(m.get_type());
                 }
+*/
             } else {
                 eprintln!("could not find path\nfrom {:?}\nto {:?}", &self.root, &goal);
                 return None;
@@ -136,7 +144,7 @@ impl PathApproxSteinerTreeSolver {
         Some(SteinerTree {
             weight: 0,
             goals: vec![],
-            edges: tree
+            edges
         })
     }
 }

src/test/halo.rs

@@ -0,0 +1,39 @@
+use crate::{dict::BimapTypeDict, parser::*, unparser::*};
+
+#[test]
+fn test_common_halo() {
+    let mut dict = BimapTypeDict::new();
+
+    assert_eq!(
+        crate::common_halo(
+            &dict.parse("A~B~C").expect("parse error"),
+            &dict.parse("A~B~C").expect("parse error")
+        ),
+        Some(dict.parse("A~B~C").expect("parse error"))
+    );
+
+    assert_eq!(
+        crate::common_halo(
+            &dict.parse("A~B~X").expect("parse error"),
+            &dict.parse("A~B~Y").expect("parse error")
+        ),
+        Some(dict.parse("A~B").expect("parse error"))
+    );
+
+    assert_eq!(
+        crate::common_halo(
+            &dict.parse("A~<B C~D>").expect("parse error"),
+            &dict.parse("A~<B C~E>").expect("parse error")
+        ),
+        Some(dict.parse("A~<B C>").expect("parse error"))
+    );
+
+
+    assert_eq!(
+            crate::common_halo(
+                &dict.parse("A").expect("parse error"),
+                &dict.parse("A~<B C~E>").expect("parse error")
+            ),
+            Some(dict.parse("A").expect("parse error"))
+        );
+}

src/test/mod.rs

@@ -8,4 +8,4 @@ pub mod subtype;
 pub mod substitution;
 pub mod unification;
 pub mod morphism;
-
+pub mod halo;

src/test/unification.rs

@@ -173,12 +173,12 @@ fn test_subtype_unification() {
         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()),
+            (dict.parse("<Seq~<LengthPrefix x86.UInt64> ℕ~<PosInt 10 BigEndian>>").unwrap(),
+                dict.parse("<<LengthPrefix x86.UInt64> W>").unwrap()),
         ]).solve_subtype(),
         Ok((
             dict.parse("
-                <Seq~<LengthPrefix x86.UInt64> ℕ~<PosInt 10 BigEndian>>
+                <Seq ℕ~<PosInt 10 BigEndian>>
             ").unwrap(),
             vec![
                 // W

src/unification.rs

@@ -92,16 +92,19 @@ impl UnificationProblem {
             },
 
             (t, TypeTerm::Ladder(mut a1)) => {
-                if let Ok(mut halo) = self.eval_subtype( t.clone(), a1.first().unwrap().clone(), addr.clone() ) {
+                /*
+                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 {