fix returned halo type in find_morphism_with_subtyping()
This commit is contained in:
parent
811adde1b9
commit
e0334f4d5c
2 changed files with 45 additions and 2 deletions
|
@ -230,7 +230,10 @@ impl<M: Morphism + Clone> MorphismBase<M> {
|
||||||
src_type: TypeTerm::Ladder(src_lnf.clone()),
|
src_type: TypeTerm::Ladder(src_lnf.clone()),
|
||||||
dst_type: TypeTerm::Ladder(dst_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 {
|
} else {
|
||||||
if src_lnf[0] == dst_lnf[0] {
|
if src_lnf[0] == dst_lnf[0] {
|
||||||
src_lnf.remove(0);
|
src_lnf.remove(0);
|
||||||
|
|
|
@ -4,7 +4,7 @@ use {
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||||
|
|
||||||
#[derive(Clone)]
|
#[derive(Clone, Debug, PartialEq)]
|
||||||
struct DummyMorphism(MorphismType);
|
struct DummyMorphism(MorphismType);
|
||||||
|
|
||||||
impl Morphism for DummyMorphism {
|
impl Morphism for DummyMorphism {
|
||||||
|
@ -83,5 +83,45 @@ fn test_morphism_path() {
|
||||||
]
|
]
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
|
||||||
|
assert_eq!(
|
||||||
|
base.find_morphism_path(MorphismType {
|
||||||
|
src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
|
||||||
|
dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
|
||||||
|
}),
|
||||||
|
Some(
|
||||||
|
vec![
|
||||||
|
dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().normalize(),
|
||||||
|
dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
|
||||||
|
dict.parse("Symbol ~ ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
|
||||||
|
dict.parse("Symbol ~ ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
|
||||||
|
dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
|
||||||
|
dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().normalize(),
|
||||||
|
]
|
||||||
|
)
|
||||||
|
);
|
||||||
|
|
||||||
|
assert_eq!(
|
||||||
|
base.find_morphism_with_subtyping(
|
||||||
|
&MorphismType {
|
||||||
|
src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
|
||||||
|
dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
|
||||||
|
}
|
||||||
|
),
|
||||||
|
|
||||||
|
Some((
|
||||||
|
DummyMorphism(MorphismType{
|
||||||
|
src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
|
||||||
|
dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
|
||||||
|
}),
|
||||||
|
|
||||||
|
dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>>").unwrap(),
|
||||||
|
|
||||||
|
vec![
|
||||||
|
(dict.get_typeid(&"Radix".into()).unwrap(),
|
||||||
|
dict.parse("10").unwrap())
|
||||||
|
].into_iter().collect::<std::collections::HashMap<TypeID, TypeTerm>>()
|
||||||
|
))
|
||||||
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue