diff --git a/src/morphism_base_sugared.rs b/src/morphism_base_sugared.rs
index 1fb1dcf..93d3b10 100644
--- a/src/morphism_base_sugared.rs
+++ b/src/morphism_base_sugared.rs
@@ -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,7 +84,8 @@ impl<M: SugaredMorphism + Clone> SugaredMorphismBase<M> {
if ! failed && necessary {
Some(MorphismInstance2::MapStruct {
ψ: src_ψ,
- struct_repr: struct_repr_lhs.clone(),
+ src_struct_repr: struct_repr_lhs.clone(),
+ dst_struct_repr: struct_repr_rhs.clone(),
member_morph
})
} else {
diff --git a/src/morphism_sugared.rs b/src/morphism_sugared.rs
index f9c36eb..5e10f65 100644
--- a/src/morphism_sugared.rs
+++ b/src/morphism_sugared.rs
@@ -15,7 +15,7 @@ pub struct SugaredMorphismType {
impl SugaredMorphismType {
pub fn strip_halo(&self) -> SugaredMorphismType {
- match (&self.src_type, &self.dst_type) {
+ match (&self.src_type.clone().strip(), &self.dst_type.clone().strip()) {
(SugaredTypeTerm::Ladder(rungs_lhs), SugaredTypeTerm::Ladder(rungs_rhs)) => {
let mut lhs_iter = rungs_lhs.iter();
@@ -63,7 +63,9 @@ 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()
)
@@ -78,12 +80,15 @@ impl SugaredMorphismType {
}
}
- (SugaredTypeTerm::Struct { struct_repr:seq_repr_lhs, members:items_lhs }, SugaredTypeTerm::Struct { struct_repr: seq_repr_rhs, members:items_rhs }) => {
+ (SugaredTypeTerm::Struct { struct_repr:struct_repr_lhs, members:members_lhs },
+ SugaredTypeTerm::Struct { struct_repr: struct_repr_rhs, members:members_rhs })
+ => {
let mut rl = Vec::new();
let mut rr = Vec::new();
- for ar in items_rhs.iter() {
- for al in items_lhs.iter() {
+ for ar in members_rhs.iter() {
+ let mut found = false;
+ for al in members_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{
@@ -94,24 +99,34 @@ 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: seq_repr_lhs.clone(), members: rl },
- dst_type: SugaredTypeTerm::Struct{ struct_repr: seq_repr_rhs.clone(), members: rr }
+ src_type: SugaredTypeTerm::Struct{ struct_repr: struct_repr_lhs.clone(), members: rl },
+ dst_type: SugaredTypeTerm::Struct{ struct_repr: struct_repr_rhs.clone(), members: rr }
}
}
- (SugaredTypeTerm::Enum { enum_repr:seq_repr_lhs, variants:items_lhs }, SugaredTypeTerm::Enum { enum_repr: seq_repr_rhs, variants:items_rhs }) => {
-
+ (SugaredTypeTerm::Enum { enum_repr:enum_repr_lhs, variants:variants_lhs },
+ SugaredTypeTerm::Enum { enum_repr: enum_repr_rhs, variants:variants_rhs })
+ => {
let mut rl = Vec::new();
let mut rr = Vec::new();
- for ar in items_rhs.iter() {
- for al in items_lhs.iter() {
+ for ar in variants_rhs.iter() {
+ let mut found = false;
+ for al in variants_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{
@@ -122,13 +137,22 @@ 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: seq_repr_lhs.clone(), variants: rl },
- dst_type: SugaredTypeTerm::Enum { enum_repr: seq_repr_rhs.clone(), variants: rr }
+ src_type: SugaredTypeTerm::Enum{ enum_repr: enum_repr_lhs.clone(), variants: rl },
+ dst_type: SugaredTypeTerm::Enum { enum_repr: enum_repr_rhs.clone(), variants: rr }
}
}
@@ -151,7 +175,7 @@ pub trait SugaredMorphism : Sized {
}
}
-#[derive(Clone)]
+#[derive(Clone, PartialEq, Debug)]
pub enum MorphismInstance2<M: SugaredMorphism + Clone> {
Primitive{
ψ: SugaredTypeTerm,
@@ -168,7 +192,8 @@ pub enum MorphismInstance2<M: SugaredMorphism + Clone> {
},
MapStruct{
ψ: SugaredTypeTerm,
- struct_repr: Option<Box<SugaredTypeTerm>>,
+ src_struct_repr: Option<Box<SugaredTypeTerm>>,
+ dst_struct_repr: Option<Box<SugaredTypeTerm>>,
member_morph: Vec< (String, MorphismInstance2<M>) >
},
MapEnum{
@@ -204,14 +229,15 @@ 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,
- dst_type: path.last().unwrap().get_type().dst_type
+ 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()
}
} else {
SugaredMorphismType {
- src_type: SugaredTypeTerm::TypeID(TypeID::Var(45454)),
- dst_type: SugaredTypeTerm::TypeID(TypeID::Var(45454))
+ src_type: SugaredTypeTerm::TypeID(TypeID::Fun(45454)),
+ dst_type: SugaredTypeTerm::TypeID(TypeID::Fun(45454))
}
}
}
@@ -229,11 +255,11 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
]).strip()
}
}
- MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
+ MorphismInstance2::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
SugaredMorphismType {
src_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
SugaredTypeTerm::Struct{
- struct_repr: struct_repr.clone(),
+ struct_repr: src_struct_repr.clone(),
members:
member_morph.iter().map(|(symbol, morph)| {
SugaredStructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
@@ -242,7 +268,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
]).strip(),
dst_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
SugaredTypeTerm::Struct{
- struct_repr: struct_repr.clone(),
+ struct_repr: dst_struct_repr.clone(),
members: member_morph.iter().map(|(symbol, morph)| {
SugaredStructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
}).collect()
@@ -289,7 +315,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
MorphismInstance2::MapSeq { ψ, seq_repr, item_morph } => {
item_morph.get_subst()
},
- MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
+ MorphismInstance2::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
let mut σ = HashMap::new();
for (symbol, m) in member_morph.iter() {
σ = σ.append(&mut m.get_subst());
@@ -304,10 +330,21 @@ 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(σ);
- *σ = σ.clone().append(γ);
+ ψ.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());
+ }
+ }
+ }
},
MorphismInstance2::Chain { path } => {
for n in path.iter_mut() {
@@ -318,7 +355,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
ψ.apply_subst(γ);
item_morph.apply_subst(γ);
}
- MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
+ MorphismInstance2::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
for (_,ty) in member_morph {
ty.apply_subst(γ);
}
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index dbc03dc..56d3059 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -1,99 +1,82 @@
use {
- crate::{dict::*, parser::*, unparser::*, morphism::*, TypeTerm, morphism_base::*, morphism_path::*}
+ crate::{dict::*, morphism::*, morphism_base::*, morphism_base_sugared::SugaredMorphismBase, morphism_path::*, morphism_path_sugared::SugaredShortestPathProblem, morphism_sugared::{MorphismInstance2, SugaredMorphism, SugaredMorphismType}, parser::*, unparser::*, SugaredTypeTerm, TypeTerm}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-fn print_subst(m: &std::collections::HashMap<TypeID, TypeTerm>, dict: &mut impl TypeDict) {
+fn print_subst(m: &std::collections::HashMap<TypeID, SugaredTypeTerm>, dict: &mut impl TypeDict) {
eprintln!("{{");
for (k,v) in m.iter() {
eprintln!(" {} --> {}",
dict.get_typename(k).unwrap(),
- dict.unparse(v)
+ v.pretty(dict, 0)
);
}
eprintln!("}}");
}
-fn print_path(dict: &mut impl TypeDict, path: &Vec<MorphismInstance<DummyMorphism>>) {
+fn print_path(dict: &mut impl TypeDict, path: &Vec<MorphismInstance2<DummyMorphism>>) {
for n in path.iter() {
eprintln!("
-ψ = {}
morph {}
--> {}
with
",
- 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),
+ n.get_type().src_type.pretty(dict, 0),
+ n.get_type().dst_type.pretty(dict, 0),
);
- print_subst(&n.σ, dict)
+ print_subst(&n.get_subst(), dict)
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-#[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()
- ])
- }))
+#[derive(Clone, Debug, PartialEq, Eq)]
+struct DummyMorphism(SugaredMorphismType);
+impl SugaredMorphism for DummyMorphism {
+ fn get_type(&self) -> SugaredMorphismType {
+ self.0.clone()
}
}
-fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
+fn morphism_test_setup() -> ( BimapTypeDict, SugaredMorphismBase<DummyMorphism> ) {
let mut dict = BimapTypeDict::new();
- let mut base = MorphismBase::<DummyMorphism>::new( vec![ dict.parse("Seq").expect("") ] );
+ let mut base = SugaredMorphismBase::<DummyMorphism>::new();
dict.add_varname("Radix".into());
dict.add_varname("SrcRadix".into());
dict.add_varname("DstRadix".into());
base.add_morphism(
- DummyMorphism(MorphismType{
- src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
- dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
+ 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)
})
);
base.add_morphism(
- DummyMorphism(MorphismType{
- src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
- dst_type: dict.parse("<Digit Radix> ~ Char").unwrap()
+ 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)
})
);
base.add_morphism(
- 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()
+ 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)
})
);
base.add_morphism(
- 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()
+ 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)
})
);
base.add_morphism(
- 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()
+ 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)
})
);
@@ -104,23 +87,23 @@ fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
fn test_morphism_path1() {
let (mut dict, mut base) = morphism_test_setup();
- 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(),
+ 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),
}).solve();
assert_eq!(
path,
Some(
vec![
- MorphismInstance {
+ MorphismInstance2::Primitive {
σ: vec![
- (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+ (dict.get_typeid(&"Radix".into()).unwrap(), SugaredTypeTerm::Num(10)),
].into_iter().collect(),
- 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()
+ ψ: 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)
}),
}
]
@@ -132,24 +115,28 @@ fn test_morphism_path1() {
fn test_morphism_path2() {
let (mut dict, mut base) = morphism_test_setup();
- 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(),
+ 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),
}).solve();
assert_eq!(
path,
Some(
vec![
- 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()
- }),
+ 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)
+ }),
+ })
}
]
));
@@ -160,9 +147,9 @@ fn test_morphism_path2() {
fn test_morphism_path3() {
let (mut dict, mut base) = morphism_test_setup();
- 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(),
+ 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),
}).solve();
if let Some(path) = path.as_ref() {
@@ -173,26 +160,30 @@ fn test_morphism_path3() {
path,
Some(
vec![
- 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::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 {
+ MorphismInstance2::Primitive {
σ: vec![
- (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
- (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
+ (dict.get_typeid(&"SrcRadix".into()).unwrap(), SugaredTypeTerm::Num(10)),
+ (dict.get_typeid(&"DstRadix".into()).unwrap(), SugaredTypeTerm::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()
+ ψ: 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)
}),
}
]
@@ -205,9 +196,9 @@ fn test_morphism_path3() {
fn test_morphism_path4() {
let (mut dict, mut base) = morphism_test_setup();
- 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()
+ 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)
}).solve();
if let Some(path) = path.as_ref() {
@@ -218,40 +209,47 @@ fn test_morphism_path4() {
path,
Some(
vec![
- MorphismInstance {
+ 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 {
σ: vec![
- (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+ (dict.get_typeid(&"SrcRadix".into()).unwrap(), SugaredTypeTerm::Num(10)),
+ (dict.get_typeid(&"DstRadix".into()).unwrap(), SugaredTypeTerm::Num(16)),
].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()
+ ψ: 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)
}),
},
- 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()
- }),
+ 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(&"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()
- }),
- },
-
]
));
}
@@ -263,9 +261,9 @@ fn test_morphism_path4() {
fn test_morphism_path_posint() {
let (mut dict, mut base) = morphism_test_setup();
- 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(),
+ 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),
}).solve();
if let Some(path) = path.as_ref() {
@@ -276,62 +274,72 @@ fn test_morphism_path_posint() {
path,
Some(
vec![
- 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::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)
+ }),
})
- }
+ },
+
+ 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();
@@ -459,3 +467,4 @@ fn test_morphism_path_listedit()
])
);
}
+*/
diff --git a/src/test/unification.rs b/src/test/unification.rs
index ae99a18..aa20398 100644
--- a/src/test/unification.rs
+++ b/src/test/unification.rs
@@ -397,7 +397,7 @@ fn test_list_subtype_sugared() {
];
assert_eq!(
- SugaredUnificationProblem::new_sub(&mut dict, subtype_constraints).solve(),
+ SugaredUnificationProblem::new_sub(subtype_constraints).solve(),
Ok((
vec![ SugaredTypeTerm::Ladder(vec![]) ],
vec![
@@ -437,7 +437,7 @@ pub fn test_subtype_delim_sugared() {
];
assert_eq!(
- SugaredUnificationProblem::new_sub(&mut dict, subtype_constraints).solve(),
+ SugaredUnificationProblem::new_sub(subtype_constraints).solve(),
Ok((
// halo types for each rhs in the sub-equations
vec![
diff --git a/src/unification_sugared.rs b/src/unification_sugared.rs
index 499e2f1..c3e631e 100644
--- a/src/unification_sugared.rs
+++ b/src/unification_sugared.rs
@@ -138,7 +138,17 @@ impl SugaredUnificationProblem {
(SugaredTypeTerm::Seq{ seq_repr: lhs_seq_repr, items: lhs_items },
SugaredTypeTerm::Seq { seq_repr: rhs_seq_repr, items: rhs_items })
=> {
- // todo: unify seq reprü
+ 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 });
+ }
+ }
+
if lhs_items.len() == rhs_items.len() {
for (i, (lhs_ty, rhs_ty)) in lhs_items.into_iter().zip(rhs_items.into_iter()).enumerate()
@@ -155,7 +165,14 @@ impl SugaredUnificationProblem {
(SugaredTypeTerm::Struct{ struct_repr: lhs_struct_repr, members: lhs_members },
SugaredTypeTerm::Struct{ struct_repr: rhs_struct_repr, members: rhs_members })
=> {
- // todo: unify struct repr
+ 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 });
+ }
+ }
if lhs_members.len() == rhs_members.len() {
for (i,
@@ -176,7 +193,15 @@ impl SugaredUnificationProblem {
(SugaredTypeTerm::Enum{ enum_repr: lhs_enum_repr, variants: lhs_variants },
SugaredTypeTerm::Enum{ enum_repr: rhs_enum_repr, variants: rhs_variants })
=> {
- // todo: unify enum repr
+ 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 });
+ }
+ }
+
if lhs_variants.len() == rhs_variants.len() {
for (i,