feat: add Predicate::General{Less, Greater, Not}Equal

This commit is contained in:
Shunsuke Shibayama 2024-01-28 20:24:14 +09:00
parent 8350ad0581
commit 06a4a6e5fc
10 changed files with 304 additions and 18 deletions

View file

@ -1535,7 +1535,10 @@ impl Context {
} }
} }
// REVIEW // REVIEW
Predicate::GeneralEqual { rhs, .. } => self.get_pred_type(rhs), Predicate::GeneralEqual { rhs, .. }
| Predicate::GeneralGreaterEqual { rhs, .. }
| Predicate::GeneralLessEqual { rhs, .. }
| Predicate::GeneralNotEqual { rhs, .. } => self.get_pred_type(rhs),
// x == 1 or x == "a" => Int or Str // x == 1 or x == "a" => Int or Str
Predicate::Or(lhs, rhs) => { Predicate::Or(lhs, rhs) => {
self.union(&self.get_pred_type(lhs), &self.get_pred_type(rhs)) self.union(&self.get_pred_type(lhs), &self.get_pred_type(rhs))
@ -1673,6 +1676,27 @@ impl Context {
lhs: lhs2, lhs: lhs2,
rhs: rhs2, rhs: rhs2,
}, },
)
| (
Pred::GeneralGreaterEqual { lhs, rhs },
Pred::GeneralGreaterEqual {
lhs: lhs2,
rhs: rhs2,
},
)
| (
Pred::GeneralLessEqual { lhs, rhs },
Pred::GeneralLessEqual {
lhs: lhs2,
rhs: rhs2,
},
)
| (
Pred::GeneralNotEqual { lhs, rhs },
Pred::GeneralNotEqual {
lhs: lhs2,
rhs: rhs2,
},
) => self.is_super_pred_of(lhs, lhs2) && self.is_super_pred_of(rhs, rhs2), ) => self.is_super_pred_of(lhs, lhs2) && self.is_super_pred_of(rhs, rhs2),
// {T >= 0} :> {T >= 1}, {T >= 0} :> {T == 1} // {T >= 0} :> {T >= 1}, {T >= 0} :> {T == 1}
( (

View file

@ -2609,6 +2609,37 @@ impl Context {
(lhs, rhs) => Ok(Predicate::general_eq(lhs, rhs)), (lhs, rhs) => Ok(Predicate::general_eq(lhs, rhs)),
} }
} }
Predicate::GeneralNotEqual { lhs, rhs } => {
match (self.eval_pred(*lhs)?, self.eval_pred(*rhs)?) {
(Predicate::Value(lhs), Predicate::Value(rhs)) => {
Ok(Predicate::Value(ValueObj::Bool(lhs != rhs)))
}
(lhs, rhs) => Ok(Predicate::general_ne(lhs, rhs)),
}
}
Predicate::GeneralGreaterEqual { lhs, rhs } => {
match (self.eval_pred(*lhs)?, self.eval_pred(*rhs)?) {
(Predicate::Value(lhs), Predicate::Value(rhs)) => {
let Some(ValueObj::Bool(res)) = lhs.try_ge(rhs) else {
// TODO:
return feature_error!(self, Location::Unknown, "evaluating >=");
};
Ok(Predicate::Value(ValueObj::Bool(res)))
}
(lhs, rhs) => Ok(Predicate::general_ge(lhs, rhs)),
}
}
Predicate::GeneralLessEqual { lhs, rhs } => {
match (self.eval_pred(*lhs)?, self.eval_pred(*rhs)?) {
(Predicate::Value(lhs), Predicate::Value(rhs)) => {
let Some(ValueObj::Bool(res)) = lhs.try_le(rhs) else {
return feature_error!(self, Location::Unknown, "evaluating <=");
};
Ok(Predicate::Value(ValueObj::Bool(res)))
}
(lhs, rhs) => Ok(Predicate::general_le(lhs, rhs)),
}
}
Predicate::Equal { lhs, rhs } => Ok(Predicate::eq(lhs, self.eval_tp(rhs)?)), Predicate::Equal { lhs, rhs } => Ok(Predicate::eq(lhs, self.eval_tp(rhs)?)),
Predicate::NotEqual { lhs, rhs } => Ok(Predicate::ne(lhs, self.eval_tp(rhs)?)), Predicate::NotEqual { lhs, rhs } => Ok(Predicate::ne(lhs, self.eval_tp(rhs)?)),
Predicate::LessEqual { lhs, rhs } => Ok(Predicate::le(lhs, self.eval_tp(rhs)?)), Predicate::LessEqual { lhs, rhs } => Ok(Predicate::le(lhs, self.eval_tp(rhs)?)),

