Struct term_rewriting::Rule

pub struct Rule {
    pub lhs: Term,
    pub rhs: Vec<Term>,
}

A rewrite rule equating a left-hand-side Term with one or more right-hand-side Terms.

Examples

let mut sig = Signature::default();

// Constructing a Rule manually
let a = parse_term(&mut sig, "A(B C)").expect("parse of A(B C)");
let b = parse_term(&mut sig, "B").expect("parse of B");
let c = parse_term(&mut sig, "C").expect("parse of C");

let r = Rule::new(a, vec![b, c]);

// When constructing rules manually, keep in mind that each call to
// ``parse_term`` uses a distinct set of variables.
let x0 = parse_term(&mut sig, "x_").expect("parse of x_");
let x1 = parse_term(&mut sig, "x_").expect("parse of x_");
let vars: Vec<_> = sig.variables().into_iter().map(Term::Variable).collect();

assert_eq!(x0, vars[0]);
assert_eq!(x1, vars[1]);
assert_ne!(x0, x1);

// Constructing a Rule using parser
let r = parse_rule(&mut sig, "A(x_ y_) = B(x_) | C(y)").expect("parse of A(x_ y_) = B(x_) | C(y_)");

Fields

lhs: Term

The left hand side (lhs) of the Rule.

rhs: Vec<Term>

The right hand sides (rhs) of the Rule.

Methods

impl Rule

pub fn display(&self) -> String

Serialize a Rule.

Examples

let mut sig = Signature::default();

let rule = parse_rule(&mut sig, "A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5) = CONS(A CONS(B(x_) CONS( SUCC(SUCC(ZERO)) NIL)))")
    .expect("parse of A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5) = CONS(A CONS(B(x_) CONS( SUCC(SUCC(ZERO)) NIL)))");

assert_eq!(rule.display(), ".(.(.(A B(x_)) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL)))) DECC(DECC(DIGIT(1) 0) 5)) = CONS(A CONS(B(x_) CONS(SUCC(SUCC(ZERO)) NIL)))");

pub fn pretty(&self) -> String

A human-readable serialization of the Rule.

Examples

let mut sig = Signature::default();

let rule = parse_rule(&mut sig, "A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5) = CONS(A CONS(B(x_) CONS( SUCC(SUCC(ZERO)) NIL)))")
    .expect("parse of A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5) = CONS(A CONS(B(x_) CONS( SUCC(SUCC(ZERO)) NIL)))");

assert_eq!(rule.pretty(), "A B(x_) [2, 1, 0] 105 = [A, B(x_), 2]");

pub fn size(&self) -> usize

The total number of subterms across all Terms in the Rule.

Examples

let mut sig = Signature::default();

let r = parse_rule(&mut sig, "A(x_) = B(x_) | C").expect("parse of A(x_) = B(x_) | C");

assert_eq!(r.size(), 5);

pub fn len(&self) -> usize

The number of RHSs in the Rule.

Examples

let mut sig = Signature::default();

let r = parse_rule(&mut sig, "A(x_) = B(x_) | C").expect("parse of A(x_) = B(x_) | C");

assert_eq!(r.len(), 2);

pub fn is_empty(&self) -> bool

Is the Rule empty?

Examples

let mut sig = Signature::default();

let r = parse_rule(&mut sig, "A(x_) = B(x_) | C").expect("parse of A(x_) = B(x_) | C");

assert!(!r.is_empty());

let lhs = parse_term(&mut sig, "A").expect("parse of A");
let rhs : Vec<Term> = vec![];
let r = Rule::new(lhs, rhs).unwrap();

assert!(r.is_empty());

pub fn rhs(&self) -> Option<Term>

The lone RHS, if it exists. Otherwise, return None.

Examples

let mut sig = Signature::default();

let r = parse_rule(&mut sig, "A = B").expect("parse of A = B");
let b = parse_term(&mut sig, "B").expect("parse of B");

assert_eq!(r.rhs().unwrap(), b);

let r = parse_rule(&mut sig, "A = B | C").expect("parse of A = B | C");

