Skip to main content

TermBased

razor_fol::transform

Trait TermBased 

Source 
pub trait TermBased {
    // Required methods
    fn transform(&self, f: &impl Fn(&Term) -> Term) -> Self;
    fn rename_vars(&self, renaming: &impl VariableRenaming) -> Self;
    fn substitute(&self, sub: &impl Substitution) -> Self;
}
Expand description

Is the trait of objects constructed atop Terms.

Required Methods§

Source

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

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

Source

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())
Source

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())

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§