From eec78f24ab9806380ea230c0f221bfb08491b8d2 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Mon, 28 Oct 2024 19:58:59 +0100
Subject: [PATCH] fix find_morphism_path

* also apply substitution from src-type match
* get this substitution as result from `enum_morphisms_with_subtyping`
---
 src/morphism.rs     | 61 +++++++++++++++++++++------------------------
 src/steiner_tree.rs |  6 ++---
 2 files changed, 31 insertions(+), 36 deletions(-)

diff --git a/src/morphism.rs b/src/morphism.rs
index 9160610..9ba1ecb 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -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));
                         }
                     }
                 }
diff --git a/src/steiner_tree.rs b/src/steiner_tree.rs
index f854dd9..d168812 100644
--- a/src/steiner_tree.rs
+++ b/src/steiner_tree.rs
@@ -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();