syntaxAlchemist/lib-laddertypes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Compare commits

...

5 commits
7f96b66324 ... a9967f8183

Author SHA1 Message Date
Michael Sippel
a9967f8183
fix tests 2025-04-03 15:40:42 +02:00
Michael Sippel
8c170baad3
morphism instance: fix apply subst 2025-04-03 15:39:25 +02:00
Michael Sippel
6731f7fdea
MorphismType: strip_halo() add strip(), and dont skip struct/enum if members dont match 2025-04-03 15:38:32 +02:00
Michael Sippel
f5fc2979c7
SugaredMorphismType::Struct add src/dst repr 2025-04-03 15:37:23 +02:00
Michael Sippel
ebaa1350ac
unification sugared: check Seq-/Enum-/Struct- Representations for subtype 2025-04-03 14:33:29 +02:00
5 changed files with 276 additions and 204 deletions

5
src/morphism_base_sugared.rs
View file

@ -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 {

89
src/morphism_sugared.rs
View file

@ -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(γ);
}

351
src/test/morphism.rs
View file

@ -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()
])
);
}
*/

4
src/test/unification.rs
View file

@ -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![

31
src/unification_sugared.rs
View file

@ -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,