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

more work on sugared pnf

Browse source 
- add more tests
- add struct & enum cases
This commit is contained in:
Michael Sippel 2025-04-07 18:10:08 +02:00
parent 69ec5ad8bb
commit b7832aed94
Signed by: senvas
GPG key ID: F96CF119C34B64A6
5 changed files with 206 additions and 58 deletions

7
src/morphism_base_sugared.rs
View file

@ -127,11 +127,14 @@ impl<M: SugaredMorphism + Clone> SugaredMorphismBase<M> {
// morphisms source type,
// i.e. check if `src_type` is a subtype of `m_src_type`
if let Ok((ψ, σ)) = crate::unification_sugared::subtype_unify(src_type, &m_src_type) {
morphs.push(MorphismInstance2::Primitive { ψ, σ, morph: m.clone() });
let morph_inst = MorphismInstance2::Primitive { ψ, σ, morph: m.clone() };
//eprintln!("..found direct morph to {:?}", morph_inst.get_type().dst_type);
morphs.push(morph_inst);
}
/* 2. check complex types */
if let Some(complex_morph) = self.complex_morphism_decomposition(src_type, &m_src_type) {
else if let Some(complex_morph) = self.complex_morphism_decomposition(src_type, &m_src_type) {
//eprintln!("found complex morph to {:?}", complex_morph.get_type().dst_type);
morphs.push(complex_morph);
}
}

28
src/morphism_sugared.rs
View file

@ -166,6 +166,14 @@ impl SugaredMorphismType {
dst_type: self.dst_type.clone().apply_subst(σ).clone()
}
}
pub fn normalize(&self) -> SugaredMorphismType {
SugaredMorphismType {
src_type: self.src_type.clone().normalize(),
dst_type: self.dst_type.clone().normalize(),
}
}
}
pub trait SugaredMorphism : Sized {
@ -231,9 +239,9 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
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.clone(),
dst_type: path.last().unwrap().get_type().dst_type.clone()
}.apply_subst(&s)
} else {
SugaredMorphismType {
src_type: SugaredTypeTerm::TypeID(TypeID::Fun(45454)),
@ -247,12 +255,12 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
ψ.clone(),
SugaredTypeTerm::Seq{ seq_repr: seq_repr.clone(),
items: vec![ item_morph.get_type().src_type ]}
]).strip(),
]),
dst_type: SugaredTypeTerm::Ladder(vec![
ψ.clone(),
SugaredTypeTerm::Seq{ seq_repr: seq_repr.clone(),
items: vec![ item_morph.get_type().dst_type ]}
]).strip()
])
}
}
MorphismInstance2::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
@ -265,7 +273,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
SugaredStructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
}).collect()
}
]).strip(),
]),
dst_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
SugaredTypeTerm::Struct{
struct_repr: dst_struct_repr.clone(),
@ -273,7 +281,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
SugaredStructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
}).collect()
}
]).strip()
])
}
}
MorphismInstance2::MapEnum { ψ, enum_repr, variant_morph } => {
@ -286,7 +294,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
SugaredStructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
}).collect()
}
]).strip(),
]),
dst_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
SugaredTypeTerm::Struct{
struct_repr: enum_repr.clone(),
@ -294,10 +302,10 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
SugaredStructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
}).collect()
}
]).strip()
])
}
}
}
}.normalize()
}
pub fn get_subst(&self) -> std::collections::HashMap< TypeID, SugaredTypeTerm > {

171
src/pnf_sugared.rs
View file

@ -1,8 +1,9 @@
use crate::{sugar::SugaredTypeTerm, SugaredEnumVariant, SugaredStructMember};
use crate::{sugar::SugaredTypeTerm, unification_sugared, SugaredEnumVariant, SugaredStructMember};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub fn splice_ladders( mut upper: Vec< SugaredTypeTerm >, mut lower: Vec< SugaredTypeTerm > ) -> Vec< SugaredTypeTerm > {
eprintln!("splice ladders {:?} <<<====>>> {:?} ", upper, lower);
// check for overlap
for i in 0 .. upper.len() {
if upper[i] == lower[0] {
@ -27,7 +28,6 @@ impl SugaredTypeTerm {
/// ⇒ <Seq <Digit 10>~Char>
/// ```
pub fn normalize(mut self) -> Self {
eprintln!("normalize {:?}", self);
match self {
SugaredTypeTerm::Ladder(mut rungs) => {
if rungs.len() == 0 {
@ -44,7 +44,6 @@ impl SugaredTypeTerm {
(SugaredTypeTerm::Seq { seq_repr: seq_repr1, items: items1 },
SugaredTypeTerm::Seq { seq_repr: seq_repr2, items: items2 })
=> {
eprintln!("popped two seq {:?} , {:?}", items1, items2);
r2 = SugaredTypeTerm::Seq {
seq_repr:
if seq_repr1.is_some() || seq_repr2.is_some() {
@ -111,36 +110,135 @@ impl SugaredTypeTerm {
(SugaredTypeTerm::Struct { struct_repr: struct_repr1, members: members1 },
SugaredTypeTerm::Struct { struct_repr: struct_repr2, members: members2 }) => {
todo!();
let mut condensed_struct_repr = None;
let mut condensed_members = Vec::new();
let mut require_break = false;
if let Some(struct_repr1) = struct_repr1 {
if let Some(struct_repr2) = struct_repr2 {
condensed_struct_repr = Some(Box::new(SugaredTypeTerm::Ladder(
vec![
struct_repr1.as_ref().clone(),
struct_repr2.as_ref().clone()
]
).normalize()))
} else {
condensed_struct_repr = Some(Box::new(struct_repr1.as_ref().clone()));
}
} else {
condensed_struct_repr = struct_repr2.clone();
}
for SugaredStructMember{ symbol: symbol2, ty: ty2 } in members2.iter() {
let mut found = false;
for SugaredStructMember{ symbol: symbol1, ty: ty1 } in members1.iter() {
if symbol2 == symbol1 {
condensed_members.push(SugaredStructMember {
symbol: symbol1.clone(),
ty: SugaredTypeTerm::Ladder(vec![
ty1.clone(),
ty2.clone()
]).normalize()
});
found = true;
break;
}
}
if ! found {
require_break = true;
}
}
if require_break {
new_rungs.push(r2);
r2 = r1;
} else {
r2 = SugaredTypeTerm::Struct {
struct_repr: condensed_struct_repr,
members: condensed_members
};
}
}
(SugaredTypeTerm::Enum { enum_repr: enum_repr1, variants: variants1 },
SugaredTypeTerm::Enum { enum_repr: enum_repr2, variants: variants2 }) => {
todo!();
let mut condensed_enum_repr = None;
let mut condensed_variants = Vec::new();
let mut require_break = false;
if let Some(enum_repr1) = enum_repr1 {
if let Some(enum_repr2) = enum_repr2 {
condensed_enum_repr = Some(Box::new(SugaredTypeTerm::Ladder(
vec![
enum_repr1.as_ref().clone(),
enum_repr2.as_ref().clone()
]
).normalize()))
} else {
condensed_enum_repr = Some(Box::new(enum_repr1.as_ref().clone()));
}
} else {
condensed_enum_repr = enum_repr2.clone();
}
for SugaredEnumVariant{ symbol: symbol2, ty: ty2 } in variants2.iter() {
let mut found = false;
for SugaredEnumVariant{ symbol: symbol1, ty: ty1 } in variants1.iter() {
if symbol2 == symbol1 {
condensed_variants.push(SugaredEnumVariant {
symbol: symbol1.clone(),
ty: SugaredTypeTerm::Ladder(vec![
ty1.clone(),
ty2.clone()
]).normalize()
});
found = true;
break;
}
}
if ! found {
require_break = true;
}
}
if require_break {
new_rungs.push(r2);
r2 = r1;
} else {
r2 = SugaredTypeTerm::Enum {
enum_repr: condensed_enum_repr,
variants: condensed_variants
};
}
}
(SugaredTypeTerm::Spec(args1), SugaredTypeTerm::Spec(args2)) => {
eprintln!("popped two spec {:?} , {:?}", args1, args2);
if args1.len() == args2.len() {
r2 = SugaredTypeTerm::Spec(
args1.into_iter().zip(args2.into_iter())
.map(|(a1,a2)|
if a1 == SugaredTypeTerm::unit() {
a2
} else if a1 == a2 {
a2
} else if a2 == SugaredTypeTerm::unit() {
a1
} else {
SugaredTypeTerm::Ladder(vec![ a1, a2 ]).normalize()
})
.collect()
);
if let Ok((ψ,σ)) = unification_sugared::subtype_unify(&args1[0], &args2[0]) {
let mut new_args = Vec::new();
for (a1, a2) in args1.into_iter().zip(args2.into_iter()) {
new_args.push(SugaredTypeTerm::Ladder(vec![ a1, a2 ]).normalize());
}
r2 = SugaredTypeTerm::Spec(new_args);
//new_rungs.push(r2.clone());
} else {
new_rungs.push(r2);
r2 = r1;
}
} else {
new_rungs.push(r2);
r2 = r1;
}
}
(SugaredTypeTerm::Univ(args1), SugaredTypeTerm::Univ(args2)) => {
todo!();
}
@ -148,49 +246,44 @@ impl SugaredTypeTerm {
(SugaredTypeTerm::Func(args1), SugaredTypeTerm::Func(args2)) => {
todo!();
}
(SugaredTypeTerm::Morph(args1), SugaredTypeTerm::Morph(args2)) => {
todo!();
}
(SugaredTypeTerm::Ladder(rr1), SugaredTypeTerm::Ladder(rr2)) => {
eprintln!("popped two ladders {:?} , {:?}", rr1, rr2);
if rr1.len() > 0 {
let l = splice_ladders(rr1, rr2);
eprintln!("splice ladders .. = {:?}",l);
r2 = SugaredTypeTerm::Ladder(l).normalize();
}
}
(atomic1, SugaredTypeTerm::Ladder(mut rr2)) => {
if !atomic1.is_empty() {
eprintln!("add head of ladder");
if rr2.first() != Some(&atomic1) {
rr2.insert(0, atomic1);
} else {
eprintln!("skip equal head at ladder");
}
} else {
eprintln!("skip empty atomic at head of ladder");
}
r2 = SugaredTypeTerm::Ladder(rr2).normalize();
}
(atomic1, atomic2) => {
eprintln!("popped two atomics {:?} , {:?}", atomic1, atomic2);
if atomic1.is_empty() {
eprintln!("skip atomic1 (empty)");
} else if atomic1 == atomic2 {
eprintln!("atomic are equal");
if !atomic2.is_empty() {
new_rungs.push(atomic2);
(SugaredTypeTerm::Ladder(mut rr1), atomic2) => {
if !atomic2.is_empty() {
if rr1.last() != Some(&atomic2) {
rr1.push(atomic2);
}
r2 = atomic1;
}
r2 = SugaredTypeTerm::Ladder(rr1).normalize();
}
(atomic1, atomic2) => {
if atomic1.is_empty() {
} else if atomic1 == atomic2 {
} else if atomic2.is_empty() {
eprintln!("lol");
r2 = atomic1;
} else {
eprintln!("differnt, take atomic2");
new_rungs.push(atomic2);
r2 = atomic1;
}

48
src/test/pnf.rs
View file

@ -26,7 +26,7 @@ fn test_normalize_spec() {
assert_eq!(
dict.parse("<A~Y B>").expect("parse error").sugar(&mut dict),
dict.parse("<A B>~<Y B>").expect("parse error").sugar(&mut dict).normalize(),
dict.parse("<A~Y B>~<Y B>").expect("parse error").sugar(&mut dict).normalize(),
);
assert_eq!(
@ -36,7 +36,7 @@ fn test_normalize_spec() {
assert_eq!(
dict.parse("<A~X B~C D~E>").expect("parse error").sugar(&mut dict),
dict.parse("<A B D>~<A B~C E>~<X C E>").expect("parse errror").sugar(&mut dict).normalize(),
dict.parse("<A~X B D>~<A~X B~C E>~<X C E>").expect("parse errror").sugar(&mut dict).normalize(),
);
}
@ -71,9 +71,47 @@ fn test_normalize_complex_spec() {
let mut dict = BimapTypeDict::new();
assert_eq!(
dict.parse("<A~Y <B C~D~E> F H H>").expect("parse error").sugar(&mut dict),
dict.parse("<A <B C> F H H>
~<A <B D> F H H>
~<A~Y <B E> F H H>").expect("parse errror").sugar(&mut dict)
dict.parse("<A~Y <B C> F H H>
~<A~Y <B D> F H H>
~<Y <B E> F H H>").expect("parse errror").sugar(&mut dict)
.normalize(),
);
}
#[test]
fn test_normalize_struct() {
let mut dict = BimapTypeDict::new();
assert_eq!(
dict.parse("< Struct~Aligned
< a TimePoint~<TimeSince UnixEpoch>~Seconds~native.UInt64 >
< b Angle ~ Degrees ~ ℝ ~ native.Float32 >
>
").expect("parse error").sugar(&mut dict),
dict.parse("
< Struct <a TimePoint> <b Angle> >
~ < Struct <a <TimeSince UnixEpoch>~Seconds> <b Angle~Degrees~ℝ> >
~ < Struct~Aligned <a native.UInt64> <b native.Float32> >
").expect("parse errror")
.sugar(&mut dict)
.normalize(),
);
}
#[test]
fn test_normalize_enum() {
let mut dict = BimapTypeDict::new();
assert_eq!(
dict.parse("< Enum
< a TimePoint~<TimeSince UnixEpoch>~Seconds~native.UInt64 >
< b Angle ~ Degrees ~ ℝ ~ native.Float32 >
>
").expect("parse error").sugar(&mut dict),
dict.parse("
< Enum <a TimePoint> <b Angle> >
~ < Enum <a <TimeSince UnixEpoch>~Seconds> <b Angle~Degrees~ℝ> >
~ < Enum <a native.UInt64> <b native.Float32> >
").expect("parse errror")
.sugar(&mut dict)
.normalize(),
);
}

10
src/unification_sugared.rs
View file

@ -11,6 +11,7 @@ pub struct SugaredUnificationError {
pub t2: SugaredTypeTerm
}
// todo : rename -> ConstraintPair
#[derive(Clone)]
pub struct SugaredUnificationPair {
addr: Vec<usize>,
@ -26,6 +27,7 @@ impl SugaredUnificationPair {
}
}
// todo : Rename -> ConstraintSystem
pub struct SugaredUnificationProblem {
// dict: &'a Dict,
@ -358,9 +360,13 @@ impl SugaredUnificationProblem {
new_addr.push(0);
if let Some(rhs_seq_repr) = rhs_seq_repr.as_ref() {
//eprintln!("subtype unify: rhs has seq-repr: {:?}", rhs_seq_repr);
if let Some(lhs_seq_repr) = lhs_seq_repr.as_ref() {
//eprintln!("check if it maches lhs seq-repr: {:?}", lhs_seq_repr);
let _seq_repr_ψ = self.eval_subtype(SugaredUnificationPair { addr: new_addr.clone(), lhs: *lhs_seq_repr.clone(), rhs: *rhs_seq_repr.clone() })?;
//eprintln!("..yes!");
} else {
//eprintln!("...but lhs has none.");
return Err(SugaredUnificationError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
}
}
@ -668,7 +674,7 @@ impl SugaredUnificationProblem {
}
// solve subtypes
// eprintln!("------ SOLVE SUBTYPES ---- ");
//eprintln!("------ SOLVE SUBTYPES ---- ");
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
subtype_pair.lhs.apply_subst(&self.σ);
subtype_pair.rhs.apply_subst(&self.σ);
@ -688,7 +694,7 @@ impl SugaredUnificationProblem {
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_subst(&self.σ).clone().strip();