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

fix path search & unification

Browse source 
add more path search tests
This commit is contained in:
Michael Sippel 2025-03-09 13:26:51 +01:00
parent ee75d23755
commit 911411791a
Signed by: senvas
GPG key ID: 060F22F65102F95C
3 changed files with 315 additions and 93 deletions

75
src/morphism.rs
View file

@ -174,83 +174,104 @@ impl<M: Morphism + Clone> MorphismBase<M> {
/* try to find shortest morphism-path for a given type
*/
pub fn find_morphism_path(&self, ty: MorphismType
/*, type_dict: &mut impl TypeDict*/
// , type_dict: &mut impl TypeDict
)
-> Option< Vec<MorphismInstance<M>> >
{
let ty = ty.normalize();
let mut queue = vec![
MorphismPath { weight: 0, cur_type: ty.src_type.clone(), morphisms: vec![] }
MorphismPath::<M> { weight: 0, cur_type: ty.src_type.clone(), morphisms: vec![] }
];
while ! queue.is_empty() {
queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
if let Some(mut cur_path) = queue.pop() {
if let Ok((halo, σ)) = crate::unification::subtype_unify( &cur_path.cur_type, &ty.dst_type ) {
// found path
/* found path,
* now apply substitution and trim to variables in terms of each step
*/
for n in cur_path.morphisms.iter_mut() {
let src_type = n.m.get_type().src_type;
let dst_type = n.m.get_type().dst_type;
let mut new_σ = HashMap::new();
for (k,v) in σ.iter() {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone()
);
if let TypeID::Var(varid) = k {
if src_type.contains_var(*varid)
|| dst_type.contains_var(*varid) {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone().strip()
);
}
}
}
for (k,v) in n.σ.iter() {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone()
);
if let TypeID::Var(varid) = k {
if src_type.contains_var(*varid)
|| dst_type.contains_var(*varid) {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone().strip()
);
}
}
}
n.halo = n.halo.clone().apply_substitution(
&|k| σ.get(k).cloned()
).clone().strip();
n.σ = new_σ;
}
return Some(cur_path.morphisms);
}
//eprintln!("cur path (w ={}) : @ {}", cur_path.weight, cur_path.cur_type.clone().sugar(type_dict).pretty(type_dict, 0) );
for next_morph_inst in self.enum_morphisms(&cur_path.cur_type) {
//eprintln!("cur path (w ={}) : @ {:?}", cur_path.weight, cur_path.cur_type);//.clone().sugar(type_dict).pretty(type_dict, 0) );
for mut next_morph_inst in self.enum_morphisms(&cur_path.cur_type) {
let dst_type = next_morph_inst.get_type().dst_type;
// eprintln!("try morph to {}", dst_type.clone().sugar(type_dict).pretty(type_dict, 0));
let mut creates_loop = false;
let mut new_path = cur_path.clone();
for n in new_path.morphisms.iter_mut() {
let mut new_σ = HashMap::new();
for (k,v) in n.σ.iter() {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&|k| next_morph_inst.σ.get(k).cloned()).clone()
);
}
for (k,v) in next_morph_inst.σ.iter() {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&|k| next_morph_inst.σ.get(k).cloned()).clone()
);
}
for (k,v) in n.σ.iter() {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&|k| next_morph_inst.σ.get(k).cloned()).clone()
);
}
n.halo = n.halo.clone().apply_substitution(
&|k| next_morph_inst.σ.get(k).cloned()
).clone().strip();
n.σ = new_σ;
}
for m in new_path.morphisms.iter() {
if m.get_type().src_type == dst_type {
creates_loop = true;
//eprintln!("creates loop..");
break;
}
}
if ! creates_loop {
/*eprintln!("next morph ? \n {}\n--> {} ",
next_morph_inst.get_type().src_type.sugar(type_dict).pretty(type_dict, 0),
next_morph_inst.get_type().dst_type.sugar(type_dict).pretty(type_dict, 0)
);
eprintln!("....take!\n :: halo = {}\n :: σ = {:?}", next_morph_inst.halo.clone().sugar(type_dict).pretty(type_dict, 0), next_morph_inst.σ);
*/
new_path.weight += next_morph_inst.m.weight();
new_path.cur_type = dst_type;
new_path.morphisms.push(next_morph_inst);
queue.push(new_path);
}

219
src/test/morphism.rs
View file

