[−][src]Enum term_rewriting::Term
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 Term
s (e.g. (f(x, y)
, g()
).
A Term
that is an application of an Operator
with arity 0 applied to 0 Term
s 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
Methods
impl Term
[src]
pub fn display(&self) -> String
[src]
Serialize a Term
.
Examples
let mut sig = Signature::default(); let term = parse_term(&mut sig, "A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)") .expect("parse of A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)"); assert_eq!(term.display(), ".(.(.(A B(x_)) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL)))) DECC(DECC(DIGIT(1) 0) 5))");
pub fn pretty(&self) -> String
[src]
A human-readable serialization of the Term
.
Examples
let mut sig = Signature::default(); let term = parse_term(&mut sig, "A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)") .expect("parse of A B(x_) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)"); assert_eq!(term.pretty(), "A B(x_) [2, 1, 0] 105");
pub fn atoms(&self) -> Vec<Atom>
[src]
Every Atom
used in the Term
.
Examples
let mut sig = Signature::default(); let example_term = parse_term(&mut sig, "A(B x_)").expect("parse of A(B x_)"); let atoms: Vec<String> = example_term.atoms().iter().map(|a| a.display()).collect(); assert_eq!(atoms, vec!["x_", "B", "A"]);
pub fn variables(&self) -> Vec<Variable>
[src]
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 var_names: Vec<String> = t.variables().iter().map(|v| v.display()).collect(); assert_eq!(var_names, vec!["y_", "z_"]);
pub fn operators(&self) -> Vec<Operator>
[src]
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 op_names: Vec<String> = t.operators().iter().map(|v| v.display()).collect(); assert_eq!(op_names, vec!["A", "B", "."]);
pub fn head(&self) -> Atom
[src]
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>
[src]
The arguments of the Term
.
Examples
let mut sig = Signature::default(); let t = parse_term(&mut sig, "C(A B)").expect("parse of C(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.args(), vec![arg0, arg1]); let t2 = parse_term(&mut sig, "A").expect("parse of A"); assert_eq!(t2.args(), vec![]);
pub fn subterms(&self) -> Vec<(&Term, Place)>
[src]
Every subterm
and its Place
, starting with the Term
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.clone(), args: vec![Term::Application { op: b.clone(), args: vec![], }], }; let subterm1 = Term::Application { op: b.clone(), args: vec![], }; assert_eq!(t.subterms(), vec![(&subterm0, p), (&subterm1, p1)]);
pub fn size(&self) -> usize
[src]
The number of distinct Place
s in the Term
.
Examples
let mut sig = Signature::default(); let t = parse_term(&mut sig, "A B").expect("parse of A B"); assert_eq!(t.size(), 3); let t = parse_term(&mut sig, "A(B)").expect("parse of A(B)"); assert_eq!(t.size(), 2);
pub fn at(&self, place: &[usize]) -> Option<&Term>
[src]
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>
[src]
Create a copy of the Term
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 replace_all(&self, old_term: &Term, new_term: &Term) -> Term
[src]
Replace all occurrences of old_term
with new_term
pub fn shared_score(t1: &Term, t2: &Term) -> f64
[src]
Compute the percentage of shared subterms between two Term
s.
Examples
let mut sig = Signature::default(); let t1 = parse_term(&mut sig, "S (K y_ z_)").expect("parse of S K y_ z_"); let t2 = parse_term(&mut sig, "S (K w_ x_)").expect("parse of S K w_ x_"); let t3 = parse_term(&mut sig, "K (K w_ x_) S").expect("parse of S K w_ x_"); // Identical Terms assert_eq!(Term::shared_score(&t1, &t1), 1.0); // Alpha-equivalent Terms assert_eq!(Term::shared_score(&t1, &t2), 1.0); // Distinct Terms assert_eq!(Term::shared_score(&t1, &t3), 0.75);
pub fn substitute(&self, sub: &HashMap<&Variable, &Term>) -> Term
[src]
Given a mapping from Variable
s to Term
s, 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<'a>(
t1: &'a Term,
t2: &'a Term
) -> Option<HashMap<&'a Variable, &'a Term>>
[src]
t1: &'a Term,
t2: &'a Term
) -> Option<HashMap<&'a Variable, &'a Term>>
Compute the alpha equivalence for two Term
s.
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(), "y_".to_string()); assert_eq!(z.display(), "z_".to_string()); assert_eq!(a.display(), "a_".to_string()); assert_eq!(b.display(), "b_".to_string()); let ta = Term::Variable(a.clone()); let tb = Term::Variable(b.clone()); let mut expected_alpha: HashMap<&Variable, &Term> = HashMap::new(); expected_alpha.insert(y, &ta); expected_alpha.insert(z, &tb); 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
[src]
Returns whether two Term
s are shape equivalent.
Shape equivalence is where two Term
s 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<'a>(
cs: Vec<(&'a Term, &'a Term)>
) -> Option<HashMap<&'a Variable, &'a Term>>
[src]
cs: Vec<(&'a Term, &'a Term)>
) -> Option<HashMap<&'a Variable, &'a 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.
For more information see Pattern Matching
.
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 t_k = &t2.variables()[0]; let t_v = Term::Variable(t3.variables()[0].clone()); let mut expected_sub = HashMap::new(); // maps variable x in term t2 to variable y in term t3 expected_sub.insert(t_k, &t_v); assert_eq!(Term::pmatch(vec![(&t2, &t3)]), Some(expected_sub)); assert_eq!(Term::pmatch(vec![(&t3, &t4)]), None);
pub fn unify<'a>(
cs: Vec<(&'a Term, &'a Term)>
) -> Option<HashMap<&'a Variable, &'a Term>>
[src]
cs: Vec<(&'a Term, &'a Term)>
) -> Option<HashMap<&'a Variable, &'a Term>>
Given a vector of contraints, return a substitution which satisfies the constrants.
If the constraints are not satisfiable, return None
.
For more information see Unification
.
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 t_k = &t2.variables()[0]; let t_v = Term::Application { op: t.operators()[0].clone(), args:vec![], }; let mut expected_sub = HashMap::new(); // maps variable x in term t2 to constant A in term t expected_sub.insert(t_k, &t_v); assert_eq!(Term::unify(vec![(&t, &t2)]), Some(expected_sub)); let t_v = Term::Variable(t3.variables()[0].clone()); let mut expected_sub = HashMap::new(); // maps variable x in term t2 to variable y in term t3 expected_sub.insert(t_k, &t_v); 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
[src]
impl PartialEq<Term> for Term
[src]
impl Clone for Term
[src]
fn clone(&self) -> Term
[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]
Performs copy-assignment from source
. Read more
impl Eq for Term
[src]
impl Debug for Term
[src]
impl Hash for Term
[src]
Auto Trait Implementations
Blanket Implementations
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> From<T> for T
[src]
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,