assert_eq!(r.rhs(), Option::None);

pub fn clauses(&self) -> Vec<Rule>

A list of the clauses in the Rule.

Examples

let mut sig = Signature::default();

let r = parse_rule(&mut sig, "A = B").expect("parse of A = B");

assert_eq!(r.clauses(), vec![r]);

let r = parse_rule(&mut sig, "A = B | C").expect("parse of A = B | C");
let r1 = parse_rule(&mut sig, "A = B").expect("parse of A = B");
let r2 = parse_rule(&mut sig, "A = C").expect("parse of A = C");

assert_eq!(r.clauses(), vec![r1, r2]);

pub fn new(lhs: Term, rhs: Vec<Term>) -> Option<Rule>

Construct a rewrite Rule from a left-hand-side (LHS) Term with one or more right-hand-side (RHS) Terms. Return None if the Rule is not valid.

Valid rules meet two conditions:

1. lhs is an Application. This prevents a single rule from matching all possible Terms
2. A Term in rhs can only use a Variable if it appears in lhs. This prevents rewrites from inventing arbitrary Terms.

Examples

let mut sig = Signature::default();

let lhs = parse_term(&mut sig, "A").expect("parse of A");
let rhs = vec![parse_term(&mut sig, "B").expect("parse of B")];
let r = Rule::new(lhs, rhs).unwrap();

let r2 = parse_rule(&mut sig, "A = B").expect("parse of A = B");

assert_eq!(r, r2);

let left = parse_term(&mut sig, "A").expect("parse of A");
let right = vec![parse_term(&mut sig, "B").expect("parse of B")];
let r2 = Rule { lhs: left, rhs: right };

assert_eq!(r, r2);

pub fn add(&mut self, t: Term)

Add a clause to the Rule from a Term.

Examples

let mut sig = Signature::default();

let c = parse_term(&mut sig, "C").expect("parse of C");
let mut r = parse_rule(&mut sig, "A = B").expect("parse of A = B");

assert_eq!(r.display(), "A = B");

r.add(c);

assert_eq!(r.display(), "A = B | C");

pub fn merge(&mut self, r: &Rule)

Add clauses to the Rule from another Rule.

Examples

let mut sig = Signature::default();

let mut r = parse_rule(&mut sig, "A(x_) = B").expect("parse A(x_) = B");
let r2 = parse_rule(&mut sig, "A(y_) = C(y_)").expect("parse A(y_) = C(y_)");
r.merge(&r2);

assert_eq!(r.display(), "A(x_) = B | C(x_)");

pub fn discard(&mut self, r: &Rule) -> Option<Rule>

Discard clauses from the Rule.

Examples

let mut sig = Signature::default();

let mut r = parse_rule(&mut sig, "A(x_) = B(x_) | C").expect("parse of A(x_) = B(x_) | C");
let mut r2 = parse_rule(&mut sig, "A(y_) = B(y_)").expect("parse of A(y_) = B(y_)");
r.discard(&r2);

assert_eq!(r.display(), "A(x_) = C");

pub fn contains<'a>(
    &'a self,
    r: &'a Rule
) -> Option<HashMap<&'a Variable, &'a Term>>

Check whether the Rule contains certain clauses, and if so, return the alpha-equivalence mapping.

Examples

let mut sig = Signature::default();

let mut r = parse_rule(&mut sig, "A(x_) = B(x_) | C").expect("parse of A(x_) = B(x_) | C");
let mut r2 = parse_rule(&mut sig, "A(y_) = B(y_)").expect("parse of A(y_) = B(y_)");

assert_eq!(r2.contains(&r), None);

let x = Term::Variable(r.variables()[0].clone());
let y = &r2.variables()[0];
let mut sub = HashMap::default();
sub.insert(y, &x);

assert_eq!(r.contains(&r2).unwrap(), sub);

pub fn variables(&self) -> Vec<Variable>

All the Variables in the Rule.

Examples

let mut sig = Signature::default();

let r = parse_rule(&mut sig, "A(x_) = C(x_)").expect("parse of A(x_) = C(x_)");
let r_variables: Vec<String> = r.variables().iter().map(|v| v.display()).collect();

