[−][src]Struct term_rewriting::Rule
A rewrite rule equating a left-hand-side Term
with one or more
right-hand-side Term
s.
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
[src]
pub fn display(&self) -> String
[src]
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
[src]
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
[src]
The total number of subterms across all Term
s 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
[src]
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
[src]
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>
[src]
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>
[src]
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>
[src]
Construct a rewrite Rule
from a left-hand-side (LHS) Term
with one
or more right-hand-side (RHS) Term
s. Return None
if the Rule
is
not valid.
Valid rules meet two conditions:
lhs
is anApplication
. This prevents a single rule from matching all possibleTerm
s- A
Term
inrhs
can only use aVariable
if it appears inlhs
. This prevents rewrites from inventing arbitraryTerm
s.
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)
[src]
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)
[src]
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>
[src]
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>>
[src]
&'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>
[src]
All the Variable
s 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>
[src]
All the Operator
s 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)>
[src]
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>
[src]
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>
[src]
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>>
[src]
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>>
[src]
r1: &'a Rule,
r2: &'a Rule
) -> Option<HashMap<&'a Variable, &'a Term>>
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>>
[src]
r1: &'a Rule,
r2: &'a Rule
) -> Option<HashMap<&'a Variable, &'a Term>>
Compute the Alpha Equivalence
between two Rule
s.
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
[src]
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 From<Rule> for RuleContext
[src]
fn from(r: Rule) -> RuleContext
[src]
impl PartialEq<Rule> for Rule
[src]
impl Clone for Rule
[src]
fn clone(&self) -> Rule
[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]
Performs copy-assignment from source
. Read more
impl Eq for Rule
[src]
impl Debug for Rule
[src]
impl Hash for Rule
[src]
Auto Trait Implementations
Blanket Implementations
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> From<T> for T
[src]
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,