Enum razor_fol::syntax::Term

pub enum Term {
    Var {
        variable: V,
    },
    Const {
        constant: C,
    },
    App {
        function: F,
        terms: Vec<Term>,
    },
}

Represents a first-order term and consists of variables, constants and function applications.

Variants

Var

Is a variable term, wrapping a variable symbol.

Fields of Var

variable: V

Const

Is a constant term, wrapping a constant symbol.

Fields of Const

constant: C

App

Is a composite term, made by applying a function on a list of terms.

Fields of App

function: Fterms: Vec<Term>

Methods

impl Term

pub fn free_vars(&self) -> Vec<&V>

Returns a list of all free variable symbols in the term.

Note: In the list of free variables, each variable symbol appears only once even if it is present at multiple positions of the receiver term.

Example:

// `x_sym` and `y_sym` are variable symbols:
let x_sym = V::from("x");
let y_sym = V::from("y");

// `c_sym` is a constant symbol:
let c_sym = C::from("c");

// `x` and `y` are variable terms:
let x = Term::from(x_sym.clone());
let y = Term::from(y_sym.clone());

// `c` is a constant term:
let c = Term::from(c_sym.clone());

// `f` and `g` are function
let f = F::from("f");
let g = F::from("g");

// f(x, g(y, c, x)):
let t = f.app2(x.clone(), g.app3(y, c, x.clone()));

// comparing the two (unordered) lists:
assert_eq!(vec![&x_sym, &y_sym].iter().sorted(), t.free_vars().iter().sorted())

pub fn equals(self, term: Term) -> Formula

Returns an equation (formula) between the receiver and term.

Trait Implementations

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.

impl Debug for Term

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

Formats the value using the given formatter.

impl Display for Term

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

Formats the value using the given formatter.

impl Eq for Term

impl FApp for Term

fn apply(function: F, terms: Vec<Term>) -> Self

Builds a composite term by applying function on terms as arguments.

impl From<C> for Term

fn from(constant: C) -> Self

Performs the conversion.

impl From<V> for Term

fn from(variable: V) -> Self

Performs the conversion.

impl Hash for Term

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].

impl Ord for Term

fn cmp(&self, other: &Term) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

🔬 This is a nightly-only experimental API. (clamp)

Restrict a value to a certain interval.

impl PartialEq<Term> for Term

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

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

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

This method tests for !=.

impl PartialOrd<Term> for Term

fn partial_cmp(&self, other: &Term) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Term) -> bool

This method tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Term) -> bool

This method tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Term) -> bool

This method tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Term) -> bool

This method tests greater than or equal to (for self and other) and is used by the >= operator.

impl StructuralEq for Term

impl StructuralPartialEq for Term

impl TermBased for Term

fn transform(&self, f: &impl Fn(&Term) -> Term) -> Self

Applies a transformation function f on the [Term]s of the receiver.

fn rename_vars(&self, renaming: &impl VariableRenaming) -> Self

Applies a [VariableRenaming] on the variable sub-terms of the receiver.

fn substitute(&self, sub: &impl Substitution) -> Self

Applies a [Substitution] on the variable sub-terms of the receiver.