Enum term_rewriting::Term

pub enum Term {
    Variable(Variable),
    Application {
        op: Operator,
        args: Vec<Term>,
    },
}

A first-order term: either a Variable or an application of an Operator.

Variants

Variable(Variable)

A concrete but unspecified Term (e.g. x, y)

Application

An Operator applied to zero or more Terms (e.g. (f(x, y), g())

Fields of Application

op: Operator
args: Vec<Term>

Methods

impl Term

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

Every Variable used in the term.

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

Every Operator used in the term.

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

Every subterm and its place, starting with the original term itself.

pub fn at(&self, place: &Place) -> Option<&Term>

Get the subterm at the given Place, or None if the place does not exist in the term.

pub fn replace(&self, place: &Place, subterm: Term) -> Option<Term>

Create a copy of self where the term at the given Place has been replaced with subterm.

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

Given a mapping from Variables to Terms, perform a substitution.

pub fn alpha_equivalent(t1: &Term, t2: &Term) -> bool

Whether two terms are alpha equivalent.

pub fn shape_equivalent(t1: &Term, t2: &Term) -> bool

pub fn pmatch(cs: Vec<(Term, Term)>) -> Option<HashMap<Variable, Term>>

Given a vector of contraints, return a substitution which satisfies the constrants. If the constraints are not satisfiable, None is retuned. Constraints are in the form of patterns, where substitutions are only considered for variables in the first term of each pair.

pub fn unify(cs: Vec<(Term, Term)>) -> Option<HashMap<Variable, Term>>

Given a vector of contraints, return a substitution which satisfies the constrants. If the constraints are not satisfiable, None is retuned.

Trait Implementations

impl From<Term> for Context

fn from(t: Term) -> Context

Performs the conversion.

impl Debug for Term

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

Formats the value using the given formatter.

impl PartialEq for Term

fn eq(&self, __arg_0: &Term) -> bool

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

fn ne(&self, __arg_0: &Term) -> bool

This method tests for !=.

impl Eq for Term

impl Hash for Term

fn hash<__H: Hasher>(&self, __arg_0: &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].

impl Clone for Term

fn clone(&self) -> Term

Returns a copy of the value.

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

Performs copy-assignment from source.