View file

@ -341,6 +341,21 @@ impl Generalizer {
let rhs = self.generalize_pred(*rhs, uninit); let rhs = self.generalize_pred(*rhs, uninit);
Predicate::general_eq(lhs, rhs) Predicate::general_eq(lhs, rhs)
} }
Predicate::GeneralGreaterEqual { lhs, rhs } => {
let lhs = self.generalize_pred(*lhs, uninit);
let rhs = self.generalize_pred(*rhs, uninit);
Predicate::general_ge(lhs, rhs)
}
Predicate::GeneralLessEqual { lhs, rhs } => {
let lhs = self.generalize_pred(*lhs, uninit);
let rhs = self.generalize_pred(*rhs, uninit);
Predicate::general_le(lhs, rhs)
}
Predicate::GeneralNotEqual { lhs, rhs } => {
let lhs = self.generalize_pred(*lhs, uninit);
let rhs = self.generalize_pred(*rhs, uninit);
Predicate::general_ne(lhs, rhs)
}
Predicate::Equal { lhs, rhs } => { Predicate::Equal { lhs, rhs } => {
let rhs = self.generalize_tp(rhs, uninit); let rhs = self.generalize_tp(rhs, uninit);
Predicate::eq(lhs, rhs) Predicate::eq(lhs, rhs)
@ -597,6 +612,51 @@ impl<'c, 'q, 'l, L: Locational> Dereferencer<'c, 'q, 'l, L> {
(lhs, rhs) => Ok(Predicate::general_eq(lhs, rhs)), (lhs, rhs) => Ok(Predicate::general_eq(lhs, rhs)),
} }
} }
Predicate::GeneralNotEqual { lhs, rhs } => {
let lhs = self.deref_pred(*lhs)?;
let rhs = self.deref_pred(*rhs)?;
match (lhs, rhs) {
(Predicate::Value(lhs), Predicate::Value(rhs)) => {
Ok(Predicate::Value(ValueObj::Bool(lhs != rhs)))
}
(lhs, rhs) => Ok(Predicate::general_ne(lhs, rhs)),
}
}
Predicate::GeneralGreaterEqual { lhs, rhs } => {
let lhs = self.deref_pred(*lhs)?;
let rhs = self.deref_pred(*rhs)?;
match (lhs, rhs) {
(Predicate::Value(lhs), Predicate::Value(rhs)) => {
let Some(ValueObj::Bool(res)) = lhs.try_ge(rhs) else {
// TODO:
return Err(TyCheckErrors::from(TyCheckError::dummy_infer_error(
self.ctx.cfg.input.clone(),
fn_name!(),
line!(),
)));
};
Ok(Predicate::Value(ValueObj::Bool(res)))
}
(lhs, rhs) => Ok(Predicate::general_ge(lhs, rhs)),
}
}
Predicate::GeneralLessEqual { lhs, rhs } => {
let lhs = self.deref_pred(*lhs)?;
let rhs = self.deref_pred(*rhs)?;
match (lhs, rhs) {
(Predicate::Value(lhs), Predicate::Value(rhs)) => {
let Some(ValueObj::Bool(res)) = lhs.try_le(rhs) else {
return Err(TyCheckErrors::from(TyCheckError::dummy_infer_error(
self.ctx.cfg.input.clone(),
fn_name!(),
line!(),
)));
};
Ok(Predicate::Value(ValueObj::Bool(res)))
}
(lhs, rhs) => Ok(Predicate::general_le(lhs, rhs)),
}
}
Predicate::Call { Predicate::Call {
receiver, receiver,
name, name,

View file

@ -1637,6 +1637,19 @@ impl Context {
None, None,
))); )));
array_.register_builtin_const(FUNC_PROD, Visibility::BUILTIN_PUBLIC, prod); array_.register_builtin_const(FUNC_PROD, Visibility::BUILTIN_PUBLIC, prod);
let reversed_t = no_var_fn_met(
array_t(T.clone(), TyParam::erased(Nat)),
vec![],
vec![],
array_t(T.clone(), TyParam::erased(Nat)),
);
let reversed = ValueObj::Subr(ConstSubr::Builtin(BuiltinConstSubr::new(
FUNC_REVERSED,
array_reversed,
reversed_t.quantify(),
None,
)));
array_.register_builtin_const(FUNC_REVERSED, Visibility::BUILTIN_PUBLIC, reversed);
/* Slice */ /* Slice */
let mut slice = Self::builtin_mono_class(SLICE, 3); let mut slice = Self::builtin_mono_class(SLICE, 3);
slice.register_superclass(Obj, &obj); slice.register_superclass(Obj, &obj);

