[−][src]Trait razor_fol::transform::TermBased

pub trait TermBased {
    fn transform(&self, f: &impl Fn(&Term) -> Term) -> Self;

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

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

Is the trait of objects constructed atop Terms.

Required methods

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

Applies a transformation function f on the Terms of the receiver.

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

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

Example:

use razor_fol::transform::TermBased;
use std::collections::HashMap;

// variable symbols:
let x_sym = V::from("x");
let y_sym = V::from("y");
let z_sym = V::from("z");
let a_sym = V::from("a");
let b_sym = V::from("b");

// A variable renaming map that renames variable `x` to `a` and variable `y` to `b`
let mut renaming = HashMap::new();
renaming.insert(&x_sym, a_sym);
renaming.insert(&y_sym, b_sym);

let x = Term::from(x_sym.clone());
let y = Term::from(y_sym.clone());
let z = Term::from(z_sym.clone());
let f = F::from("f");
let g = F::from("g");

// t = f(x, z, g(x, y, x))
let t = f.app3(x.clone(), z.clone(), g.app3(x.clone(), y.clone(), x.clone()));

let s = t.rename_vars(&renaming); // s = f(a, z, g(a, b, a))
assert_eq!("f(a, z, g(a, b, a))", s.to_string())

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

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

Example:

use razor_fol::transform::TermBased;

// A substitution function that maps all variable symbols `x` to a constant term `c`.
// Otherwise, wraps the variable symbol in a variable term.
fn x_to_c(v: &V) -> Term {
    let x = V::from("x");
    let c = C::from("c");

    if v == &x {
        Term::from(c)
    } else {
        Term::from(v.clone())
    }
}

let x = Term::from(V::from("x"));
let y = Term::from(V::from("y"));
let f = F::from("f");
let g = F::from("g");

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

let s = t.substitute(&x_to_c); // s = f('c, g('c, y, 'c))
assert_eq!("f('c, g('c, y, 'c))", s.to_string())
Loading content...

Implementors

impl TermBased for Formula[src]

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

Note: Applies a VariableRenaming on the free variables of the formula, keeping the bound variables unchanged.

fn substitute(&self, substitution: &impl Substitution) -> Self[src]

Note: Applies a Substitution on the free variables of the formula, keeping the bound variables unchanged.

impl TermBased for Term[src]

Loading content...