wip

src/morphism.rs

@@ -182,7 +182,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
         let mut queue = vec![
             MorphismPath::<M> { weight: 0, cur_type: ty.src_type.clone(), morphisms: vec![] }
         ];
- 
+
         while ! queue.is_empty() {
             queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
 
@@ -307,19 +307,11 @@ impl<M: Morphism + Clone> MorphismBase<M> {
                     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: halo,
+                        halo,
                         σ,
                     });
                 }

src/test/morphism.rs

@@ -266,11 +266,11 @@ with
                     ].into_iter().collect(),
                     halo: dict.parse("ℕ ~ <PosInt 16 LittleEndian>").expect(""),
                     m: DummyMorphism(MorphismType {
-                        src_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),                        
+                        src_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
                         dst_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap()
                     }),
                 },
-                
+
             ]
     ));
 }
@@ -374,6 +374,9 @@ with
             ]
         )
     );
+
+
+
 /*
     assert_eq!(
         base.find_morphism_path(MorphismType {
@@ -392,8 +395,6 @@ with
         )
     );
     */
-
-
 /*
     assert_eq!(
         base.find_morphism_with_subtyping(
@@ -417,15 +418,14 @@ with
                 ].into_iter().collect::<std::collections::HashMap<TypeID, TypeTerm>>()
         ))
     );
-    */
+*/
 }
-/*
+
 #[test]
 fn test_steiner_tree() {
     let (mut dict, mut base) = morphism_test_setup();
 
-
-    let mut steiner_tree_problem = SteinerTreeProblem::new(
+    let mut steiner_tree_problem = crate::steiner_tree::SteinerTreeProblem::new(
         // source reprs
         vec![
             dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
@@ -447,4 +447,3 @@ fn test_steiner_tree() {
         eprintln!("no solution");
     }
 }
-*/

src/test/unification.rs

@@ -222,6 +222,24 @@ fn test_subtype_unification() {
 }
 
 
+#[test]
+fn test_trait_not_subtype() {
+    let mut dict = BimapTypeDict::new();
+
+    assert_eq!(
+            subtype_unify(
+                &dict.parse("A ~ B").expect(""),
+                &dict.parse("A ~ B ~ C").expect("")
+            ),
+            Err(UnificationError {
+                addr: vec![],
+                t1: dict.parse("A ~ B").expect(""),
+                t2: dict.parse("A ~ B ~ C").expect("")
+            })
+        );
+}
+
+
 #[test]
 pub fn test_subtype_delim() {
     let mut dict = BimapTypeDict::new();

src/unification.rs

@@ -237,6 +237,14 @@ impl UnificationProblem {
 
             (TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) => {
                 let mut halo = Vec::new();
+                if a1.len() < a2.len() {
+                    return Err(UnificationError {
+                        addr: vec![],
+                        t1: unification_pair.lhs,
+                        t2: unification_pair.rhs
+                    });
+                }
+
                 for i in 0..a1.len() {
                     let mut new_addr = unification_pair.addr.clone();
                     new_addr.push(i);
@@ -247,8 +255,6 @@ impl UnificationProblem {
                         halo: TypeTerm::unit(),
                         addr: new_addr
                     }) {
-//                        eprintln!("unified ladders at {}, r_halo = {:?}", i, r_halo);
-
                         for j in 0..a2.len() {
                             if i+j < a1.len() {
                                 let mut new_addr = unification_pair.addr.clone();
@@ -264,9 +270,7 @@ impl UnificationProblem {
                                         halo: TypeTerm::unit()
                                     }
                                 ) {
-                                    if rung_halo != TypeTerm::unit() {
-                                        halo.push(rung_halo);
-                                    }
+                                    halo.push(rung_halo);
                                 } else {
                                     return Err(UnificationError{ addr: new_addr, t1: lhs, t2: rhs })
                                 }
@@ -277,7 +281,7 @@ impl UnificationProblem {
                             if halo.len() == 1 {
                                 halo.pop().unwrap()
                             } else {
-                                TypeTerm::Ladder(halo)
+                                TypeTerm::Ladder(halo).strip()
                             });
                     } else {
                         halo.push(a1[i].clone());