View file

@ -619,6 +619,26 @@ pub(crate) fn array_prod(mut args: ValueArgs, ctx: &Context) -> EvalValueResult<
Ok(arr) Ok(arr)
} }
fn _array_reversed(arr: ValueObj, _ctx: &Context) -> Result<ValueObj, String> {
match arr {
ValueObj::Array(a) => {
let mut vec = a.to_vec();
vec.reverse();
Ok(ValueObj::Array(vec.into()))
}
_ => Err(format!("Cannot reverse {arr}")),
}
}
pub(crate) fn array_reversed(mut args: ValueArgs, ctx: &Context) -> EvalValueResult<TyParam> {
let arr = args
.remove_left_or_key("Self")
.ok_or_else(|| not_passed("Self"))?;
let res = _array_reversed(arr, ctx).unwrap();
let arr = TyParam::Value(res);
Ok(arr)
}
pub(crate) fn __range_getitem__(mut args: ValueArgs, _ctx: &Context) -> EvalValueResult<TyParam> { pub(crate) fn __range_getitem__(mut args: ValueArgs, _ctx: &Context) -> EvalValueResult<TyParam> {
let slf = args let slf = args
.remove_left_or_key("Self") .remove_left_or_key("Self")

View file

@ -600,6 +600,21 @@ impl Context {
let rhs = self.instantiate_pred(*rhs, tmp_tv_cache, loc)?; let rhs = self.instantiate_pred(*rhs, tmp_tv_cache, loc)?;
Ok(Predicate::general_eq(lhs, rhs)) Ok(Predicate::general_eq(lhs, rhs))
} }
Predicate::GeneralGreaterEqual { lhs, rhs } => {
let lhs = self.instantiate_pred(*lhs, tmp_tv_cache, loc)?;
let rhs = self.instantiate_pred(*rhs, tmp_tv_cache, loc)?;
Ok(Predicate::general_ge(lhs, rhs))
}
Predicate::GeneralLessEqual { lhs, rhs } => {
let lhs = self.instantiate_pred(*lhs, tmp_tv_cache, loc)?;
let rhs = self.instantiate_pred(*rhs, tmp_tv_cache, loc)?;
Ok(Predicate::general_le(lhs, rhs))
}
Predicate::GeneralNotEqual { lhs, rhs } => {
let lhs = self.instantiate_pred(*lhs, tmp_tv_cache, loc)?;
let rhs = self.instantiate_pred(*rhs, tmp_tv_cache, loc)?;
Ok(Predicate::general_ne(lhs, rhs))
}
_ => Ok(pred), _ => Ok(pred),
} }
} }

View file

