From e0334f4d5ca6cf41c671e5217bccd8240815db33 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Tue, 6 Aug 2024 15:37:23 +0200 Subject: [PATCH] fix returned halo type in find_morphism_with_subtyping() --- src/morphism.rs | 5 ++++- src/test/morphism.rs | 42 +++++++++++++++++++++++++++++++++++++++++- 2 files changed, 45 insertions(+), 2 deletions(-) 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::>() + )) + ); }