Skip to content

Commit

Permalink
fix: Predicate::Or(Set<Predicate>)
Browse files Browse the repository at this point in the history
  • Loading branch information
@mtshiba
mtshiba committed Nov 30, 2024
1 parent 353b403 commit 2e60507
Show file tree
Hide file tree
Showing 6 changed files with 165 additions and 114 deletions.
33 changes: 18 additions & 15 deletions crates/erg_compiler/context/compare.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2217,9 +2217,9 @@ impl Context {
| Predicate::GeneralLessEqual { rhs, .. }
| Predicate::GeneralNotEqual { rhs, .. } => self.get_pred_type(rhs),
// x == 1 or x == "a" => Int or Str
Predicate::Or(lhs, rhs) => {
self.union(&self.get_pred_type(lhs), &self.get_pred_type(rhs))
}
Predicate::Or(ors) => ors
.iter()
.fold(Never, |l, r| self.union(&l, &self.get_pred_type(r))),
// REVIEW:
Predicate::And(lhs, rhs) => {
self.intersection(&self.get_pred_type(lhs), &self.get_pred_type(rhs))
Expand Down Expand Up @@ -2345,14 +2345,17 @@ impl Context {
(None, None) => None,
}
}
Predicate::Or(l, r) => {
let l = self.eliminate_type_mismatched_preds(var, t, *l);
let r = self.eliminate_type_mismatched_preds(var, t, *r);
match (l, r) {
(Some(l), Some(r)) => Some(l | r),
(Some(l), None) => Some(l),
(None, Some(r)) => Some(r),
(None, None) => None,
Predicate::Or(preds) => {
let mut new_preds = Set::with_capacity(preds.len());
for pred in preds {
if let Some(new_pred) = self.eliminate_type_mismatched_preds(var, t, pred) {
new_preds.insert(new_pred);
}
}
if new_preds.is_empty() {
None
} else {
Some(Predicate::Or(new_preds))
}
}
_ => Some(pred),
Expand Down Expand Up @@ -2462,7 +2465,7 @@ impl Context {
// {I == 1 or I == 0} !:> {I == 0 or I == 1 or I == 3}
// NG: (self.is_super_pred_of(l1, l2) && self.is_super_pred_of(r1, r2))
// || (self.is_super_pred_of(l1, r2) && self.is_super_pred_of(r1, l2))
(Pred::Or(_, _), Pred::Or(_, _)) => {
(Pred::Or(_), Pred::Or(_)) => {
let lhs_ors = self.reduce_preds("or", lhs.ors());
let rhs_ors = self.reduce_preds("or", rhs.ors());
for r_val in rhs_ors.iter() {
Expand Down Expand Up @@ -2509,8 +2512,8 @@ impl Context {
(lhs, Pred::And(l, r)) => {
self.is_super_pred_of(lhs, l) || self.is_super_pred_of(lhs, r)
}
(lhs, Pred::Or(l, r)) => self.is_super_pred_of(lhs, l) && self.is_super_pred_of(lhs, r),
(Pred::Or(l, r), rhs) => self.is_super_pred_of(l, rhs) || self.is_super_pred_of(r, rhs),
(lhs, Pred::Or(ors)) => ors.iter().all(|or| self.is_super_pred_of(lhs, or)),
(Pred::Or(ors), rhs) => ors.iter().any(|or| self.is_super_pred_of(or, rhs)),
(Pred::And(l, r), rhs) => {
self.is_super_pred_of(l, rhs) && self.is_super_pred_of(r, rhs)
}
Expand All @@ -2523,7 +2526,7 @@ impl Context {
}
}

fn is_sub_pred_of(&self, lhs: &Predicate, rhs: &Predicate) -> bool {
pub(crate) fn is_sub_pred_of(&self, lhs: &Predicate, rhs: &Predicate) -> bool {
self.is_super_pred_of(rhs, lhs)
}

Expand Down
29 changes: 13 additions & 16 deletions crates/erg_compiler/context/eval.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4166,22 +4166,19 @@ impl Context {
};
lhs & rhs
}
Predicate::Or(l, r) => {
let lhs = match self.eval_pred(*l) {
Ok(pred) => pred,
Err((pred, es)) => {
errs.extend(es);
pred
}
};
let rhs = match self.eval_pred(*r) {
Ok(pred) => pred,
Err((pred, es)) => {
errs.extend(es);
pred
}
};
lhs | rhs
Predicate::Or(preds) => {
let mut new_preds = Set::with_capacity(preds.len());
for pred in preds {
let pred = match self.eval_pred(pred) {
Ok(pred) => pred,
Err((pred, es)) => {
errs.extend(es);
pred
}
};
new_preds.insert(pred);
}
Predicate::Or(new_preds)
}
Predicate::Not(pred) => {
let pred = match self.eval_pred(*pred) {
Expand Down
21 changes: 12 additions & 9 deletions crates/erg_compiler/context/generalize.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -434,11 +434,12 @@ impl<'c> Generalizer<'c> {
let rhs = self.generalize_pred(*rhs, uninit);
Predicate::and(lhs, rhs)
}
Predicate::Or(lhs, rhs) => {
let lhs = self.generalize_pred(*lhs, uninit);
let rhs = self.generalize_pred(*rhs, uninit);
Predicate::or(lhs, rhs)
}
Predicate::Or(preds) => Predicate::Or(
preds
.into_iter()
.map(|pred| self.generalize_pred(pred, uninit))
.collect(),
),
Predicate::Not(pred) => {
let pred = self.generalize_pred(*pred, uninit);
!pred
Expand Down Expand Up @@ -816,10 +817,12 @@ impl<'c, 'q, 'l, L: Locational> Dereferencer<'c, 'q, 'l, L> {
let rhs = self.deref_pred(*rhs)?;
Ok(Predicate::and(lhs, rhs))
}
Predicate::Or(lhs, rhs) => {
let lhs = self.deref_pred(*lhs)?;
let rhs = self.deref_pred(*rhs)?;
Ok(Predicate::or(lhs, rhs))
Predicate::Or(preds) => {
let mut new_preds = Set::with_capacity(preds.len());
for pred in preds.into_iter() {
new_preds.insert(self.deref_pred(pred)?);
}
Ok(Predicate::Or(new_preds))
}
Predicate::Not(pred) => {
let pred = self.deref_pred(*pred)?;
Expand Down
10 changes: 6 additions & 4 deletions crates/erg_compiler/context/instantiate.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -630,10 +630,12 @@ impl Context {
let r = self.instantiate_pred(*r, tmp_tv_cache, loc)?;
Ok(Predicate::and(l, r))
}
Predicate::Or(l, r) => {
let l = self.instantiate_pred(*l, tmp_tv_cache, loc)?;
let r = self.instantiate_pred(*r, tmp_tv_cache, loc)?;
Ok(Predicate::or(l, r))
Predicate::Or(preds) => {
let mut new_preds = Set::with_capacity(preds.len());
for pred in preds {
new_preds.insert(self.instantiate_pred(pred, tmp_tv_cache, loc)?);
}
Ok(Predicate::Or(new_preds))
}
Predicate::Not(pred) => {
let pred = self.instantiate_pred(*pred, tmp_tv_cache, loc)?;
Expand Down
20 changes: 19 additions & 1 deletion crates/erg_compiler/context/unify.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -848,12 +848,30 @@ impl<L: Locational> Unifier<'_, '_, '_, L> {
| (Pred::NotEqual { rhs, .. }, Pred::NotEqual { rhs: rhs2, .. }) => {
self.sub_unify_tp(rhs, rhs2, None, false)
}
(Pred::And(l1, r1), Pred::And(l2, r2)) | (Pred::Or(l1, r1), Pred::Or(l2, r2)) => {
(Pred::And(l1, r1), Pred::And(l2, r2)) => {
match (self.sub_unify_pred(l1, l2), self.sub_unify_pred(r1, r2)) {
(Ok(()), Ok(())) => Ok(()),
(Ok(()), Err(e)) | (Err(e), Ok(())) | (Err(e), Err(_)) => Err(e),
}
}
(Pred::Or(l_preds), Pred::Or(r_preds)) => {
let mut l_preds_ = l_preds.clone();
let mut r_preds_ = r_preds.clone();
for l_pred in l_preds {
if r_preds_.linear_remove(l_pred) {
l_preds_.linear_remove(l_pred);
}
}
for l_pred in l_preds_.iter() {
for r_pred in r_preds_.iter() {
if self.ctx.is_sub_pred_of(l_pred, r_pred) {
self.sub_unify_pred(l_pred, r_pred)?;
continue;
}
}
}
Ok(())
}
(Pred::Not(l), Pred::Not(r)) => self.sub_unify_pred(r, l),
// sub_unify_pred(I == M, I <= ?N(: Nat)) ==> ?N(: M..)
(Pred::Equal { rhs, .. }, Pred::LessEqual { rhs: rhs2, .. }) => {
Expand Down
Loading

0 comments on commit 2e60507

Please sign in to comment.