diff --git a/src/test/morphism.rs b/src/test/morphism.rs index 294ac00..fc0419a 100644 --- a/src/test/morphism.rs +++ b/src/test/morphism.rs @@ -419,6 +419,12 @@ fn test_morphism_path_listedit() dst_type: dict.parse("Char ~ EditTree").unwrap() }) ); + base.add_morphism( + DummyMorphism(MorphismType{ + src_type: dict.parse("<List~Vec Char>").unwrap(), + dst_type: dict.parse("<List Char>").unwrap() + }) + ); base.add_morphism( DummyMorphism(MorphismType{ src_type: dict.parse("<List Char>").unwrap(), @@ -483,12 +489,12 @@ fn test_morphism_path_listedit() }, MorphismInstance { m: DummyMorphism(MorphismType{ - src_type: dict.parse("<List~Vec ReprTree>").unwrap(), - dst_type: dict.parse("<List ReprTree> ~ EditTree").unwrap() + src_type: dict.parse("<List~Vec Char~ReprTree>").unwrap(), + dst_type: dict.parse("<List Char> ~ EditTree").unwrap() }), - halo: dict.parse("<Seq~List <Digit 10>~Char>").unwrap(), + halo: dict.parse("<Seq~List <Digit 10>>").unwrap(), σ: HashMap::new() - } + }, ]) ); } diff --git a/src/test/unification.rs b/src/test/unification.rs index de31d5b..dfff9d2 100644 --- a/src/test/unification.rs +++ b/src/test/unification.rs @@ -142,7 +142,7 @@ fn test_subtype_unification() { assert_eq!( UnificationProblem::new_sub(vec![ - (dict.parse("<Seq~T <Digit 10> ~ Char>").unwrap(), + (dict.parse("<Seq~T <Digit 10> ~ Char ~ Ascii>").unwrap(), dict.parse("<Seq~<LengthPrefix x86.UInt64> Char ~ Ascii>").unwrap()), ]).solve(), Ok(( diff --git a/src/unification.rs b/src/unification.rs index eb55646..5fb0818 100644 --- a/src/unification.rs +++ b/src/unification.rs @@ -255,6 +255,7 @@ impl UnificationProblem { halo: TypeTerm::unit(), addr: new_addr }) { + if a1.len() == i+a2.len() { for j in 0..a2.len() { if i+j < a1.len() { let mut new_addr = unification_pair.addr.clone(); @@ -283,6 +284,13 @@ impl UnificationProblem { } else { TypeTerm::Ladder(halo).strip() }); + } else { + /* after the first match, the remaining ladders dont have the same length + * thus it cannot be a subtype, + * at most it could be a trait type + */ + } + } else { halo.push(a1[i].clone()); //eprintln!("could not unify ladders"); @@ -339,7 +347,7 @@ impl UnificationProblem { // eprintln!("after strip: {:?}", y); // eprintln!("APP<> eval {:?} \n ?<=? {:?} ", x, y); - if let Ok(halo) = self.eval_subtype( + match self.eval_subtype( UnificationPair { lhs: x.clone(), rhs: y.clone(), @@ -347,6 +355,7 @@ impl UnificationProblem { addr: new_addr, } ) { + Ok(halo) => { if halo == TypeTerm::unit() { let mut y = y.clone(); y.apply_substitution(&|k| self.σ.get(k).cloned()); @@ -376,8 +385,8 @@ impl UnificationProblem { halo_args.push(halo); n_halos_required += 1; } - } else { - return Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }); + }, + Err(err) => { return Err(err); } } }