language-servers/erg
1
0
Fork 0
mirror of https://github.com/erg-lang/erg.git synced 2025-08-03 18:29:00 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: refinement types bug

Browse source
This commit is contained in:
Shunsuke Shibayama 2023-07-03 19:51:33 +09:00
parent ed8125a468
commit 9e6f1ffa9a
5 changed files with 47 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

27
crates/erg_compiler/context/compare.rs
View file

@ -625,8 +625,16 @@ impl Context {
}
// ({I: Int | True} :> Int) == true, ({N: Nat | ...} :> Int) == false, ({I: Int | I >= 0} :> Int) == false
(Refinement(l), r) => {
if l.pred.mentions(&l.var) && l.pred.can_be_false() {
return false;
if l.pred.mentions(&l.var) {
match l.pred.can_be_false() {
Some(true) => {
return false;
}
None => {
log!(err "evaluating {}", l.pred);
}
Some(false) => {}
}
}
self.supertype_of(&l.t, r)
}
@ -1420,8 +1428,19 @@ impl Context {
Pred::GreaterEqual { .. } | Pred::LessEqual { .. } | Pred::NotEqual { .. },
)
| (Pred::LessEqual { .. }, Pred::GreaterEqual { .. })
| (Pred::GreaterEqual { .. }, Pred::LessEqual { .. })
| (Pred::NotEqual { .. }, Pred::Equal { .. }) => false,
| (Pred::GreaterEqual { .. }, Pred::LessEqual { .. }) => false,
// I != 1 == All - {1} :> I == 2
(Pred::NotEqual { rhs: rhs_ne, .. }, Pred::Equal { rhs: rhs_eq, .. }) => {
rhs_ne != rhs_eq
}
// I != 1 == All - {1} :> I >= 2
(Pred::NotEqual { rhs: rhs_ne, .. }, Pred::GreaterEqual { rhs: rhs_ge, .. }) => {
self.try_cmp(rhs_ne, rhs_ge).is_some_and(|ord| ord.is_lt())
}
// I != 1 == All - {1} :> I <= 0
(Pred::NotEqual { rhs: rhs_ne, .. }, Pred::LessEqual { rhs: rhs_le, .. }) => {
self.try_cmp(rhs_ne, rhs_le).is_some_and(|ord| ord.is_gt())
}
(Pred::NotEqual { rhs, .. }, Pred::NotEqual { rhs: rhs2, .. }) => self
.try_cmp(rhs, rhs2)
.map(|ord| ord.canbe_eq())