From 68627f140edf8da50aafbe1f3233ead4e54b2169 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 2 Apr 2025 13:58:58 +0200
Subject: [PATCH] add strip_halo()
---
src/morphism_sugared.rs | 135 ++++++++++++++++++++++++++++++++++++++--
1 file changed, 129 insertions(+), 6 deletions(-)
diff --git a/src/morphism_sugared.rs b/src/morphism_sugared.rs
index cd41216..0f63191 100644
--- a/src/morphism_sugared.rs
+++ b/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 } => {