From 78c83cc48173946a48d8111fc007916a8c19f656 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Thu, 3 Apr 2025 15:57:18 +0200
Subject: [PATCH 1/4] add failing test (failed to find morphism instance)
---
src/test/morphism.rs | 33 ++++++++++++++++++++++++++++++++-
1 file changed, 32 insertions(+), 1 deletion(-)
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index 56d3059..4754575 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -1,5 +1,5 @@
use {
- crate::{dict::*, morphism::*, morphism_base::*, morphism_base_sugared::SugaredMorphismBase, morphism_path::*, morphism_path_sugared::SugaredShortestPathProblem, morphism_sugared::{MorphismInstance2, SugaredMorphism, SugaredMorphismType}, parser::*, unparser::*, SugaredTypeTerm, TypeTerm}
+ crate::{dict::*, morphism::*, morphism_base::*, morphism_base_sugared::SugaredMorphismBase, morphism_path::*, morphism_path_sugared::SugaredShortestPathProblem, morphism_sugared::{MorphismInstance2, SugaredMorphism, SugaredMorphismType}, parser::*, unparser::*, SugaredTypeTerm, TypeTerm}, std::collections::HashMap
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -339,6 +339,37 @@ fn test_morphism_path_posint() {
)
);
}
+
+#[test]
+fn morphism_test_seq_repr() {
+ let mut dict = BimapTypeDict::new();
+ let mut base = SugaredMorphismBase::<DummyMorphism>::new();
+
+ base.add_morphism(
+ DummyMorphism(SugaredMorphismType{
+ src_type: dict.parse("<Seq~<ValueTerminated 0> native.UInt8>").unwrap().sugar(&mut dict),
+ dst_type: dict.parse("<Seq~<LengthPrefix native.UInt64> native.UInt8>").unwrap().sugar(&mut dict)
+ })
+ );
+
+ assert_eq!(
+ base.get_morphism_instance(&SugaredMorphismType {
+ src_type: dict.parse("<Seq~<ValueTerminated 0> Char~Ascii~native.UInt8>").expect("parse").sugar(&mut dict),
+ dst_type: dict.parse("<Seq~<LengthPrefix native.UInt64> Char~Ascii~native.UInt8>").expect("parse").sugar(&mut dict)
+ }),
+ Some(
+ MorphismInstance2::Primitive {
+ ψ: dict.parse("<Seq Char~Ascii>").expect("").sugar(&mut dict),
+ σ: HashMap::new(),
+ morph: DummyMorphism(SugaredMorphismType{
+ src_type: dict.parse("<Seq~<ValueTerminated 0> native.UInt8>").unwrap().sugar(&mut dict),
+ dst_type: dict.parse("<Seq~<LengthPrefix native.UInt64> native.UInt8>").unwrap().sugar(&mut dict)
+ })
+ }
+ )
+ );
+}
+
/*
#[test]
fn test_steiner_tree() {
From 2ecbc842332cc6d8c17f1b1e26603307d17f0cb8 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sat, 5 Apr 2025 22:55:20 +0200
Subject: [PATCH 2/4] switch pnf tests to sugared terms
---
src/test/pnf.rs | 115 ++++++++++++++++++++++++++++--------------------
1 file changed, 68 insertions(+), 47 deletions(-)
diff --git a/src/test/pnf.rs b/src/test/pnf.rs
index a1d5a33..55c2c31 100644
--- a/src/test/pnf.rs
+++ b/src/test/pnf.rs
@@ -1,58 +1,79 @@
use crate::{dict::BimapTypeDict, parser::*};
#[test]
-fn test_param_normalize() {
+fn test_normalize_id() {
let mut dict = BimapTypeDict::new();
assert_eq!(
- dict.parse("A~B~C").expect("parse error"),
- dict.parse("A~B~C").expect("parse error").param_normalize(),
+ dict.parse("A~B~C").expect("parse error").sugar(&mut dict),
+ dict.parse("A~B~C").expect("parse error").sugar(&mut dict).normalize(),
);
assert_eq!(
- dict.parse("<A B>~C").expect("parse error"),
- dict.parse("<A B>~C").expect("parse error").param_normalize(),
- );
-
- assert_eq!(
- dict.parse("<A B~C>").expect("parse error"),
- dict.parse("<A B>~<A C>").expect("parse error").param_normalize(),
- );
-
- assert_eq!(
- dict.parse("<A~Y B>").expect("parse error"),
- dict.parse("<A B>~<Y B>").expect("parse error").param_normalize(),
- );
-
- assert_eq!(
- dict.parse("<A B~C D~E>").expect("parse error"),
- dict.parse("<A B D>~<A C D>~<A C E>").expect("parse errror").param_normalize(),
- );
-
- assert_eq!(
- dict.parse("<A~X B~C D~E>").expect("parse error"),
- dict.parse("<A B D>~<A B~C E>~<X C E>").expect("parse errror").param_normalize(),
- );
-
- assert_eq!(
- dict.parse("<Seq <Digit 10>~Char>").expect("parse error"),
- dict.parse("<Seq <Digit 10>>~<Seq Char>").expect("parse errror").param_normalize(),
- );
-
- assert_eq!(
- dict.parse("<Seq Char> ~ <<ValueDelim '\\0'> Char> ~ <<ValueDelim '\\0'> Ascii~x86.UInt8>").expect("parse error").param_normalize(),
- dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~x86.UInt8>").expect("parse error")
- );
- assert_eq!(
- dict.parse("<Seq Char~Ascii> ~ <<ValueDelim '\\0'> Char~Ascii> ~ <<ValueDelim '\\0'> x86.UInt8>").expect("parse error").param_normalize(),
- dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~x86.UInt8>").expect("parse error")
- );
-
- assert_eq!(
- dict.parse("<A~Y <B C~D~E> F H H>").expect("parse error"),
- dict.parse("<A <B C> F H H>
- ~<A <B D> F H H>
- ~<A~Y <B E> F H H>").expect("parse errror")
- .param_normalize(),
+ dict.parse("<A B>~C").expect("parse error").sugar(&mut dict),
+ dict.parse("<A B>~C").expect("parse error").sugar(&mut dict).normalize(),
+ );
+}
+
+#[test]
+fn test_normalize_spec() {
+ let mut dict = BimapTypeDict::new();
+
+ assert_eq!(
+ dict.parse("<A B~C>").expect("parse error").sugar(&mut dict),
+ dict.parse("<A B>~<A C>").expect("parse error").sugar(&mut dict).normalize(),
+ );
+
+ 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(),
+ );
+
+ assert_eq!(
+ dict.parse("<A B~C D~E>").expect("parse error").sugar(&mut dict),
+ dict.parse("<A B D>~<A C D>~<A C E>").expect("parse errror").sugar(&mut dict).normalize(),
+ );
+
+ 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(),
+ );
+}
+
+#[test]
+fn test_normalize_seq() {
+ let mut dict = BimapTypeDict::new();
+ assert_eq!(
+ dict.parse("<Seq Char~Ascii>").expect("parse error").sugar(&mut dict),
+ dict.parse("<Seq Char>~<Seq Ascii>").expect("parse errror").sugar(&mut dict).normalize(),
+ );
+
+ eprintln!("---------------");
+ assert_eq!(
+ dict.parse("<Seq <Digit 10>~Char>").expect("parse error").sugar(&mut dict),
+ dict.parse("<Seq <Digit 10>>~<Seq Char>").expect("parse errror").sugar(&mut dict).normalize(),
+ );
+ eprintln!("---------------");
+ assert_eq!(
+ dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~native.UInt8>").expect("parse error").sugar(&mut dict),
+ dict.parse("<Seq Char> ~ <<ValueDelim '\\0'> Char> ~ <<ValueDelim '\\0'> Ascii~native.UInt8>").expect("parse error").sugar(&mut dict).normalize(),
+ );
+
+ eprintln!("---------------");
+ assert_eq!(
+ dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~native.UInt8>").expect("parse error").sugar(&mut dict),
+ dict.parse("<Seq Char~Ascii> ~ <<ValueDelim '\\0'> Char~Ascii> ~ <<ValueDelim '\\0'> native.UInt8>").expect("parse error").sugar(&mut dict).normalize(),
+ );
+}
+
+#[test]
+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)
+ .normalize(),
);
}
From 69ec5ad8bbc6aa8d52bb41ae612affe32859b2b1 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sat, 5 Apr 2025 22:55:34 +0200
Subject: [PATCH 3/4] rewrite of pnf sugared
---
src/pnf_sugared.rs | 274 +++++++++++++++++++++++++++++----------------
1 file changed, 177 insertions(+), 97 deletions(-)
diff --git a/src/pnf_sugared.rs b/src/pnf_sugared.rs
index f5a72d7..17828c1 100644
--- a/src/pnf_sugared.rs
+++ b/src/pnf_sugared.rs
@@ -3,6 +3,7 @@ use crate::{sugar::SugaredTypeTerm, SugaredEnumVariant, SugaredStructMember};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub fn splice_ladders( mut upper: Vec< SugaredTypeTerm >, mut lower: Vec< SugaredTypeTerm > ) -> Vec< SugaredTypeTerm > {
+ // check for overlap
for i in 0 .. upper.len() {
if upper[i] == lower[0] {
let mut result_ladder = Vec::<SugaredTypeTerm>::new();
@@ -12,6 +13,7 @@ pub fn splice_ladders( mut upper: Vec< SugaredTypeTerm >, mut lower: Vec< Sugare
}
}
+ // no overlap found, just concatenate ladders
upper.append(&mut lower);
upper
}
@@ -24,132 +26,210 @@ impl SugaredTypeTerm {
/// <Seq <Digit 10>>~<Seq Char>
/// ⇒ <Seq <Digit 10>~Char>
/// ```
- pub fn param_normalize(mut self) -> Self {
-
+ pub fn normalize(mut self) -> Self {
+ eprintln!("normalize {:?}", self);
match self {
SugaredTypeTerm::Ladder(mut rungs) => {
- if rungs.len() > 0 {
- let mut new_rungs = Vec::new();
- while let Some(bottom) = rungs.pop() {
- if let Some(last_but) = rungs.last_mut() {
- match (bottom, last_but) {
- (SugaredTypeTerm::Spec(bot_args), SugaredTypeTerm::Spec(last_args)) => {
- if bot_args.len() == last_args.len() {
- let mut new_rung_params = Vec::new();
- let mut require_break = false;
+ if rungs.len() == 0 {
+ return SugaredTypeTerm::unit();
+ } else if rungs.len() == 1 {
+ return rungs.pop().unwrap().normalize();
+ }
- if bot_args.len() > 0 {
- todo!();
- /*
- if let Ok(_idx) = last_args[0].is_syntactic_subtype_of(&bot_args[0]) {
- for i in 0 .. bot_args.len() {
+ let mut new_rungs = Vec::new();
+ let mut r2 = rungs.pop().unwrap().strip();
+ while let Some(r1) = rungs.pop() {
+ let r1 = r1.strip();
+ match (r1.clone(), r2.clone()) {
+ (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() {
+ let sr1 = if let Some(seq_repr1) = seq_repr1 { *seq_repr1.clone() }
+ else { SugaredTypeTerm::unit() };
+ let sr2 = if let Some(seq_repr2) = seq_repr2 { *seq_repr2 }
+ else { SugaredTypeTerm::unit() };
- let spliced_type_ladder = splice_ladders(
- last_args[i].clone().get_lnf_vec(),
- bot_args[i].clone().get_lnf_vec()
- );
- let spliced_type =
- if spliced_type_ladder.len() == 1 {
- spliced_type_ladder[0].clone()
- } else if spliced_type_ladder.len() > 1 {
- SugaredTypeTerm::Ladder(spliced_type_ladder)
- } else {
- SugaredTypeTerm::unit()
- };
-
- new_rung_params.push( spliced_type.param_normalize() );
- }
-
- } else {
- new_rung_params.push(
- SugaredTypeTerm::Ladder(vec![
- last_args[0].clone(),
- bot_args[0].clone()
- ])//.normalize()
- );
-
- for i in 1 .. bot_args.len() {
- if let Ok(_idx) = last_args[i].is_syntactic_subtype_of(&bot_args[i]) {
- let spliced_type_ladder = splice_ladders(
- last_args[i].clone().get_lnf_vec(),
- bot_args[i].clone().get_lnf_vec()
- );
- let spliced_type =
- if spliced_type_ladder.len() == 1 {
- spliced_type_ladder[0].clone()
- } else if spliced_type_ladder.len() > 1 {
- SugaredTypeTerm::Ladder(spliced_type_ladder)
- } else {
- SugaredTypeTerm::unit()
- };
-
- new_rung_params.push( spliced_type.param_normalize() );
- } else {
- new_rung_params.push( bot_args[i].clone() );
- require_break = true;
- }
- }
- }
- */
- }
-
- if require_break {
- new_rungs.push( SugaredTypeTerm::Spec(new_rung_params) );
+ Some(Box::new(
+ if sr1 == sr2 {
+ sr1
+ } else if sr1 == SugaredTypeTerm::unit() {
+ sr2
+ } else {
+ SugaredTypeTerm::Ladder(vec![ sr1, sr2 ]).normalize()
+ }))
} else {
- rungs.pop();
- rungs.push(SugaredTypeTerm::Spec(new_rung_params));
- }
+ None
+ },
+ items:
+ items1.into_iter()
+ .zip(items2.into_iter())
+ .map(|(item1, item2)| {
+ if item1 == item2 {
+ item1
+ } else {
+ SugaredTypeTerm::Ladder(vec![ item1.clone(), item2 ])
+ }
+ })
+ .collect()
+ };
+ }
- } else {
- new_rungs.push( SugaredTypeTerm::Spec(bot_args) );
- }
- }
- (bottom, last_buf) => {
- new_rungs.push( bottom );
- }
+ (SugaredTypeTerm::Seq { seq_repr, items },
+ SugaredTypeTerm::Spec( mut args )
+ ) => {
+ if args.len() == items.len()+1 {
+ r2 = SugaredTypeTerm::Seq {
+ seq_repr: Some(Box::new(SugaredTypeTerm::Ladder(vec![
+ if let Some(seq_repr) = seq_repr {
+ *seq_repr.clone()
+ } else {
+ SugaredTypeTerm::unit()
+ },
+ args.remove(0)
+ ]).normalize())),
+
+ items: items.into_iter()
+ .zip(args.into_iter())
+ .map(|(i1, i2)| {
+ if i1 == i2 {
+ i1
+ } else {
+ SugaredTypeTerm::Ladder(vec![ i1, i2 ]).normalize()
+ }
+ })
+ .collect()
+ };
+ } else {
+ new_rungs.push(r2);
+ r2 = r1;
+ }
+ }
+
+ (SugaredTypeTerm::Struct { struct_repr: struct_repr1, members: members1 },
+ SugaredTypeTerm::Struct { struct_repr: struct_repr2, members: members2 }) => {
+ todo!();
+ }
+
+ (SugaredTypeTerm::Enum { enum_repr: enum_repr1, variants: variants1 },
+ SugaredTypeTerm::Enum { enum_repr: enum_repr2, variants: variants2 }) => {
+ todo!();
+ }
+
+ (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()
+ );
+ } else {
+ new_rungs.push(r2);
+ r2 = r1;
+ }
+ }
+ (SugaredTypeTerm::Univ(args1), SugaredTypeTerm::Univ(args2)) => {
+ todo!();
+ }
+
+ (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);
+ }
+ r2 = atomic1;
+ } else if atomic2.is_empty() {
+ eprintln!("lol");
+ r2 = atomic1;
+ } else {
+ eprintln!("differnt, take atomic2");
+ new_rungs.push(atomic2);
+ r2 = atomic1;
}
- } else {
- new_rungs.push( bottom );
}
}
+ }
+ if new_rungs.len() > 0 {
+ new_rungs.push(r2);
new_rungs.reverse();
-
- if new_rungs.len() > 1 {
- SugaredTypeTerm::Ladder(new_rungs)
- } else if new_rungs.len() == 1 {
- new_rungs[0].clone()
- } else {
- SugaredTypeTerm::unit()
- }
+ return SugaredTypeTerm::Ladder(new_rungs);
} else {
- SugaredTypeTerm::unit()
+ return r2;
}
}
SugaredTypeTerm::Spec(params) => {
SugaredTypeTerm::Spec(
params.into_iter()
- .map(|p| p.param_normalize())
+ .map(|p| p.normalize())
.collect())
}
SugaredTypeTerm::Seq { seq_repr, items } => SugaredTypeTerm::Seq {
- seq_repr: if let Some(seq_repr) = seq_repr { Some(Box::new(seq_repr.param_normalize())) } else { None },
- items: items.into_iter().map(|p| p.param_normalize()).collect()
+ seq_repr: if let Some(seq_repr) = seq_repr { Some(Box::new(seq_repr.normalize())) } else { None },
+ items: items.into_iter().map(|p| p.normalize()).collect()
},
- SugaredTypeTerm::Struct { struct_repr, members } =>SugaredTypeTerm::Struct {
- struct_repr: if let Some(struct_repr) = struct_repr { Some(Box::new(struct_repr.param_normalize())) } else { None },
+ SugaredTypeTerm::Struct { struct_repr, members } => SugaredTypeTerm::Struct {
+ struct_repr: if let Some(struct_repr) = struct_repr { Some(Box::new(struct_repr.normalize())) } else { None },
members: members.into_iter()
.map(|SugaredStructMember{symbol, ty}|
- SugaredStructMember{ symbol, ty: ty.param_normalize() })
+ SugaredStructMember{ symbol, ty: ty.normalize() })
.collect()
},
- SugaredTypeTerm::Enum{ enum_repr, variants } => SugaredTypeTerm::Enum{
- enum_repr: if let Some(enum_repr) = enum_repr { Some(Box::new(enum_repr.param_normalize())) } else { None },
+ SugaredTypeTerm::Enum { enum_repr, variants } => SugaredTypeTerm::Enum{
+ enum_repr: if let Some(enum_repr) = enum_repr { Some(Box::new(enum_repr.normalize())) } else { None },
variants: variants.into_iter()
.map(|SugaredEnumVariant{symbol, ty}|
- SugaredEnumVariant{ symbol, ty: ty.param_normalize() })
+ SugaredEnumVariant{ symbol, ty: ty.normalize() })
.collect()
},
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 4/4] 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();