Enum term_rewriting::Context

pub enum Context {
    Hole,
    Variable(Variable),
    Application {
        op: Operator,
        args: Vec<Context>,
    },
}

A first-order Context: a Term that may have Holes; a sort of Term template.

Examples

let mut sig = Signature::default();

// Constructing a Context manually.
let a = sig.new_op(3, Some("A".to_string()));
let b = sig.new_op(0, Some("B".to_string()));
let x = sig.new_var(Some("x".to_string()));

let b_context = Context::Application { op: b, args: vec![] };
let x_context = Context::Variable(x);

let context = Context::Application { op: a, args: vec![ b_context, x_context, Context::Hole ] };

// Constructing a Context using the Parser.
let context2 = parse_context(&mut sig, "A(B x_ [!])").expect("parse of A(B x_ [!])");

assert_eq!(context.display(), context2.display());

Variants

Hole

An empty place in the Context.

Examples

// Constructing a hole manually.
let h = Context::Hole;

// Constructing a hole using the parser.
let mut sig = Signature::default();
let h2 = parse_context(&mut sig, "[!]").expect("parse of [!]");

assert_eq!(h.display(), h2.display());

Variable(Variable)

A concrete but unspecified Context (e.g. x, y)

Examples

let mut sig = Signature::default();

// Constructing a Context Variable manually.
let v = sig.new_var(Some("x".to_string()));
let var = Context::Variable(v);

//Contstructing a Context Variable using the parser.
let var2 = parse_context(&mut sig, "x_").expect("parse of x_");

assert_eq!(var.display(), var2.display());

Application

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

Examples

let mut sig = Signature::default();

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

// Constructing a Context Application using the parser.
let app2 = parse_context(&mut sig, "A").expect("parse of A");

assert_eq!(app, app2);

Fields of Application

op: Operatorargs: Vec<Context>

Methods

impl Context

pub fn display(&self) -> String

Serialize a Context.

Examples

let mut sig = Signature::default();

let context = parse_context(&mut sig, "x_ [!] A CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)")
    .expect("parse of x_ [!] A CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)") ;

assert_eq!(context.display(), ".(.(.(.(x_ [!]) A) CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL)))) DECC(DECC(DIGIT(1) 0) 5))");

pub fn pretty(&self) -> String

A human-readable serialization of the Context.

Examples

let mut sig = Signature::default();

let context = parse_context(&mut sig, "x_ [!] A CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)")
    .expect("parse of x_ [!] A CONS(SUCC(SUCC(ZERO)) CONS(SUCC(ZERO) CONS(ZERO NIL))) DECC(DECC(DIGIT(1) 0) 5)") ;

assert_eq!(context.pretty(), "x_ [!] A [2, 1, 0] 105");

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

Every Atom used in the Context.

Examples

let mut sig = Signature::default();

let context = parse_context(&mut sig, "A(B x_ [!])").expect("parse of A(B x_ [!])");

let atoms: Vec<String> = context.atoms().iter().map(|a| a.display()).collect();

assert_eq!(atoms, vec!["x_", "B", "A"]);

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

Every Variable used in the Context.

Examples

let mut sig = Signature::default();

let context = parse_context(&mut sig, "A([!]) B y_ z_").expect("parse of A([!]) B y_ z_");

let var_names: Vec<String> = context.variables().iter().map(|v| v.display()).collect();

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

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

Every Operator used in the Context.

Examples

let mut sig = Signature::default();

let context = parse_context(&mut sig, "A([!]) B y_ z_").expect("parse of A([!]) B y_ z_");

let op_names: Vec<String> = context.operators().iter().map(|v| v.display()).collect();

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

pub fn holes(&self) -> Vec<Place>

A list of the Places in the Context that are Holes.

Examples

let mut sig = Signature::default();

let context = parse_context(&mut sig, "A([!] B([!]) y_ z_)").expect("parse of A([!] B([!]) y_ z_)");

let p: &[usize] = &[0];
let p2: &[usize] = &[1, 0];

assert_eq!(context.holes(), vec![p, p2]);

pub fn head(&self) -> Option<Atom>

The head of the Context.

Examples

let mut sig = Signature::default();

let context = parse_context(&mut sig, "A(B([!]) z_)").expect("parse of A(B([!]) z_)");

assert_eq!(context.head().unwrap().display(), "A");

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

The args of the Context.

Examples

let mut sig = Signature::default();

let context = parse_context(&mut sig, "A B").expect("parse of A B");
let args: Vec<String> = context.args().iter().map(|arg| arg.display()).collect();

assert_eq!(args, vec!["A", "B"]);

let context = parse_context(&mut sig, "A(y_)").expect("parse of A(y_)");
let args: Vec<String> = context.args().iter().map(|arg| arg.display()).collect();

assert_eq!(args, vec!["y_"]);

pub fn subcontexts(&self) -> Vec<(&Context, Place)>

Every subcontext and its Place, starting with the original Context itself.

Examples

let mut sig = Signature::default();

let context = parse_context(&mut sig, "A(B [!])").expect("parse of A(B [!])");

let p: Vec<usize> = vec![];
let subcontext0 = parse_context(&mut sig, "A(B [!])").expect("parse of A(B [!])");

let p1: Vec<usize> = vec![0];
let subcontext1 = parse_context(&mut sig, "B").expect("parse of B");

let p2: Vec<usize> = vec![1];
let subcontext2 = Context::Hole;

assert_eq!(context.subcontexts(), vec![(&subcontext0, p), (&subcontext1, p1), (&subcontext2, p2)]);

pub fn size(&self) -> usize

The number of distinct Places in the Context.

Examples

let mut sig = Signature::default();
let context = parse_context(&mut sig, "A B").expect("parse of A B");

assert_eq!(context.size(), 3);

let context = parse_context(&mut sig, "A(B)").expect("parse of A(B)");

assert_eq!(context.size(), 2);

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

Get the subcontext at the given Place, or None if the Place does not exist.

Examples

let mut sig = Signature::default();
let context = parse_context(&mut sig, "B(A)").expect("parse of B(A)");

let p: &[usize] = &[7];

assert_eq!(context.at(p), None);

let p: &[usize] = &[0];

assert_eq!(context.at(p).unwrap().display(), "A");

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

Create a copy of the Context where the subcontext at the given Place has been replaced with subcontext.

Examples

let mut sig = Signature::default();

let context = parse_context(&mut sig, "B(A)").expect("parse of B(A)");
let context2 = parse_context(&mut sig, "C [!]").expect("parse of C [!]");

let p: &[usize] = &[0];
let new_context = context.replace(p, context2);

assert_eq!(new_context.unwrap().pretty(), "B(C [!])");

pub fn to_term(&self) -> Result<Term, ()>

Translate the Context into a Term, if possible.

Examples

let mut sig = Signature::default();

let context = parse_context(&mut sig, "A(B [!])").expect("parse of A(B [!])");

assert!(context.to_term().is_err());

let context = parse_context(&mut sig, "A(B C)").expect("parse of A(B C)");

let term = context.to_term().expect("converting context to term");

assert_eq!(term.display(), "A(B C)");

Trait Implementations

impl From<Term> for Context

fn from(t: Term) -> Context

Performs the conversion.

impl PartialEq<Context> for Context

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

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

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

This method tests for !=.

impl Clone for Context

fn clone(&self) -> Context

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Eq for Context

impl Debug for Context

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

Formats the value using the given formatter.

impl Hash for Context

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