Compare commits
No commits in common. "a9967f8183423b5f26ae6b9c78c71a0fbcfc1563" and "7f96b663240de36c2495fffa6985475ed225ca55" have entirely different histories.
a9967f8183
...
7f96b66324
5 changed files with 204 additions and 276 deletions
|
|
@ -48,7 +48,7 @@ impl<M: SugaredMorphism + Clone> SugaredMorphismBase<M> {
|
|||
|
||||
match (src_floor, dst_floor) {
|
||||
(SugaredTypeTerm::Struct{ struct_repr: struct_repr_lhs, members: members_lhs},
|
||||
SugaredTypeTerm::Struct { struct_repr: struct_repr_rhs, members: members_rhs })
|
||||
SugaredTypeTerm::Struct { struct_repr: _struct_repr_rhs, members: members_rhs })
|
||||
=> {
|
||||
// todo: optimization: check if struct repr match
|
||||
|
||||
|
|
@ -84,8 +84,7 @@ impl<M: SugaredMorphism + Clone> SugaredMorphismBase<M> {
|
|||
if ! failed && necessary {
|
||||
Some(MorphismInstance2::MapStruct {
|
||||
ψ: src_ψ,
|
||||
src_struct_repr: struct_repr_lhs.clone(),
|
||||
dst_struct_repr: struct_repr_rhs.clone(),
|
||||
struct_repr: struct_repr_lhs.clone(),
|
||||
member_morph
|
||||
})
|
||||
} else {
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ pub struct SugaredMorphismType {
|
|||
|
||||
impl SugaredMorphismType {
|
||||
pub fn strip_halo(&self) -> SugaredMorphismType {
|
||||
match (&self.src_type.clone().strip(), &self.dst_type.clone().strip()) {
|
||||
match (&self.src_type, &self.dst_type) {
|
||||
(SugaredTypeTerm::Ladder(rungs_lhs), SugaredTypeTerm::Ladder(rungs_rhs)) => {
|
||||
|
||||
let mut lhs_iter = rungs_lhs.iter();
|
||||
|
|
@ -63,9 +63,7 @@ impl SugaredMorphismType {
|
|||
}
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Seq { seq_repr:seq_repr_lhs, items:items_lhs },
|
||||
SugaredTypeTerm::Seq { seq_repr: seq_repr_rhs, items:items_rhs })
|
||||
=> {
|
||||
(SugaredTypeTerm::Seq { seq_repr:seq_repr_lhs, items:items_lhs }, SugaredTypeTerm::Seq { seq_repr: seq_repr_rhs, items:items_rhs }) => {
|
||||
let (rl, rr) = items_lhs.iter().zip(items_rhs.iter()).map(
|
||||
|(al,ar)| SugaredMorphismType{ src_type: al.clone(), dst_type: ar.clone() }.strip_halo()
|
||||
)
|
||||
|
|
@ -80,15 +78,12 @@ impl SugaredMorphismType {
|
|||
}
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Struct { struct_repr:struct_repr_lhs, members:members_lhs },
|
||||
SugaredTypeTerm::Struct { struct_repr: struct_repr_rhs, members:members_rhs })
|
||||
=> {
|
||||
(SugaredTypeTerm::Struct { struct_repr:seq_repr_lhs, members:items_lhs }, SugaredTypeTerm::Struct { struct_repr: seq_repr_rhs, members:items_rhs }) => {
|
||||
let mut rl = Vec::new();
|
||||
let mut rr = Vec::new();
|
||||
|
||||
for ar in members_rhs.iter() {
|
||||
let mut found = false;
|
||||
for al in members_lhs.iter() {
|
||||
for ar in items_rhs.iter() {
|
||||
for al in items_lhs.iter() {
|
||||
if al.symbol == ar.symbol {
|
||||
let x = SugaredMorphismType{ src_type: al.ty.clone(), dst_type: ar.ty.clone() }.strip_halo();
|
||||
rl.push( SugaredStructMember{
|
||||
|
|
@ -99,34 +94,24 @@ impl SugaredMorphismType {
|
|||
symbol: ar.symbol.clone(),
|
||||
ty: x.dst_type
|
||||
});
|
||||
found = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if !found {
|
||||
return SugaredMorphismType {
|
||||
src_type: SugaredTypeTerm::Struct { struct_repr: struct_repr_lhs.clone(), members:members_lhs.clone() },
|
||||
dst_type: SugaredTypeTerm::Struct { struct_repr: struct_repr_rhs.clone(), members:members_rhs.clone() }
|
||||
};
|
||||
}
|
||||
}
|
||||
|
||||
SugaredMorphismType {
|
||||
src_type: SugaredTypeTerm::Struct{ struct_repr: struct_repr_lhs.clone(), members: rl },
|
||||
dst_type: SugaredTypeTerm::Struct{ struct_repr: struct_repr_rhs.clone(), members: rr }
|
||||
src_type: SugaredTypeTerm::Struct{ struct_repr: seq_repr_lhs.clone(), members: rl },
|
||||
dst_type: SugaredTypeTerm::Struct{ struct_repr: seq_repr_rhs.clone(), members: rr }
|
||||
}
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Enum { enum_repr:enum_repr_lhs, variants:variants_lhs },
|
||||
SugaredTypeTerm::Enum { enum_repr: enum_repr_rhs, variants:variants_rhs })
|
||||
=> {
|
||||
(SugaredTypeTerm::Enum { enum_repr:seq_repr_lhs, variants:items_lhs }, SugaredTypeTerm::Enum { enum_repr: seq_repr_rhs, variants:items_rhs }) => {
|
||||
|
||||
let mut rl = Vec::new();
|
||||
let mut rr = Vec::new();
|
||||
|
||||
for ar in variants_rhs.iter() {
|
||||
let mut found = false;
|
||||
for al in variants_lhs.iter() {
|
||||
for ar in items_rhs.iter() {
|
||||
for al in items_lhs.iter() {
|
||||
if al.symbol == ar.symbol {
|
||||
let x = SugaredMorphismType{ src_type: al.ty.clone(), dst_type: ar.ty.clone() }.strip_halo();
|
||||
rl.push( SugaredEnumVariant{
|
||||
|
|
@ -137,22 +122,13 @@ impl SugaredMorphismType {
|
|||
symbol: ar.symbol.clone(),
|
||||
ty: x.dst_type
|
||||
});
|
||||
found = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if !found {
|
||||
return SugaredMorphismType {
|
||||
src_type: SugaredTypeTerm::Enum { enum_repr: enum_repr_lhs.clone(), variants:variants_lhs.clone() },
|
||||
dst_type: SugaredTypeTerm::Enum { enum_repr: enum_repr_rhs.clone(), variants:variants_rhs.clone() }
|
||||
};
|
||||
}
|
||||
}
|
||||
|
||||
SugaredMorphismType {
|
||||
src_type: SugaredTypeTerm::Enum{ enum_repr: enum_repr_lhs.clone(), variants: rl },
|
||||
dst_type: SugaredTypeTerm::Enum { enum_repr: enum_repr_rhs.clone(), variants: rr }
|
||||
src_type: SugaredTypeTerm::Enum{ enum_repr: seq_repr_lhs.clone(), variants: rl },
|
||||
dst_type: SugaredTypeTerm::Enum { enum_repr: seq_repr_rhs.clone(), variants: rr }
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -175,7 +151,7 @@ pub trait SugaredMorphism : Sized {
|
|||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Debug)]
|
||||
#[derive(Clone)]
|
||||
pub enum MorphismInstance2<M: SugaredMorphism + Clone> {
|
||||
Primitive{
|
||||
ψ: SugaredTypeTerm,
|
||||
|
|
@ -192,8 +168,7 @@ pub enum MorphismInstance2<M: SugaredMorphism + Clone> {
|
|||
},
|
||||
MapStruct{
|
||||
ψ: SugaredTypeTerm,
|
||||
src_struct_repr: Option<Box<SugaredTypeTerm>>,
|
||||
dst_struct_repr: Option<Box<SugaredTypeTerm>>,
|
||||
struct_repr: Option<Box<SugaredTypeTerm>>,
|
||||
member_morph: Vec< (String, MorphismInstance2<M>) >
|
||||
},
|
||||
MapEnum{
|
||||
|
|
@ -229,15 +204,14 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
}
|
||||
MorphismInstance2::Chain { path } => {
|
||||
if path.len() > 0 {
|
||||
let s = self.get_subst();
|
||||
SugaredMorphismType {
|
||||
src_type: path.first().unwrap().get_type().src_type.clone().apply_subst(&s).clone(),
|
||||
dst_type: path.last().unwrap().get_type().dst_type.clone().apply_subst(&s).clone()
|
||||
src_type: path.first().unwrap().get_type().src_type,
|
||||
dst_type: path.last().unwrap().get_type().dst_type
|
||||
}
|
||||
} else {
|
||||
SugaredMorphismType {
|
||||
src_type: SugaredTypeTerm::TypeID(TypeID::Fun(45454)),
|
||||
dst_type: SugaredTypeTerm::TypeID(TypeID::Fun(45454))
|
||||
src_type: SugaredTypeTerm::TypeID(TypeID::Var(45454)),
|
||||
dst_type: SugaredTypeTerm::TypeID(TypeID::Var(45454))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -255,11 +229,11 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
]).strip()
|
||||
}
|
||||
}
|
||||
MorphismInstance2::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
|
||||
MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
|
||||
SugaredMorphismType {
|
||||
src_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
|
||||
SugaredTypeTerm::Struct{
|
||||
struct_repr: src_struct_repr.clone(),
|
||||
struct_repr: struct_repr.clone(),
|
||||
members:
|
||||
member_morph.iter().map(|(symbol, morph)| {
|
||||
SugaredStructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
|
||||
|
|
@ -268,7 +242,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
]).strip(),
|
||||
dst_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
|
||||
SugaredTypeTerm::Struct{
|
||||
struct_repr: dst_struct_repr.clone(),
|
||||
struct_repr: struct_repr.clone(),
|
||||
members: member_morph.iter().map(|(symbol, morph)| {
|
||||
SugaredStructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
|
||||
}).collect()
|
||||
|
|
@ -315,7 +289,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
MorphismInstance2::MapSeq { ψ, seq_repr, item_morph } => {
|
||||
item_morph.get_subst()
|
||||
},
|
||||
MorphismInstance2::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
|
||||
MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
|
||||
let mut σ = HashMap::new();
|
||||
for (symbol, m) in member_morph.iter() {
|
||||
σ = σ.append(&mut m.get_subst());
|
||||
|
|
@ -330,21 +304,10 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
}
|
||||
|
||||
pub fn apply_subst(&mut self, γ: &std::collections::HashMap< TypeID, SugaredTypeTerm >) {
|
||||
let ty = self.get_type();
|
||||
match self {
|
||||
MorphismInstance2::Primitive { ψ, σ, morph } => {
|
||||
ψ.apply_subst(γ);
|
||||
for (n,t) in σ.iter_mut() {
|
||||
t.apply_subst(γ);
|
||||
}
|
||||
for (n,t) in γ.iter() {
|
||||
if let TypeID::Var(varid) = n {
|
||||
if morph.get_type().src_type.apply_subst(σ).contains_var(*varid)
|
||||
|| morph.get_type().dst_type.apply_subst(σ).contains_var(*varid) {
|
||||
σ.insert(n.clone(), t.clone());
|
||||
}
|
||||
}
|
||||
}
|
||||
ψ.apply_subst(σ);
|
||||
*σ = σ.clone().append(γ);
|
||||
},
|
||||
MorphismInstance2::Chain { path } => {
|
||||
for n in path.iter_mut() {
|
||||
|
|
@ -355,7 +318,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
ψ.apply_subst(γ);
|
||||
item_morph.apply_subst(γ);
|
||||
}
|
||||
MorphismInstance2::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
|
||||
MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
|
||||
for (_,ty) in member_morph {
|
||||
ty.apply_subst(γ);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,82 +1,99 @@
|
|||
use {
|
||||
crate::{dict::*, morphism::*, morphism_base::*, morphism_base_sugared::SugaredMorphismBase, morphism_path::*, morphism_path_sugared::SugaredShortestPathProblem, morphism_sugared::{MorphismInstance2, SugaredMorphism, SugaredMorphismType}, parser::*, unparser::*, SugaredTypeTerm, TypeTerm}
|
||||
crate::{dict::*, parser::*, unparser::*, morphism::*, TypeTerm, morphism_base::*, morphism_path::*}
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
fn print_subst(m: &std::collections::HashMap<TypeID, SugaredTypeTerm>, dict: &mut impl TypeDict) {
|
||||
fn print_subst(m: &std::collections::HashMap<TypeID, TypeTerm>, dict: &mut impl TypeDict) {
|
||||
eprintln!("{{");
|
||||
|
||||
for (k,v) in m.iter() {
|
||||
eprintln!(" {} --> {}",
|
||||
dict.get_typename(k).unwrap(),
|
||||
v.pretty(dict, 0)
|
||||
dict.unparse(v)
|
||||
);
|
||||
}
|
||||
|
||||
eprintln!("}}");
|
||||
}
|
||||
|
||||
fn print_path(dict: &mut impl TypeDict, path: &Vec<MorphismInstance2<DummyMorphism>>) {
|
||||
fn print_path(dict: &mut impl TypeDict, path: &Vec<MorphismInstance<DummyMorphism>>) {
|
||||
for n in path.iter() {
|
||||
eprintln!("
|
||||
ψ = {}
|
||||
morph {}
|
||||
--> {}
|
||||
with
|
||||
",
|
||||
n.get_type().src_type.pretty(dict, 0),
|
||||
n.get_type().dst_type.pretty(dict, 0),
|
||||
n.halo.clone().sugar(dict).pretty(dict, 0),
|
||||
n.m.get_type().src_type.sugar(dict).pretty(dict, 0),
|
||||
n.m.get_type().dst_type.sugar(dict).pretty(dict, 0),
|
||||
);
|
||||
print_subst(&n.get_subst(), dict)
|
||||
print_subst(&n.σ, dict)
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
#[derive(Clone, Debug, PartialEq, Eq)]
|
||||
struct DummyMorphism(SugaredMorphismType);
|
||||
impl SugaredMorphism for DummyMorphism {
|
||||
fn get_type(&self) -> SugaredMorphismType {
|
||||
self.0.clone()
|
||||
#[derive(Clone, Debug, PartialEq)]
|
||||
struct DummyMorphism(MorphismType);
|
||||
|
||||
impl Morphism for DummyMorphism {
|
||||
fn get_type(&self) -> MorphismType {
|
||||
self.0.clone().normalize()
|
||||
}
|
||||
|
||||
fn map_morphism(&self, seq_type: TypeTerm) -> Option<DummyMorphism> {
|
||||
Some(DummyMorphism(MorphismType {
|
||||
src_type: TypeTerm::App(vec![
|
||||
seq_type.clone(),
|
||||
self.0.src_type.clone()
|
||||
]),
|
||||
|
||||
dst_type: TypeTerm::App(vec![
|
||||
seq_type.clone(),
|
||||
self.0.dst_type.clone()
|
||||
])
|
||||
}))
|
||||
}
|
||||
}
|
||||
|
||||
fn morphism_test_setup() -> ( BimapTypeDict, SugaredMorphismBase<DummyMorphism> ) {
|
||||
fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
|
||||
let mut dict = BimapTypeDict::new();
|
||||
let mut base = SugaredMorphismBase::<DummyMorphism>::new();
|
||||
let mut base = MorphismBase::<DummyMorphism>::new( vec![ dict.parse("Seq").expect("") ] );
|
||||
|
||||
dict.add_varname("Radix".into());
|
||||
dict.add_varname("SrcRadix".into());
|
||||
dict.add_varname("DstRadix".into());
|
||||
|
||||
base.add_morphism(
|
||||
DummyMorphism(SugaredMorphismType{
|
||||
src_type: dict.parse("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
|
||||
DummyMorphism(MorphismType{
|
||||
src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
|
||||
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
|
||||
})
|
||||
);
|
||||
base.add_morphism(
|
||||
DummyMorphism(SugaredMorphismType{
|
||||
src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Digit Radix> ~ Char").unwrap().sugar(&mut dict)
|
||||
DummyMorphism(MorphismType{
|
||||
src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
|
||||
dst_type: dict.parse("<Digit Radix> ~ Char").unwrap()
|
||||
})
|
||||
);
|
||||
base.add_morphism(
|
||||
DummyMorphism(SugaredMorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict)
|
||||
DummyMorphism(MorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap()
|
||||
})
|
||||
);
|
||||
base.add_morphism(
|
||||
DummyMorphism(SugaredMorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict)
|
||||
DummyMorphism(MorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap()
|
||||
})
|
||||
);
|
||||
base.add_morphism(
|
||||
DummyMorphism(SugaredMorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict)
|
||||
DummyMorphism(MorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix>~ℤ_2^64~machine.UInt64>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix>~ℤ_2^64~machine.UInt64>").unwrap()
|
||||
})
|
||||
);
|
||||
|
||||
|
|
@ -87,23 +104,23 @@ fn morphism_test_setup() -> ( BimapTypeDict, SugaredMorphismBase<DummyMorphism>
|
|||
fn test_morphism_path1() {
|
||||
let (mut dict, mut base) = morphism_test_setup();
|
||||
|
||||
let path = SugaredShortestPathProblem::new(&base, SugaredMorphismType {
|
||||
src_type: dict.parse("<Digit 10> ~ Char").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Digit 10> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict),
|
||||
let path = ShortestPathProblem::new(&base, MorphismType {
|
||||
src_type: dict.parse("<Digit 10> ~ Char").unwrap(),
|
||||
dst_type: dict.parse("<Digit 10> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
|
||||
}).solve();
|
||||
|
||||
assert_eq!(
|
||||
path,
|
||||
Some(
|
||||
vec![
|
||||
MorphismInstance2::Primitive {
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), SugaredTypeTerm::Num(10)),
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType {
|
||||
src_type: dict.parse("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
|
||||
halo: TypeTerm::unit(),
|
||||
m: DummyMorphism(MorphismType {
|
||||
src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
|
||||
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
|
||||
}),
|
||||
}
|
||||
]
|
||||
|
|
@ -115,28 +132,24 @@ fn test_morphism_path1() {
|
|||
fn test_morphism_path2() {
|
||||
let (mut dict, mut base) = morphism_test_setup();
|
||||
|
||||
let path = SugaredShortestPathProblem::new(&base, SugaredMorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
|
||||
let path = ShortestPathProblem::new(&base, MorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
|
||||
}).solve();
|
||||
|
||||
assert_eq!(
|
||||
path,
|
||||
Some(
|
||||
vec![
|
||||
MorphismInstance2::MapSeq {
|
||||
ψ: dict.parse("ℕ ~ <PosInt 10 BigEndian>").expect("").sugar(&mut dict),
|
||||
seq_repr: None,
|
||||
item_morph: Box::new(MorphismInstance2::Primitive {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), SugaredTypeTerm::Num(10)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType {
|
||||
src_type: dict.parse("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
|
||||
}),
|
||||
})
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
|
||||
].into_iter().collect(),
|
||||
halo: dict.parse("ℕ ~ <PosInt 10 BigEndian>").expect(""),
|
||||
m: DummyMorphism(MorphismType {
|
||||
src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
|
||||
dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
|
||||
}),
|
||||
}
|
||||
]
|
||||
));
|
||||
|
|
@ -147,9 +160,9 @@ fn test_morphism_path2() {
|
|||
fn test_morphism_path3() {
|
||||
let (mut dict, mut base) = morphism_test_setup();
|
||||
|
||||
let path = SugaredShortestPathProblem::new(&base, SugaredMorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
|
||||
let path = ShortestPathProblem::new(&base, MorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
|
||||
}).solve();
|
||||
|
||||
if let Some(path) = path.as_ref() {
|
||||
|
|
@ -160,30 +173,26 @@ fn test_morphism_path3() {
|
|||
path,
|
||||
Some(
|
||||
vec![
|
||||
MorphismInstance2::MapSeq {
|
||||
ψ: dict.parse("ℕ ~ <PosInt 10 LittleEndian>").expect("").sugar(&mut dict),
|
||||
seq_repr: None,
|
||||
item_morph: Box::new(MorphismInstance2::Primitive {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), SugaredTypeTerm::Num(10)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType {
|
||||
src_type: dict.parse("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
|
||||
}),
|
||||
})
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
|
||||
].into_iter().collect(),
|
||||
halo: dict.parse("ℕ ~ <PosInt 10 LittleEndian>").expect(""),
|
||||
m: DummyMorphism(MorphismType {
|
||||
src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
|
||||
dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
|
||||
}),
|
||||
},
|
||||
|
||||
MorphismInstance2::Primitive {
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"SrcRadix".into()).unwrap(), SugaredTypeTerm::Num(10)),
|
||||
(dict.get_typeid(&"DstRadix".into()).unwrap(), SugaredTypeTerm::Num(16)),
|
||||
(dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
|
||||
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict)
|
||||
halo: TypeTerm::unit(),
|
||||
m: DummyMorphism(MorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
|
||||
}),
|
||||
}
|
||||
]
|
||||
|
|
@ -196,9 +205,9 @@ fn test_morphism_path3() {
|
|||
fn test_morphism_path4() {
|
||||
let (mut dict, mut base) = morphism_test_setup();
|
||||
|
||||
let path = SugaredShortestPathProblem::new(&base, SugaredMorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().sugar(&mut dict)
|
||||
let path = ShortestPathProblem::new(&base, MorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
|
||||
}).solve();
|
||||
|
||||
if let Some(path) = path.as_ref() {
|
||||
|
|
@ -209,47 +218,40 @@ fn test_morphism_path4() {
|
|||
path,
|
||||
Some(
|
||||
vec![
|
||||
MorphismInstance2::MapSeq {
|
||||
ψ: dict.parse("ℕ ~ <PosInt 10 LittleEndian>").expect("").sugar(&mut dict),
|
||||
seq_repr: None,
|
||||
item_morph: Box::new(MorphismInstance2::Primitive {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), SugaredTypeTerm::Num(10)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType {
|
||||
src_type: dict.parse("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
|
||||
}),
|
||||
})
|
||||
},
|
||||
|
||||
MorphismInstance2::Primitive {
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"SrcRadix".into()).unwrap(), SugaredTypeTerm::Num(10)),
|
||||
(dict.get_typeid(&"DstRadix".into()).unwrap(), SugaredTypeTerm::Num(16)),
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict)
|
||||
halo: dict.parse("ℕ ~ <PosInt 10 LittleEndian>").expect(""),
|
||||
m: DummyMorphism(MorphismType {
|
||||
src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
|
||||
dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
|
||||
}),
|
||||
},
|
||||
|
||||
MorphismInstance2::MapSeq {
|
||||
ψ: dict.parse("ℕ ~ <PosInt 16 LittleEndian>").expect("").sugar(&mut dict),
|
||||
seq_repr: None,
|
||||
item_morph: Box::new(MorphismInstance2::Primitive {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), SugaredTypeTerm::Num(16)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType {
|
||||
src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Digit Radix> ~ Char").unwrap().sugar(&mut dict)
|
||||
}),
|
||||
})
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
|
||||
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
|
||||
].into_iter().collect(),
|
||||
halo: TypeTerm::unit(),
|
||||
m: DummyMorphism(MorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
|
||||
}),
|
||||
},
|
||||
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
|
||||
].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(),
|
||||
dst_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap()
|
||||
}),
|
||||
},
|
||||
|
||||
]
|
||||
));
|
||||
}
|
||||
|
|
@ -261,9 +263,9 @@ fn test_morphism_path4() {
|
|||
fn test_morphism_path_posint() {
|
||||
let (mut dict, mut base) = morphism_test_setup();
|
||||
|
||||
let path = SugaredShortestPathProblem::new(&base, SugaredMorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().sugar(&mut dict),
|
||||
let path = ShortestPathProblem::new(&base, MorphismType {
|
||||
src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap(),
|
||||
}).solve();
|
||||
|
||||
if let Some(path) = path.as_ref() {
|
||||
|
|
@ -274,72 +276,62 @@ fn test_morphism_path_posint() {
|
|||
path,
|
||||
Some(
|
||||
vec![
|
||||
MorphismInstance2::MapSeq {
|
||||
ψ: dict.parse("ℕ ~ <PosInt 10 BigEndian>").expect("").sugar(&mut dict),
|
||||
seq_repr: None,
|
||||
item_morph: Box::new(MorphismInstance2::Primitive {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), SugaredTypeTerm::Num(10)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType {
|
||||
src_type: dict.parse("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
|
||||
}),
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
|
||||
].into_iter().collect(),
|
||||
halo: dict.parse("ℕ ~ <PosInt 10 BigEndian>").unwrap(),
|
||||
m: DummyMorphism(MorphismType {
|
||||
src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
|
||||
dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
|
||||
}),
|
||||
},
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
|
||||
].into_iter().collect(),
|
||||
halo: TypeTerm::unit(),
|
||||
m: DummyMorphism(MorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
|
||||
}),
|
||||
},
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
|
||||
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
|
||||
].into_iter().collect(),
|
||||
halo: TypeTerm::unit(),
|
||||
m: DummyMorphism(MorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
|
||||
}),
|
||||
},
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
|
||||
].into_iter().collect(),
|
||||
halo: TypeTerm::unit(),
|
||||
m: DummyMorphism(MorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
|
||||
}),
|
||||
},
|
||||
MorphismInstance {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16))
|
||||
].into_iter().collect(),
|
||||
halo: dict.parse("ℕ ~ <PosInt 16 BigEndian>").unwrap(),
|
||||
m: DummyMorphism(MorphismType{
|
||||
src_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
|
||||
dst_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap()
|
||||
})
|
||||
},
|
||||
|
||||
MorphismInstance2::Primitive {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), SugaredTypeTerm::Num(10)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict)
|
||||
}),
|
||||
},
|
||||
MorphismInstance2::Primitive {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"SrcRadix".into()).unwrap(), SugaredTypeTerm::Num(10)),
|
||||
(dict.get_typeid(&"DstRadix".into()).unwrap(), SugaredTypeTerm::Num(16)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict)
|
||||
}),
|
||||
},
|
||||
MorphismInstance2::Primitive {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), SugaredTypeTerm::Num(16)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType{
|
||||
src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
|
||||
}),
|
||||
},
|
||||
|
||||
MorphismInstance2::MapSeq {
|
||||
ψ: dict.parse("ℕ ~ <PosInt 16 BigEndian>").expect("").sugar(&mut dict),
|
||||
seq_repr: None,
|
||||
item_morph: Box::new(MorphismInstance2::Primitive {
|
||||
σ: vec![
|
||||
(dict.get_typeid(&"Radix".into()).unwrap(), SugaredTypeTerm::Num(16)),
|
||||
].into_iter().collect(),
|
||||
ψ: SugaredTypeTerm::unit(),
|
||||
morph: DummyMorphism(SugaredMorphismType {
|
||||
src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Digit Radix> ~ Char").unwrap().sugar(&mut dict)
|
||||
}),
|
||||
})
|
||||
},
|
||||
}
|
||||
]
|
||||
)
|
||||
);
|
||||
}
|
||||
/*
|
||||
|
||||
#[test]
|
||||
fn test_steiner_tree() {
|
||||
let (mut dict, mut base) = morphism_test_setup();
|
||||
|
|
@ -467,4 +459,3 @@ fn test_morphism_path_listedit()
|
|||
])
|
||||
);
|
||||
}
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -397,7 +397,7 @@ fn test_list_subtype_sugared() {
|
|||
];
|
||||
|
||||
assert_eq!(
|
||||
SugaredUnificationProblem::new_sub(subtype_constraints).solve(),
|
||||
SugaredUnificationProblem::new_sub(&mut dict, subtype_constraints).solve(),
|
||||
Ok((
|
||||
vec![ SugaredTypeTerm::Ladder(vec![]) ],
|
||||
vec![
|
||||
|
|
@ -437,7 +437,7 @@ pub fn test_subtype_delim_sugared() {
|
|||
];
|
||||
|
||||
assert_eq!(
|
||||
SugaredUnificationProblem::new_sub(subtype_constraints).solve(),
|
||||
SugaredUnificationProblem::new_sub(&mut dict, subtype_constraints).solve(),
|
||||
Ok((
|
||||
// halo types for each rhs in the sub-equations
|
||||
vec![
|
||||
|
|
|
|||
|
|
@ -138,17 +138,7 @@ impl SugaredUnificationProblem {
|
|||
(SugaredTypeTerm::Seq{ seq_repr: lhs_seq_repr, items: lhs_items },
|
||||
SugaredTypeTerm::Seq { seq_repr: rhs_seq_repr, items: rhs_items })
|
||||
=> {
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
new_addr.push(0);
|
||||
|
||||
if let Some(rhs_seq_repr) = rhs_seq_repr.as_ref() {
|
||||
if let Some(lhs_seq_repr) = lhs_seq_repr.as_ref() {
|
||||
let _seq_repr_ψ = self.eval_equation(SugaredUnificationPair { addr: new_addr.clone(), lhs: *lhs_seq_repr.clone(), rhs: *rhs_seq_repr.clone() })?;
|
||||
} else {
|
||||
return Err(SugaredUnificationError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
|
||||
}
|
||||
}
|
||||
|
||||
// todo: unify seq reprü
|
||||
|
||||
if lhs_items.len() == rhs_items.len() {
|
||||
for (i, (lhs_ty, rhs_ty)) in lhs_items.into_iter().zip(rhs_items.into_iter()).enumerate()
|
||||
|
|
@ -165,14 +155,7 @@ impl SugaredUnificationProblem {
|
|||
(SugaredTypeTerm::Struct{ struct_repr: lhs_struct_repr, members: lhs_members },
|
||||
SugaredTypeTerm::Struct{ struct_repr: rhs_struct_repr, members: rhs_members })
|
||||
=> {
|
||||
let new_addr = unification_pair.addr.clone();
|
||||
if let Some(rhs_struct_repr) = rhs_struct_repr.as_ref() {
|
||||
if let Some(lhs_struct_repr) = lhs_struct_repr.as_ref() {
|
||||
let _struct_repr_ψ = self.eval_subtype(SugaredUnificationPair { addr: new_addr.clone(), lhs: *lhs_struct_repr.clone(), rhs: *rhs_struct_repr.clone() })?;
|
||||
} else {
|
||||
return Err(SugaredUnificationError{ addr: new_addr.clone(), t1: unification_pair.lhs, t2: unification_pair.rhs });
|
||||
}
|
||||
}
|
||||
// todo: unify struct repr
|
||||
|
||||
if lhs_members.len() == rhs_members.len() {
|
||||
for (i,
|
||||
|
|
@ -193,15 +176,7 @@ impl SugaredUnificationProblem {
|
|||
(SugaredTypeTerm::Enum{ enum_repr: lhs_enum_repr, variants: lhs_variants },
|
||||
SugaredTypeTerm::Enum{ enum_repr: rhs_enum_repr, variants: rhs_variants })
|
||||
=> {
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
if let Some(rhs_enum_repr) = rhs_enum_repr.as_ref() {
|
||||
if let Some(lhs_enum_repr) = lhs_enum_repr.as_ref() {
|
||||
let _enum_repr_ψ = self.eval_subtype(SugaredUnificationPair { addr: new_addr.clone(), lhs: *lhs_enum_repr.clone(), rhs: *rhs_enum_repr.clone() })?;
|
||||
} else {
|
||||
return Err(SugaredUnificationError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
|
||||
}
|
||||
}
|
||||
|
||||
// todo: unify enum repr
|
||||
|
||||
if lhs_variants.len() == rhs_variants.len() {
|
||||
for (i,
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue