Compare commits
7 commits
dev
...
topic-morp
Author | SHA1 | Date | |
---|---|---|---|
5d7668573a | |||
493b8a864c | |||
e0334f4d5c | |||
811adde1b9 | |||
42286bcadc | |||
b835cddcf1 | |||
486760f3e2 |
6 changed files with 590 additions and 2 deletions
|
@ -2,7 +2,7 @@ use crate::bimap::Bimap;
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||||
|
|
||||||
#[derive(Eq, PartialEq, Hash, Clone, Debug)]
|
#[derive(Eq, PartialEq, Hash, Clone, Copy, Debug)]
|
||||||
pub enum TypeID {
|
pub enum TypeID {
|
||||||
Fun(u64),
|
Fun(u64),
|
||||||
Var(u64)
|
Var(u64)
|
||||||
|
|
|
@ -10,6 +10,8 @@ pub mod lnf;
|
||||||
pub mod pnf;
|
pub mod pnf;
|
||||||
pub mod subtype;
|
pub mod subtype;
|
||||||
pub mod unification;
|
pub mod unification;
|
||||||
|
pub mod morphism;
|
||||||
|
pub mod steiner_tree;
|
||||||
|
|
||||||
#[cfg(test)]
|
#[cfg(test)]
|
||||||
mod test;
|
mod test;
|
||||||
|
@ -17,6 +19,7 @@ mod test;
|
||||||
pub use {
|
pub use {
|
||||||
dict::*,
|
dict::*,
|
||||||
term::*,
|
term::*,
|
||||||
unification::*
|
unification::*,
|
||||||
|
morphism::*
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
261
src/morphism.rs
Normal file
261
src/morphism.rs
Normal file
|
@ -0,0 +1,261 @@
|
||||||
|
use {
|
||||||
|
crate::{
|
||||||
|
TypeTerm, TypeID,
|
||||||
|
unification::UnificationProblem,
|
||||||
|
},
|
||||||
|
std::collections::HashMap
|
||||||
|
};
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||||
|
|
||||||
|
#[derive(Clone, PartialEq, Eq, Debug)]
|
||||||
|
pub struct MorphismType {
|
||||||
|
pub src_type: TypeTerm,
|
||||||
|
pub dst_type: TypeTerm,
|
||||||
|
}
|
||||||
|
|
||||||
|
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)]
|
||||||
|
pub struct MorphismBase<M: Morphism + Clone> {
|
||||||
|
morphisms: Vec< M >,
|
||||||
|
list_typeid: TypeID
|
||||||
|
}
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||||
|
|
||||||
|
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(list_typeid: TypeID) -> Self {
|
||||||
|
MorphismBase {
|
||||||
|
morphisms: Vec::new(),
|
||||||
|
list_typeid
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn add_morphism(&mut self, m: M) {
|
||||||
|
self.morphisms.push( m );
|
||||||
|
}
|
||||||
|
|
||||||
|
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 m in self.morphisms.iter() {
|
||||||
|
if let Ok(σ) = crate::unification::unify(
|
||||||
|
&m.get_type().src_type,
|
||||||
|
&src_type.clone().normalize()
|
||||||
|
) {
|
||||||
|
let dst_type =
|
||||||
|
m.get_type().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
|
||||||
|
}
|
||||||
|
|
||||||
|
/* 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 queue = vec![
|
||||||
|
(0, vec![ ty.src_type.clone().normalize() ])
|
||||||
|
];
|
||||||
|
|
||||||
|
while ! queue.is_empty() {
|
||||||
|
queue.sort_by( |&(w1,_),&(w2,_)| w2.cmp(&w1));
|
||||||
|
|
||||||
|
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 ! 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 );
|
||||||
|
|
||||||
|
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_weight, new_path) );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
None
|
||||||
|
}
|
||||||
|
|
||||||
|
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
|
||||||
|
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<( 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;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
None
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||||
|
|
162
src/steiner_tree.rs
Normal file
162
src/steiner_tree.rs
Normal file
|
@ -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
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
|
@ -7,4 +7,5 @@ pub mod pnf;
|
||||||
pub mod subtype;
|
pub mod subtype;
|
||||||
pub mod substitution;
|
pub mod substitution;
|
||||||
pub mod unification;
|
pub mod unification;
|
||||||
|
pub mod morphism;
|
||||||
|
|
||||||
|
|
161
src/test/morphism.rs
Normal file
161
src/test/morphism.rs
Normal file
|
@ -0,0 +1,161 @@
|
||||||
|
use {
|
||||||
|
crate::{dict::*, morphism::*, steiner_tree::*, TypeTerm}
|
||||||
|
};
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||||
|
|
||||||
|
#[derive(Clone, Debug, PartialEq)]
|
||||||
|
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()
|
||||||
|
])
|
||||||
|
}))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn morphism_test_setup() -> ( TypeDict, MorphismBase<DummyMorphism> ) {
|
||||||
|
let mut dict = TypeDict::new();
|
||||||
|
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(
|
||||||
|
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();
|
||||||
|
|
||||||
|
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(),
|
||||||
|
]
|
||||||
|
)
|
||||||
|
);
|
||||||
|
|
||||||
|
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( &dict, &base ) {
|
||||||
|
for e in solution.edges.iter() {
|
||||||
|
eprintln!(" :: {}\n--> {}", dict.unparse(&e.src_type), dict.unparse(&e.dst_type));
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
eprintln!("no solution");
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
Loading…
Reference in a new issue