assert_eq!(r_variables, vec!["x_"]);

let r = parse_rule(&mut sig, "B(y_ z_) = C").expect("parse of B(y_ z_) = C");
let r_variables: Vec<String> = r.variables().iter().map(|v| v.display()).collect();

assert_eq!(r_variables, vec!["y_", "z_"]);

pub fn operators(&self) -> Vec<Operator>

All the Operators in the Rule.

Examples

let mut sig = Signature::default();

let r = parse_rule(&mut sig, "A(D E) = C").expect("parse of A(D E) = C");
let r_ops: Vec<String> = r.operators().iter().map(|o| o.display()).collect();

assert_eq!(r_ops, vec!["D", "E", "A", "C"]);

let r = parse_rule(&mut sig, "B(F x_) = C").expect("parse of B(F x_) = C");
let r_ops: Vec<String> = r.operators().iter().map(|o| o.display()).collect();

assert_eq!(r_ops, vec!["F", "B", "C"]);

pub fn subterms(&self) -> Vec<(&Term, Place)>

All the subterms and places in a Rule.

See Term for more information.

Examples

let mut sig = Signature::default();

let r =
    parse_rule(&mut sig, "A(x_ B) = C(x_) | D(B)").expect("parse of A(x_ B) = C(x_) | D(B)");

let subterms: Vec<String> = r.subterms()
    .iter()
    .map(|(t, p)| format!("{}, {:?}", t.display(), p))
    .collect();

assert_eq!(
    subterms,
    vec![
        "A(x_ B), [0]",
        "x_, [0, 0]",
        "B, [0, 1]",
        "C(x_), [1]",
        "x_, [1, 0]",
        "D(B), [2]",
        "B, [2, 0]",
    ]
);

pub fn at(&self, p: &[usize]) -> Option<&Term>

Get a specific subterm in a Rule.

See Term::at for more information.

Examples

let mut sig = Signature::default();

let r = parse_rule(&mut sig, "A(x_) = B | C(x_)").expect("parse of A(x_) = B | C(x_)");

assert_eq!(r.at(&[0]).unwrap().display(), "A(x_)");
assert_eq!(r.at(&[0,0]).unwrap().display(), "x_");
assert_eq!(r.at(&[1]).unwrap().display(), "B");
assert_eq!(r.at(&[2]).unwrap().display(), "C(x_)");

pub fn replace(&self, place: &[usize], subterm: Term) -> Option<Rule>

Replace one subterm with another in a Rule. Returns a new Rule without changing the original.

See Term::at for more information.

Examples

let mut sig = Signature::default();

let mut r = parse_rule(&mut sig, "A(x_) = B | C(x_)").expect("parse of A(x_) = B| C(x_)");
let new_term = parse_term(&mut sig, "E").expect("parse of E");
let new_rule = r.replace(&[1], new_term);

assert_ne!(r, new_rule.clone().unwrap());

assert_eq!(new_rule.unwrap().display(), "A(x_) = E | C(x_)");

pub fn pmatch<'a>(
    r1: &'a Rule,
    r2: &'a Rule
) -> Option<HashMap<&'a Variable, &'a Term>>

Pattern Match one Rule against another.

Examples

let mut sig = Signature::default();

let r = parse_rule(&mut sig, "A(x_) = B").expect("parse of A(x_) = B");
let r2 = parse_rule(&mut sig, "A(y_) = y_").expect("parse of A(y_) = y_");
let r3 = parse_rule(&mut sig, "A(z_) = C").expect("parse of A(z_) = C");
let r4 = parse_rule(&mut sig, "D(w_) = B").expect("parse of D(w_) = B");
let r5 = parse_rule(&mut sig, "A(t_) = B").expect("parse of A(t_) = B");

assert_eq!(Rule::pmatch(&r, &r2), None);
assert_eq!(Rule::pmatch(&r, &r3), None);
assert_eq!(Rule::pmatch(&r, &r4), None);