@ -70,7 +70,216 @@ fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
}
#[test]
fn test_morphism_path() {
fn test_morphism_path1() {
let (mut dict, mut base) = morphism_test_setup();
let path = base.find_morphism_path(MorphismType {
src_type: dict.parse("<Digit 10> ~ Char").unwrap(),
dst_type: dict.parse("<Digit 10> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
});
assert_eq!(
path,
Some(
vec![
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::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()
}),
}
]
));
}
#[test]
fn test_morphism_path2() {
let (mut dict, mut base) = morphism_test_setup();
let path = base.find_morphism_path(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(),
});
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()
}),
}
]
));
}
#[test]
fn test_morphism_path3() {
let (mut dict, mut base) = morphism_test_setup();
let path = base.find_morphism_path(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(),
});
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(),
dict.unparse(v)
);
}
eprintln!("}}");
}
if let Some(path) = path.as_ref() {
for n in path.iter() {
eprintln!("
ψ = {}
morph {}
--> {}
with
",
n.halo.clone().sugar(&mut dict).pretty(&mut dict, 0),
n.m.get_type().src_type.sugar(&mut dict).pretty(&mut dict, 0),
n.m.get_type().dst_type.sugar(&mut dict).pretty(&mut dict, 0),
);
print_subst(&n.σ, &mut dict)
}
}
assert_eq!(
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()
}),
},
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()
}),
}
]
));
}
#[test]
fn test_morphism_path4() {
let (mut dict, mut base) = morphism_test_setup();
let path = base.find_morphism_path(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()
});
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(),
dict.unparse(v)
);
}
eprintln!("}}");
}
if let Some(path) = path.as_ref() {
for n in path.iter() {
eprintln!("
ψ = {}
morph {}
--> {}
with
",
n.halo.clone().sugar(&mut dict).pretty(&mut dict, 0),
n.m.get_type().src_type.sugar(&mut dict).pretty(&mut dict, 0),
n.m.get_type().dst_type.sugar(&mut dict).pretty(&mut dict, 0),
);
print_subst(&n.σ, &mut dict)
}
}
assert_eq!(
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()
}),
},
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()
}),
},
]
));
}
#[test]
fn test_morphism_path_posint() {
let (mut dict, mut base) = morphism_test_setup();
let path = base.find_morphism_path(MorphismType {
@ -114,8 +323,6 @@ with
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
(dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16))
].into_iter().collect(),
halo: dict.parse("ℕ ~ <PosInt 10 BigEndian>").unwrap(),
m: DummyMorphism(MorphismType {
@ -126,8 +333,6 @@ with
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
(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{
@ -139,7 +344,6 @@ with
σ: vec![
(dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
].into_iter().collect(),
halo: TypeTerm::unit(),
m: DummyMorphism(MorphismType{
@ -150,7 +354,6 @@ with
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16))
].into_iter().collect(),
halo: TypeTerm::unit(),
m: DummyMorphism(MorphismType{
@ -162,7 +365,7 @@ with
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16))
].into_iter().collect(),
halo: dict.parse("ℕ ~ <PosInt Radix BigEndian>").unwrap(),
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()

114
src/unification.rs
View file

@ -149,15 +149,58 @@ impl UnificationProblem {
Variables
*/
(t, TypeTerm::TypeID(TypeID::Var(varid))) => {
// eprintln!("t <= variable");
if ! t.contains_var( varid ) {
// let x = self.σ.get(&TypeID::Var(varid)).cloned();
if let Some(lower_bound) = self.lower_bounds.get(&varid).cloned() {
// eprintln!("var already exists. check max. type");
if let Ok(halo) = self.eval_subtype(
UnificationPair {
lhs: lower_bound.clone(),
rhs: t.clone(),
halo: TypeTerm::unit(),
addr: vec![]
}
) {
// eprintln!("found more general lower bound");
// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
// generalize variable type to supertype
self.lower_bounds.insert(varid, t.clone());
} else if let Ok(halo) = self.eval_subtype(
UnificationPair{
lhs: t.clone(),
rhs: lower_bound.clone(),
halo: TypeTerm::unit(),
addr: vec![]
}
) {
// eprintln!("OK, is already larger type");
} else {
// eprintln!("violated subtype restriction");
return Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t });
}
} else {
// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
self.lower_bounds.insert(varid, t.clone());
}
self.reapply_subst();
Ok(TypeTerm::unit())
} else if t == TypeTerm::TypeID(TypeID::Var(varid)) {
Ok(TypeTerm::unit())
} else {
Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t })
}
}
(TypeTerm::TypeID(TypeID::Var(varid)), t) => {
eprintln!("variable <= t");
// eprintln!("variable <= t");
if let Some(upper_bound) = self.upper_bounds.get(&varid).cloned() {
if let Ok(_halo) = self.eval_subtype(
UnificationPair {
lhs: t.clone(),
rhs: upper_bound,
halo: TypeTerm::unit(),
addr: vec![]
}
@ -171,49 +214,6 @@ impl UnificationProblem {
Ok(TypeTerm::unit())
}
(t, TypeTerm::TypeID(TypeID::Var(varid))) => {
eprintln!("t <= variable");
if ! t.contains_var( varid ) {
// let x = self.σ.get(&TypeID::Var(varid)).cloned();
if let Some(lower_bound) = self.lower_bounds.get(&varid).cloned() {
eprintln!("var already exists. check max. type");
if let Ok(halo) = self.eval_subtype(
UnificationPair {
lhs: lower_bound.clone(),
rhs: t.clone(),
halo: TypeTerm::unit(),
addr: vec![]
}
) {
eprintln!("found more general lower bound");
eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
// generalize variable type to supertype
self.lower_bounds.insert(varid, t.clone());
} else if let Ok(halo) = self.eval_subtype(
UnificationPair{
lhs: t.clone(),
rhs: lower_bound.clone(),
halo: TypeTerm::unit(),
addr: vec![]
}
) {
eprintln!("OK, is already larger type");
} else {
eprintln!("violated subtype restriction");
return Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t });
}
} else {
eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
self.lower_bounds.insert(varid, t.clone());
}
self.reapply_subst();
Ok(TypeTerm::unit())
} else if t == TypeTerm::TypeID(TypeID::Var(varid)) {
Ok(TypeTerm::unit())
} else {
Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t })
}
}
/*
@ -247,7 +247,7 @@ impl UnificationProblem {
halo: TypeTerm::unit(),
addr: new_addr
}) {
eprintln!("unified ladders at {}, r_halo = {:?}", i, r_halo);
// eprintln!("unified ladders at {}, r_halo = {:?}", i, r_halo);
for j in 0..a2.len() {
if i+j < a1.len() {
@ -320,7 +320,6 @@ impl UnificationProblem {
*/
(TypeTerm::App(a1), TypeTerm::App(a2)) => {
eprintln!("sub unify {:?}, {:?}", a1, a2);
if a1.len() == a2.len() {
let mut halo_args = Vec::new();
let mut n_halos_required = 0;
@ -331,11 +330,10 @@ impl UnificationProblem {
x = x.strip();
eprintln!("before strip: {:?}", y);
// eprintln!("before strip: {:?}", y);
y = y.strip();
eprintln!("after strip: {:?}", y);
eprintln!("APP<> eval {:?} \n ?<=? {:?} ", x, y);
// eprintln!("after strip: {:?}", y);
// eprintln!("APP<> eval {:?} \n ?<=? {:?} ", x, y);
if let Ok(halo) = self.eval_subtype(
UnificationPair {
@ -351,9 +349,9 @@ impl UnificationProblem {
y = y.strip();
let mut top = y.get_lnf_vec().first().unwrap().clone();
halo_args.push(top.clone());
eprintln!("add top {:?}", top);
// eprintln!("add top {:?}", top);
} else {
eprintln!("add halo {:?}", halo);
// eprintln!("add halo {:?}", halo);
if n_halos_required > 0 {
let x = &mut halo_args[n_halos_required-1];
if let TypeTerm::Ladder(argrs) = x {
@ -380,7 +378,7 @@ impl UnificationProblem {
}
if n_halos_required > 0 {
eprintln!("halo args : {:?}", halo_args);
// eprintln!("halo args : {:?}", halo_args);
Ok(TypeTerm::App(halo_args))
} else {
Ok(TypeTerm::unit())
@ -404,7 +402,7 @@ impl UnificationProblem {
}
// solve subtypes
eprintln!("------ SOLVE SUBTYPES ---- ");
// eprintln!("------ SOLVE SUBTYPES ---- ");
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
subtype_pair.lhs.apply_substitution(&|v| self.σ.get(v).cloned());
subtype_pair.rhs.apply_substitution(&|v| self.σ.get(v).cloned());
@ -413,18 +411,18 @@ impl UnificationProblem {
// add variables from subtype bounds
for (var_id, t) in self.upper_bounds.iter() {
eprintln!("VAR {} upper bound {:?}", var_id, t);
// eprintln!("VAR {} upper bound {:?}", var_id, t);
self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
}
for (var_id, t) in self.lower_bounds.iter() {
eprintln!("VAR {} lower bound {:?}", var_id, t);
// eprintln!("VAR {} lower bound {:?}", var_id, t);
self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
}
self.reapply_subst();
eprintln!("------ MAKE HALOS -----");
// eprintln!("------ MAKE HALOS -----");
let mut halo_types = Vec::new();
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
subtype_pair.lhs = subtype_pair.lhs.apply_substitution(&|v| self.σ.get(v).cloned()).clone().strip();