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 { + pub halo: TypeTerm, + pub m: M, + pub σ: HashMap +} + +impl MorphismInstance { + 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 { + pub weight: u64, + pub cur_type: TypeTerm, + pub morphisms: Vec< MorphismInstance > +} + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ + #[derive(Clone)] pub struct MorphismBase { 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 MorphismBase { pub fn new(seq_types: Vec) -> Self { MorphismBase { @@ -54,176 +91,196 @@ impl MorphismBase { self.morphisms.push( m ); } - pub fn enum_morphisms(&self, src_type: &TypeTerm) - -> Vec< (HashMap, TypeTerm) > + pub fn enum_direct_morphisms(&self, src_type: &TypeTerm) + -> Vec< MorphismInstance > { 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 > { + 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)> { - 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 > { 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 > + pub fn find_morphism_path(&self, ty: MorphismType + /*, type_dict: &mut impl TypeDict*/ + ) + -> Option< Vec> > { 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 ) > { - - // try to find primitive morphism +/* + pub fn find_direct_morphism(&self, ty: &MorphismType) -> Option< (M, HashMap) > { 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) > { 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 MorphismBase { None } - pub fn find_morphism_with_subtyping(&self, ty: &MorphismType) - -> Option<( M, TypeTerm, HashMap )> { - 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 ) > { + 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 ) { fn test_morphism_path() { let (mut dict, mut base) = morphism_test_setup(); + let path = base.find_morphism_path(MorphismType { + src_type: dict.parse("ℕ ~ ~ ~ Char>").unwrap(), + dst_type: dict.parse("ℕ ~ ~ ~ Char>").unwrap(), + }); + + fn print_subst(m: &std::collections::HashMap, 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("ℕ ~ ~ ~ Char>").unwrap(), - dst_type: dict.parse("ℕ ~ ~ ~ Char>").unwrap() - }), + path, Some( vec![ - dict.parse("ℕ ~ ~ ~ Char>").unwrap().normalize(), - dict.parse("ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), - dict.parse("ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), - dict.parse("ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), - dict.parse("ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), - dict.parse("ℕ ~ ~ ~ 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("ℕ ~ ").unwrap(), + m: DummyMorphism(MorphismType { + src_type: dict.parse(" ~ Char>").unwrap(), + dst_type: dict.parse(" ~ ℤ_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("ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap(), + dst_type: dict.parse("ℕ ~ ~ ~ ℤ_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("ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap(), + dst_type: dict.parse("ℕ ~ ~ ~ ℤ_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("ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap(), + dst_type: dict.parse("ℕ ~ ~ ~ ℤ_2^64 ~ machine.UInt64>").unwrap(), + }), + }, + MorphismInstance { + σ: vec![ + (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)) + ].into_iter().collect(), + halo: dict.parse("ℕ ~ ").unwrap(), + m: DummyMorphism(MorphismType{ + src_type: dict.parse(" ~ ℤ_2^64 ~ machine.UInt64>").unwrap(), + dst_type: dict.parse(" ~ Char>").unwrap() + }) + } ] ) ); - +/* assert_eq!( base.find_morphism_path(MorphismType { src_type: dict.parse("Symbol ~ ℕ ~ ~ ~ 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::>() )) ); + */ } - +/* #[test] fn test_steiner_tree() { let (mut dict, mut base) = morphism_test_setup(); @@ -158,3 +244,4 @@ fn test_steiner_tree() { eprintln!("no solution"); } } +*/