Struct Trs 

pub struct Trs {
    pub rules: Vec<Rule>,
}

A Term Rewriting System: a list of rewrite rules.

Fields

rules: Vec<Rule>

Implementations

impl Trs

pub fn new() -> Self

Creates an empty TRS.

pub fn add_rule(&mut self, rule: Rule)

Adds a rule to the TRS.

pub fn is_left_linear(&self) -> bool

Returns true if all rules are left-linear.

pub fn reduce_innermost(&self, term: &Term) -> Option<Term>

One-step innermost reduction: reduces the leftmost-innermost redex.

pub fn reduce_outermost(&self, term: &Term) -> Option<Term>

One-step outermost reduction: reduces the leftmost-outermost redex.

pub fn normalize_innermost(&self, term: &Term, limit: usize) -> Term

Fully reduces a term to normal form under innermost strategy (up to limit steps).

pub fn normalize_outermost(&self, term: &Term, limit: usize) -> Term

Fully reduces a term to normal form under outermost strategy (up to limit steps).

pub fn is_normal_form(&self, t: &Term) -> bool

Checks whether t is a normal form (no rule applies at any position).

Trait Implementations

impl Clone for Trs

fn clone(&self) -> Trs

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Trs

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

Formats the value using the given formatter.

impl Default for Trs

fn default() -> Trs

Returns the “default value” for a type.