let t_k = &r.variables()[0];
let t_v = Term::Variable(r5.variables()[0].clone());
let mut expected_map = HashMap::default();
expected_map.insert(t_k, &t_v);

assert_eq!(Rule::pmatch(&r, &r5), Some(expected_map));

pub fn unify<'a>(
    r1: &'a Rule,
    r2: &'a Rule
) -> Option<HashMap<&'a Variable, &'a Term>>

Unify two Rules.

Examples

let mut sig = Signature::default();

let r = parse_rule(&mut sig, "A(x_) = B").expect("parse of A(x_) = B");
let r2 = parse_rule(&mut sig, "A(y_) = y_").expect("parse of A(y_) = y_");
let r3 = parse_rule(&mut sig, "A(z_) = C").expect("parse of A(z_) = C");
let r4 = parse_rule(&mut sig, "D(w_) = B").expect("parse of D(w_) = B");
let r5 = parse_rule(&mut sig, "A(t_) = B").expect("parse of A(t_) = B");

let t_k0 = &r.variables()[0];
let t_k1 = &r2.variables()[0];
let b = parse_term(&mut sig, "B").expect("parse of B");
let mut expected_map = HashMap::default();
expected_map.insert(t_k0, &b);
expected_map.insert(t_k1, &b);

assert_eq!(Rule::unify(&r, &r2), Some(expected_map));

assert_eq!(Rule::unify(&r, &r3), None);
assert_eq!(Rule::unify(&r, &r4), None);

let t_k = &r.variables()[0];
let t_v = Term::Variable(r5.variables()[0].clone());
let mut expected_map = HashMap::default();
expected_map.insert(t_k, &t_v);

assert_eq!(Rule::unify(&r, &r5), Some(expected_map));

pub fn alpha<'a>(
    r1: &'a Rule,
    r2: &'a Rule
) -> Option<HashMap<&'a Variable, &'a Term>>

Compute the Alpha Equivalence between two Rules.

Examples

let mut sig = Signature::default();

let r = parse_rule(&mut sig, "A(x_) = B").expect("parse of A(x_) = B");
let r2 = parse_rule(&mut sig, "A(y_) = y_").expect("parse of A(y_) = y_");
let r3 = parse_rule(&mut sig, "A(z_) = C").expect("parse of A(z_) = C");
let r4 = parse_rule(&mut sig, "D(w_) = B").expect("parse of D(w_) = B");
let r5 = parse_rule(&mut sig, "A(t_) = B").expect("parse of A(t_) = B");

assert_eq!(Rule::alpha(&r, &r2), None);
assert_eq!(Rule::alpha(&r, &r3), None);
assert_eq!(Rule::alpha(&r, &r4), None);

let t_k = &r.variables()[0];
let t_v = Term::Variable(r5.variables()[0].clone());
let mut expected_map = HashMap::default();
expected_map.insert(t_k, &t_v);

assert_eq!(Rule::alpha(&r, &r5), Some(expected_map));

pub fn substitute(&self, sub: &HashMap<&Variable, &Term>) -> Rule

Substitute through a Rule.

Examples

let mut sig = Signature::default();

let mut r = parse_rule(&mut sig, "A(x_ y_) = A(x_) | B(y_)").expect("parse of A(x_ y_) = A(x_) | B(y_)");
let c = parse_term(&mut sig, "C").expect("parse of C");
let vars = r.variables();
let x = &vars[0];

let mut substitution = HashMap::default();
substitution.insert(x, &c);

let r2 = r.substitute(&substitution);

assert_eq!(r2.display(), "A(C y_) = A(C) | B(y_)");

Trait Implementations

impl PartialEq<Rule> for Rule

fn eq(&self, other: &Rule) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rule) -> bool

This method tests for !=.

impl From<Rule> for RuleContext

fn from(r: Rule) -> RuleContext

Performs the conversion.

impl Clone for Rule

fn clone(&self) -> Rule

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Eq for Rule

impl Debug for Rule

fn fmt(&self, f: &mut Formatter) -> Result

Formats the value using the given formatter.

impl Hash for Rule

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given [Hasher].