fix: structural Predicate comparison

This commit is contained in:
Shunsuke Shibayama 2023-08-07 23:14:11 +09:00
parent 187259a008
commit 27f191b687
5 changed files with 59 additions and 3 deletions

View file

@ -11,3 +11,5 @@ abs_ x = x.abs()
Norm = Trait { .norm = (self: Self) -> Nat }
norm x = x.norm()
a = [1, 2] + [3, 4]

View file

@ -1,6 +1,7 @@
use erg_common::config::ErgConfig;
use erg_common::error::MultiErrorDisplay;
use erg_common::io::Output;
use erg_common::set;
use erg_common::spawn::exec_new_thread;
use erg_common::traits::Runnable;
@ -9,7 +10,8 @@ use erg_compiler::error::CompileErrors;
use erg_compiler::lower::ASTLowerer;
use erg_compiler::ty::constructors::{
func0, func1, func2, kw, mono, nd_func, nd_proc, or, poly, proc1, subtype_q, ty_tp, type_q,
array_t, func0, func1, func2, kw, mono, nd_func, nd_proc, or, poly, proc1, subtype_q, ty_tp,
type_q, v_enum,
};
use erg_compiler::ty::Type::*;
@ -64,6 +66,11 @@ fn _test_infer_types() -> Result<(), ()> {
module.context.assert_var_type("abs_", &abs_t)?;
let norm_t = func1(mono("<module>::Norm"), Nat);
module.context.assert_var_type("norm", &norm_t)?;
let a_t = array_t(
v_enum(set! {1.into(), 2.into(), 3.into(), 4.into()}),
4.into(),
);
module.context.assert_var_type("a", &a_t)?;
Ok(())
}

View file

@ -1534,7 +1534,7 @@ impl StructuralEq for Type {
}
(Self::FreeVar(fv), Self::FreeVar(fv2)) => fv.structural_eq(fv2),
(Self::Refinement(refine), Self::Refinement(refine2)) => {
refine.t.structural_eq(&refine2.t) && refine.pred == refine2.pred
refine.t.structural_eq(&refine2.t) && refine.pred.structural_eq(&refine2.pred)
}
(Self::Record(rec), Self::Record(rec2)) => {
for (k, v) in rec.iter() {

View file

@ -4,7 +4,7 @@ use std::ops::{BitAnd, BitOr, Not};
#[allow(unused_imports)]
use erg_common::log;
use erg_common::set::Set;
use erg_common::traits::LimitedDisplay;
use erg_common::traits::{LimitedDisplay, StructuralEq};
use erg_common::{set, Str};
use super::free::{Constraint, HasLevel};
@ -102,6 +102,50 @@ impl LimitedDisplay for Predicate {
}
}
impl StructuralEq for Predicate {
fn structural_eq(&self, other: &Self) -> bool {
match (self, other) {
(Self::Equal { rhs, .. }, Self::Equal { rhs: r2, .. })
| (Self::NotEqual { rhs, .. }, Self::NotEqual { rhs: r2, .. })
| (Self::GreaterEqual { rhs, .. }, Self::GreaterEqual { rhs: r2, .. })
| (Self::LessEqual { rhs, .. }, Self::LessEqual { rhs: r2, .. }) => {
rhs.structural_eq(r2)
}
(Self::Or(_, _), Self::Or(_, _)) => {
let self_ors = self.ors();
let other_ors = other.ors();
if self_ors.len() != other_ors.len() {
return false;
}
for l_val in self_ors.iter() {
if other_ors.get_by(l_val, |l, r| l.structural_eq(r)).is_none() {
return false;
}
}
true
}
(Self::And(_, _), Self::And(_, _)) => {
let self_ands = self.ands();
let other_ands = other.ands();
if self_ands.len() != other_ands.len() {
return false;
}
for l_val in self_ands.iter() {
if other_ands
.get_by(l_val, |l, r| l.structural_eq(r))
.is_none()
{
return false;
}
}
true
}
(Self::Not(p1), Self::Not(p2)) => p1.structural_eq(p2),
_ => self == other,
}
}
}
impl HasLevel for Predicate {
fn level(&self) -> Option<usize> {
match self {

View file

@ -797,6 +797,9 @@ impl StructuralEq for TyParam {
true
}
(Self::Set(l), Self::Set(r)) => {
if l.len() != r.len() {
return false;
}
for l_val in l.iter() {
if r.get_by(l_val, |l, r| l.structural_eq(r)).is_none() {
return false;