From b7832aed947f7b61b4aa63defe04985615206f45 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Mon, 7 Apr 2025 18:10:08 +0200
Subject: [PATCH] more work on sugared pnf
- add more tests
- add struct & enum cases
---
src/morphism_base_sugared.rs | 7 +-
src/morphism_sugared.rs | 28 ++++--
src/pnf_sugared.rs | 171 +++++++++++++++++++++++++++--------
src/test/pnf.rs | 48 +++++++++-
src/unification_sugared.rs | 10 +-
5 files changed, 206 insertions(+), 58 deletions(-)
diff --git a/src/morphism_base_sugared.rs b/src/morphism_base_sugared.rs
index 93d3b10..23720c7 100644
--- a/src/morphism_base_sugared.rs
+++ b/src/morphism_base_sugared.rs
@@ -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);
}
}
diff --git a/src/morphism_sugared.rs b/src/morphism_sugared.rs
index 5e10f65..2b5684d 100644
--- a/src/morphism_sugared.rs
+++ b/src/morphism_sugared.rs
@@ -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 > {
diff --git a/src/pnf_sugared.rs b/src/pnf_sugared.rs
index 17828c1..8fd3e71 100644
--- a/src/pnf_sugared.rs
+++ b/src/pnf_sugared.rs
@@ -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;
}
diff --git a/src/test/pnf.rs b/src/test/pnf.rs
index 55c2c31..03c1901 100644
--- a/src/test/pnf.rs
+++ b/src/test/pnf.rs
@@ -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(),
+ );
+}
diff --git a/src/unification_sugared.rs b/src/unification_sugared.rs
index c3e631e..f116f0b 100644
--- a/src/unification_sugared.rs
+++ b/src/unification_sugared.rs
@@ -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();