From f05ef075896b66f25b3997a7ae2b4ea1dc048936 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Thu, 13 Feb 2025 12:27:48 +0100
Subject: [PATCH 01/20] subtype unification
---
src/unification.rs | 149 +++++++++++++++++++++++++++++++++++++--------
1 file changed, 125 insertions(+), 24 deletions(-)
diff --git a/src/unification.rs b/src/unification.rs
index 443a9a2..1c0d2d9 100644
--- a/src/unification.rs
+++ b/src/unification.rs
@@ -25,7 +25,20 @@ impl UnificationProblem {
}
}
- pub fn eval_subtype(&mut self, lhs: TypeTerm, rhs: TypeTerm, addr: Vec<usize>) -> Result<(), UnificationError> {
+ pub fn reapply_subst(&mut self) {
+ // update all values in substitution
+ let mut new_σ = HashMap::new();
+ for (v, tt) in self.σ.iter() {
+ let mut tt = tt.clone().normalize();
+ tt.apply_substitution(&|v| self.σ.get(v).cloned());
+ tt = tt.normalize();
+ //eprintln!("update σ : {:?} --> {:?}", v, tt);
+ new_σ.insert(v.clone(), tt);
+ }
+ self.σ = new_σ;
+ }
+
+ pub fn eval_subtype(&mut self, lhs: TypeTerm, rhs: TypeTerm, addr: Vec<usize>) -> Result<Vec<TypeTerm>, UnificationError> {
match (lhs.clone(), rhs.clone()) {
(TypeTerm::TypeID(TypeID::Var(varid)), t) |
(t, TypeTerm::TypeID(TypeID::Var(varid))) => {
@@ -45,44 +58,56 @@ impl UnificationProblem {
}
(TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
- if a1 == a2 { Ok(()) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
+ if a1 == a2 { Ok(vec![]) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
}
(TypeTerm::Num(n1), TypeTerm::Num(n2)) => {
- if n1 == n2 { Ok(()) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
+ if n1 == n2 { Ok(vec![]) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
}
(TypeTerm::Char(c1), TypeTerm::Char(c2)) => {
- if c1 == c2 { Ok(()) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
+ if c1 == c2 { Ok(vec![]) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
}
(TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) => {
- eprintln!("unification: check two ladders");
+ let mut halo = Vec::new();
for i in 0..a1.len() {
- if let Some((_, _)) = a1[i].is_semantic_subtype_of( &a2[0] ) {
+ if let Ok((r_halo, σ)) = subtype_unify( &a1[i], &a2[0] ) {
+ //eprintln!("unified ladders at {}, r_halo = {:?}", i, r_halo);
+ for (k,v) in σ.iter() {
+ self.σ.insert(k.clone(),v.clone());
+ }
+
for j in 0..a2.len() {
if i+j < a1.len() {
let mut new_addr = addr.clone();
new_addr.push(i+j);
- self.eqs.push((a1[i+j].clone(), a2[j].clone(), new_addr))
+ self.eqs.push((a1[i+j].clone().apply_substitution(&|k| σ.get(k).cloned()).clone(),
+ a2[j].clone().apply_substitution(&|k| σ.get(k).cloned()).clone(),
+ new_addr));
}
}
- return Ok(())
+ return Ok(halo)
+ } else {
+ halo.push(a1[i].clone());
+ //eprintln!("could not unify ladders");
}
}
Err(UnificationError{ addr, t1: lhs, t2: rhs })
},
- (t, TypeTerm::Ladder(a1)) => {
- if let Some((idx, τ)) = TypeTerm::Ladder(a1.clone()).is_semantic_subtype_of(&t) {
- Ok(())
+ (t, TypeTerm::Ladder(mut a1)) => {
+ if let Ok(mut halo) = self.eval_subtype( t.clone(), a1.first().unwrap().clone(), addr.clone() ) {
+ a1.append(&mut halo);
+ Ok(a1)
} else {
- Err(UnificationError{ addr, t1: TypeTerm::Ladder(a1), t2: t })
+ Err(UnificationError{ addr, t1: t, t2: TypeTerm::Ladder(a1) })
}
}
- (TypeTerm::Ladder(a1), t) => {
- if let Some((idx, τ)) = TypeTerm::Ladder(a1.clone()).is_semantic_subtype_of(&t) {
- Ok(())
+ (TypeTerm::Ladder(mut a1), t) => {
+ if let Ok(mut halo) = self.eval_subtype( a1.pop().unwrap(), t.clone(), addr.clone() ) {
+ a1.append(&mut halo);
+ Ok(a1)
} else {
Err(UnificationError{ addr, t1: TypeTerm::Ladder(a1), t2: t })
}
@@ -90,12 +115,31 @@ impl UnificationProblem {
(TypeTerm::App(a1), TypeTerm::App(a2)) => {
if a1.len() == a2.len() {
+ let mut halo_args = Vec::new();
+ let mut halo_required = false;
+
for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
let mut new_addr = addr.clone();
new_addr.push(i);
- self.eqs.push((x, y, new_addr));
+ //self.eqs.push((x, y, new_addr));
+
+ if let Ok(halo) = self.eval_subtype( x.clone(), y.clone(), new_addr ) {
+ if halo.len() == 0 {
+ halo_args.push(y.get_lnf_vec().first().unwrap().clone());
+ } else {
+ halo_args.push(TypeTerm::Ladder(halo));
+ halo_required = true;
+ }
+ } else {
+ return Err(UnificationError{ addr, t1: x, t2: y })
+ }
+ }
+
+ if halo_required {
+ Ok(vec![ TypeTerm::App(halo_args) ])
+ } else {
+ Ok(vec![])
}
- Ok(())
} else {
Err(UnificationError{ addr, t1: lhs, t2: rhs })
}
@@ -118,7 +162,9 @@ impl UnificationProblem {
tt.apply_substitution(&|v| self.σ.get(v).cloned());
new_σ.insert(v.clone(), tt);
}
- self.σ = new_σ;
+
+ self.σ.insert(TypeID::Var(varid), t.clone());
+ self.reapply_subst();
Ok(())
}
@@ -160,16 +206,63 @@ impl UnificationProblem {
Ok(self.σ)
}
+ pub fn solve_subtype(mut self) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), UnificationError> {
- pub fn solve_subtype(mut self) -> Result<HashMap<TypeID, TypeTerm>, UnificationError> {
- while let Some( (mut lhs,mut rhs,addr) ) = self.eqs.pop() {
+ pub fn insert_halo_at(
+ t: &mut TypeTerm,
+ mut addr: Vec<usize>,
+ halo_type: TypeTerm
+ ) {
+ match t {
+ TypeTerm::Ladder(rungs) => {
+ if let Some(idx) = addr.pop() {
+ for i in rungs.len()..idx+1 {
+ rungs.push(TypeTerm::unit());
+ }
+ insert_halo_at( &mut rungs[idx], addr, halo_type );
+ } else {
+ rungs.push(halo_type);
+ }
+ },
+
+ TypeTerm::App(args) => {
+ if let Some(idx) = addr.pop() {
+ insert_halo_at( &mut args[idx], addr, halo_type );
+ } else {
+ *t = TypeTerm::Ladder(vec![
+ halo_type,
+ t.clone()
+ ]);
+ }
+ }
+
+ atomic => {
+
+ }
+ }
+ }
+
+ //let mut halo_type = TypeTerm::unit();
+ let mut halo_rungs = Vec::new();
+
+ while let Some( (mut lhs, mut rhs, mut addr) ) = self.eqs.pop() {
lhs.apply_substitution(&|v| self.σ.get(v).cloned());
rhs.apply_substitution(&|v| self.σ.get(v).cloned());
- eprintln!("eval subtype LHS={:?} || RHS={:?}", lhs, rhs);
- self.eval_subtype(lhs, rhs, addr)?;
+ //eprintln!("eval subtype\n\tLHS={:?}\n\tRHS={:?}\n", lhs, rhs);
+ let mut new_halo = self.eval_subtype(lhs, rhs, addr.clone())?;
+ if new_halo.len() > 0 {
+ //insert_halo_at( &mut halo_type, addr, TypeTerm::Ladder(new_halo) );
+ if addr.len() == 0 {
+ halo_rungs.push(TypeTerm::Ladder(new_halo))
+ }
+ }
}
- Ok(self.σ)
- }
+
+ let mut halo_type = TypeTerm::Ladder(halo_rungs);
+ halo_type = halo_type.normalize();
+ halo_type = halo_type.apply_substitution(&|k| self.σ.get(k).cloned()).clone();
+
+ Ok((halo_type.param_normalize(), self.σ))
}
pub fn unify(
@@ -180,4 +273,12 @@ pub fn unify(
unification.solve()
}
+pub fn subtype_unify(
+ t1: &TypeTerm,
+ t2: &TypeTerm
+) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), UnificationError> {
+ let mut unification = UnificationProblem::new(vec![ (t1.clone(), t2.clone()) ]);
+ unification.solve_subtype()
+}
+
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
From b502b62479b42806b8076c23881a4744fda42359 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sat, 15 Feb 2025 17:21:12 +0100
Subject: [PATCH 02/20] unification: reject non-identity loops & add test cases
---
src/term.rs | 16 +++++++++++++++
src/test/unification.rs | 30 ++++++++++++++++++++++------
src/unification.rs | 44 +++++++++++++++++------------------------
3 files changed, 58 insertions(+), 32 deletions(-)
diff --git a/src/term.rs b/src/term.rs
index 29c7d27..240996f 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -79,6 +79,22 @@ impl TypeTerm {
self.arg(TypeTerm::Char(c))
}
+ pub fn contains_var(&self, var_id: u64) -> bool {
+ match self {
+ TypeTerm::TypeID(TypeID::Var(v)) => (&var_id == v),
+ TypeTerm::App(args) |
+ TypeTerm::Ladder(args) => {
+ for a in args.iter() {
+ if a.contains_var(var_id) {
+ return true;
+ }
+ }
+ false
+ }
+ _ => false
+ }
+ }
+
/// recursively apply substitution to all subterms,
/// which will replace all occurences of variables which map
/// some type-term in `subst`
diff --git a/src/test/unification.rs b/src/test/unification.rs
index 239b384..6c55a80 100644
--- a/src/test/unification.rs
+++ b/src/test/unification.rs
@@ -61,6 +61,19 @@ fn test_unification_error() {
t2: dict.parse("B").unwrap()
})
);
+
+ assert_eq!(
+ crate::unify(
+ &dict.parse("T").unwrap(),
+ &dict.parse("<Seq T>").unwrap()
+ ),
+
+ Err(UnificationError {
+ addr: vec![],
+ t1: dict.parse("T").unwrap(),
+ t2: dict.parse("<Seq T>").unwrap()
+ })
+ );
}
#[test]
@@ -131,12 +144,13 @@ fn test_subtype_unification() {
(dict.parse("<Seq~T <Digit 10> ~ Char>").unwrap(),
dict.parse("<Seq~<LengthPrefix x86.UInt64> Char ~ Ascii>").unwrap()),
]).solve_subtype(),
- Ok(
+ Ok((
+ dict.parse("<Seq <Digit 10>>").unwrap(),
vec![
// T
(TypeID::Var(0), dict.parse("<LengthPrefix x86.UInt64>").unwrap())
].into_iter().collect()
- )
+ ))
);
assert_eq!(
@@ -144,7 +158,8 @@ fn test_subtype_unification() {
(dict.parse("U").unwrap(), dict.parse("<Seq Char>").unwrap()),
(dict.parse("T").unwrap(), dict.parse("<Seq U>").unwrap()),
]).solve_subtype(),
- Ok(
+ Ok((
+ TypeTerm::unit(),
vec![
// T
(TypeID::Var(0), dict.parse("<Seq <Seq Char>>").unwrap()),
@@ -152,7 +167,7 @@ fn test_subtype_unification() {
// U
(TypeID::Var(1), dict.parse("<Seq Char>").unwrap())
].into_iter().collect()
- )
+ ))
);
assert_eq!(
@@ -162,7 +177,10 @@ fn test_subtype_unification() {
(dict.parse("<Seq ℕ~<PosInt 10 BigEndian>>").unwrap(),
dict.parse("<Seq~<LengthPrefix x86.UInt64> W>").unwrap()),
]).solve_subtype(),
- Ok(
+ Ok((
+ dict.parse("
+ <Seq~<LengthPrefix x86.UInt64> ℕ~<PosInt 10 BigEndian>>
+ ").unwrap(),
vec![
// W
(TypeID::Var(3), dict.parse("ℕ~<PosInt 10 BigEndian>").unwrap()),
@@ -170,6 +188,6 @@ fn test_subtype_unification() {
// T
(TypeID::Var(0), dict.parse("ℕ~<PosInt 10 BigEndian>~<Seq Char>").unwrap())
].into_iter().collect()
- )
+ ))
);
}
diff --git a/src/unification.rs b/src/unification.rs
index 1c0d2d9..e605af4 100644
--- a/src/unification.rs
+++ b/src/unification.rs
@@ -42,19 +42,15 @@ impl UnificationProblem {
match (lhs.clone(), rhs.clone()) {
(TypeTerm::TypeID(TypeID::Var(varid)), t) |
(t, TypeTerm::TypeID(TypeID::Var(varid))) => {
- self.σ.insert(TypeID::Var(varid), t.clone());
-
- // update all values in substitution
- let mut new_σ = HashMap::new();
- for (v, tt) in self.σ.iter() {
- let mut tt = tt.clone().normalize();
- tt.apply_substitution(&|v| self.σ.get(v).cloned());
- eprintln!("update σ : {:?} --> {:?}", v, tt);
- new_σ.insert(v.clone(), tt);
+ if ! t.contains_var( varid ) {
+ self.σ.insert(TypeID::Var(varid), t.clone());
+ self.reapply_subst();
+ Ok(vec![])
+ } else if t == TypeTerm::TypeID(TypeID::Var(varid)) {
+ Ok(vec![])
+ } else {
+ Err(UnificationError{ addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t })
}
- self.σ = new_σ;
-
- Ok(())
}
(TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
@@ -153,20 +149,15 @@ impl UnificationProblem {
match (lhs.clone(), rhs.clone()) {
(TypeTerm::TypeID(TypeID::Var(varid)), t) |
(t, TypeTerm::TypeID(TypeID::Var(varid))) => {
- self.σ.insert(TypeID::Var(varid), t.clone());
-
- // update all values in substitution
- let mut new_σ = HashMap::new();
- for (v, tt) in self.σ.iter() {
- let mut tt = tt.clone();
- tt.apply_substitution(&|v| self.σ.get(v).cloned());
- new_σ.insert(v.clone(), tt);
+ if ! t.contains_var( varid ) {
+ self.σ.insert(TypeID::Var(varid), t.clone());
+ self.reapply_subst();
+ Ok(())
+ } else if t == TypeTerm::TypeID(TypeID::Var(varid)) {
+ Ok(())
+ } else {
+ Err(UnificationError{ addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t })
}
-
- self.σ.insert(TypeID::Var(varid), t.clone());
- self.reapply_subst();
-
- Ok(())
}
(TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
@@ -182,7 +173,7 @@ impl UnificationProblem {
(TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) |
(TypeTerm::App(a1), TypeTerm::App(a2)) => {
if a1.len() == a2.len() {
- for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
+ for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate().rev() {
let mut new_addr = addr.clone();
new_addr.push(i);
self.eqs.push((x, y, new_addr));
@@ -263,6 +254,7 @@ impl UnificationProblem {
halo_type = halo_type.apply_substitution(&|k| self.σ.get(k).cloned()).clone();
Ok((halo_type.param_normalize(), self.σ))
+ }
}
pub fn unify(
From e962dfb41ae773c8cd232292166ba415186795ac Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sun, 4 Aug 2024 23:23:20 +0200
Subject: [PATCH 03/20] initial MorphismBase with DFS to find morphism paths
---
src/lib.rs | 1 +
src/morphism.rs | 204 ++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 205 insertions(+)
create mode 100644 src/morphism.rs
diff --git a/src/lib.rs b/src/lib.rs
index 2e9a163..6d64576 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -11,6 +11,7 @@ pub mod lnf;
pub mod pnf;
pub mod subtype;
pub mod unification;
+pub mod morphism;
#[cfg(test)]
mod test;
diff --git a/src/morphism.rs b/src/morphism.rs
new file mode 100644
index 0000000..31a8e31
--- /dev/null
+++ b/src/morphism.rs
@@ -0,0 +1,204 @@
+use {
+ crate::{
+ TypeTerm, TypeID,
+ unification::UnificationProblem,
+ },
+ std::collections::HashMap
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+pub struct MorphismType {
+ pub src_type: TypeTerm,
+ pub dst_type: TypeTerm,
+}
+
+pub struct MorphismBase<Morphism: Clone> {
+ morphisms: Vec< (MorphismType, Morphism) >,
+ list_typeid: TypeID
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+impl MorphismType {
+ fn normalize(self) -> Self {
+ MorphismType {
+ src_type: self.src_type.normalize(),
+ dst_type: self.dst_type.normalize()
+ }
+ }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+impl<Morphism: Clone> MorphismBase<Morphism> {
+ pub fn new() -> Self {
+ MorphismBase {
+ morphisms: Vec::new(),
+
+ // FIXME: magic number
+ list_typeid: TypeID::Fun(10)
+ }
+ }
+
+ pub fn add_morphism(&mut self, morph_type: MorphismType, morphism: Morphism) {
+ self.morphisms.push( (morph_type.normalize(), morphism) );
+ }
+
+ pub fn enum_morphisms(&self, src_type: &TypeTerm)
+ -> Vec< (HashMap<TypeID, TypeTerm>, TypeTerm) >
+ {
+ let mut dst_types = Vec::new();
+
+ // first enumerate all "direct" morphisms,
+ for (ty,m) in self.morphisms.iter() {
+ if let Ok(σ) = crate::unification::unify(
+ &ty.src_type,
+ &src_type.clone().normalize()
+ ) {
+ let dst_type =
+ ty.dst_type.clone()
+ .apply_substitution(
+ &|x| σ.get(x).cloned()
+ )
+ .clone();
+
+ dst_types.push( (σ, dst_type) );
+ }
+ }
+
+ // ..then all "list-map" morphisms.
+ // Check if we have a List type, and if so, see what the Item type is
+
+ // TODO: function for generating fresh variables
+ let item_variable = TypeID::Var(100);
+
+ if let Ok(σ) = crate::unification::unify(
+ &TypeTerm::App(vec![
+ TypeTerm::TypeID(self.list_typeid),
+ TypeTerm::TypeID(item_variable)
+ ]),
+ &src_type.clone().param_normalize(),
+ ) {
+ let src_item_type = σ.get(&item_variable).unwrap().clone();
+
+ for (γ, dst_item_type) in self.enum_morphisms( &src_item_type ) {
+ let dst_type =
+ TypeTerm::App(vec![
+ TypeTerm::TypeID(self.list_typeid),
+ dst_item_type.clone()
+ .apply_substitution(
+ &|x| γ.get(x).cloned()
+ ).clone()
+ ]).normalize();
+
+ dst_types.push( (γ.clone(), dst_type) );
+ }
+ }
+
+ dst_types
+ }
+
+ pub fn enum_morphisms_with_subtyping(&self, src_type: &TypeTerm)
+ -> Vec< (TypeTerm, TypeTerm) >
+ {
+ let mut src_lnf = src_type.clone().get_lnf_vec();
+ let mut halo_lnf = vec![];
+ let mut dst_types = Vec::new();
+
+ while src_lnf.len() > 0 {
+ let src_type = TypeTerm::Ladder( src_lnf.clone() );
+ let halo_type = TypeTerm::Ladder( halo_lnf.clone() );
+
+ for (σ, t) in self.enum_morphisms( &src_type ) {
+ dst_types.push(
+ (halo_type.clone()
+ .apply_substitution(
+ &|x| σ.get(x).cloned()
+ ).clone(),
+ t.clone()
+ .apply_substitution(
+ &|x| σ.get(x).cloned()
+ ).clone()
+ )
+ );
+ }
+
+ // continue with next supertype
+ halo_lnf.push(src_lnf.remove(0));
+ }
+
+ dst_types
+ }
+
+ /* performs DFS to find a morphism-path for a given type
+ * will return the first matching path, not the shortest
+ */
+ pub fn find_morphism_path(&self, ty: MorphismType)
+ -> Option< Vec<TypeTerm> >
+ {
+ let ty = ty.normalize();
+ let mut visited = Vec::new();
+ let mut queue = vec![
+ vec![ ty.src_type.clone().normalize() ]
+ ];
+
+ while let Some(current_path) = queue.pop() {
+ let current_type = current_path.last().unwrap();
+
+ if ! visited.contains( current_type ) {
+ visited.push( current_type.clone() );
+
+ for (h, t) in self.enum_morphisms_with_subtyping(¤t_type) {
+ let tt = TypeTerm::Ladder( vec![ h, t ] ).normalize();
+
+ if ! visited.contains( &tt ) {
+ let unification_result = crate::unification::unify(&tt, &ty.dst_type);
+ let mut new_path = current_path.clone();
+
+ new_path.push( tt );
+
+ if let Ok(σ) = unification_result {
+ new_path = new_path.into_iter().map(
+ |mut t: TypeTerm| t.apply_substitution(&|x| σ.get(x).cloned()).clone()
+ ).collect::<Vec<TypeTerm>>();
+
+ return Some(new_path);
+ } else {
+ queue.push( new_path );
+ }
+ }
+ }
+ }
+ }
+
+ None
+ }
+
+ pub fn find_morphism(&self, ty: &MorphismType)
+ -> Option< Morphism > {
+
+ // TODO
+
+ None
+ }
+
+ pub fn find_list_map_morphism(&self, item_ty: &MorphismType)
+ -> Option< Morphism > {
+
+ // TODO
+
+ None
+ }
+
+ pub fn find_morphism_with_subtyping(&self, ty: &MorphismType)
+ -> Option<( Morphism, TypeTerm, HashMap<TypeID, TypeTerm> )> {
+
+ // TODO
+
+ None
+ }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
From 2ddd4c4a6186e86b9303196d99a1c868324ba475 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sun, 4 Aug 2024 23:47:59 +0200
Subject: [PATCH 04/20] add test for find_morphism_path()
---
src/morphism.rs | 6 ++--
src/test/mod.rs | 1 +
src/test/morphism.rs | 70 ++++++++++++++++++++++++++++++++++++++++++++
3 files changed, 73 insertions(+), 4 deletions(-)
create mode 100644 src/test/morphism.rs
diff --git a/src/morphism.rs b/src/morphism.rs
index 31a8e31..6b921bf 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -32,12 +32,10 @@ impl MorphismType {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl<Morphism: Clone> MorphismBase<Morphism> {
- pub fn new() -> Self {
+ pub fn new(list_typeid: TypeID) -> Self {
MorphismBase {
morphisms: Vec::new(),
-
- // FIXME: magic number
- list_typeid: TypeID::Fun(10)
+ list_typeid
}
}
diff --git a/src/test/mod.rs b/src/test/mod.rs
index 29c14bc..41f5e71 100644
--- a/src/test/mod.rs
+++ b/src/test/mod.rs
@@ -7,4 +7,5 @@ pub mod pnf;
pub mod subtype;
pub mod substitution;
pub mod unification;
+pub mod morphism;
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
new file mode 100644
index 0000000..d2328d7
--- /dev/null
+++ b/src/test/morphism.rs
@@ -0,0 +1,70 @@
+use {
+ crate::{dict::*, morphism::*}
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[test]
+fn test_morphism_path() {
+ let mut dict = TypeDict::new();
+ let mut base = MorphismBase::<u64>::new( dict.add_typename("Seq".into()) );
+
+ dict.add_varname("Radix".into());
+ dict.add_varname("SrcRadix".into());
+ dict.add_varname("DstRadix".into());
+
+ base.add_morphism(
+ MorphismType{
+ src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
+ dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
+ },
+ 11
+ );
+ base.add_morphism(
+ MorphismType{
+ src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
+ dst_type: dict.parse("<Digit Radix> ~ Char").unwrap()
+ },
+ 22
+ );
+ base.add_morphism(
+ 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()
+ },
+ 333
+ );
+ base.add_morphism(
+ 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()
+ },
+ 444
+ );
+ base.add_morphism(
+ 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()
+ },
+ 555
+ );
+
+
+ assert_eq!(
+ base.find_morphism_path(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()
+ }),
+ Some(
+ vec![
+ dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().normalize(),
+ dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
+ dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
+ dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
+ dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
+ dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().normalize(),
+ ]
+ )
+ );
+}
+
From a0f71b1223ecfb8f1715b72ed644325a9f56b49b Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Mon, 5 Aug 2024 02:54:35 +0200
Subject: [PATCH 05/20] turn Morphism into trait and add find_morphism()
function
---
src/lib.rs | 1 +
src/morphism.rs | 91 +++++++++++++++++++++++++++++++++-----------
src/test/morphism.rs | 53 +++++++++++++++++---------
3 files changed, 105 insertions(+), 40 deletions(-)
diff --git a/src/lib.rs b/src/lib.rs
index 6d64576..3361a6a 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -24,4 +24,5 @@ pub use {
term::*,
sugar::*,
unification::*,
+ morphism::*
};
diff --git a/src/morphism.rs b/src/morphism.rs
index 6b921bf..3211651 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -8,20 +8,27 @@ use {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+#[derive(Clone, PartialEq, Eq, Debug)]
pub struct MorphismType {
pub src_type: TypeTerm,
pub dst_type: TypeTerm,
}
-pub struct MorphismBase<Morphism: Clone> {
- morphisms: Vec< (MorphismType, Morphism) >,
+pub trait Morphism : Sized {
+ fn get_type(&self) -> MorphismType;
+ fn list_map_morphism(&self, list_typeid: TypeID) -> Option< Self >;
+}
+
+#[derive(Clone)]
+pub struct MorphismBase<M: Morphism + Clone> {
+ morphisms: Vec< M >,
list_typeid: TypeID
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl MorphismType {
- fn normalize(self) -> Self {
+ pub fn normalize(self) -> Self {
MorphismType {
src_type: self.src_type.normalize(),
dst_type: self.dst_type.normalize()
@@ -31,7 +38,7 @@ impl MorphismType {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-impl<Morphism: Clone> MorphismBase<Morphism> {
+impl<M: Morphism + Clone> MorphismBase<M> {
pub fn new(list_typeid: TypeID) -> Self {
MorphismBase {
morphisms: Vec::new(),
@@ -39,8 +46,8 @@ impl<Morphism: Clone> MorphismBase<Morphism> {
}
}
- pub fn add_morphism(&mut self, morph_type: MorphismType, morphism: Morphism) {
- self.morphisms.push( (morph_type.normalize(), morphism) );
+ pub fn add_morphism(&mut self, m: M) {
+ self.morphisms.push( m );
}
pub fn enum_morphisms(&self, src_type: &TypeTerm)
@@ -49,17 +56,15 @@ impl<Morphism: Clone> MorphismBase<Morphism> {
let mut dst_types = Vec::new();
// first enumerate all "direct" morphisms,
- for (ty,m) in self.morphisms.iter() {
+ for m in self.morphisms.iter() {
if let Ok(σ) = crate::unification::unify(
- &ty.src_type,
+ &m.get_type().src_type,
&src_type.clone().normalize()
) {
let dst_type =
- ty.dst_type.clone()
- .apply_substitution(
- &|x| σ.get(x).cloned()
- )
- .clone();
+ m.get_type().dst_type.clone()
+ .apply_substitution( &|x| σ.get(x).cloned() )
+ .clone();
dst_types.push( (σ, dst_type) );
}
@@ -173,26 +178,68 @@ impl<Morphism: Clone> MorphismBase<Morphism> {
None
}
+
pub fn find_morphism(&self, ty: &MorphismType)
- -> Option< Morphism > {
+ -> Option< ( M, HashMap<TypeID, TypeTerm> ) > {
- // TODO
+ // try list-map morphism
+ if let Ok(σ) = UnificationProblem::new(vec![
+ (ty.src_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(self.list_typeid), TypeTerm::TypeID(TypeID::Var(100)) ])),
+ (ty.dst_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(self.list_typeid), TypeTerm::TypeID(TypeID::Var(101)) ])),
+ ]).solve() {
- None
- }
+ // TODO: use real fresh variable names
+ let item_morph_type = MorphismType {
+ src_type: σ.get(&TypeID::Var(100)).unwrap().clone(),
+ dst_type: σ.get(&TypeID::Var(101)).unwrap().clone(),
+ }.normalize();
- pub fn find_list_map_morphism(&self, item_ty: &MorphismType)
- -> Option< Morphism > {
+ if let Some((m, σ)) = self.find_morphism( &item_morph_type ) {
+ if let Some(list_morph) = m.list_map_morphism( self.list_typeid ) {
+ return Some( (list_morph, σ) );
+ }
+ }
+ }
- // TODO
+ // otherwise
+ for m in self.morphisms.iter() {
+ let unification_problem = UnificationProblem::new(
+ vec![
+ ( ty.src_type.clone().normalize(), m.get_type().src_type.clone() ),
+ ( ty.dst_type.clone().normalize(), m.get_type().dst_type.clone() )
+ ]
+ );
+
+ let unification_result = unification_problem.solve();
+ if let Ok(σ) = unification_result {
+ return Some((m.clone(), σ));
+ }
+ }
None
}
pub fn find_morphism_with_subtyping(&self, ty: &MorphismType)
- -> Option<( Morphism, TypeTerm, HashMap<TypeID, TypeTerm> )> {
+ -> Option<( M, TypeTerm, HashMap<TypeID, TypeTerm> )> {
+ let mut src_lnf = ty.src_type.clone().get_lnf_vec();
+ let mut dst_lnf = ty.dst_type.clone().get_lnf_vec();
+ let mut halo = vec![];
- // TODO
+ while src_lnf.len() > 0 && dst_lnf.len() > 0 {
+ if let Some((m, σ)) = self.find_morphism(&MorphismType{
+ src_type: TypeTerm::Ladder(src_lnf.clone()),
+ dst_type: TypeTerm::Ladder(dst_lnf.clone())
+ }) {
+ return Some((m, TypeTerm::Ladder(halo), σ));
+ } else {
+ if src_lnf[0] == dst_lnf[0] {
+ src_lnf.remove(0);
+ halo.push(dst_lnf.remove(0));
+ } else {
+ return None;
+ }
+ }
+ }
None
}
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index d2328d7..fa4b492 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -1,55 +1,72 @@
use {
- crate::{dict::*, morphism::*}
+ crate::{dict::*, morphism::*, TypeTerm}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+#[derive(Clone)]
+struct DummyMorphism(MorphismType);
+
+impl Morphism for DummyMorphism {
+ fn get_type(&self) -> MorphismType {
+ self.0.clone().normalize()
+ }
+
+ fn list_map_morphism(&self, list_typeid: TypeID) -> Option<DummyMorphism> {
+ Some(DummyMorphism(MorphismType {
+ src_type: TypeTerm::App(vec![
+ TypeTerm::TypeID( list_typeid ),
+ self.0.src_type.clone()
+ ]),
+
+ dst_type: TypeTerm::App(vec![
+ TypeTerm::TypeID( list_typeid ),
+ self.0.dst_type.clone()
+ ])
+ }))
+ }
+}
+
#[test]
fn test_morphism_path() {
let mut dict = TypeDict::new();
- let mut base = MorphismBase::<u64>::new( dict.add_typename("Seq".into()) );
+ let mut base = MorphismBase::<DummyMorphism>::new( dict.add_typename("Seq".into()) );
dict.add_varname("Radix".into());
dict.add_varname("SrcRadix".into());
dict.add_varname("DstRadix".into());
base.add_morphism(
- MorphismType{
+ DummyMorphism(MorphismType{
src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
- },
- 11
+ })
);
base.add_morphism(
- MorphismType{
+ DummyMorphism(MorphismType{
src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
dst_type: dict.parse("<Digit Radix> ~ Char").unwrap()
- },
- 22
+ })
);
base.add_morphism(
- MorphismType{
+ 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()
- },
- 333
+ })
);
base.add_morphism(
- MorphismType{
+ 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()
- },
- 444
+ })
);
base.add_morphism(
- MorphismType{
+ 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()
- },
- 555
+ })
);
-
assert_eq!(
base.find_morphism_path(MorphismType {
src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
From 802480d0891a5cdb70e8dea207c526477fa2561e Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Tue, 6 Aug 2024 15:37:23 +0200
Subject: [PATCH 06/20] fix returned halo type in
find_morphism_with_subtyping()
---
src/morphism.rs | 5 ++++-
src/test/morphism.rs | 42 +++++++++++++++++++++++++++++++++++++++++-
2 files changed, 45 insertions(+), 2 deletions(-)
diff --git a/src/morphism.rs b/src/morphism.rs
index 3211651..0796c91 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -230,7 +230,10 @@ impl<M: Morphism + Clone> MorphismBase<M> {
src_type: TypeTerm::Ladder(src_lnf.clone()),
dst_type: TypeTerm::Ladder(dst_lnf.clone())
}) {
- return Some((m, TypeTerm::Ladder(halo), σ));
+ halo.push(src_lnf.get(0).unwrap().clone());
+ return Some((m,
+ TypeTerm::Ladder(halo).apply_substitution(&|x| σ.get(x).cloned()).clone(),
+ σ));
} else {
if src_lnf[0] == dst_lnf[0] {
src_lnf.remove(0);
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index fa4b492..47bd100 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -4,7 +4,7 @@ use {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-#[derive(Clone)]
+#[derive(Clone, Debug, PartialEq)]
struct DummyMorphism(MorphismType);
impl Morphism for DummyMorphism {
@@ -83,5 +83,45 @@ fn test_morphism_path() {
]
)
);
+
+ assert_eq!(
+ base.find_morphism_path(MorphismType {
+ src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+ dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
+ }),
+ Some(
+ vec![
+ dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().normalize(),
+ dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
+ dict.parse("Symbol ~ ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
+ dict.parse("Symbol ~ ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
+ dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
+ dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().normalize(),
+ ]
+ )
+ );
+
+ assert_eq!(
+ base.find_morphism_with_subtyping(
+ &MorphismType {
+ src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+ dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+ }
+ ),
+
+ Some((
+ DummyMorphism(MorphismType{
+ src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
+ dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+ }),
+
+ dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>>").unwrap(),
+
+ vec![
+ (dict.get_typeid(&"Radix".into()).unwrap(),
+ dict.parse("10").unwrap())
+ ].into_iter().collect::<std::collections::HashMap<TypeID, TypeTerm>>()
+ ))
+ );
}
From 81e87f111acf6a028069aae2018c04227fbc06dc Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sun, 11 Aug 2024 22:50:48 +0200
Subject: [PATCH 07/20] morphism base: find shortest path instead of just some
path
---
src/morphism.rs | 34 ++++++++++++++++++++++------------
1 file changed, 22 insertions(+), 12 deletions(-)
diff --git a/src/morphism.rs b/src/morphism.rs
index 0796c91..33eafd5 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -17,6 +17,10 @@ pub struct MorphismType {
pub trait Morphism : Sized {
fn get_type(&self) -> MorphismType;
fn list_map_morphism(&self, list_typeid: TypeID) -> Option< Self >;
+
+ fn weight(&self) -> u64 {
+ 1
+ }
}
#[derive(Clone)]
@@ -134,41 +138,47 @@ impl<M: Morphism + Clone> MorphismBase<M> {
dst_types
}
- /* performs DFS to find a morphism-path for a given type
- * will return the first matching path, not the shortest
+ /* try to find shortest morphism-path for a given type
*/
pub fn find_morphism_path(&self, ty: MorphismType)
-> Option< Vec<TypeTerm> >
{
let ty = ty.normalize();
- let mut visited = Vec::new();
+
let mut queue = vec![
- vec![ ty.src_type.clone().normalize() ]
+ (0, vec![ ty.src_type.clone().normalize() ])
];
- while let Some(current_path) = queue.pop() {
- let current_type = current_path.last().unwrap();
+ while ! queue.is_empty() {
+ queue.sort_by( |&(w1,_),&(w2,_)| w2.cmp(&w1));
- if ! visited.contains( current_type ) {
- visited.push( current_type.clone() );
+ if let Some((current_weight, current_path)) = queue.pop() {
+ let current_type = current_path.last().unwrap();
for (h, t) in self.enum_morphisms_with_subtyping(¤t_type) {
let tt = TypeTerm::Ladder( vec![ h, t ] ).normalize();
- if ! visited.contains( &tt ) {
+ if ! current_path.contains( &tt ) {
let unification_result = crate::unification::unify(&tt, &ty.dst_type);
- let mut new_path = current_path.clone();
+ let morphism_weight = 1;
+ /*
+ {
+ self.find_morphism( &tt ).unwrap().0.get_weight()
+ };
+ */
+
+ let new_weight = current_weight + morphism_weight;
+ let mut new_path = current_path.clone();
new_path.push( tt );
if let Ok(σ) = unification_result {
new_path = new_path.into_iter().map(
|mut t: TypeTerm| t.apply_substitution(&|x| σ.get(x).cloned()).clone()
).collect::<Vec<TypeTerm>>();
-
return Some(new_path);
} else {
- queue.push( new_path );
+ queue.push( (new_weight, new_path) );
}
}
}
From 8e6885197a55e2315e37951fe067e7139ff71115 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Mon, 12 Aug 2024 21:18:17 +0200
Subject: [PATCH 08/20] initial implementation of solver for steiner trees
---
src/lib.rs | 1 +
src/morphism.rs | 1 -
src/steiner_tree.rs | 162 +++++++++++++++++++++++++++++++++++++++++++
src/test/morphism.rs | 42 +++++++++--
4 files changed, 201 insertions(+), 5 deletions(-)
create mode 100644 src/steiner_tree.rs
diff --git a/src/lib.rs b/src/lib.rs
index 3361a6a..11a001f 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -12,6 +12,7 @@ pub mod pnf;
pub mod subtype;
pub mod unification;
pub mod morphism;
+pub mod steiner_tree;
#[cfg(test)]
mod test;
diff --git a/src/morphism.rs b/src/morphism.rs
index 33eafd5..9160610 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -188,7 +188,6 @@ impl<M: Morphism + Clone> MorphismBase<M> {
None
}
-
pub fn find_morphism(&self, ty: &MorphismType)
-> Option< ( M, HashMap<TypeID, TypeTerm> ) > {
diff --git a/src/steiner_tree.rs b/src/steiner_tree.rs
new file mode 100644
index 0000000..f5338e9
--- /dev/null
+++ b/src/steiner_tree.rs
@@ -0,0 +1,162 @@
+use {
+ std::collections::HashMap,
+ crate::{
+ TypeID,
+ TypeTerm,
+ morphism::{
+ MorphismType,
+ Morphism,
+ MorphismBase
+ }
+ }
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct SteinerTree {
+ weight: u64,
+ goals: Vec< TypeTerm >,
+ pub edges: Vec< MorphismType >,
+}
+
+impl SteinerTree {
+ fn add_edge(&mut self, ty: MorphismType) {
+ self.weight += 1;
+
+ let ty = ty.normalize();
+
+ // check if by adding this new edge, we reach a goal
+ let mut new_goals = Vec::new();
+ let mut added = false;
+
+ for g in self.goals.clone() {
+ if let Ok(σ) = crate::unify(&ty.dst_type, &g) {
+ if !added {
+ self.edges.push(ty.clone());
+
+ // goal reached.
+ for e in self.edges.iter_mut() {
+ e.src_type = e.src_type.apply_substitution(&|x| σ.get(x).cloned()).clone();
+ e.dst_type = e.dst_type.apply_substitution(&|x| σ.get(x).cloned()).clone();
+ }
+ added = true;
+ } else {
+ new_goals.push(g);
+ }
+ } else {
+ new_goals.push(g);
+ }
+ }
+
+ if !added {
+ self.edges.push(ty.clone());
+ }
+
+ self.goals = new_goals;
+ }
+
+ fn is_solved(&self) -> bool {
+ self.goals.len() == 0
+ }
+
+ fn contains(&self, t: &TypeTerm) -> Option< HashMap<TypeID, TypeTerm> > {
+ for e in self.edges.iter() {
+ if let Ok(σ) = crate::unify(&e.dst_type, t) {
+ return Some(σ)
+ }
+ }
+
+ None
+ }
+}
+
+/* given a representation tree with the available
+ * represenatations `src_types`, try to find
+ * a sequence of morphisms that span up all
+ * representations in `dst_types`.
+ */
+pub struct SteinerTreeProblem {
+ src_types: Vec< TypeTerm >,
+ queue: Vec< SteinerTree >
+}
+
+impl SteinerTreeProblem {
+ pub fn new(
+ src_types: Vec< TypeTerm >,
+ dst_types: Vec< TypeTerm >
+ ) -> Self {
+ SteinerTreeProblem {
+ src_types: src_types.into_iter().map(|t| t.normalize()).collect(),
+ queue: vec![
+ SteinerTree {
+ weight: 0,
+ goals: dst_types.into_iter().map(|t| t.normalize()).collect(),
+ edges: Vec::new()
+ }
+ ]
+ }
+ }
+
+ pub fn next(&mut self) -> Option< SteinerTree > {
+ eprintln!("queue size = {}", self.queue.len());
+
+ /* FIXME: by giving the highest priority to
+ * candidate tree with the least remaining goals,
+ * the optimality of the search algorithm
+ * is probably destroyed, but it dramatically helps
+ * to tame the combinatorical explosion in this algorithm.
+ */
+ self.queue.sort_by(|t1, t2|
+ if t1.goals.len() < t2.goals.len() {
+ std::cmp::Ordering::Greater
+ } else if t1.goals.len() == t2.goals.len() {
+ if t1.weight < t2.weight {
+ std::cmp::Ordering::Greater
+ } else {
+ std::cmp::Ordering::Less
+ }
+ } else {
+ std::cmp::Ordering::Less
+ }
+ );
+ self.queue.pop()
+ }
+
+ pub fn solve_bfs<M: Morphism + Clone>(&mut self, dict: &crate::dict::TypeDict, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
+
+ // take the currently smallest tree and extend it by one step
+ while let Some( mut current_tree ) = self.next() {
+
+ // check if current tree is a solution
+ if current_tree.goals.len() == 0 {
+ return Some(current_tree);
+ }
+
+ // get all vertices spanned by this tree
+ let mut current_nodes = self.src_types.clone();
+ for e in current_tree.edges.iter() {
+ current_nodes.push( e.dst_type.clone() );
+ }
+
+ // extend the tree by one edge and add it to the queue
+ for src_type in current_nodes.iter() {
+ for (dst_halo,dst_ty) in morphisms.enum_morphisms_with_subtyping( &src_type ) {
+ let dst_type = TypeTerm::Ladder(vec![
+ dst_halo, dst_ty
+ ]).normalize();
+
+ if !current_nodes.contains( &dst_type ) {
+ let mut new_tree = current_tree.clone();
+ let src_type = src_type.clone();
+ new_tree.add_edge(MorphismType { src_type, dst_type }.normalize());
+ self.queue.push( new_tree );
+ }
+ }
+ }
+ }
+
+ None
+ }
+}
+
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index 47bd100..b908101 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -1,5 +1,5 @@
use {
- crate::{dict::*, morphism::*, TypeTerm}
+ crate::{dict::*, morphism::*, steiner_tree::*, TypeTerm}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -26,9 +26,8 @@ impl Morphism for DummyMorphism {
}))
}
}
-
-#[test]
-fn test_morphism_path() {
+
+fn morphism_test_setup() -> ( TypeDict, MorphismBase<DummyMorphism> ) {
let mut dict = TypeDict::new();
let mut base = MorphismBase::<DummyMorphism>::new( dict.add_typename("Seq".into()) );
@@ -67,6 +66,13 @@ fn test_morphism_path() {
})
);
+ (dict, base)
+}
+
+#[test]
+fn test_morphism_path() {
+ let (mut dict, mut base) = morphism_test_setup();
+
assert_eq!(
base.find_morphism_path(MorphismType {
src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
@@ -125,3 +131,31 @@ fn test_morphism_path() {
);
}
+#[test]
+fn test_steiner_tree() {
+ let (mut dict, mut base) = morphism_test_setup();
+
+
+ let mut steiner_tree_problem = SteinerTreeProblem::new(
+ // source reprs
+ vec![
+ dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+ ],
+
+ // destination reprs
+ vec![
+ dict.parse("ℕ ~ <PosInt 2 BigEndian> ~ <Seq <Digit 2> ~ Char>").unwrap(),
+ dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+ dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
+ ]
+ );
+
+ if let Some(solution) = steiner_tree_problem.solve_bfs( &dict, &base ) {
+ for e in solution.edges.iter() {
+ eprintln!(" :: {}\n--> {}", dict.unparse(&e.src_type), dict.unparse(&e.dst_type));
+ }
+ } else {
+ eprintln!("no solution");
+ }
+}
+
From d795ba45e96432e22f025f0e6de2e52d5b3173ed Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Fri, 27 Sep 2024 12:15:40 +0200
Subject: [PATCH 09/20] add steiner tree solver based on shortest path
---
src/steiner_tree.rs | 93 ++++++++++++++++++++++++++++++++++++++++++---
1 file changed, 87 insertions(+), 6 deletions(-)
diff --git a/src/steiner_tree.rs b/src/steiner_tree.rs
index f5338e9..f854dd9 100644
--- a/src/steiner_tree.rs
+++ b/src/steiner_tree.rs
@@ -17,10 +17,14 @@ use {
pub struct SteinerTree {
weight: u64,
goals: Vec< TypeTerm >,
- pub edges: Vec< MorphismType >,
+ edges: Vec< MorphismType >,
}
impl SteinerTree {
+ pub fn into_edges(self) -> Vec< MorphismType > {
+ self.edges
+ }
+
fn add_edge(&mut self, ty: MorphismType) {
self.weight += 1;
@@ -71,6 +75,72 @@ impl SteinerTree {
}
}
+
+pub struct PathApproxSteinerTreeSolver {
+ root: TypeTerm,
+ leaves: Vec< TypeTerm >
+}
+
+impl PathApproxSteinerTreeSolver {
+ pub fn new(
+ root: TypeTerm,
+ leaves: Vec<TypeTerm>
+ ) -> Self {
+ PathApproxSteinerTreeSolver {
+ root, leaves
+ }
+ }
+
+ pub fn solve<M: Morphism + Clone>(self, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
+ let mut tree = Vec::<MorphismType>::new();
+
+ for goal in self.leaves {
+ // try to find shortest path from root to current leaf
+ if let Some(new_path) = morphisms.find_morphism_path(
+ MorphismType {
+ src_type: self.root.clone(),
+ dst_type: goal.clone()
+ }
+ ) {
+ // reduce new path so that it does not collide with any existing path
+ let mut src_type = self.root.clone();
+ let mut new_path_iter = new_path.into_iter().peekable();
+
+ // check all existing nodes..
+ for mt in tree.iter() {
+// assert!( mt.src_type == &src_type );
+ if let Some(t) = new_path_iter.peek() {
+ if &mt.dst_type == t {
+ // eliminate this node from new path
+ src_type = new_path_iter.next().unwrap().clone();
+ }
+ } else {
+ break;
+ }
+ }
+
+ for dst_type in new_path_iter {
+ tree.push(MorphismType {
+ src_type: src_type.clone(),
+ dst_type: dst_type.clone()
+ });
+ src_type = dst_type;
+ }
+ } else {
+ eprintln!("could not find path\nfrom {:?}\nto {:?}", &self.root, &goal);
+ return None;
+ }
+ }
+
+ Some(SteinerTree {
+ weight: 0,
+ goals: vec![],
+ edges: tree
+ })
+ }
+}
+
+
/* given a representation tree with the available
* represenatations `src_types`, try to find
* a sequence of morphisms that span up all
@@ -122,8 +192,15 @@ impl SteinerTreeProblem {
);
self.queue.pop()
}
+/*
+ pub fn solve_approx_path<M: Morphism + Clone>(&mut self, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
+ if let Some(master) = self.src_types.first() {
- pub fn solve_bfs<M: Morphism + Clone>(&mut self, dict: &crate::dict::TypeDict, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
+
+ }
+ }
+*/
+ pub fn solve_bfs<M: Morphism + Clone>(&mut self, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
// take the currently smallest tree and extend it by one step
while let Some( mut current_tree ) = self.next() {
@@ -140,16 +217,20 @@ impl SteinerTreeProblem {
}
// extend the tree by one edge and add it to the queue
- for src_type in current_nodes.iter() {
+ for src_type in current_nodes {
for (dst_halo,dst_ty) in morphisms.enum_morphisms_with_subtyping( &src_type ) {
let dst_type = TypeTerm::Ladder(vec![
dst_halo, dst_ty
]).normalize();
- if !current_nodes.contains( &dst_type ) {
+ if current_tree.contains( &dst_type ).is_none() {
let mut new_tree = current_tree.clone();
- let src_type = src_type.clone();
- new_tree.add_edge(MorphismType { src_type, dst_type }.normalize());
+ {
+ let src_type = src_type.clone();
+ let dst_type = dst_type.clone();
+ new_tree.add_edge(MorphismType { src_type, dst_type }.normalize());
+ }
+
self.queue.push( new_tree );
}
}
From a144521566fa092c98aaf390eceda4e03ced0f5c Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Thu, 3 Oct 2024 23:40:04 +0200
Subject: [PATCH 10/20] make TypeDict a trait & BimapTypeDict an impl
---
src/dict.rs | 76 ++++++++++++++++++++++++++++++++++++-------------
src/parser.rs | 17 +++++++++--
src/sugar.rs | 7 +++--
src/unparser.rs | 8 ++++--
4 files changed, 82 insertions(+), 26 deletions(-)
diff --git a/src/dict.rs b/src/dict.rs
index 419d599..4d5b35b 100644
--- a/src/dict.rs
+++ b/src/dict.rs
@@ -8,9 +8,27 @@ pub enum TypeID {
Var(u64)
}
+pub trait TypeDict {
+ fn insert(&mut self, name: String, id: TypeID);
+ fn add_varname(&mut self, vn: String) -> TypeID;
+ fn add_typename(&mut self, tn: String) -> TypeID;
+ fn get_typeid(&self, tn: &String) -> Option<TypeID>;
+ fn get_typename(&self, tid: &TypeID) -> Option<String>;
+
+ fn get_varname(&self, var_id: u64) -> Option<String> {
+ self.get_typename(&TypeID::Var(var_id))
+ }
+
+ fn add_synonym(&mut self, new: String, old: String) {
+ if let Some(tyid) = self.get_typeid(&old) {
+ self.insert(new, tyid);
+ }
+ }
+}
+
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-pub struct TypeDict {
+pub struct BimapTypeDict {
typenames: Bimap<String, TypeID>,
type_lit_counter: u64,
type_var_counter: u64,
@@ -18,46 +36,66 @@ pub struct TypeDict {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-impl TypeDict {
+impl BimapTypeDict {
pub fn new() -> Self {
- TypeDict {
+ BimapTypeDict {
typenames: Bimap::new(),
type_lit_counter: 0,
type_var_counter: 0,
}
}
+}
- pub fn add_varname(&mut self, tn: String) -> TypeID {
+impl TypeDict for BimapTypeDict {
+ fn insert(&mut self, name: String, id: TypeID) {
+ self.typenames.insert(name, id);
+ }
+
+ fn add_varname(&mut self, tn: String) -> TypeID {
let tyid = TypeID::Var(self.type_var_counter);
self.type_var_counter += 1;
- self.typenames.insert(tn, tyid.clone());
+ self.insert(tn, tyid.clone());
tyid
}
- pub fn add_typename(&mut self, tn: String) -> TypeID {
+ fn add_typename(&mut self, tn: String) -> TypeID {
let tyid = TypeID::Fun(self.type_lit_counter);
self.type_lit_counter += 1;
- self.typenames.insert(tn, tyid.clone());
+ self.insert(tn, tyid.clone());
tyid
}
- pub fn add_synonym(&mut self, new: String, old: String) {
- if let Some(tyid) = self.get_typeid(&old) {
- self.typenames.insert(new, tyid);
- }
- }
-
- pub fn get_typename(&self, tid: &TypeID) -> Option<String> {
+ fn get_typename(&self, tid: &TypeID) -> Option<String> {
self.typenames.my.get(tid).cloned()
}
- pub fn get_typeid(&self, tn: &String) -> Option<TypeID> {
+ fn get_typeid(&self, tn: &String) -> Option<TypeID> {
self.typenames.mλ.get(tn).cloned()
}
-
- pub fn get_varname(&self, var_id: u64) -> Option<String> {
- self.typenames.my.get(&TypeID::Var(var_id)).cloned()
- }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
+
+use std::sync::Arc;
+use std::ops::{Deref, DerefMut};
+use std::sync::RwLock;
+
+impl<T: TypeDict> TypeDict for Arc<RwLock<T>> {
+ fn insert(&mut self, name: String, id: TypeID) {
+ self.write().unwrap().insert(name, id);
+ }
+ fn add_varname(&mut self, vn: String) -> TypeID {
+ self.write().unwrap().add_varname(vn)
+ }
+ fn add_typename(&mut self, tn: String) -> TypeID {
+ self.write().unwrap().add_typename(tn)
+ }
+ fn get_typename(&self, tid: &TypeID)-> Option<String> {
+ self.read().unwrap().get_typename(tid)
+ }
+ fn get_typeid(&self, tn: &String) -> Option<TypeID> {
+ self.read().unwrap().get_typeid(tn)
+ }
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
diff --git a/src/parser.rs b/src/parser.rs
index 85ff9b4..6160ca6 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -18,10 +18,23 @@ pub enum ParseError {
UnexpectedToken
}
+pub trait ParseLadderType {
+ fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError>;
+
+ fn parse_app<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
+ where It: Iterator<Item = char>;
+
+ fn parse_rung<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
+ where It: Iterator<Item = char>;
+
+ fn parse_ladder<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
+ where It: Iterator<Item = char>;
+}
+
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-impl TypeDict {
- pub fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError> {
+impl<T: TypeDict> ParseLadderType for T {
+ fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError> {
let mut tokens = LadderTypeLexer::from(s.chars()).peekable();
match self.parse_ladder(&mut tokens) {
diff --git a/src/sugar.rs b/src/sugar.rs
index 4d13f78..dea73ba 100644
--- a/src/sugar.rs
+++ b/src/sugar.rs
@@ -1,7 +1,8 @@
use {
- crate::{TypeTerm, TypeID}
+ crate::{TypeTerm, TypeID, parser::ParseLadderType}
};
+#[derive(Clone)]
pub enum SugaredTypeTerm {
TypeID(TypeID),
Num(i64),
@@ -17,7 +18,7 @@ pub enum SugaredTypeTerm {
}
impl TypeTerm {
- pub fn sugar(self: TypeTerm, dict: &mut crate::TypeDict) -> SugaredTypeTerm {
+ pub fn sugar(self: TypeTerm, dict: &mut impl crate::TypeDict) -> SugaredTypeTerm {
match self {
TypeTerm::TypeID(id) => SugaredTypeTerm::TypeID(id),
TypeTerm::Num(n) => SugaredTypeTerm::Num(n),
@@ -61,7 +62,7 @@ impl TypeTerm {
}
impl SugaredTypeTerm {
- pub fn desugar(self, dict: &mut crate::TypeDict) -> TypeTerm {
+ pub fn desugar(self, dict: &mut impl crate::TypeDict) -> TypeTerm {
match self {
SugaredTypeTerm::TypeID(id) => TypeTerm::TypeID(id),
SugaredTypeTerm::Num(n) => TypeTerm::Num(n),
diff --git a/src/unparser.rs b/src/unparser.rs
index ccf754d..b78494e 100644
--- a/src/unparser.rs
+++ b/src/unparser.rs
@@ -2,8 +2,12 @@ use crate::{dict::*, term::*};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-impl TypeDict {
- pub fn unparse(&self, t: &TypeTerm) -> String {
+pub trait UnparseLadderType {
+ fn unparse(&self, t: &TypeTerm) -> String;
+}
+
+impl<T: TypeDict> UnparseLadderType for T {
+ fn unparse(&self, t: &TypeTerm) -> String {
match t {
TypeTerm::TypeID(id) => self.get_typename(id).unwrap(),
TypeTerm::Num(n) => format!("{}", n),
From 27a0ca5e56e5ce91a67c9f18cabc02582cdcc1e5 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sun, 6 Oct 2024 14:38:41 +0200
Subject: [PATCH 11/20] add Debug for Bimap & BimapTypeDict
---
src/bimap.rs | 1 +
src/dict.rs | 1 +
2 files changed, 2 insertions(+)
diff --git a/src/bimap.rs b/src/bimap.rs
index 9ea311a..9d0a96c 100644
--- a/src/bimap.rs
+++ b/src/bimap.rs
@@ -2,6 +2,7 @@ use std::{collections::HashMap, hash::Hash};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+#[derive(Debug)]
pub struct Bimap<V: Eq + Hash, Λ: Eq + Hash> {
pub mλ: HashMap<V, Λ>,
pub my: HashMap<Λ, V>,
diff --git a/src/dict.rs b/src/dict.rs
index 4d5b35b..67e22b3 100644
--- a/src/dict.rs
+++ b/src/dict.rs
@@ -28,6 +28,7 @@ pub trait TypeDict {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+#[derive(Debug)]
pub struct BimapTypeDict {
typenames: Bimap<String, TypeID>,
type_lit_counter: u64,
From bc1941d1bcda270acd140d8bfefdfb40fbc96145 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sun, 6 Oct 2024 14:39:05 +0200
Subject: [PATCH 12/20] check if term is empty
---
src/sugar.rs | 20 +++++++++++++++++++-
1 file changed, 19 insertions(+), 1 deletion(-)
diff --git a/src/sugar.rs b/src/sugar.rs
index dea73ba..4734b6f 100644
--- a/src/sugar.rs
+++ b/src/sugar.rs
@@ -2,7 +2,7 @@ use {
crate::{TypeTerm, TypeID, parser::ParseLadderType}
};
-#[derive(Clone)]
+#[derive(Clone, PartialEq)]
pub enum SugaredTypeTerm {
TypeID(TypeID),
Num(i64),
@@ -92,5 +92,23 @@ impl SugaredTypeTerm {
).collect()),
}
}
+
+ pub fn is_empty(&self) -> bool {
+ match self {
+ SugaredTypeTerm::TypeID(_) => false,
+ SugaredTypeTerm::Num(_) => false,
+ SugaredTypeTerm::Char(_) => false,
+ SugaredTypeTerm::Univ(t) => t.is_empty(),
+ SugaredTypeTerm::Spec(ts) |
+ SugaredTypeTerm::Ladder(ts) |
+ SugaredTypeTerm::Func(ts) |
+ SugaredTypeTerm::Morph(ts) |
+ SugaredTypeTerm::Struct(ts) |
+ SugaredTypeTerm::Enum(ts) |
+ SugaredTypeTerm::Seq(ts) => {
+ ts.iter().fold(true, |s,t|s&&t.is_empty())
+ }
+ }
+ }
}
From b869c5f59fc486c66367195ab0eaca1b3faa0d1d Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Mon, 28 Oct 2024 19:58:59 +0100
Subject: [PATCH 13/20] fix find_morphism_path
* also apply substitution from src-type match
* get this substitution as result from `enum_morphisms_with_subtyping`
---
src/morphism.rs | 61 +++++++++++++++++++++------------------------
src/steiner_tree.rs | 6 ++---
2 files changed, 31 insertions(+), 36 deletions(-)
diff --git a/src/morphism.rs b/src/morphism.rs
index 9160610..9ba1ecb 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -106,29 +106,27 @@ impl<M: Morphism + Clone> MorphismBase<M> {
dst_types
}
- pub fn enum_morphisms_with_subtyping(&self, src_type: &TypeTerm)
- -> Vec< (TypeTerm, TypeTerm) >
- {
+ pub fn enum_morphisms_with_subtyping(
+ &self,
+ src_type: &TypeTerm,
+ ) -> Vec<(TypeTerm, TypeTerm, HashMap<TypeID, TypeTerm>)> {
let mut src_lnf = src_type.clone().get_lnf_vec();
let mut halo_lnf = vec![];
let mut dst_types = Vec::new();
while src_lnf.len() > 0 {
- let src_type = TypeTerm::Ladder( src_lnf.clone() );
- let halo_type = TypeTerm::Ladder( halo_lnf.clone() );
+ let src_type = TypeTerm::Ladder(src_lnf.clone());
+ let halo_type = TypeTerm::Ladder(halo_lnf.clone());
- for (σ, t) in self.enum_morphisms( &src_type ) {
- dst_types.push(
- (halo_type.clone()
- .apply_substitution(
- &|x| σ.get(x).cloned()
- ).clone(),
- t.clone()
- .apply_substitution(
- &|x| σ.get(x).cloned()
- ).clone()
- )
- );
+ for (σ, t) in self.enum_morphisms(&src_type) {
+ dst_types.push((
+ halo_type
+ .clone()
+ .apply_substitution(&|x| σ.get(x).cloned())
+ .clone(),
+ t.clone().apply_substitution(&|x| σ.get(x).cloned()).clone(),
+ σ,
+ ));
}
// continue with next supertype
@@ -154,31 +152,30 @@ impl<M: Morphism + Clone> MorphismBase<M> {
if let Some((current_weight, current_path)) = queue.pop() {
let current_type = current_path.last().unwrap();
+ for (h, t, σp) in self.enum_morphisms_with_subtyping(¤t_type) {
+ let tt = TypeTerm::Ladder(vec![h, t]).normalize();
- for (h, t) in self.enum_morphisms_with_subtyping(¤t_type) {
- let tt = TypeTerm::Ladder( vec![ h, t ] ).normalize();
-
- if ! current_path.contains( &tt ) {
+ if !current_path.contains(&tt) {
let unification_result = crate::unification::unify(&tt, &ty.dst_type);
-
let morphism_weight = 1;
- /*
- {
- self.find_morphism( &tt ).unwrap().0.get_weight()
- };
- */
+ /*self.find_morphism( &tt ).unwrap().0.get_weight()*/
let new_weight = current_weight + morphism_weight;
let mut new_path = current_path.clone();
- new_path.push( tt );
+
+ new_path.push(tt);
+
+ for n in new_path.iter_mut() {
+ n.apply_substitution(&|x| σp.get(x).cloned());
+ }
if let Ok(σ) = unification_result {
- new_path = new_path.into_iter().map(
- |mut t: TypeTerm| t.apply_substitution(&|x| σ.get(x).cloned()).clone()
- ).collect::<Vec<TypeTerm>>();
+ for n in new_path.iter_mut() {
+ n.apply_substitution(&|x| σ.get(x).cloned());
+ }
return Some(new_path);
} else {
- queue.push( (new_weight, new_path) );
+ queue.push((new_weight, new_path));
}
}
}
diff --git a/src/steiner_tree.rs b/src/steiner_tree.rs
index f854dd9..d168812 100644
--- a/src/steiner_tree.rs
+++ b/src/steiner_tree.rs
@@ -218,10 +218,8 @@ impl SteinerTreeProblem {
// extend the tree by one edge and add it to the queue
for src_type in current_nodes {
- for (dst_halo,dst_ty) in morphisms.enum_morphisms_with_subtyping( &src_type ) {
- let dst_type = TypeTerm::Ladder(vec![
- dst_halo, dst_ty
- ]).normalize();
+ for (dst_halo, dst_ty, σ) in morphisms.enum_morphisms_with_subtyping(&src_type) {
+ let dst_type = TypeTerm::Ladder(vec![dst_halo, dst_ty]).normalize();
if current_tree.contains( &dst_type ).is_none() {
let mut new_tree = current_tree.clone();
From 32ca6457784d0aeccfb89a051c7a7f782ef2bd91 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Mon, 28 Oct 2024 20:00:11 +0100
Subject: [PATCH 14/20] add Send+Sync trait bound to TypeDict
---
src/dict.rs | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/dict.rs b/src/dict.rs
index 67e22b3..333f8dd 100644
--- a/src/dict.rs
+++ b/src/dict.rs
@@ -8,7 +8,7 @@ pub enum TypeID {
Var(u64)
}
-pub trait TypeDict {
+pub trait TypeDict : Send + Sync {
fn insert(&mut self, name: String, id: TypeID);
fn add_varname(&mut self, vn: String) -> TypeID;
fn add_typename(&mut self, tn: String) -> TypeID;
From 2a8f7e0759ec96843f5037b8ba2ffe07d271904c Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Tue, 24 Dec 2024 12:54:43 +0100
Subject: [PATCH 15/20] steiner tree: eliminate identity loops
---
src/morphism.rs | 4 ++--
src/steiner_tree.rs | 12 ++++++++----
src/term.rs | 5 +----
3 files changed, 11 insertions(+), 10 deletions(-)
diff --git a/src/morphism.rs b/src/morphism.rs
index 9ba1ecb..a433bdc 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -65,7 +65,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
&m.get_type().src_type,
&src_type.clone().normalize()
) {
- let dst_type =
+ let dst_type =
m.get_type().dst_type.clone()
.apply_substitution( &|x| σ.get(x).cloned() )
.clone();
@@ -185,6 +185,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
None
}
+ /// finde a morphism that matches the given morphism type
pub fn find_morphism(&self, ty: &MorphismType)
-> Option< ( M, HashMap<TypeID, TypeTerm> ) > {
@@ -255,4 +256,3 @@ impl<M: Morphism + Clone> MorphismBase<M> {
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
diff --git a/src/steiner_tree.rs b/src/steiner_tree.rs
index d168812..c8984dd 100644
--- a/src/steiner_tree.rs
+++ b/src/steiner_tree.rs
@@ -34,7 +34,7 @@ impl SteinerTree {
let mut new_goals = Vec::new();
let mut added = false;
- for g in self.goals.clone() {
+ for g in self.goals.clone() {
if let Ok(σ) = crate::unify(&ty.dst_type, &g) {
if !added {
self.edges.push(ty.clone());
@@ -107,8 +107,13 @@ impl PathApproxSteinerTreeSolver {
let mut new_path_iter = new_path.into_iter().peekable();
// check all existing nodes..
+
+ if new_path_iter.peek().unwrap() == &src_type {
+ new_path_iter.next();
+ }
+
for mt in tree.iter() {
-// assert!( mt.src_type == &src_type );
+ //assert!( mt.src_type == &src_type );
if let Some(t) = new_path_iter.peek() {
if &mt.dst_type == t {
// eliminate this node from new path
@@ -196,7 +201,7 @@ impl SteinerTreeProblem {
pub fn solve_approx_path<M: Morphism + Clone>(&mut self, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
if let Some(master) = self.src_types.first() {
-
+
}
}
*/
@@ -238,4 +243,3 @@ impl SteinerTreeProblem {
None
}
}
-
diff --git a/src/term.rs b/src/term.rs
index 240996f..c93160b 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -14,8 +14,6 @@ pub enum TypeTerm {
Num(i64),
Char(char),
-
-
/* Complex Terms */
// Type Parameters
@@ -47,10 +45,9 @@ impl TypeTerm {
*self = TypeTerm::App(vec![
self.clone(),
t.into()
- ])
+ ])
}
}
-
self
}
From 804c688f4c8351c672a2d1a386e276d5bc8c16e2 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Tue, 4 Feb 2025 14:26:37 +0100
Subject: [PATCH 16/20] pretty: output escape character for \0 and \n
---
src/pretty.rs | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/pretty.rs b/src/pretty.rs
index 1a4aa60..c5edf3d 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -17,7 +17,11 @@ impl SugaredTypeTerm {
}
SugaredTypeTerm::Char(c) => {
- format!("'{}'", c)
+ match c {
+ '\0' => format!("'\\0'"),
+ '\n' => format!("'\\n'"),
+ _ => format!("'{}'", c)
+ }
}
SugaredTypeTerm::Univ(t) => {
@@ -116,7 +120,7 @@ impl SugaredTypeTerm {
s.push('\n');
for x in 0..(indent*indent_width) {
s.push(' ');
- }
+ }
s.push_str(&"--> ".bright_yellow());
} else {
// s.push_str(" ");
@@ -144,5 +148,3 @@ impl SugaredTypeTerm {
}
}
}
-
-
From 75aaf096eb9775c11f3d6967d995372585e7dda1 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Tue, 4 Feb 2025 14:34:55 +0100
Subject: [PATCH 17/20] fix tests
---
src/steiner_tree.rs | 2 +-
src/test/curry.rs | 8 ++++----
src/test/lnf.rs | 7 +++----
src/test/morphism.rs | 13 ++++++-------
src/test/parser.rs | 33 ++++++++++++++++-----------------
src/test/pnf.rs | 5 ++---
src/test/substitution.rs | 5 ++---
src/test/subtype.rs | 21 ++++++++++-----------
src/test/unification.rs | 11 +++++------
9 files changed, 49 insertions(+), 56 deletions(-)
diff --git a/src/steiner_tree.rs b/src/steiner_tree.rs
index c8984dd..6e2443d 100644
--- a/src/steiner_tree.rs
+++ b/src/steiner_tree.rs
@@ -17,7 +17,7 @@ use {
pub struct SteinerTree {
weight: u64,
goals: Vec< TypeTerm >,
- edges: Vec< MorphismType >,
+ pub edges: Vec< MorphismType >,
}
impl SteinerTree {
diff --git a/src/test/curry.rs b/src/test/curry.rs
index c728a37..a814ab2 100644
--- a/src/test/curry.rs
+++ b/src/test/curry.rs
@@ -1,12 +1,12 @@
use {
- crate::{dict::*}
+ crate::{dict::*, parser::*}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[test]
fn test_curry() {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
assert_eq!(
dict.parse("<A B C>").unwrap().curry(),
@@ -33,7 +33,7 @@ fn test_curry() {
#[test]
fn test_decurry() {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
assert_eq!(
dict.parse("<<A B> C>").unwrap().decurry(),
@@ -47,7 +47,7 @@ fn test_decurry() {
dict.parse("<<<<<<<<<<A B> C> D> E> F> G> H> I> J> K>").unwrap().decurry(),
dict.parse("<A B C D E F G H I J K>").unwrap()
);
-
+
assert_eq!(
dict.parse("<<A~X B> C>").unwrap().decurry(),
dict.parse("<A~X B C>").unwrap()
diff --git a/src/test/lnf.rs b/src/test/lnf.rs
index 1c81a55..4b2a7c2 100644
--- a/src/test/lnf.rs
+++ b/src/test/lnf.rs
@@ -1,8 +1,8 @@
-use crate::dict::TypeDict;
+use crate::{dict::{BimapTypeDict}, parser::*};
#[test]
fn test_flat() {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
assert!( dict.parse("A").expect("parse error").is_flat() );
assert!( dict.parse("10").expect("parse error").is_flat() );
@@ -17,7 +17,7 @@ fn test_flat() {
#[test]
fn test_normalize() {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
assert_eq!(
dict.parse("A~B~C").expect("parse error").normalize(),
@@ -54,4 +54,3 @@ fn test_normalize() {
);
}
-
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index b908101..309d881 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -1,5 +1,5 @@
use {
- crate::{dict::*, morphism::*, steiner_tree::*, TypeTerm}
+ crate::{dict::*, parser::*, unparser::*, morphism::*, steiner_tree::*, TypeTerm}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -27,8 +27,8 @@ impl Morphism for DummyMorphism {
}
}
-fn morphism_test_setup() -> ( TypeDict, MorphismBase<DummyMorphism> ) {
- let mut dict = TypeDict::new();
+fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
+ let mut dict = BimapTypeDict::new();
let mut base = MorphismBase::<DummyMorphism>::new( dict.add_typename("Seq".into()) );
dict.add_varname("Radix".into());
@@ -118,7 +118,7 @@ fn test_morphism_path() {
Some((
DummyMorphism(MorphismType{
src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
- dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+ dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
}),
dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>>").unwrap(),
@@ -145,12 +145,12 @@ fn test_steiner_tree() {
// destination reprs
vec![
dict.parse("ℕ ~ <PosInt 2 BigEndian> ~ <Seq <Digit 2> ~ Char>").unwrap(),
- dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+ dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
]
);
- if let Some(solution) = steiner_tree_problem.solve_bfs( &dict, &base ) {
+ if let Some(solution) = steiner_tree_problem.solve_bfs( &base ) {
for e in solution.edges.iter() {
eprintln!(" :: {}\n--> {}", dict.unparse(&e.src_type), dict.unparse(&e.dst_type));
}
@@ -158,4 +158,3 @@ fn test_steiner_tree() {
eprintln!("no solution");
}
}
-
diff --git a/src/test/parser.rs b/src/test/parser.rs
index 1166229..f650ae3 100644
--- a/src/test/parser.rs
+++ b/src/test/parser.rs
@@ -7,7 +7,7 @@ use {
#[test]
fn test_parser_id() {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
dict.add_varname("T".into());
@@ -26,7 +26,7 @@ fn test_parser_id() {
fn test_parser_num() {
assert_eq!(
Ok(TypeTerm::Num(1234)),
- TypeDict::new().parse("1234")
+ BimapTypeDict::new().parse("1234")
);
}
@@ -34,21 +34,21 @@ fn test_parser_num() {
fn test_parser_char() {
assert_eq!(
Ok(TypeTerm::Char('x')),
- TypeDict::new().parse("'x'")
+ BimapTypeDict::new().parse("'x'")
);
}
#[test]
fn test_parser_app() {
assert_eq!(
- TypeDict::new().parse("<A B>"),
+ BimapTypeDict::new().parse("<A B>"),
Ok(TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)),
TypeTerm::TypeID(TypeID::Fun(1)),
]))
);
assert_eq!(
- TypeDict::new().parse("<A B C>"),
+ BimapTypeDict::new().parse("<A B C>"),
Ok(TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)),
TypeTerm::TypeID(TypeID::Fun(1)),
@@ -60,7 +60,7 @@ fn test_parser_app() {
#[test]
fn test_parser_unexpected_close() {
assert_eq!(
- TypeDict::new().parse(">"),
+ BimapTypeDict::new().parse(">"),
Err(ParseError::UnexpectedClose)
);
}
@@ -68,7 +68,7 @@ fn test_parser_unexpected_close() {
#[test]
fn test_parser_unexpected_token() {
assert_eq!(
- TypeDict::new().parse("A B"),
+ BimapTypeDict::new().parse("A B"),
Err(ParseError::UnexpectedToken)
);
}
@@ -76,14 +76,14 @@ fn test_parser_unexpected_token() {
#[test]
fn test_parser_ladder() {
assert_eq!(
- TypeDict::new().parse("A~B"),
+ BimapTypeDict::new().parse("A~B"),
Ok(TypeTerm::Ladder(vec![
TypeTerm::TypeID(TypeID::Fun(0)),
TypeTerm::TypeID(TypeID::Fun(1)),
]))
);
assert_eq!(
- TypeDict::new().parse("A~B~C"),
+ BimapTypeDict::new().parse("A~B~C"),
Ok(TypeTerm::Ladder(vec![
TypeTerm::TypeID(TypeID::Fun(0)),
TypeTerm::TypeID(TypeID::Fun(1)),
@@ -95,7 +95,7 @@ fn test_parser_ladder() {
#[test]
fn test_parser_ladder_outside() {
assert_eq!(
- TypeDict::new().parse("<A B>~C"),
+ BimapTypeDict::new().parse("<A B>~C"),
Ok(TypeTerm::Ladder(vec![
TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)),
@@ -103,13 +103,13 @@ fn test_parser_ladder_outside() {
]),
TypeTerm::TypeID(TypeID::Fun(2)),
]))
- );
+ );
}
#[test]
fn test_parser_ladder_inside() {
assert_eq!(
- TypeDict::new().parse("<A B~C>"),
+ BimapTypeDict::new().parse("<A B~C>"),
Ok(TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)),
TypeTerm::Ladder(vec![
@@ -117,13 +117,13 @@ fn test_parser_ladder_inside() {
TypeTerm::TypeID(TypeID::Fun(2)),
])
]))
- );
+ );
}
#[test]
fn test_parser_ladder_between() {
assert_eq!(
- TypeDict::new().parse("<A B~<C D>>"),
+ BimapTypeDict::new().parse("<A B~<C D>>"),
Ok(TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)),
TypeTerm::Ladder(vec![
@@ -134,14 +134,14 @@ fn test_parser_ladder_between() {
])
])
]))
- );
+ );
}
#[test]
fn test_parser_ladder_large() {
assert_eq!(
- TypeDict::new().parse(
+ BimapTypeDict::new().parse(
"<Seq Date
~<TimeSince UnixEpoch>
~<Duration Seconds>
@@ -203,4 +203,3 @@ fn test_parser_ladder_large() {
)
);
}
-
diff --git a/src/test/pnf.rs b/src/test/pnf.rs
index e668849..a1d5a33 100644
--- a/src/test/pnf.rs
+++ b/src/test/pnf.rs
@@ -1,8 +1,8 @@
-use crate::dict::TypeDict;
+use crate::{dict::BimapTypeDict, parser::*};
#[test]
fn test_param_normalize() {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
assert_eq!(
dict.parse("A~B~C").expect("parse error"),
@@ -56,4 +56,3 @@ fn test_param_normalize() {
.param_normalize(),
);
}
-
diff --git a/src/test/substitution.rs b/src/test/substitution.rs
index 7959b08..e8906b9 100644
--- a/src/test/substitution.rs
+++ b/src/test/substitution.rs
@@ -1,6 +1,6 @@
use {
- crate::{dict::*, term::*},
+ crate::{dict::*, term::*, parser::*, unparser::*},
std::iter::FromIterator
};
@@ -8,7 +8,7 @@ use {
#[test]
fn test_subst() {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
let mut σ = std::collections::HashMap::new();
@@ -29,4 +29,3 @@ fn test_subst() {
dict.parse("<Seq ℕ~<Seq Char>>").unwrap()
);
}
-
diff --git a/src/test/subtype.rs b/src/test/subtype.rs
index 08cc5c7..c993063 100644
--- a/src/test/subtype.rs
+++ b/src/test/subtype.rs
@@ -1,8 +1,8 @@
-use crate::dict::TypeDict;
+use crate::{dict::BimapTypeDict, parser::*, unparser::*};
#[test]
fn test_semantic_subtype() {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
assert_eq!(
dict.parse("A~B~C").expect("parse error")
@@ -19,11 +19,11 @@ fn test_semantic_subtype() {
),
Some((0, dict.parse("A~B1~C1").expect("parse errror")))
);
-
+
assert_eq!(
dict.parse("A~B~C1").expect("parse error")
.is_semantic_subtype_of(
- &dict.parse("B~C2").expect("parse errror")
+ &dict.parse("B~C2").expect("parse errror")
),
Some((1, dict.parse("B~C1").expect("parse errror")))
);
@@ -31,12 +31,12 @@ fn test_semantic_subtype() {
#[test]
fn test_syntactic_subtype() {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
assert_eq!(
dict.parse("A~B~C").expect("parse error")
.is_syntactic_subtype_of(
- &dict.parse("A~B~C").expect("parse errror")
+ &dict.parse("A~B~C").expect("parse errror")
),
Ok(0)
);
@@ -44,7 +44,7 @@ fn test_syntactic_subtype() {
assert_eq!(
dict.parse("A~B~C").expect("parse error")
.is_syntactic_subtype_of(
- &dict.parse("B~C").expect("parse errror")
+ &dict.parse("B~C").expect("parse errror")
),
Ok(1)
);
@@ -52,7 +52,7 @@ fn test_syntactic_subtype() {
assert_eq!(
dict.parse("A~B~C~D~E").expect("parse error")
.is_syntactic_subtype_of(
- &dict.parse("C~D").expect("parse errror")
+ &dict.parse("C~D").expect("parse errror")
),
Ok(2)
);
@@ -60,7 +60,7 @@ fn test_syntactic_subtype() {
assert_eq!(
dict.parse("A~B~C~D~E").expect("parse error")
.is_syntactic_subtype_of(
- &dict.parse("C~G").expect("parse errror")
+ &dict.parse("C~G").expect("parse errror")
),
Err((2,3))
);
@@ -68,7 +68,7 @@ fn test_syntactic_subtype() {
assert_eq!(
dict.parse("A~B~C~D~E").expect("parse error")
.is_syntactic_subtype_of(
- &dict.parse("G~F~K").expect("parse errror")
+ &dict.parse("G~F~K").expect("parse errror")
),
Err((0,0))
);
@@ -94,4 +94,3 @@ fn test_syntactic_subtype() {
Ok(4)
);
}
-
diff --git a/src/test/unification.rs b/src/test/unification.rs
index 6c55a80..56e88e2 100644
--- a/src/test/unification.rs
+++ b/src/test/unification.rs
@@ -1,13 +1,13 @@
use {
- crate::{dict::*, term::*, unification::*},
+ crate::{dict::*, parser::*, unparser::*, term::*, unification::*},
std::iter::FromIterator
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
dict.add_varname(String::from("T"));
dict.add_varname(String::from("U"));
dict.add_varname(String::from("V"));
@@ -33,7 +33,7 @@ fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
#[test]
fn test_unification_error() {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
dict.add_varname(String::from("T"));
assert_eq!(
@@ -89,7 +89,7 @@ fn test_unification() {
true
);
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
dict.add_varname(String::from("T"));
dict.add_varname(String::from("U"));
@@ -129,10 +129,9 @@ fn test_unification() {
);
}
-
#[test]
fn test_subtype_unification() {
- let mut dict = TypeDict::new();
+ let mut dict = BimapTypeDict::new();
dict.add_varname(String::from("T"));
dict.add_varname(String::from("U"));
From 62a80fcd2fdfc3046493b468242ec77f48924a7b Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Tue, 4 Feb 2025 14:36:05 +0100
Subject: [PATCH 18/20] morphism base: store vec of seq-types
---
src/morphism.rs | 61 +++++++++++++++++++++++++-------------------
src/test/morphism.rs | 8 +++---
2 files changed, 39 insertions(+), 30 deletions(-)
diff --git a/src/morphism.rs b/src/morphism.rs
index a433bdc..ba7cc23 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -16,7 +16,7 @@ pub struct MorphismType {
pub trait Morphism : Sized {
fn get_type(&self) -> MorphismType;
- fn list_map_morphism(&self, list_typeid: TypeID) -> Option< Self >;
+ fn map_morphism(&self, seq_type: TypeTerm) -> Option< Self >;
fn weight(&self) -> u64 {
1
@@ -26,7 +26,7 @@ pub trait Morphism : Sized {
#[derive(Clone)]
pub struct MorphismBase<M: Morphism + Clone> {
morphisms: Vec< M >,
- list_typeid: TypeID
+ seq_types: Vec< TypeTerm >
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -43,10 +43,10 @@ impl MorphismType {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl<M: Morphism + Clone> MorphismBase<M> {
- pub fn new(list_typeid: TypeID) -> Self {
+ pub fn new(seq_types: Vec<TypeTerm>) -> Self {
MorphismBase {
morphisms: Vec::new(),
- list_typeid
+ seq_types
}
}
@@ -80,9 +80,10 @@ impl<M: Morphism + Clone> MorphismBase<M> {
// TODO: function for generating fresh variables
let item_variable = TypeID::Var(100);
+ for seq_type in self.seq_types.iter() {
if let Ok(σ) = crate::unification::unify(
&TypeTerm::App(vec![
- TypeTerm::TypeID(self.list_typeid),
+ seq_type.clone(),
TypeTerm::TypeID(item_variable)
]),
&src_type.clone().param_normalize(),
@@ -92,7 +93,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
for (γ, dst_item_type) in self.enum_morphisms( &src_item_type ) {
let dst_type =
TypeTerm::App(vec![
- TypeTerm::TypeID(self.list_typeid),
+ seq_type.clone(),
dst_item_type.clone()
.apply_substitution(
&|x| γ.get(x).cloned()
@@ -102,6 +103,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
dst_types.push( (γ.clone(), dst_type) );
}
}
+ }
dst_types
}
@@ -189,26 +191,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
pub fn find_morphism(&self, ty: &MorphismType)
-> Option< ( M, HashMap<TypeID, TypeTerm> ) > {
- // try list-map morphism
- if let Ok(σ) = UnificationProblem::new(vec![
- (ty.src_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(self.list_typeid), TypeTerm::TypeID(TypeID::Var(100)) ])),
- (ty.dst_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(self.list_typeid), TypeTerm::TypeID(TypeID::Var(101)) ])),
- ]).solve() {
-
- // TODO: use real fresh variable names
- let item_morph_type = MorphismType {
- src_type: σ.get(&TypeID::Var(100)).unwrap().clone(),
- dst_type: σ.get(&TypeID::Var(101)).unwrap().clone(),
- }.normalize();
-
- if let Some((m, σ)) = self.find_morphism( &item_morph_type ) {
- if let Some(list_morph) = m.list_map_morphism( self.list_typeid ) {
- return Some( (list_morph, σ) );
- }
- }
- }
-
- // otherwise
+ // try to find primitive morphism
for m in self.morphisms.iter() {
let unification_problem = UnificationProblem::new(
vec![
@@ -223,6 +206,32 @@ impl<M: Morphism + Clone> MorphismBase<M> {
}
}
+ // try list-map morphism
+ for seq_type in self.seq_types.iter() {
+ eprintln!("try seq type {:?}", seq_type);
+
+ eprintln!("");
+
+ if let Ok(σ) = UnificationProblem::new(vec![
+ (ty.src_type.clone().param_normalize(),
+ TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(100)) ])),
+ (ty.dst_type.clone().param_normalize(),
+ TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(101)) ])),
+ ]).solve() {
+ // TODO: use real fresh variable names
+ let item_morph_type = MorphismType {
+ src_type: σ.get(&TypeID::Var(100)).unwrap().clone(),
+ dst_type: σ.get(&TypeID::Var(101)).unwrap().clone(),
+ }.normalize();
+
+ if let Some((m, σ)) = self.find_morphism( &item_morph_type ) {
+ if let Some(list_morph) = m.map_morphism( seq_type.clone() ) {
+ return Some( (list_morph, σ) );
+ }
+ }
+ }
+ }
+
None
}
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index 309d881..ae3775f 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -12,15 +12,15 @@ impl Morphism for DummyMorphism {
self.0.clone().normalize()
}
- fn list_map_morphism(&self, list_typeid: TypeID) -> Option<DummyMorphism> {
+ fn map_morphism(&self, seq_type: TypeTerm) -> Option<DummyMorphism> {
Some(DummyMorphism(MorphismType {
src_type: TypeTerm::App(vec![
- TypeTerm::TypeID( list_typeid ),
+ seq_type.clone(),
self.0.src_type.clone()
]),
dst_type: TypeTerm::App(vec![
- TypeTerm::TypeID( list_typeid ),
+ seq_type.clone(),
self.0.dst_type.clone()
])
}))
@@ -29,7 +29,7 @@ impl Morphism for DummyMorphism {
fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
let mut dict = BimapTypeDict::new();
- let mut base = MorphismBase::<DummyMorphism>::new( dict.add_typename("Seq".into()) );
+ let mut base = MorphismBase::<DummyMorphism>::new( vec![ dict.parse("Seq").expect("") ] );
dict.add_varname("Radix".into());
dict.add_varname("SrcRadix".into());
From b0ebf49d03b00d0feef699e84a11a5bd3e72140b Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Fri, 14 Feb 2025 20:55:02 +0100
Subject: [PATCH 19/20] pretty format: use different colors for variables
---
src/pretty.rs | 17 ++++++++++++-----
1 file changed, 12 insertions(+), 5 deletions(-)
diff --git a/src/pretty.rs b/src/pretty.rs
index c5edf3d..40a7541 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -1,5 +1,5 @@
use {
- crate::TypeDict,
+ crate::{TypeDict, dict::TypeID},
crate::sugar::SugaredTypeTerm,
tiny_ansi::TinyAnsi
};
@@ -9,11 +9,18 @@ impl SugaredTypeTerm {
let indent_width = 4;
match self {
SugaredTypeTerm::TypeID(id) => {
- format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).bright_blue()
+ match id {
+ TypeID::Var(varid) => {
+ format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).bright_magenta()
+ },
+ TypeID::Fun(funid) => {
+ format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).blue().bold()
+ }
+ }
},
SugaredTypeTerm::Num(n) => {
- format!("{}", n).bright_cyan()
+ format!("{}", n).green().bold()
}
SugaredTypeTerm::Char(c) => {
@@ -34,7 +41,7 @@ impl SugaredTypeTerm {
SugaredTypeTerm::Spec(args) => {
let mut s = String::new();
- s.push_str(&"<".yellow().bold());
+ s.push_str(&"<".yellow());
for i in 0..args.len() {
let arg = &args[i];
if i > 0 {
@@ -42,7 +49,7 @@ impl SugaredTypeTerm {
}
s.push_str( &arg.pretty(dict,indent+1) );
}
- s.push_str(&">".yellow().bold());
+ s.push_str(&">".yellow());
s
}
From 19e29759d2dd050321a0a0f4e0f5304bccde25fd Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sat, 15 Feb 2025 17:17:43 +0100
Subject: [PATCH 20/20] rewrite enum_morphisms & find_morphism_path
- introduce `MorphismInstantiation` which instantiates a
morphism-template using a type-substitution and a halo type.
- find_morphism_path returns list of `MorphismInstatiation`.
---
src/morphism.rs | 335 ++++++++++++++++++++++++-------------------
src/steiner_tree.rs | 19 ++-
src/test/morphism.rs | 113 +++++++++++++--
3 files changed, 296 insertions(+), 171 deletions(-)
diff --git a/src/morphism.rs b/src/morphism.rs
index ba7cc23..8cf6a02 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -1,9 +1,10 @@
use {
crate::{
- TypeTerm, TypeID,
- unification::UnificationProblem,
+ unification::UnificationProblem, TypeDict, TypeID, TypeTerm,
+ pretty::*,
+ sugar::SugaredTypeTerm,
},
- std::collections::HashMap
+ std::{collections::HashMap, u64}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -14,6 +15,17 @@ pub struct MorphismType {
pub dst_type: TypeTerm,
}
+impl MorphismType {
+ pub fn normalize(self) -> Self {
+ MorphismType {
+ src_type: self.src_type.normalize().param_normalize(),
+ dst_type: self.dst_type.normalize().param_normalize()
+ }
+ }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
pub trait Morphism : Sized {
fn get_type(&self) -> MorphismType;
fn map_morphism(&self, seq_type: TypeTerm) -> Option< Self >;
@@ -23,25 +35,50 @@ pub trait Morphism : Sized {
}
}
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, Debug, PartialEq)]
+pub struct MorphismInstance<M: Morphism + Clone> {
+ pub halo: TypeTerm,
+ pub m: M,
+ pub σ: HashMap<TypeID, TypeTerm>
+}
+
+impl<M: Morphism + Clone> MorphismInstance<M> {
+ pub fn get_type(&self) -> MorphismType {
+ MorphismType {
+ src_type: TypeTerm::Ladder(vec![
+ self.halo.clone(),
+ self.m.get_type().src_type.clone()
+ ]).apply_substitution(&|k| self.σ.get(k).cloned())
+ .clone(),
+
+ dst_type: TypeTerm::Ladder(vec![
+ self.halo.clone(),
+ self.m.get_type().dst_type.clone()
+ ]).apply_substitution(&|k| self.σ.get(k).cloned())
+ .clone()
+ }.normalize()
+ }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct MorphismPath<M: Morphism + Clone> {
+ pub weight: u64,
+ pub cur_type: TypeTerm,
+ pub morphisms: Vec< MorphismInstance<M> >
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
#[derive(Clone)]
pub struct MorphismBase<M: Morphism + Clone> {
morphisms: Vec< M >,
seq_types: Vec< TypeTerm >
}
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-impl MorphismType {
- pub fn normalize(self) -> Self {
- MorphismType {
- src_type: self.src_type.normalize(),
- dst_type: self.dst_type.normalize()
- }
- }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
impl<M: Morphism + Clone> MorphismBase<M> {
pub fn new(seq_types: Vec<TypeTerm>) -> Self {
MorphismBase {
@@ -54,176 +91,196 @@ impl<M: Morphism + Clone> MorphismBase<M> {
self.morphisms.push( m );
}
- pub fn enum_morphisms(&self, src_type: &TypeTerm)
- -> Vec< (HashMap<TypeID, TypeTerm>, TypeTerm) >
+ pub fn enum_direct_morphisms(&self, src_type: &TypeTerm)
+ -> Vec< MorphismInstance<M> >
{
let mut dst_types = Vec::new();
-
- // first enumerate all "direct" morphisms,
for m in self.morphisms.iter() {
- if let Ok(σ) = crate::unification::unify(
- &m.get_type().src_type,
- &src_type.clone().normalize()
+ if let Ok((halo, σ)) = crate::unification::subtype_unify(
+ &src_type.clone().param_normalize(),
+ &m.get_type().src_type.param_normalize(),
) {
- let dst_type =
- m.get_type().dst_type.clone()
- .apply_substitution( &|x| σ.get(x).cloned() )
- .clone();
-
- dst_types.push( (σ, dst_type) );
+ dst_types.push(MorphismInstance{ halo, m: m.clone(), σ });
}
}
+ dst_types
+ }
+
+ pub fn enum_map_morphisms(&self, src_type: &TypeTerm)
+ -> Vec< MorphismInstance<M> > {
+ let src_type = src_type.clone().param_normalize();
+ let mut dst_types = Vec::new();
- // ..then all "list-map" morphisms.
// Check if we have a List type, and if so, see what the Item type is
-
// TODO: function for generating fresh variables
- let item_variable = TypeID::Var(100);
+ let item_variable = TypeID::Var(800);
for seq_type in self.seq_types.iter() {
- if let Ok(σ) = crate::unification::unify(
- &TypeTerm::App(vec![
- seq_type.clone(),
- TypeTerm::TypeID(item_variable)
- ]),
- &src_type.clone().param_normalize(),
- ) {
- let src_item_type = σ.get(&item_variable).unwrap().clone();
+ if let Ok((halo, σ)) = crate::unification::subtype_unify(
+ &src_type,
+ &TypeTerm::App(vec![
+ seq_type.clone(),
+ TypeTerm::TypeID(item_variable)
+ ])
+ ) {
+ let src_item_type = σ.get(&item_variable).expect("var not in unificator").clone();
+ for item_morph_inst in self.enum_morphisms( &src_item_type ) {
- for (γ, dst_item_type) in self.enum_morphisms( &src_item_type ) {
- let dst_type =
- TypeTerm::App(vec![
- seq_type.clone(),
- dst_item_type.clone()
- .apply_substitution(
- &|x| γ.get(x).cloned()
- ).clone()
- ]).normalize();
+ let mut dst_halo_ladder = vec![ halo.clone() ];
+ if item_morph_inst.halo != TypeTerm::unit() {
+ dst_halo_ladder.push(
+ TypeTerm::App(vec![
+ seq_type.clone().get_lnf_vec().first().unwrap().clone(),
+ item_morph_inst.halo.clone()
+ ]));
+ }
- dst_types.push( (γ.clone(), dst_type) );
+ dst_types.push(
+ MorphismInstance {
+ halo: TypeTerm::Ladder(dst_halo_ladder).normalize(),
+ m: item_morph_inst.m.map_morphism(seq_type.clone()).expect("couldnt get map morphism"),
+ σ: item_morph_inst.σ
+ }
+ );
+ }
}
}
- }
dst_types
}
- pub fn enum_morphisms_with_subtyping(
- &self,
- src_type: &TypeTerm,
- ) -> Vec<(TypeTerm, TypeTerm, HashMap<TypeID, TypeTerm>)> {
- let mut src_lnf = src_type.clone().get_lnf_vec();
- let mut halo_lnf = vec![];
+ pub fn enum_morphisms(&self, src_type: &TypeTerm) -> Vec< MorphismInstance<M> > {
let mut dst_types = Vec::new();
-
- while src_lnf.len() > 0 {
- let src_type = TypeTerm::Ladder(src_lnf.clone());
- let halo_type = TypeTerm::Ladder(halo_lnf.clone());
-
- for (σ, t) in self.enum_morphisms(&src_type) {
- dst_types.push((
- halo_type
- .clone()
- .apply_substitution(&|x| σ.get(x).cloned())
- .clone(),
- t.clone().apply_substitution(&|x| σ.get(x).cloned()).clone(),
- σ,
- ));
- }
-
- // continue with next supertype
- halo_lnf.push(src_lnf.remove(0));
- }
-
+ dst_types.append(&mut self.enum_direct_morphisms(src_type));
+ dst_types.append(&mut self.enum_map_morphisms(src_type));
dst_types
}
/* try to find shortest morphism-path for a given type
*/
- pub fn find_morphism_path(&self, ty: MorphismType)
- -> Option< Vec<TypeTerm> >
+ pub fn find_morphism_path(&self, ty: MorphismType
+ /*, type_dict: &mut impl TypeDict*/
+ )
+ -> Option< Vec<MorphismInstance<M>> >
{
let ty = ty.normalize();
-
let mut queue = vec![
- (0, vec![ ty.src_type.clone().normalize() ])
+ MorphismPath { weight: 0, cur_type: ty.src_type.clone(), morphisms: vec![] }
];
while ! queue.is_empty() {
- queue.sort_by( |&(w1,_),&(w2,_)| w2.cmp(&w1));
+ queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
- if let Some((current_weight, current_path)) = queue.pop() {
- let current_type = current_path.last().unwrap();
- for (h, t, σp) in self.enum_morphisms_with_subtyping(¤t_type) {
- let tt = TypeTerm::Ladder(vec![h, t]).normalize();
-
- if !current_path.contains(&tt) {
- let unification_result = crate::unification::unify(&tt, &ty.dst_type);
- let morphism_weight = 1;
- /*self.find_morphism( &tt ).unwrap().0.get_weight()*/
-
- let new_weight = current_weight + morphism_weight;
- let mut new_path = current_path.clone();
-
- new_path.push(tt);
-
- for n in new_path.iter_mut() {
- n.apply_substitution(&|x| σp.get(x).cloned());
+ 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
+ for n in cur_path.morphisms.iter_mut() {
+ let mut new_σ = HashMap::new();
+ for (k,v) in σ.iter() {
+ new_σ.insert(
+ k.clone(),
+ v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone()
+ );
+ }
+ for (k,v) in n.σ.iter() {
+ new_σ.insert(
+ k.clone(),
+ v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone()
+ );
}
- if let Ok(σ) = unification_result {
- for n in new_path.iter_mut() {
- n.apply_substitution(&|x| σ.get(x).cloned());
- }
- return Some(new_path);
- } else {
- queue.push((new_weight, new_path));
+ 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) {
+ let dst_type = next_morph_inst.get_type().dst_type;
+
+ 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()
+ );
+ }
+ 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);
}
}
}
}
-
None
}
- /// finde a morphism that matches the given morphism type
- pub fn find_morphism(&self, ty: &MorphismType)
- -> Option< ( M, HashMap<TypeID, TypeTerm> ) > {
-
- // try to find primitive morphism
+/*
+ pub fn find_direct_morphism(&self, ty: &MorphismType) -> Option< (M, HashMap<TypeID, TypeTerm>) > {
for m in self.morphisms.iter() {
let unification_problem = UnificationProblem::new(
vec![
- ( ty.src_type.clone().normalize(), m.get_type().src_type.clone() ),
- ( ty.dst_type.clone().normalize(), m.get_type().dst_type.clone() )
+ ( ty.src_type.clone(), m.get_type().src_type.clone() ),
+ ( m.get_type().dst_type.clone(), ty.dst_type.clone() )
]
);
- let unification_result = unification_problem.solve();
- if let Ok(σ) = unification_result {
+ let unification_result = unification_problem.solve_subtype();
+ if let Ok((halo, σ)) = unification_result {
return Some((m.clone(), σ));
}
}
+ None
+ }
- // try list-map morphism
+ pub fn find_map_morphism(&self, ty: &MorphismType) -> Option< (M, HashMap<TypeID, TypeTerm>) > {
for seq_type in self.seq_types.iter() {
eprintln!("try seq type {:?}", seq_type);
- eprintln!("");
-
- if let Ok(σ) = UnificationProblem::new(vec![
+ if let Ok((halo, σ)) = UnificationProblem::new(vec![
(ty.src_type.clone().param_normalize(),
TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(100)) ])),
- (ty.dst_type.clone().param_normalize(),
- TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(101)) ])),
- ]).solve() {
+
+ (TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(101)) ]),
+ ty.dst_type.clone().param_normalize()),
+ ]).solve_subtype() {
// TODO: use real fresh variable names
let item_morph_type = MorphismType {
src_type: σ.get(&TypeID::Var(100)).unwrap().clone(),
dst_type: σ.get(&TypeID::Var(101)).unwrap().clone(),
}.normalize();
+ //eprintln!("Map Morph: try to find item-morph with type {:?}", item_morph_type);
if let Some((m, σ)) = self.find_morphism( &item_morph_type ) {
if let Some(list_morph) = m.map_morphism( seq_type.clone() ) {
return Some( (list_morph, σ) );
@@ -235,33 +292,17 @@ impl<M: Morphism + Clone> MorphismBase<M> {
None
}
- pub fn find_morphism_with_subtyping(&self, ty: &MorphismType)
- -> Option<( M, TypeTerm, HashMap<TypeID, TypeTerm> )> {
- let mut src_lnf = ty.src_type.clone().get_lnf_vec();
- let mut dst_lnf = ty.dst_type.clone().get_lnf_vec();
- let mut halo = vec![];
-
- while src_lnf.len() > 0 && dst_lnf.len() > 0 {
- if let Some((m, σ)) = self.find_morphism(&MorphismType{
- src_type: TypeTerm::Ladder(src_lnf.clone()),
- dst_type: TypeTerm::Ladder(dst_lnf.clone())
- }) {
- halo.push(src_lnf.get(0).unwrap().clone());
- return Some((m,
- TypeTerm::Ladder(halo).apply_substitution(&|x| σ.get(x).cloned()).clone(),
- σ));
- } else {
- if src_lnf[0] == dst_lnf[0] {
- src_lnf.remove(0);
- halo.push(dst_lnf.remove(0));
- } else {
- return None;
- }
- }
+ pub fn find_morphism(&self, ty: &MorphismType)
+ -> Option< ( M, HashMap<TypeID, TypeTerm> ) > {
+ if let Some((m,σ)) = self.find_direct_morphism(ty) {
+ return Some((m,σ));
+ }
+ if let Some((m,σ)) = self.find_map_morphism(ty) {
+ return Some((m, σ));
}
-
None
}
+ */
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/steiner_tree.rs b/src/steiner_tree.rs
index 6e2443d..091d764 100644
--- a/src/steiner_tree.rs
+++ b/src/steiner_tree.rs
@@ -108,28 +108,24 @@ impl PathApproxSteinerTreeSolver {
// check all existing nodes..
- if new_path_iter.peek().unwrap() == &src_type {
+ if new_path_iter.peek().unwrap().get_type().src_type == src_type {
new_path_iter.next();
}
for mt in tree.iter() {
//assert!( mt.src_type == &src_type );
if let Some(t) = new_path_iter.peek() {
- if &mt.dst_type == t {
+ if &mt.dst_type == &t.get_type().src_type {
// eliminate this node from new path
- src_type = new_path_iter.next().unwrap().clone();
+ src_type = new_path_iter.next().unwrap().get_type().src_type;
}
} else {
break;
}
}
- for dst_type in new_path_iter {
- tree.push(MorphismType {
- src_type: src_type.clone(),
- dst_type: dst_type.clone()
- });
- src_type = dst_type;
+ for m in new_path_iter {
+ tree.push(m.get_type());
}
} else {
eprintln!("could not find path\nfrom {:?}\nto {:?}", &self.root, &goal);
@@ -223,8 +219,9 @@ impl SteinerTreeProblem {
// extend the tree by one edge and add it to the queue
for src_type in current_nodes {
- for (dst_halo, dst_ty, σ) in morphisms.enum_morphisms_with_subtyping(&src_type) {
- let dst_type = TypeTerm::Ladder(vec![dst_halo, dst_ty]).normalize();
+ for next_morph_inst in morphisms.enum_morphisms(&src_type) {
+ //let dst_type = TypeTerm::Ladder(vec![dst_halo, dst_ty]).normalize();
+ let dst_type = next_morph_inst.get_type().dst_type;
if current_tree.contains( &dst_type ).is_none() {
let mut new_tree = current_tree.clone();
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index ae3775f..4d33df6 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -1,5 +1,5 @@
use {
- crate::{dict::*, parser::*, unparser::*, morphism::*, steiner_tree::*, TypeTerm}
+ crate::{dict::*, parser::*, unparser::*, morphism::*, TypeTerm}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -73,23 +73,105 @@ fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
fn test_morphism_path() {
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 16 BigEndian> ~ <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!(
- base.find_morphism_path(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()
- }),
+ path,
Some(
vec![
- dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().normalize(),
- dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
- dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
- dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
- dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
- dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().normalize(),
+ 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 {
+ 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)),
+ (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 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)),
+ (dict.get_typeid(&"Radix".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)),
+ (dict.get_typeid(&"DstRadix".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 Radix 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()
+ })
+ }
]
)
);
-
+/*
assert_eq!(
base.find_morphism_path(MorphismType {
src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
@@ -106,7 +188,10 @@ fn test_morphism_path() {
]
)
);
+ */
+
+/*
assert_eq!(
base.find_morphism_with_subtyping(
&MorphismType {
@@ -129,8 +214,9 @@ fn test_morphism_path() {
].into_iter().collect::<std::collections::HashMap<TypeID, TypeTerm>>()
))
);
+ */
}
-
+/*
#[test]
fn test_steiner_tree() {
let (mut dict, mut base) = morphism_test_setup();
@@ -158,3 +244,4 @@ fn test_steiner_tree() {
eprintln!("no solution");
}
}
+*/