add strip_halo()

src/morphism_sugared.rs

@@ -1,11 +1,6 @@
 use {
     crate::{
-        substitution_sugared::SugaredSubstitution,
-        sugar::{SugaredStructMember, SugaredTypeTerm},
-        unification::UnificationProblem,
-        unification_sugared::SugaredUnificationProblem,
-        unparser::*, TypeDict,
-        TypeID, TypeTerm
+        substitution_sugared::SugaredSubstitution, sugar::{SugaredStructMember, SugaredTypeTerm}, unification::UnificationProblem, unification_sugared::SugaredUnificationProblem, unparser::*, SugaredEnumVariant, TypeDict, TypeID, TypeTerm
     },
     std::{collections::HashMap, u64}
 };
@@ -18,6 +13,130 @@ pub struct SugaredMorphismType {
     pub dst_type: SugaredTypeTerm
 }
 
+impl SugaredMorphismType {
+    pub fn strip_halo(&self) -> SugaredMorphismType {
+        match (&self.src_type, &self.dst_type) {
+            (SugaredTypeTerm::Ladder(rungs_lhs), SugaredTypeTerm::Ladder(rungs_rhs)) => {
+
+                let mut lhs_iter = rungs_lhs.iter();
+                let mut rhs_iter = rungs_rhs.iter();
+                let mut last = SugaredMorphismType { src_type: SugaredTypeTerm::unit(), dst_type: SugaredTypeTerm::unit() };
+
+                while let (Some(lhs_top), Some(rhs_top)) = (lhs_iter.next(), rhs_iter.next()) {
+                    last = SugaredMorphismType{
+                        src_type: lhs_top.clone(),
+                        dst_type: rhs_top.clone()
+                    };
+
+                    if lhs_top != rhs_top {
+                        let x = SugaredMorphismType{ src_type: lhs_top.clone(), dst_type: rhs_top.clone() }.strip_halo();
+
+                        let mut rl : Vec<_> = lhs_iter.cloned().collect();
+                        rl.insert(0, x.src_type);
+                        let mut rr : Vec<_> = rhs_iter.cloned().collect();
+                        rr.insert(0, x.dst_type);
+
+                        return SugaredMorphismType {
+                            src_type: SugaredTypeTerm::Ladder(rl),
+                            dst_type: SugaredTypeTerm::Ladder(rr)
+                        };
+                    }
+                }
+
+                last
+            }
+
+            (SugaredTypeTerm::Spec(args_lhs), SugaredTypeTerm::Spec(args_rhs)) => {
+
+                let (rl, rr) = args_lhs.iter().zip(args_rhs.iter()).map(
+                    |(al,ar)| SugaredMorphismType{ src_type: al.clone(), dst_type: ar.clone() }.strip_halo()
+                )
+                .fold((vec![], vec![]), |(mut rl, mut rr), x| {
+                    rl.push(x.src_type);
+                    rr.push(x.dst_type);
+                    (rl,rr)
+                });
+
+                SugaredMorphismType {
+                    src_type: SugaredTypeTerm::Spec(rl),
+                    dst_type: SugaredTypeTerm::Spec(rr)
+                }
+            }
+
+            (SugaredTypeTerm::Seq { seq_repr:seq_repr_lhs, items:items_lhs }, SugaredTypeTerm::Seq { seq_repr: seq_repr_rhs, items:items_rhs }) => {
+                let (rl, rr) = items_lhs.iter().zip(items_rhs.iter()).map(
+                    |(al,ar)| SugaredMorphismType{ src_type: al.clone(), dst_type: ar.clone() }.strip_halo()
+                )
+                .fold((vec![], vec![]), |(mut rl, mut rr), x| {
+                    rl.push(x.src_type);
+                    rr.push(x.dst_type);
+                    (rl,rr)
+                });
+                SugaredMorphismType  {
+                    src_type: SugaredTypeTerm::Seq{ seq_repr: seq_repr_lhs.clone(), items: rl },
+                    dst_type: SugaredTypeTerm::Seq { seq_repr: seq_repr_rhs.clone(), items: rr }
+                }
+            }
+
+            (SugaredTypeTerm::Struct { struct_repr:seq_repr_lhs, members:items_lhs }, SugaredTypeTerm::Struct { struct_repr: seq_repr_rhs, members:items_rhs }) => {
+                let mut rl = Vec::new();
+                let mut rr = Vec::new();
+
+                for ar in items_rhs.iter() {
+                    for al in items_lhs.iter() {
+                        if al.symbol == ar.symbol {
+                            let x = SugaredMorphismType{ src_type: al.ty.clone(), dst_type: ar.ty.clone() }.strip_halo();
+                            rl.push( SugaredStructMember{
+                                symbol: al.symbol.clone(),
+                                ty: x.src_type
+                            });
+                            rr.push( SugaredStructMember{
+                                symbol: ar.symbol.clone(),
+                                ty: x.dst_type
+                            });
+                            break;
+                        }
+                    }
+                }
+
+                SugaredMorphismType  {
+                    src_type: SugaredTypeTerm::Struct{ struct_repr: seq_repr_lhs.clone(), members: rl },
+                    dst_type: SugaredTypeTerm::Struct{ struct_repr: seq_repr_rhs.clone(), members: rr }
+                }
+            }
+
+            (SugaredTypeTerm::Enum { enum_repr:seq_repr_lhs, variants:items_lhs }, SugaredTypeTerm::Enum { enum_repr: seq_repr_rhs, variants:items_rhs }) => {
+
+                let mut rl = Vec::new();
+                let mut rr = Vec::new();
+
+                for ar in items_rhs.iter() {
+                    for al in items_lhs.iter() {
+                        if al.symbol == ar.symbol {
+                            let x = SugaredMorphismType{ src_type: al.ty.clone(), dst_type: ar.ty.clone() }.strip_halo();
+                            rl.push( SugaredEnumVariant{
+                                symbol: al.symbol.clone(),
+                                ty: x.src_type
+                            });
+                            rr.push( SugaredEnumVariant{
+                                symbol: ar.symbol.clone(),
+                                ty: x.dst_type
+                            });
+                        }
+                    }
+                }
+
+                SugaredMorphismType  {
+                    src_type: SugaredTypeTerm::Enum{ enum_repr: seq_repr_lhs.clone(), variants: rl },
+                    dst_type: SugaredTypeTerm::Enum { enum_repr: seq_repr_rhs.clone(), variants: rr }
+                }
+            }
+
+            (x,y) => SugaredMorphismType { src_type: x.clone(), dst_type: y.clone() }
+        }
+    }
+}
+
 pub trait SugaredMorphism : Sized {
     fn get_type(&self) -> SugaredMorphismType;
     fn weight(&self) -> u64 {
@@ -54,6 +173,10 @@ pub enum MorphismInstance2<M: SugaredMorphism + Clone> {
 
 
 impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
+    pub fn get_haloless_type(&self) -> SugaredMorphismType {
+        self.get_type().strip_halo()
+    }
+
     pub fn get_type(&self) -> SugaredMorphismType {
         match self {
             MorphismInstance2::Primitive { ψ, σ, morph } => {