diff --git a/src/morphism.rs b/src/morphism.rs index 3211651..0796c91 100644 --- a/src/morphism.rs +++ b/src/morphism.rs @@ -230,7 +230,10 @@ impl MorphismBase { src_type: TypeTerm::Ladder(src_lnf.clone()), dst_type: TypeTerm::Ladder(dst_lnf.clone()) }) { - return Some((m, TypeTerm::Ladder(halo), σ)); + 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); diff --git a/src/test/morphism.rs b/src/test/morphism.rs index fa4b492..47bd100 100644 --- a/src/test/morphism.rs +++ b/src/test/morphism.rs @@ -4,7 +4,7 @@ use { //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ -#[derive(Clone)] +#[derive(Clone, Debug, PartialEq)] struct DummyMorphism(MorphismType); impl Morphism for DummyMorphism { @@ -83,5 +83,45 @@ fn test_morphism_path() { ] ) ); + + assert_eq!( + base.find_morphism_path(MorphismType { + src_type: dict.parse("Symbol ~ ℕ ~ ~ ~ Char>").unwrap(), + dst_type: dict.parse("Symbol ~ ℕ ~ ~ ~ Char>").unwrap() + }), + Some( + vec![ + dict.parse("Symbol ~ ℕ ~ ~ ~ Char>").unwrap().normalize(), + dict.parse("Symbol ~ ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), + dict.parse("Symbol ~ ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), + dict.parse("Symbol ~ ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), + dict.parse("Symbol ~ ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), + dict.parse("Symbol ~ ℕ ~ ~ ~ Char>").unwrap().normalize(), + ] + ) + ); + + assert_eq!( + base.find_morphism_with_subtyping( + &MorphismType { + src_type: dict.parse("Symbol ~ ℕ ~ ~ ~ Char>").unwrap(), + dst_type: dict.parse("Symbol ~ ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap() + } + ), + + Some(( + DummyMorphism(MorphismType{ + src_type: dict.parse(" ~ Char>").unwrap(), + dst_type: dict.parse(" ~ ℤ_2^64 ~ machine.UInt64>").unwrap() + }), + + dict.parse("Symbol ~ ℕ ~ ~ >").unwrap(), + + vec![ + (dict.get_typeid(&"Radix".into()).unwrap(), + dict.parse("10").unwrap()) + ].into_iter().collect::>() + )) + ); }