syntaxAlchemist/lib-laddertypes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

fix find_morphism_path

Browse source 
* also apply substitution from src-type match
* get this substitution as result from `enum_morphisms_with_subtyping`
This commit is contained in:
Michael Sippel 2024-10-28 19:58:59 +01:00
parent 619c2dc3e4
commit eec78f24ab
Signed by: senvas
GPG key ID: F96CF119C34B64A6
2 changed files with 31 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
src/morphism.rs
View file

@ -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(&current_type) {
let tt = TypeTerm::Ladder(vec![h, t]).normalize();
for (h, t) in self.enum_morphisms_with_subtyping(&current_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));
}
}
}

6
src/steiner_tree.rs
View file

@ -218,10 +218,8 @@ 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 (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_tree.contains( &dst_type ).is_none() {
let mut new_tree = current_tree.clone();