conjure_core/rules/normalisers/
eq_neq.rs

1//! Normalising rules for `Neq` and `Eq`.
2
3use conjure_core::ast::Expression as Expr;
4use conjure_core::metadata::Metadata;
5use conjure_core::rule_engine::{
6    register_rule, ApplicationError::RuleNotApplicable, ApplicationResult, Reduction,
7};
8
9use Expr::*;
10
11use crate::ast::SymbolTable;
12
13/// Converts a negated `Neq` to an `Eq`
14///
15/// ```text
16/// not(neq(x)) ~> eq(x)
17/// ```
18#[register_rule(("Base", 8800))]
19fn negated_neq_to_eq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
20    match expr {
21        Not(_, a) => match a.as_ref() {
22            Neq(_, b, c) if (b.is_safe() && c.is_safe()) => {
23                Ok(Reduction::pure(Eq(Metadata::new(), b.clone(), c.clone())))
24            }
25            _ => Err(RuleNotApplicable),
26        },
27        _ => Err(RuleNotApplicable),
28    }
29}
30
31/// Converts a negated `Neq` to an `Eq`
32///
33/// ```text
34/// not(eq(x)) ~> neq(x)
35/// ```
36#[register_rule(("Base", 8800))]
37fn negated_eq_to_neq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
38    match expr {
39        Not(_, a) => match a.as_ref() {
40            Eq(_, b, c) if (b.is_safe() && c.is_safe()) => {
41                Ok(Reduction::pure(Neq(Metadata::new(), b.clone(), c.clone())))
42            }
43            _ => Err(RuleNotApplicable),
44        },
45        _ => Err(RuleNotApplicable),
46    }
47}
conjure_core/rules/normalisers/eq_neq.rs

conjure_core/rules/normalisers/
eq_neq.rs
