SugaredMorphismType::Struct add src/dst repr

This commit is contained in:
Michael Sippel 2025-04-03 15:37:23 +02:00
parent ebaa1350ac
commit f5fc2979c7
Signed by: senvas
GPG key ID: F96CF119C34B64A6
2 changed files with 15 additions and 12 deletions

View file

@ -48,7 +48,7 @@ impl<M: SugaredMorphism + Clone> SugaredMorphismBase<M> {
match (src_floor, dst_floor) {
(SugaredTypeTerm::Struct{ struct_repr: struct_repr_lhs, members: members_lhs},
SugaredTypeTerm::Struct { struct_repr: _struct_repr_rhs, members: members_rhs })
SugaredTypeTerm::Struct { struct_repr: struct_repr_rhs, members: members_rhs })
=> {
// todo: optimization: check if struct repr match
@ -84,7 +84,8 @@ impl<M: SugaredMorphism + Clone> SugaredMorphismBase<M> {
if ! failed && necessary {
Some(MorphismInstance2::MapStruct {
ψ: src_ψ,
struct_repr: struct_repr_lhs.clone(),
src_struct_repr: struct_repr_lhs.clone(),
dst_struct_repr: struct_repr_rhs.clone(),
member_morph
})
} else {

View file

@ -168,7 +168,8 @@ pub enum MorphismInstance2<M: SugaredMorphism + Clone> {
},
MapStruct{
ψ: SugaredTypeTerm,
struct_repr: Option<Box<SugaredTypeTerm>>,
src_struct_repr: Option<Box<SugaredTypeTerm>>,
dst_struct_repr: Option<Box<SugaredTypeTerm>>,
member_morph: Vec< (String, MorphismInstance2<M>) >
},
MapEnum{
@ -204,14 +205,15 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
}
MorphismInstance2::Chain { path } => {
if path.len() > 0 {
let s = self.get_subst();
SugaredMorphismType {
src_type: path.first().unwrap().get_type().src_type,
dst_type: path.last().unwrap().get_type().dst_type
src_type: path.first().unwrap().get_type().src_type.clone().apply_subst(&s).clone(),
dst_type: path.last().unwrap().get_type().dst_type.clone().apply_subst(&s).clone()
}
} else {
SugaredMorphismType {
src_type: SugaredTypeTerm::TypeID(TypeID::Var(45454)),
dst_type: SugaredTypeTerm::TypeID(TypeID::Var(45454))
src_type: SugaredTypeTerm::TypeID(TypeID::Fun(45454)),
dst_type: SugaredTypeTerm::TypeID(TypeID::Fun(45454))
}
}
}
@ -229,11 +231,11 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
]).strip()
}
}
MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
MorphismInstance2::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
SugaredMorphismType {
src_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
SugaredTypeTerm::Struct{
struct_repr: struct_repr.clone(),
struct_repr: src_struct_repr.clone(),
members:
member_morph.iter().map(|(symbol, morph)| {
SugaredStructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
@ -242,7 +244,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
]).strip(),
dst_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
SugaredTypeTerm::Struct{
struct_repr: struct_repr.clone(),
struct_repr: dst_struct_repr.clone(),
members: member_morph.iter().map(|(symbol, morph)| {
SugaredStructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
}).collect()
@ -289,7 +291,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
MorphismInstance2::MapSeq { ψ, seq_repr, item_morph } => {
item_morph.get_subst()
},
MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
MorphismInstance2::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
let mut σ = HashMap::new();
for (symbol, m) in member_morph.iter() {
σ = σ.append(&mut m.get_subst());
@ -318,7 +320,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
ψ.apply_subst(γ);
item_morph.apply_subst(γ);
}
MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
MorphismInstance2::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
for (_,ty) in member_morph {
ty.apply_subst(γ);
}