Struct RewriteRule 

pub struct RewriteRule {
    pub lhs: Term,
    pub rhs: Term,
    pub name: String,
}

A rewrite rule: lhs → rhs.

Fields

lhs: Term

rhs: Term

name: String

Implementations

impl RewriteRule

pub fn new(name: &str, lhs: Term, rhs: Term) -> Self

Create a new rewrite rule.

pub fn match_term<'a>( pattern: &'a Term, target: &'a Term, subst: &mut Vec<(usize, Term)>, ) -> bool

Attempt to match pattern against target, binding variables. Returns Some(substitution) if match succeeds; each entry is (var_idx, term).

pub fn apply_subst(term: &Term, subst: &[(usize, Term)]) -> Term

Apply the substitution to a term.

pub fn try_apply_top(&self, t: &Term) -> Option<Term>

Try to apply this rule at the top level of t. Returns Some(rewritten) if the rule fires; None otherwise.

Trait Implementations

impl Clone for RewriteRule

fn clone(&self) -> RewriteRule

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RewriteRule

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

Formats the value using the given formatter.