diff --git a/src/morphism.rs b/src/morphism.rs index e713e61..7b2ac5e 100644 --- a/src/morphism.rs +++ b/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, σ, }); } diff --git a/src/test/morphism.rs b/src/test/morphism.rs index 6320f72..f9bb3ba 100644 --- a/src/test/morphism.rs +++ b/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"); } } -*/ diff --git a/src/test/unification.rs b/src/test/unification.rs index 7a1acb3..c9cedd4 100644 --- a/src/test/unification.rs +++ b/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(); diff --git a/src/unification.rs b/src/unification.rs index ef8c0fd..eb55646 100644 --- a/src/unification.rs +++ b/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());