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,