fix find_morphism_path
* also apply substitution from src-type match * get this substitution as result from `enum_morphisms_with_subtyping`
This commit is contained in:
parent
ae0d7dcffb
commit
06b0e66931
2 changed files with 33 additions and 37 deletions
src
|
@ -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));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
use {
|
||||
crate::{dict::*, morphism::*, TypeTerm}
|
||||
crate::{dict::*, morphism::*, parser::*, TypeTerm}
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
@ -26,10 +26,10 @@ impl Morphism for DummyMorphism {
|
|||
}))
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
#[test]
|
||||
fn test_morphism_path() {
|
||||
let mut dict = TypeDict::new();
|
||||
let mut dict = BimapTypeDict::new();
|
||||
let mut base = MorphismBase::<DummyMorphism>::new( dict.add_typename("Seq".into()) );
|
||||
|
||||
dict.add_varname("Radix".into());
|
||||
|
@ -112,7 +112,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(),
|
||||
|
@ -124,4 +124,3 @@ fn test_morphism_path() {
|
|||
))
|
||||
);
|
||||
}
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue