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). See Variable for more information.

Examples

let mut sig = Signature::default();

// Constructing a Variable manually
let var = sig.new_var(Some("x_".to_string()));
let var_term = Term::Variable(var);

// Constructing a Variable using the parser
let var = parse_term(&mut sig, "x_");

Application

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

A Term that is an application of an Operator with arity 0 applied to 0 Terms can be considered a constant.

Examples

let mut sig = Signature::default();

// Constructing a Constant manually
let a = sig.new_op(0, Some("A".to_string()));
let const_term = Term::Application {
    op: a,
     args: vec![],
};

// Constructing a Constant using the parser
let const_term = parse_term(&mut sig, "A");

// Constructing an Application manually
let x = sig.new_var(Some("x_".to_string()));
let b = sig.new_op(1, Some("B".to_string()));
let op_term = Term::Application {
    op: b,
    args: vec![Term::Variable(x)],
};

// Constructing an Application using the parser
let op_term = parse_term(&mut sig, "B(x_)");

Fields of Application

op: Operator
args: Vec<Term>

Methods

impl Term

pub fn display(&self, sig: &Signature) -> String

A serialized representation of the Term.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "A(B x_)").expect("parse of A(B x_)");

assert_eq!(t.display(&sig), "A(B x_)".to_string());

pub fn pretty(&self, sig: &Signature) -> String

A human-readable serialization of the Term.

pub fn atoms(&self) -> Vec<Atom>

Every Atom used in the term.

Examples

//A(B x_)
let mut sig = Signature::default();
let x = sig.new_var(Some("x".to_string()));
let a = sig.new_op(2, Some("A".to_string()));
let b = sig.new_op(0, Some("B".to_string()));

let example_term = Term::Application {
    op: a,
    args: vec![
        Term::Application{ op: b, args: vec![] },
        Term::Variable(x),
    ],
};
let expected_atoms = vec![
    Atom::Variable(x),
    Atom::Operator(b),
    Atom::Operator(a),
];

assert_eq!(example_term.atoms(), expected_atoms);

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

Every Variable used in the Term.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "A B y_ z_").expect("parse of A B y_ z_");

let vars = t.variables();
let var_names: Vec<String> = vars.iter().map(|v| v.display(&sig)).collect();

assert_eq!(var_names, vec!["y_".to_string(), "z_".to_string()]);

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

Every Operator used in the Term.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "A B y_ z_").expect("parse of A B y_ z_");

let ops = t.operators();
let op_names: Vec<String> = ops.iter().map(|v| v.display(&sig)).collect();

assert_eq!(
    op_names,
     vec!["A".to_string(), "B".to_string(), ".".to_string()]
);

pub fn head(&self) -> Atom

The head of the Term.

Examples

let mut sig = Signature::default();

let op = sig.new_op(2, Some("A".to_string()));
let t = parse_term(&mut sig, "A(B z_)").expect("parse of A(B z_)");

assert_eq!(t.atoms().len(), 3);
assert_eq!(t.head(), Atom::Operator(op));

pub fn args(&self) -> Vec<Term>

The arguments of the Term.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "A B").expect("parse of A B");
let arg0 = parse_term(&mut sig, "A").expect("parse of A");
let arg1 = parse_term(&mut sig, "B").expect("parse of B");
assert_eq!(t.atoms().len(), 3);
assert_eq!(t.args(), vec![arg0, arg1]);

let t2 = parse_term(&mut sig, "A").expect("parse of A");
assert_eq!(t2.atoms().len(), 1);
assert_eq!(t2.args(), vec![]);

let t3 = parse_term(&mut sig, "A(y_)").expect("parse of A(y_)");
let arg = Term::Variable(t3.variables()[0]);
assert_eq!(t3.atoms().len(), 2);
assert_eq!(t3.args(), vec![arg]);

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

Every subterm and its Place, starting with self and the empty Place.

Examples

let mut sig = Signature::default();
let b = sig.new_op(0, Some("B".to_string()));
let a = sig.new_op(1, Some("A".to_string()));

let p: Vec<usize> = vec![];
let p1: Vec<usize> = vec![0];
let t = parse_term(&mut sig, "A(B)").expect("parse of A(B)");
let subterm0 = Term::Application {
    op: a,
    args: vec![Term::Application {
        op: b,
        args: vec![],
    }],
};
let subterm1 = Term::Application {
    op: b,
    args: vec![],
};

assert_eq!(t.subterms(), vec![(&subterm0, p), (&subterm1, p1)]);

pub fn size(&self) -> usize

The number of distinct Places in the Term.

Examples

let mut sig = Signature::default();
let t = parse_term(&mut sig, "A B").expect("parse of A B");
let t2 = parse_term(&mut sig, "A(B)").expect("parse of A(B)");

assert_eq!(t.size(), 3);
assert_eq!(t2.size(), 2);

pub fn at(&self, place: &[usize]) -> Option<&Term>

Get the subterm at the given Place if possible. Otherwise, return None.

Examples

let mut sig = Signature::default();
let op = sig.new_op(0, Some("A".to_string()));
let t = parse_term(&mut sig, "B(A)").expect("parse of B(A)");

assert_eq!(t.size(), 2);
let p: &[usize] = &[7];
assert_eq!(t.at(p), None);

let p: &[usize] = &[0];
let args = vec![];
assert_eq!(t.at(p), Some(&Term::Application { op, args }));

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

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

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "B(A)").expect("parse of B(A)");
let t2 = parse_term(&mut sig, "C").expect("parse of C");
let expected_term = parse_term(&mut sig, "B(C)").expect("parse of B(C)");

let p: &[usize] = &[0];
let new_term = t.replace(p, t2);

assert_eq!(new_term, Some(expected_term));

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

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

Examples

let mut sig = Signature::default();

let term_before = parse_term(&mut sig, "S K y_ z_").expect("parse of S K y_ z_");
let s_term = parse_term(&mut sig, "S").expect("parse of S");
let k_term = parse_term(&mut sig, "K").expect("parse of K");

let vars = sig.variables();
let y = vars[0];
let z = vars[1];

let mut sub = HashMap::new();
sub.insert(y, s_term);
sub.insert(z, k_term);

let expected_term = parse_term(&mut sig, "S K S K").expect("parse of S K S K");
let subbed_term = term_before.substitute(&sub);

assert_eq!(subbed_term, expected_term);

pub fn alpha(t1: &Term, t2: &Term) -> Option<HashMap<Variable, Term>>

Compute the alpha equivalence for two Terms.

Examples

let mut sig = Signature::default();
let s = sig.new_op(0, Some("S".to_string()));

let t = parse_term(&mut sig, "S K y_ z_").expect("parse of S K y_ z_");
let t2 = parse_term(&mut sig, "S K a_ b_").expect("parse of S K a_ b_");
let t3 = parse_term(&mut sig, "S K y_").expect("parse of S K y_");

let vars = sig.variables();
let (y, z, a, b) = (vars[0], vars[1], vars[2], vars[3]);

assert_eq!(y.display(&sig), "y_".to_string());
assert_eq!(z.display(&sig), "z_".to_string());
assert_eq!(a.display(&sig), "a_".to_string());
assert_eq!(b.display(&sig), "b_".to_string());

let mut expected_alpha: HashMap<Variable, Term> = HashMap::new();
expected_alpha.insert(y, Term::Variable(a));
expected_alpha.insert(z, Term::Variable(b));

assert_eq!(Term::alpha(&t, &t2), Some(expected_alpha));
assert_eq!(Term::alpha(&t, &t3), None);

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

Returns whether two Terms are shape equivalent.

Shape equivalence is where two Terms may not contain the same subterms, but they share the same structure(a.k.a. shape).

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "S K y_ z_").expect("parse of S K y_ z_");
let t2 = parse_term(&mut sig, "A B x_ w_").expect("parse of A B x_ w_");
let t3 = parse_term(&mut sig, "S K y_").expect("parse of S K y_");

assert!(Term::shape_equivalent(&t, &t2));
assert!(!Term::shape_equivalent(&t, &t3));

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, return None. Constraints are in the form of patterns, where substitutions are only considered for variables in the first term of each pair.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "C(A)").expect("parse of C(A)");

let t2 = parse_term(&mut sig, "C(x_)").expect("parse of C(x_)");

let t3 = parse_term(&mut sig, "C(y_)").expect("parse of C(y_)");

let t4 = parse_term(&mut sig, "A(x_)").expect("parse of A(x_)");

assert_eq!(Term::pmatch(vec![(t, t2)]), None);

let mut expected_sub = HashMap::new();
// maps variable x in term t2 to variable y in term t3
expected_sub.insert(t2.variables()[0], Term::Variable(t3.variables()[0]));
assert_eq!(Term::pmatch(vec![(t2, t3)]), Some(expected_sub));

assert_eq!(Term::pmatch(vec![(t3, t4)]), None);

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, return None.

Examples

let mut sig = Signature::default();

let t = parse_term(&mut sig, "C(A)").expect("parse of C(A)");

let t2 = parse_term(&mut sig, "C(x_)").expect("parse of C(x_)");

let t3 = parse_term(&mut sig, "C(y_)").expect("parse of C(y_)");

let t4 = parse_term(&mut sig, "B(x_)").expect("parse of B(x_)");

let mut expected_sub = HashMap::new();
// maps variable x in term t2 to constant A in term t
expected_sub.insert(
    t2.variables()[0],
    Term::Application {
        op: t.operators()[0],
        args:vec![],
    },
);
assert_eq!(Term::unify(vec![(t, t2)]), Some(expected_sub));

let mut expected_sub = HashMap::new();
// maps variable x in term t2 to variable y in term t3
expected_sub.insert(t2.variables()[0], Term::Variable(t3.variables()[0]));
assert_eq!(Term::unify(vec![(t2, t3)]), Some(expected_sub));

assert_eq!(Term::unify(vec![(t3, t4)]), None);

Trait Implementations

impl From<Term> for Context

fn from(t: Term) -> Context

Performs the conversion.

impl Debug for Term

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

Formats the value using the given formatter.

impl PartialEq 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 Eq for Term

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