@ -1491,6 +1491,15 @@ impl Context {
other if bin.op.kind == TokenKind::DblEq => { other if bin.op.kind == TokenKind::DblEq => {
return Ok(Predicate::general_eq(other, rhs)); return Ok(Predicate::general_eq(other, rhs));
} }
other if bin.op.kind == TokenKind::NotEq => {
return Ok(Predicate::general_ne(other, rhs));
}
other if bin.op.kind == TokenKind::GreEq => {
return Ok(Predicate::general_ge(other, rhs));
}
other if bin.op.kind == TokenKind::LessEq => {
return Ok(Predicate::general_le(other, rhs));
}
_ => { _ => {
return type_feature_error!( return type_feature_error!(
self, self,
@ -1505,6 +1514,15 @@ impl Context {
other if bin.op.kind == TokenKind::DblEq => { other if bin.op.kind == TokenKind::DblEq => {
return Ok(Predicate::general_eq(Predicate::Const(var), other)); return Ok(Predicate::general_eq(Predicate::Const(var), other));
} }
other if bin.op.kind == TokenKind::NotEq => {
return Ok(Predicate::general_ne(Predicate::Const(var), other));
}
other if bin.op.kind == TokenKind::GreEq => {
return Ok(Predicate::general_ge(Predicate::Const(var), other));
}
other if bin.op.kind == TokenKind::LessEq => {
return Ok(Predicate::general_le(Predicate::Const(var), other));
}
_ => { _ => {
return type_feature_error!( return type_feature_error!(
self, self,

View file

@ -49,3 +49,10 @@
assert [1, 2, 3].product() == 6 assert [1, 2, 3].product() == 6
''' '''
prod: |T: Type|(self: Array(T, _), start := T) -> T prod: |T: Type|(self: Array(T, _), start := T) -> T
'''
Returns the reversed array.
'''
'''erg
assert [1, 2, 3].reversed() == [3, 2, 1]
'''
reversed: |T: Type, N: Nat|(self: Array(T, N)) -> Array(T, N)

View file

@ -111,6 +111,9 @@ class Array(list):
from functools import reduce from functools import reduce
return reduce(lambda x, y: x * y, self, start) return reduce(lambda x, y: x * y, self, start)
def reversed(self):
return Array(list.__reversed__(self))
class UnsizedArray: class UnsizedArray:
elem: object elem: object
def __init__(self, elem): def __init__(self, elem):

View file

@ -25,10 +25,6 @@ pub enum Predicate {
lhs: Str, lhs: Str,
rhs: TyParam, rhs: TyParam,
}, },
GeneralEqual {
lhs: Box<Predicate>,
rhs: Box<Predicate>,
},
/// i > 0 == i >= 0 and i != 0 /// i > 0 == i >= 0 and i != 0
GreaterEqual { GreaterEqual {
lhs: Str, lhs: Str,
@ -43,6 +39,22 @@ pub enum Predicate {
lhs: Str, lhs: Str,
rhs: TyParam, rhs: TyParam,
}, },
GeneralEqual {
lhs: Box<Predicate>,
rhs: Box<Predicate>,
},
GeneralLessEqual {
lhs: Box<Predicate>,
rhs: Box<Predicate>,
},
GeneralGreaterEqual {
lhs: Box<Predicate>,
rhs: Box<Predicate>,
},
GeneralNotEqual {
lhs: Box<Predicate>,
rhs: Box<Predicate>,
},
Or(Box<Predicate>, Box<Predicate>), Or(Box<Predicate>, Box<Predicate>),
And(Box<Predicate>, Box<Predicate>), And(Box<Predicate>, Box<Predicate>),
Not(Box<Predicate>), Not(Box<Predicate>),
@ -69,10 +81,13 @@ impl fmt::Display for Predicate {
) )
} }
Self::Equal { lhs, rhs } => write!(f, "{lhs} == {rhs}"), Self::Equal { lhs, rhs } => write!(f, "{lhs} == {rhs}"),
Self::GeneralEqual { lhs, rhs } => write!(f, "{lhs} == {rhs}"),
Self::GreaterEqual { lhs, rhs } => write!(f, "{lhs} >= {rhs}"), Self::GreaterEqual { lhs, rhs } => write!(f, "{lhs} >= {rhs}"),
Self::LessEqual { lhs, rhs } => write!(f, "{lhs} <= {rhs}"), Self::LessEqual { lhs, rhs } => write!(f, "{lhs} <= {rhs}"),
Self::NotEqual { lhs, rhs } => write!(f, "{lhs} != {rhs}"), Self::NotEqual { lhs, rhs } => write!(f, "{lhs} != {rhs}"),
Self::GeneralEqual { lhs, rhs } => write!(f, "{lhs} == {rhs}"),
Self::GeneralLessEqual { lhs, rhs } => write!(f, "{lhs} <= {rhs}"),
Self::GeneralGreaterEqual { lhs, rhs } => write!(f, "{lhs} >= {rhs}"),
Self::GeneralNotEqual { lhs, rhs } => write!(f, "{lhs} != {rhs}"),
Self::Or(l, r) => write!(f, "({l}) or ({r})"), Self::Or(l, r) => write!(f, "({l}) or ({r})"),
Self::And(l, r) => write!(f, "({l}) and ({r})"), Self::And(l, r) => write!(f, "({l}) and ({r})"),
Self::Not(p) => write!(f, "not ({p})"), Self::Not(p) => write!(f, "not ({p})"),
@ -108,11 +123,6 @@ impl LimitedDisplay for Predicate {
write!(f, "{lhs} == ")?; write!(f, "{lhs} == ")?;
rhs.limited_fmt(f, limit - 1) rhs.limited_fmt(f, limit - 1)
} }
Self::GeneralEqual { lhs, rhs } => {
lhs.limited_fmt(f, limit - 1)?;
write!(f, " == ")?;
rhs.limited_fmt(f, limit - 1)
}
Self::GreaterEqual { lhs, rhs } => { Self::GreaterEqual { lhs, rhs } => {
write!(f, "{lhs} >= ")?; write!(f, "{lhs} >= ")?;
rhs.limited_fmt(f, limit - 1) rhs.limited_fmt(f, limit - 1)
@ -125,6 +135,26 @@ impl LimitedDisplay for Predicate {
write!(f, "{lhs} != ")?; write!(f, "{lhs} != ")?;
rhs.limited_fmt(f, limit - 1) rhs.limited_fmt(f, limit - 1)
} }
Self::GeneralEqual { lhs, rhs } => {
lhs.limited_fmt(f, limit - 1)?;
write!(f, " == ")?;
rhs.limited_fmt(f, limit - 1)
}
Self::GeneralLessEqual { lhs, rhs } => {
lhs.limited_fmt(f, limit - 1)?;
write!(f, " <= ")?;
rhs.limited_fmt(f, limit - 1)
}
Self::GeneralGreaterEqual { lhs, rhs } => {
lhs.limited_fmt(f, limit - 1)?;
write!(f, " >= ")?;
rhs.limited_fmt(f, limit - 1)
}
Self::GeneralNotEqual { lhs, rhs } => {
lhs.limited_fmt(f, limit - 1)?;
write!(f, " != ")?;
rhs.limited_fmt(f, limit - 1)
}
Self::Or(l, r) => { Self::Or(l, r) => {
write!(f, "(")?; write!(f, "(")?;
l.limited_fmt(f, limit - 1)?; l.limited_fmt(f, limit - 1)?;
@ -216,7 +246,12 @@ impl HasLevel for Predicate {
| Self::GreaterEqual { rhs, .. } | Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. } | Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => rhs.level(), | Self::NotEqual { rhs, .. } => rhs.level(),
Self::GeneralEqual { lhs, rhs } => lhs.level().zip(rhs.level()).map(|(a, b)| a.min(b)), Self::GeneralEqual { lhs, rhs }
| Self::GeneralLessEqual { lhs, rhs }
| Self::GeneralGreaterEqual { lhs, rhs }
| Self::GeneralNotEqual { lhs, rhs } => {
lhs.level().zip(rhs.level()).map(|(a, b)| a.min(b))
}
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => { Self::And(lhs, rhs) | Self::Or(lhs, rhs) => {
lhs.level().zip(rhs.level()).map(|(a, b)| a.min(b)) lhs.level().zip(rhs.level()).map(|(a, b)| a.min(b))
} }
@ -243,7 +278,10 @@ impl HasLevel for Predicate {
| Self::NotEqual { rhs, .. } => { | Self::NotEqual { rhs, .. } => {
rhs.set_level(level); rhs.set_level(level);
} }
Self::GeneralEqual { lhs, rhs } => { Self::GeneralEqual { lhs, rhs }
| Self::GeneralLessEqual { lhs, rhs }
| Self::GeneralGreaterEqual { lhs, rhs }
| Self::GeneralNotEqual { lhs, rhs } => {
lhs.set_level(level); lhs.set_level(level);
rhs.set_level(level); rhs.set_level(level);
} }
@ -293,6 +331,27 @@ impl Predicate {
} }
} }
pub fn general_ge(lhs: Predicate, rhs: Predicate) -> Self {
Self::GeneralGreaterEqual {
lhs: Box::new(lhs),
rhs: Box::new(rhs),
}
}
pub fn general_le(lhs: Predicate, rhs: Predicate) -> Self {
Self::GeneralLessEqual {
lhs: Box::new(lhs),
rhs: Box::new(rhs),
}
}
pub fn general_ne(lhs: Predicate, rhs: Predicate) -> Self {
Self::GeneralNotEqual {
lhs: Box::new(lhs),
rhs: Box::new(rhs),
}
}
pub fn call(receiver: TyParam, name: Option<Str>, args: Vec<TyParam>) -> Self { pub fn call(receiver: TyParam, name: Option<Str>, args: Vec<TyParam>) -> Self {
Self::Call { Self::Call {
receiver, receiver,
@ -462,6 +521,18 @@ impl Predicate {
lhs.change_subject_name(name.clone()), lhs.change_subject_name(name.clone()),
rhs.change_subject_name(name), rhs.change_subject_name(name),
), ),
Self::GeneralGreaterEqual { lhs, rhs } => Self::general_ge(
lhs.change_subject_name(name.clone()),
rhs.change_subject_name(name),
),
Self::GeneralLessEqual { lhs, rhs } => Self::general_le(
lhs.change_subject_name(name.clone()),
rhs.change_subject_name(name),
),
Self::GeneralNotEqual { lhs, rhs } => Self::general_ne(
lhs.change_subject_name(name.clone()),
rhs.change_subject_name(name),
),
_ => self, _ => self,
} }
} }
@ -482,6 +553,15 @@ impl Predicate {
Self::GeneralEqual { lhs, rhs } => { Self::GeneralEqual { lhs, rhs } => {
Self::general_eq(lhs.substitute(var, tp), rhs.substitute(var, tp)) Self::general_eq(lhs.substitute(var, tp), rhs.substitute(var, tp))
} }
Self::GeneralGreaterEqual { lhs, rhs } => {
Self::general_ge(lhs.substitute(var, tp), rhs.substitute(var, tp))
}
Self::GeneralLessEqual { lhs, rhs } => {
Self::general_le(lhs.substitute(var, tp), rhs.substitute(var, tp))
}
Self::GeneralNotEqual { lhs, rhs } => {
Self::general_ne(lhs.substitute(var, tp), rhs.substitute(var, tp))
}
Self::Call { Self::Call {
receiver, receiver,
name, name,
@ -539,7 +619,10 @@ impl Predicate {
| Self::GreaterEqual { rhs, .. } | Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. } | Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => rhs.qvars(), | Self::NotEqual { rhs, .. } => rhs.qvars(),
Self::GeneralEqual { lhs, rhs } => { Self::GeneralEqual { lhs, rhs }
| Self::GeneralLessEqual { lhs, rhs }
| Self::GeneralGreaterEqual { lhs, rhs }
| Self::GeneralNotEqual { lhs, rhs } => {
lhs.qvars().concat(rhs.qvars()).into_iter().collect() lhs.qvars().concat(rhs.qvars()).into_iter().collect()
} }
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => lhs.qvars().concat(rhs.qvars()), Self::And(lhs, rhs) | Self::Or(lhs, rhs) => lhs.qvars().concat(rhs.qvars()),
@ -558,7 +641,10 @@ impl Predicate {
| Self::GreaterEqual { rhs, .. } | Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. } | Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => rhs.has_qvar(), | Self::NotEqual { rhs, .. } => rhs.has_qvar(),
Self::GeneralEqual { lhs, rhs } => lhs.has_qvar() || rhs.has_qvar(), Self::GeneralEqual { lhs, rhs }
| Self::GeneralLessEqual { lhs, rhs }
| Self::GeneralGreaterEqual { lhs, rhs }
| Self::GeneralNotEqual { lhs, rhs } => lhs.has_qvar() || rhs.has_qvar(),
Self::Or(lhs, rhs) | Self::And(lhs, rhs) => lhs.has_qvar() || rhs.has_qvar(), Self::Or(lhs, rhs) | Self::And(lhs, rhs) => lhs.has_qvar() || rhs.has_qvar(),
Self::Not(pred) => pred.has_qvar(), Self::Not(pred) => pred.has_qvar(),
} }
@ -575,7 +661,10 @@ impl Predicate {
| Self::GreaterEqual { rhs, .. } | Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. } | Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => rhs.has_unbound_var(), | Self::NotEqual { rhs, .. } => rhs.has_unbound_var(),
Self::GeneralEqual { lhs, rhs } => lhs.has_unbound_var() || rhs.has_unbound_var(), Self::GeneralEqual { lhs, rhs }
| Self::GeneralLessEqual { lhs, rhs }
| Self::GeneralGreaterEqual { lhs, rhs }
| Self::GeneralNotEqual { lhs, rhs } => lhs.has_unbound_var() || rhs.has_unbound_var(),
Self::Or(lhs, rhs) | Self::And(lhs, rhs) => { Self::Or(lhs, rhs) | Self::And(lhs, rhs) => {
lhs.has_unbound_var() || rhs.has_unbound_var() lhs.has_unbound_var() || rhs.has_unbound_var()
} }
@ -595,7 +684,10 @@ impl Predicate {
| Self::GreaterEqual { rhs, .. } | Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. } | Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => rhs.has_undoable_linked_var(), | Self::NotEqual { rhs, .. } => rhs.has_undoable_linked_var(),
Self::GeneralEqual { lhs, rhs } => { Self::GeneralEqual { lhs, rhs }
| Self::GeneralLessEqual { lhs, rhs }
| Self::GeneralGreaterEqual { lhs, rhs }
| Self::GeneralNotEqual { lhs, rhs } => {
lhs.has_undoable_linked_var() || rhs.has_undoable_linked_var() lhs.has_undoable_linked_var() || rhs.has_undoable_linked_var()
} }
Self::Or(lhs, rhs) | Self::And(lhs, rhs) => { Self::Or(lhs, rhs) | Self::And(lhs, rhs) => {
@ -650,7 +742,10 @@ impl Predicate {
| Self::GreaterEqual { rhs, .. } | Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. } | Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => vec![rhs], | Self::NotEqual { rhs, .. } => vec![rhs],
Self::GeneralEqual { .. } => vec![], Self::GeneralEqual { .. }
| Self::GeneralLessEqual { .. }
| Self::GeneralGreaterEqual { .. }
| Self::GeneralNotEqual { .. } => vec![],
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => { Self::And(lhs, rhs) | Self::Or(lhs, rhs) => {
lhs.typarams().into_iter().chain(rhs.typarams()).collect() lhs.typarams().into_iter().chain(rhs.typarams()).collect()
} }