use std::fmt;
#[allow(unused_imports)]
use erg_common::log;
use erg_common::set::Set;
use erg_common::{set, Str};
use super::free::{Constraint, HasLevel};
use super::typaram::TyParam;
use super::value::ValueObj;
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum Predicate {
Value(ValueObj), Const(Str),
Equal {
lhs: Str,
rhs: TyParam,
},
GreaterEqual {
lhs: Str,
rhs: TyParam,
},
LessEqual {
lhs: Str,
rhs: TyParam,
},
NotEqual {
lhs: Str,
rhs: TyParam,
},
Or(Box<Predicate>, Box<Predicate>),
And(Box<Predicate>, Box<Predicate>),
Not(Box<Predicate>),
}
impl fmt::Display for Predicate {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
Self::Value(v) => write!(f, "{v}"),
Self::Const(c) => write!(f, "{c}"),
Self::Equal { lhs, rhs } => write!(f, "{lhs} == {rhs}"),
Self::GreaterEqual { lhs, rhs } => write!(f, "{lhs} >= {rhs}"),
Self::LessEqual { lhs, rhs } => write!(f, "{lhs} <= {rhs}"),
Self::NotEqual { lhs, rhs } => write!(f, "{lhs} != {rhs}"),
Self::Or(l, r) => write!(f, "({l}) or ({r})"),
Self::And(l, r) => write!(f, "({l}) and ({r})"),
Self::Not(pred) => write!(f, "not({pred})"),
}
}
}
impl HasLevel for Predicate {
fn level(&self) -> Option<usize> {
match self {
Self::Value(_) | Self::Const(_) => None,
Self::Equal { rhs, .. }
| Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => rhs.level(),
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => {
lhs.level().zip(rhs.level()).map(|(a, b)| a.min(b))
}
Self::Not(pred) => pred.level(),
}
}
fn set_level(&self, level: usize) {
match self {
Self::Value(_) | Self::Const(_) => {}
Self::Equal { rhs, .. }
| Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => {
rhs.set_level(level);
}
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => {
lhs.set_level(level);
rhs.set_level(level);
}
Self::Not(pred) => {
pred.set_level(level);
}
}
}
}
impl Predicate {
pub const fn eq(lhs: Str, rhs: TyParam) -> Self {
Self::Equal { lhs, rhs }
}
pub const fn ne(lhs: Str, rhs: TyParam) -> Self {
Self::NotEqual { lhs, rhs }
}
pub const fn ge(lhs: Str, rhs: TyParam) -> Self {
Self::GreaterEqual { lhs, rhs }
}
pub fn gt(lhs: Str, rhs: TyParam) -> Self {
Self::and(Self::ge(lhs.clone(), rhs.clone()), Self::ne(lhs, rhs))
}
pub const fn le(lhs: Str, rhs: TyParam) -> Self {
Self::LessEqual { lhs, rhs }
}
pub fn lt(lhs: Str, rhs: TyParam) -> Self {
Self::and(Self::le(lhs.clone(), rhs.clone()), Self::ne(lhs, rhs))
}
pub fn and(lhs: Predicate, rhs: Predicate) -> Self {
Self::And(Box::new(lhs), Box::new(rhs))
}
pub fn or(lhs: Predicate, rhs: Predicate) -> Self {
Self::Or(Box::new(lhs), Box::new(rhs))
}
#[allow(clippy::should_implement_trait)]
pub fn not(pred: Predicate) -> Self {
Self::Not(Box::new(pred))
}
pub fn is_equal(&self) -> bool {
matches!(self, Self::Equal { .. })
}
pub fn subject(&self) -> Option<&str> {
match self {
Self::Equal { lhs, .. }
| Self::LessEqual { lhs, .. }
| Self::GreaterEqual { lhs, .. }
| Self::NotEqual { lhs, .. } => Some(&lhs[..]),
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => {
let l = lhs.subject();
let r = rhs.subject();
if l != r {
todo!()
} else {
l
}
}
Self::Not(pred) => pred.subject(),
_ => None,
}
}
pub fn change_subject_name(self, name: Str) -> Self {
match self {
Self::Equal { rhs, .. } => Self::eq(name, rhs),
Self::GreaterEqual { rhs, .. } => Self::ge(name, rhs),
Self::LessEqual { rhs, .. } => Self::le(name, rhs),
Self::NotEqual { rhs, .. } => Self::ne(name, rhs),
Self::And(lhs, rhs) => Self::and(
lhs.change_subject_name(name.clone()),
rhs.change_subject_name(name),
),
Self::Or(lhs, rhs) => Self::or(
lhs.change_subject_name(name.clone()),
rhs.change_subject_name(name),
),
Self::Not(pred) => Self::not(pred.change_subject_name(name)),
_ => self,
}
}
pub fn mentions(&self, name: &str) -> bool {
match self {
Self::Const(n) => &n[..] == name,
Self::Equal { lhs, .. }
| Self::LessEqual { lhs, .. }
| Self::GreaterEqual { lhs, .. }
| Self::NotEqual { lhs, .. } => &lhs[..] == name,
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => lhs.mentions(name) || rhs.mentions(name),
Self::Not(pred) => pred.mentions(name),
_ => false,
}
}
pub fn can_be_false(&self) -> bool {
match self {
Self::Value(l) => matches!(l, ValueObj::Bool(false)),
Self::Const(_) => todo!(),
Self::Or(lhs, rhs) => lhs.can_be_false() || rhs.can_be_false(),
Self::And(lhs, rhs) => lhs.can_be_false() && rhs.can_be_false(),
Self::Not(pred) => !pred.can_be_false(),
_ => true,
}
}
pub fn qvars(&self) -> Set<(Str, Constraint)> {
match self {
Self::Value(_) | Self::Const(_) => set! {},
Self::Equal { rhs, .. }
| Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => rhs.qvars(),
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => lhs.qvars().concat(rhs.qvars()),
Self::Not(pred) => pred.qvars(),
}
}
pub fn has_qvar(&self) -> bool {
match self {
Self::Value(_) => false,
Self::Const(_) => false,
Self::Equal { rhs, .. }
| Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => rhs.has_qvar(),
Self::Or(lhs, rhs) | Self::And(lhs, rhs) => lhs.has_qvar() || rhs.has_qvar(),
Self::Not(pred) => pred.has_qvar(),
}
}
pub fn has_unbound_var(&self) -> bool {
match self {
Self::Value(_) => false,
Self::Const(_) => false,
Self::Equal { rhs, .. }
| Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => rhs.has_unbound_var(),
Self::Or(lhs, rhs) | Self::And(lhs, rhs) => {
lhs.has_unbound_var() || rhs.has_unbound_var()
}
Self::Not(pred) => pred.has_unbound_var(),
}
}
pub fn min_max<'a>(
&'a self,
min: Option<&'a TyParam>,
max: Option<&'a TyParam>,
) -> (Option<&'a TyParam>, Option<&'a TyParam>) {
match self {
Predicate::Equal { rhs: _, .. } => todo!(),
Predicate::LessEqual { rhs, .. } => (
min,
max.map(|l: &TyParam| match l.cheap_cmp(rhs) {
Some(c) if c.is_ge() => l,
Some(_) => rhs,
_ => l,
})
.or(Some(rhs)),
),
Predicate::GreaterEqual { rhs, .. } => (
min.map(|l: &TyParam| match l.cheap_cmp(rhs) {
Some(c) if c.is_le() => l,
Some(_) => rhs,
_ => l,
})
.or(Some(rhs)),
max,
),
Predicate::And(_l, _r) => todo!(),
_ => todo!(),
}
}
pub fn typarams(&self) -> Vec<&TyParam> {
match self {
Self::Value(_) | Self::Const(_) => vec![],
Self::Equal { rhs, .. }
| Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => vec![rhs],
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => {
lhs.typarams().into_iter().chain(rhs.typarams()).collect()
}
Self::Not(pred) => pred.typarams(),
}
}
pub fn typarams_mut(&mut self) -> Vec<&mut TyParam> {
match self {
Self::Value(_) | Self::Const(_) => vec![],
Self::Equal { rhs, .. }
| Self::GreaterEqual { rhs, .. }
| Self::LessEqual { rhs, .. }
| Self::NotEqual { rhs, .. } => vec![rhs],
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => lhs
.typarams_mut()
.into_iter()
.chain(rhs.typarams_mut())
.collect(),
Self::Not(pred) => pred.typarams_mut(),
}
}
pub fn invert(self) -> Self {
match self {
Self::Value(ValueObj::Bool(b)) => Self::Value(ValueObj::Bool(!b)),
Self::Equal { lhs, rhs } => Self::ne(lhs, rhs),
Self::GreaterEqual { lhs, rhs } => Self::lt(lhs, rhs),
Self::LessEqual { lhs, rhs } => Self::gt(lhs, rhs),
Self::NotEqual { lhs, rhs } => Self::eq(lhs, rhs),
Self::Not(pred) => *pred,
other => Self::not(other),
}
}
}