From ce0103c04fd775b34f1025b8341b1f0e8763a07e Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 2 Apr 2025 23:11:40 +0200
Subject: [PATCH 1/2] find_morphism_path(): always advance with direct morph,
even if complex decomposition from goal exists
---
src/morphism_path_sugared.rs | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/morphism_path_sugared.rs b/src/morphism_path_sugared.rs
index d6a6841..3f6fe77 100644
--- a/src/morphism_path_sugared.rs
+++ b/src/morphism_path_sugared.rs
@@ -91,10 +91,10 @@ impl<'a, M:SugaredMorphism+Clone> SugaredShortestPathProblem<'a, M> {
self.morphism_base.complex_morphism_decomposition( &cur_path.cur_type, &self.goal )
{
self.advance(&cur_path, complex_morph);
- } else {
- for next_morph_inst in self.morphism_base.enum_morphisms_from(&cur_path.cur_type) {
- self.advance(&cur_path, next_morph_inst);
- }
+ }
+
+ for next_morph_inst in self.morphism_base.enum_morphisms_from(&cur_path.cur_type) {
+ self.advance(&cur_path, next_morph_inst);
}
}
}
From 7f96b663240de36c2495fffa6985475ed225ca55 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 2 Apr 2025 23:12:25 +0200
Subject: [PATCH 2/2] subtype unification: check seq-/struct-/enum-repr type
---
src/unification_sugared.rs | 35 ++++++++++++++++++++++++++++++++---
1 file changed, 32 insertions(+), 3 deletions(-)
diff --git a/src/unification_sugared.rs b/src/unification_sugared.rs
index 2e61e80..499e2f1 100644
--- a/src/unification_sugared.rs
+++ b/src/unification_sugared.rs
@@ -329,9 +329,20 @@ impl SugaredUnificationProblem {
(SugaredTypeTerm::Seq{ seq_repr: lhs_seq_repr, items: lhs_items },
SugaredTypeTerm::Seq { seq_repr: rhs_seq_repr, items: rhs_items })
=> {
+ let mut new_addr = unification_pair.addr.clone();
+ new_addr.push(0);
+
+ if let Some(rhs_seq_repr) = rhs_seq_repr.as_ref() {
+ if let Some(lhs_seq_repr) = lhs_seq_repr.as_ref() {
+ let _seq_repr_ψ = self.eval_subtype(SugaredUnificationPair { addr: new_addr.clone(), lhs: *lhs_seq_repr.clone(), rhs: *rhs_seq_repr.clone() })?;
+ } else {
+ return Err(SugaredUnificationError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
+ }
+ }
+
+ let mut new_addr = unification_pair.addr.clone();
+ new_addr.push(1);
if lhs_items.len() == rhs_items.len() && lhs_items.len() > 0 {
- let mut new_addr = unification_pair.addr.clone();
- new_addr.push(0);
match self.eval_subtype( SugaredUnificationPair { addr: new_addr.clone(), lhs: lhs_items[0].clone(), rhs: rhs_items[0].clone() } ) {
Ok(ψ) => Ok(SugaredTypeTerm::Seq {
seq_repr: None, // <<- todo
@@ -344,12 +355,21 @@ impl SugaredUnificationProblem {
})
}
} else {
- Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+ Err(SugaredUnificationError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
}
}
(SugaredTypeTerm::Struct{ struct_repr: lhs_struct_repr, members: lhs_members },
SugaredTypeTerm::Struct{ struct_repr: rhs_struct_repr, members: rhs_members })
=> {
+ let new_addr = unification_pair.addr.clone();
+ if let Some(rhs_struct_repr) = rhs_struct_repr.as_ref() {
+ if let Some(lhs_struct_repr) = lhs_struct_repr.as_ref() {
+ let _struct_repr_ψ = self.eval_subtype(SugaredUnificationPair { addr: new_addr.clone(), lhs: *lhs_struct_repr.clone(), rhs: *rhs_struct_repr.clone() })?;
+ } else {
+ return Err(SugaredUnificationError{ addr: new_addr.clone(), t1: unification_pair.lhs, t2: unification_pair.rhs });
+ }
+ }
+
if lhs_members.len() == rhs_members.len() {
let mut halo_members = Vec::new();
for (i,
@@ -375,6 +395,15 @@ impl SugaredUnificationProblem {
(SugaredTypeTerm::Enum{ enum_repr: lhs_enum_repr, variants: lhs_variants },
SugaredTypeTerm::Enum{ enum_repr: rhs_enum_repr, variants: rhs_variants })
=> {
+ let mut new_addr = unification_pair.addr.clone();
+ if let Some(rhs_enum_repr) = rhs_enum_repr.as_ref() {
+ if let Some(lhs_enum_repr) = lhs_enum_repr.as_ref() {
+ let _enum_repr_ψ = self.eval_subtype(SugaredUnificationPair { addr: new_addr.clone(), lhs: *lhs_enum_repr.clone(), rhs: *rhs_enum_repr.clone() })?;
+ } else {
+ return Err(SugaredUnificationError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
+ }
+ }
+
if lhs_variants.len() == rhs_variants.len() {
let mut halo_variants = Vec::new();
for (i,