diff --git a/src/lib.rs b/src/lib.rs
index 11a001f..a06c3d1 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -27,3 +27,70 @@ pub use {
unification::*,
morphism::*
};
+
+
+pub fn common_halo(
+ a: &TypeTerm,
+ b: &TypeTerm
+) -> Option< TypeTerm > {
+ match (a,b) {
+ (TypeTerm::Ladder(rs1), TypeTerm::Ladder(rs2)) => {
+ let mut halo_rungs = Vec::new();
+
+ for (r1, r2) in rs1.iter().zip(rs2.iter()) {
+ if let Some(h) = common_halo(r1, r2) {
+ halo_rungs.push(h);
+ } else {
+ return Some(TypeTerm::Ladder(halo_rungs).normalize());
+ }
+ }
+
+ if halo_rungs.len() == 0 {
+ None
+ } else {
+ Some(TypeTerm::Ladder(halo_rungs).normalize())
+ }
+ }
+
+ (TypeTerm::App(a1), TypeTerm::App(a2)) => {
+ let mut halo_args = Vec::new();
+
+ for (r1, r2) in a1.iter().zip(a2.iter()) {
+ if let Some(h) = common_halo(r1, r2) {
+ halo_args.push(h);
+ } else {
+ return Some(TypeTerm::Ladder(halo_args).normalize());
+ }
+ }
+
+ if halo_args.len() == 0 {
+ None
+ } else {
+ Some(TypeTerm::App(halo_args).normalize())
+ }
+ }
+
+ (TypeTerm::Ladder(rsl), r) => {
+ if rsl.first().unwrap() == r {
+ Some(r.clone())
+ } else {
+ None
+ }
+ }
+ (l, TypeTerm::Ladder(rsr)) => {
+ if rsr.first().unwrap() == l {
+ Some(l.clone())
+ } else {
+ None
+ }
+ }
+
+ (a1, a2) => {
+ if a1 == a2 {
+ Some(a1.clone())
+ } else {
+ None
+ }
+ }
+ }
+}
diff --git a/src/morphism.rs b/src/morphism.rs
index 8cf6a02..4a7d87e 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -1,8 +1,6 @@
use {
crate::{
- unification::UnificationProblem, TypeDict, TypeID, TypeTerm,
- pretty::*,
- sugar::SugaredTypeTerm,
+ subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm
},
std::{collections::HashMap, u64}
};
@@ -135,13 +133,17 @@ impl<M: Morphism + Clone> MorphismBase<M> {
]));
}
- 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.σ
- }
- );
+ if let Some( map_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
+ dst_types.push(
+ MorphismInstance {
+ halo: TypeTerm::Ladder(dst_halo_ladder).normalize(),
+ m: map_morph,
+ σ: item_morph_inst.σ
+ }
+ );
+ } else {
+ eprintln!("could not get map morphism");
+ }
}
}
}
@@ -245,28 +247,54 @@ impl<M: Morphism + Clone> MorphismBase<M> {
None
}
-/*
- 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(), m.get_type().src_type.clone() ),
- ( m.get_type().dst_type.clone(), ty.dst_type.clone() )
- ]
- );
- let unification_result = unification_problem.solve_subtype();
- if let Ok((halo, σ)) = unification_result {
- return Some((m.clone(), σ));
+ pub fn find_direct_morphism(&self,
+ ty: &MorphismType,
+ dict: &mut impl TypeDict
+ ) -> Option< MorphismInstance<M> > {
+ eprintln!("find direct morph");
+ for m in self.morphisms.iter() {
+ let ty = ty.clone().normalize();
+ let morph_type = m.get_type().normalize();
+
+ eprintln!("find direct morph:\n {} <= {}",
+ dict.unparse(&ty.src_type), dict.unparse(&morph_type.src_type),
+ );
+
+ if let Ok((halo, σ)) = subtype_unify(&ty.src_type, &morph_type.src_type) {
+ eprintln!("halo: {}", dict.unparse(&halo));
+
+ let dst_type = TypeTerm::Ladder(vec![
+ halo.clone(),
+ morph_type.dst_type.clone()
+ ]);
+ eprintln!("-----------> {} <= {}",
+ dict.unparse(&dst_type), dict.unparse(&ty.dst_type)
+ );
+
+ /*
+ let unification_problem = UnificationProblem::new(
+ vec![
+ ( ty.src_type, morph_type.src_type ),
+ ( morph_type.dst_type, ty.dst_type )
+ ]
+ );*/
+
+ if let Ok((halo2, σ2)) = subtype_unify(&dst_type, &ty.dst_type) {
+ eprintln!("match. halo2 = {}", dict.unparse(&halo2));
+ return Some(MorphismInstance {
+ m: m.clone(),
+ halo: halo2,
+ σ,
+ });
+ }
}
}
None
}
- pub fn find_map_morphism(&self, ty: &MorphismType) -> Option< (M, HashMap<TypeID, TypeTerm>) > {
+ pub fn find_map_morphism(&self, ty: &MorphismType, dict: &mut impl TypeDict) -> Option< MorphismInstance<M> > {
for seq_type in self.seq_types.iter() {
- eprintln!("try seq type {:?}", seq_type);
-
if let Ok((halo, σ)) = UnificationProblem::new(vec![
(ty.src_type.clone().param_normalize(),
TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(100)) ])),
@@ -281,9 +309,13 @@ impl<M: Morphism + Clone> MorphismBase<M> {
}.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, σ) );
+ if let Some(item_morph_inst) = self.find_morphism( &item_morph_type, dict ) {
+ if let Some( list_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
+ return Some( MorphismInstance {
+ m: list_morph,
+ σ,
+ halo
+ } );
}
}
}
@@ -292,17 +324,18 @@ impl<M: Morphism + Clone> MorphismBase<M> {
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,σ));
+ pub fn find_morphism(&self, ty: &MorphismType,
+ dict: &mut impl TypeDict
+ )
+ -> Option< MorphismInstance<M> > {
+ if let Some(m) = self.find_direct_morphism(ty, dict) {
+ return Some(m);
}
- if let Some((m,σ)) = self.find_map_morphism(ty) {
- return Some((m, σ));
+ if let Some(m) = self.find_map_morphism(ty, dict) {
+ return Some(m);
}
None
}
- */
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/steiner_tree.rs b/src/steiner_tree.rs
index 091d764..f3fa931 100644
--- a/src/steiner_tree.rs
+++ b/src/steiner_tree.rs
@@ -1,14 +1,9 @@
use {
- std::collections::HashMap,
crate::{
- TypeID,
- TypeTerm,
morphism::{
- MorphismType,
- Morphism,
- MorphismBase
- }
- }
+ Morphism, MorphismBase, MorphismType
+ }, MorphismInstance, TypeID, TypeTerm
+ }, std::collections::HashMap
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -91,10 +86,11 @@ impl PathApproxSteinerTreeSolver {
}
}
- pub fn solve<M: Morphism + Clone>(self, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
- let mut tree = Vec::<MorphismType>::new();
+ pub fn solve<M: Morphism + Clone + PartialEq>(self, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
+ let mut edges = Vec::<MorphismType>::new();
for goal in self.leaves {
+ eprintln!("solve steiner tree: find path to goal {:?}", goal);
// try to find shortest path from root to current leaf
if let Some(new_path) = morphisms.find_morphism_path(
MorphismType {
@@ -102,6 +98,15 @@ impl PathApproxSteinerTreeSolver {
dst_type: goal.clone()
}
) {
+ eprintln!("path to {:?} has len {}", goal.clone(), new_path.len());
+ for morph_inst in new_path {
+ let t = morph_inst.get_type();
+ if ! edges.contains(&t) {
+ eprintln!("add edge {:?}", t);
+ edges.push(t);
+ }
+ }
+/*
// 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();
@@ -109,12 +114,14 @@ impl PathApproxSteinerTreeSolver {
// check all existing nodes..
if new_path_iter.peek().unwrap().get_type().src_type == src_type {
+ eprintln!("skip initial node..");
new_path_iter.next();
}
for mt in tree.iter() {
//assert!( mt.src_type == &src_type );
if let Some(t) = new_path_iter.peek() {
+ eprintln!("");
if &mt.dst_type == &t.get_type().src_type {
// eliminate this node from new path
src_type = new_path_iter.next().unwrap().get_type().src_type;
@@ -127,6 +134,7 @@ impl PathApproxSteinerTreeSolver {
for m in new_path_iter {
tree.push(m.get_type());
}
+*/
} else {
eprintln!("could not find path\nfrom {:?}\nto {:?}", &self.root, &goal);
return None;
@@ -136,7 +144,7 @@ impl PathApproxSteinerTreeSolver {
Some(SteinerTree {
weight: 0,
goals: vec![],
- edges: tree
+ edges
})
}
}
diff --git a/src/test/halo.rs b/src/test/halo.rs
new file mode 100644
index 0000000..780b7fd
--- /dev/null
+++ b/src/test/halo.rs
@@ -0,0 +1,39 @@
+use crate::{dict::BimapTypeDict, parser::*, unparser::*};
+
+#[test]
+fn test_common_halo() {
+ let mut dict = BimapTypeDict::new();
+
+ assert_eq!(
+ crate::common_halo(
+ &dict.parse("A~B~C").expect("parse error"),
+ &dict.parse("A~B~C").expect("parse error")
+ ),
+ Some(dict.parse("A~B~C").expect("parse error"))
+ );
+
+ assert_eq!(
+ crate::common_halo(
+ &dict.parse("A~B~X").expect("parse error"),
+ &dict.parse("A~B~Y").expect("parse error")
+ ),
+ Some(dict.parse("A~B").expect("parse error"))
+ );
+
+ assert_eq!(
+ crate::common_halo(
+ &dict.parse("A~<B C~D>").expect("parse error"),
+ &dict.parse("A~<B C~E>").expect("parse error")
+ ),
+ Some(dict.parse("A~<B C>").expect("parse error"))
+ );
+
+
+ assert_eq!(
+ crate::common_halo(
+ &dict.parse("A").expect("parse error"),
+ &dict.parse("A~<B C~E>").expect("parse error")
+ ),
+ Some(dict.parse("A").expect("parse error"))
+ );
+}
diff --git a/src/test/mod.rs b/src/test/mod.rs
index 41f5e71..1cd4673 100644
--- a/src/test/mod.rs
+++ b/src/test/mod.rs
@@ -8,4 +8,4 @@ pub mod subtype;
pub mod substitution;
pub mod unification;
pub mod morphism;
-
+pub mod halo;
diff --git a/src/test/unification.rs b/src/test/unification.rs
index 56e88e2..7811647 100644
--- a/src/test/unification.rs
+++ b/src/test/unification.rs
@@ -173,12 +173,12 @@ fn test_subtype_unification() {
UnificationProblem::new(vec![
(dict.parse("<Seq T>").unwrap(),
dict.parse("<Seq W~<Seq Char>>").unwrap()),
- (dict.parse("<Seq ℕ~<PosInt 10 BigEndian>>").unwrap(),
- dict.parse("<Seq~<LengthPrefix x86.UInt64> W>").unwrap()),
+ (dict.parse("<Seq~<LengthPrefix x86.UInt64> ℕ~<PosInt 10 BigEndian>>").unwrap(),
+ dict.parse("<<LengthPrefix x86.UInt64> W>").unwrap()),
]).solve_subtype(),
Ok((
dict.parse("
- <Seq~<LengthPrefix x86.UInt64> ℕ~<PosInt 10 BigEndian>>
+ <Seq ℕ~<PosInt 10 BigEndian>>
").unwrap(),
vec![
// W
diff --git a/src/unification.rs b/src/unification.rs
index e605af4..850d76c 100644
--- a/src/unification.rs
+++ b/src/unification.rs
@@ -92,16 +92,19 @@ impl UnificationProblem {
},
(t, TypeTerm::Ladder(mut a1)) => {
- if let Ok(mut halo) = self.eval_subtype( t.clone(), a1.first().unwrap().clone(), addr.clone() ) {
+ /*
+ 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: t, t2: TypeTerm::Ladder(a1) })
- }
+ //}
}
(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 {