Compare commits
17 commits
97e5475f70
...
6f4316e074
Author | SHA1 | Date | |
---|---|---|---|
6f4316e074 | |||
a46e225e06 | |||
6ea50ab8d0 | |||
8cf49cb5f1 | |||
d9bda81733 | |||
751f76de46 | |||
0365cd1d34 | |||
36d8cb63e4 | |||
335a307836 | |||
1e1cdd289f | |||
85c46ae91e | |||
484294f5bd | |||
deb097acd3 | |||
aa67520184 | |||
c4a26d11da | |||
9db57488dd | |||
e15db9d1f3 |
8 changed files with 936 additions and 4 deletions
|
@ -24,6 +24,14 @@ pub trait TypeDict : Send + Sync {
|
|||
self.insert(new, tyid);
|
||||
}
|
||||
}
|
||||
|
||||
fn get_typeid_creat(&mut self, tn: &String) -> TypeID {
|
||||
if let Some(id) = self.get_typeid(tn) {
|
||||
id
|
||||
} else {
|
||||
self.add_typename(tn.clone())
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
|
|
@ -11,6 +11,8 @@ pub mod lnf;
|
|||
pub mod pnf;
|
||||
pub mod subtype;
|
||||
pub mod unification;
|
||||
pub mod morphism;
|
||||
pub mod steiner_tree;
|
||||
|
||||
#[cfg(test)]
|
||||
mod test;
|
||||
|
@ -23,4 +25,5 @@ pub use {
|
|||
term::*,
|
||||
sugar::*,
|
||||
unification::*,
|
||||
morphism::*
|
||||
};
|
||||
|
|
346
src/morphism.rs
Normal file
346
src/morphism.rs
Normal file
|
@ -0,0 +1,346 @@
|
|||
use {
|
||||
crate::{
|
||||
subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm
|
||||
},
|
||||
std::{collections::HashMap, u64}
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Debug)]
|
||||
pub struct MorphismType {
|
||||
pub src_type: TypeTerm,
|
||||
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 >;
|
||||
|
||||
fn weight(&self) -> u64 {
|
||||
1
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
#[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<M: Morphism + Clone> MorphismBase<M> {
|
||||
pub fn new(seq_types: Vec<TypeTerm>) -> Self {
|
||||
MorphismBase {
|
||||
morphisms: Vec::new(),
|
||||
seq_types
|
||||
}
|
||||
}
|
||||
|
||||
pub fn add_morphism(&mut self, m: M) {
|
||||
self.morphisms.push( m );
|
||||
}
|
||||
|
||||
pub fn enum_direct_morphisms(&self, src_type: &TypeTerm)
|
||||
-> Vec< MorphismInstance<M> >
|
||||
{
|
||||
let mut dst_types = Vec::new();
|
||||
for m in self.morphisms.iter() {
|
||||
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
|
||||
}
|
||||
|
||||
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();
|
||||
|
||||
// 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(800);
|
||||
|
||||
for seq_type in self.seq_types.iter() {
|
||||
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 ) {
|
||||
|
||||
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()
|
||||
]));
|
||||
}
|
||||
|
||||
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");
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
dst_types
|
||||
}
|
||||
|
||||
pub fn enum_morphisms(&self, src_type: &TypeTerm) -> Vec< MorphismInstance<M> > {
|
||||
let mut dst_types = Vec::new();
|
||||
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
|
||||
/*, type_dict: &mut impl TypeDict*/
|
||||
)
|
||||
-> Option< Vec<MorphismInstance<M>> >
|
||||
{
|
||||
let ty = ty.normalize();
|
||||
let mut queue = vec![
|
||||
MorphismPath { weight: 0, cur_type: ty.src_type.clone(), morphisms: vec![] }
|
||||
];
|
||||
|
||||
while ! queue.is_empty() {
|
||||
queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
|
||||
|
||||
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()
|
||||
);
|
||||
}
|
||||
|
||||
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
|
||||
}
|
||||
|
||||
|
||||
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, dict: &mut impl TypeDict) -> Option< MorphismInstance<M> > {
|
||||
for seq_type in self.seq_types.iter() {
|
||||
if let Ok((halo, σ)) = UnificationProblem::new(vec![
|
||||
(ty.src_type.clone().param_normalize(),
|
||||
TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(100)) ])),
|
||||
|
||||
(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(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
|
||||
} );
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
None
|
||||
}
|
||||
|
||||
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, dict) {
|
||||
return Some(m);
|
||||
}
|
||||
None
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
255
src/steiner_tree.rs
Normal file
255
src/steiner_tree.rs
Normal file
|
@ -0,0 +1,255 @@
|
|||
use {
|
||||
crate::{
|
||||
morphism::{
|
||||
Morphism, MorphismBase, MorphismType
|
||||
}, MorphismInstance, TypeID, TypeTerm
|
||||
}, std::collections::HashMap
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
#[derive(Clone)]
|
||||
pub struct SteinerTree {
|
||||
weight: u64,
|
||||
goals: Vec< TypeTerm >,
|
||||
pub edges: Vec< MorphismType >,
|
||||
}
|
||||
|
||||
impl SteinerTree {
|
||||
pub fn into_edges(self) -> Vec< MorphismType > {
|
||||
self.edges
|
||||
}
|
||||
|
||||
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
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
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 + 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 {
|
||||
src_type: self.root.clone(),
|
||||
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();
|
||||
|
||||
// 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().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
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/* 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_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, 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 {
|
||||
for (dst_halo,dst_ty) in morphisms.enum_morphisms_with_subtypig( &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();
|
||||
{
|
||||
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 );
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
None
|
||||
}
|
||||
}
|
18
src/sugar.rs
18
src/sugar.rs
|
@ -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())
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
63
src/term.rs
63
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
|
||||
}
|
||||
|
||||
|
@ -124,6 +121,64 @@ impl TypeTerm {
|
|||
|
||||
self
|
||||
}
|
||||
|
||||
/* strip away empty ladders
|
||||
* & unwrap singletons
|
||||
*/
|
||||
pub fn strip(self) -> Self {
|
||||
match self {
|
||||
TypeTerm::Ladder(rungs) => {
|
||||
let mut rungs :Vec<_> = rungs.into_iter()
|
||||
.filter_map(|mut r| {
|
||||
r = r.strip();
|
||||
if r != TypeTerm::unit() {
|
||||
Some(match r {
|
||||
TypeTerm::Ladder(r) => r,
|
||||
a => vec![ a ]
|
||||
})
|
||||
}
|
||||
else { None }
|
||||
})
|
||||
.flatten()
|
||||
.collect();
|
||||
|
||||
if rungs.len() == 1 {
|
||||
rungs.pop().unwrap()
|
||||
} else {
|
||||
TypeTerm::Ladder(rungs)
|
||||
}
|
||||
},
|
||||
TypeTerm::App(args) => {
|
||||
let mut args :Vec<_> = args.into_iter().map(|arg| arg.strip()).collect();
|
||||
if args.len() == 0 {
|
||||
TypeTerm::unit()
|
||||
} else if args.len() == 1 {
|
||||
args.pop().unwrap()
|
||||
} else {
|
||||
TypeTerm::App(args)
|
||||
}
|
||||
}
|
||||
atom => atom
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
pub fn get_interface_type(&self) -> TypeTerm {
|
||||
match self {
|
||||
TypeTerm::Ladder(rungs) => {
|
||||
if let Some(top) = rungs.first() {
|
||||
top.get_interface_type()
|
||||
} else {
|
||||
TypeTerm::unit()
|
||||
}
|
||||
}
|
||||
TypeTerm::App(args) => {
|
||||
TypeTerm::App(args.iter().map(|a| a.get_interface_type()).collect())
|
||||
}
|
||||
atom => atom.clone()
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
|
|
@ -7,4 +7,5 @@ pub mod pnf;
|
|||
pub mod subtype;
|
||||
pub mod substitution;
|
||||
pub mod unification;
|
||||
pub mod morphism;
|
||||
|
||||
|
|
246
src/test/morphism.rs
Normal file
246
src/test/morphism.rs
Normal file
|
@ -0,0 +1,246 @@
|
|||
use {
|
||||
crate::{dict::*, morphism::*, parser::*, unparser::*, steiner_tree::*, TypeTerm}
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
#[derive(Clone, Debug, PartialEq)]
|
||||
struct DummyMorphism(MorphismType);
|
||||
|
||||
impl Morphism for DummyMorphism {
|
||||
fn get_type(&self) -> MorphismType {
|
||||
self.0.clone().normalize()
|
||||
}
|
||||
|
||||
fn map_morphism(&self, seq_type: TypeTerm) -> Option<DummyMorphism> {
|
||||
Some(DummyMorphism(MorphismType {
|
||||
src_type: TypeTerm::App(vec![
|
||||
seq_type.clone(),
|
||||
self.0.src_type.clone()
|
||||
]),
|
||||
|
||||
dst_type: TypeTerm::App(vec![
|
||||
seq_type.clone(),
|
||||
self.0.dst_type.clone()
|
||||
])
|
||||
}))
|
||||
}
|
||||
}
|
||||
|
||||
fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
|
||||
let mut dict = BimapTypeDict::new();
|
||||
let mut base = MorphismBase::<DummyMorphism>::new( vec![ dict.parse("Seq").expect("") ] );
|
||||
|
||||
dict.add_varname("Radix".into());
|
||||
dict.add_varname("SrcRadix".into());
|
||||
dict.add_varname("DstRadix".into());
|
||||
|
||||
base.add_morphism(
|
||||
DummyMorphism(MorphismType{
|
||||
src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
|
||||
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
|
||||
})
|
||||
);
|
||||
base.add_morphism(
|
||||
DummyMorphism(MorphismType{
|
||||
src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
|
||||
dst_type: dict.parse("<Digit Radix> ~ Char").unwrap()
|
||||
})
|
||||
);
|
||||
base.add_morphism(
|
||||
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()
|
||||
})
|
||||
);
|
||||
base.add_morphism(
|
||||
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()
|
||||
})
|
||||
);
|
||||
base.add_morphism(
|
||||
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()
|
||||
})
|
||||
);
|
||||
|
||||
(dict, base)
|
||||
}
|
||||
|
||||
#[test]
|
||||
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!(
|
||||
path,
|
||||
Some(
|
||||
vec![
|
||||
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(),
|
||||
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>>()
|
||||
))
|
||||
);
|
||||
*/
|
||||
}
|
||||
|
||||
#[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( &base ) {
|
||||
for e in solution.edges.iter() {
|
||||
eprintln!(" :: {}\n--> {}", dict.unparse(&e.src_type), dict.unparse(&e.dst_type));
|
||||
}
|
||||
} else {
|
||||
eprintln!("no solution");
|
||||
}
|
||||
}
|
Loading…
Add table
Add a link
Reference in a new issue