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.

Variants

Hole

An empty place in the Context.

Examples

// How to construct a hole manually
let h = Context::Hole;

Variable(Variable)

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

Examples

let mut sig = Signature::default();

// How to construct a Context Variable manually
let v = sig.new_var(Some("x_".to_string()));
let var = Context::Variable(v);

Application

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

Examples

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

Fields of Application

op: Operator
args: Vec<Context>

Methods

impl Context

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

A serialized representation of the Context.

Examples

let mut sig = Signature::default();

let h = Context::Hole;
assert_eq!(h.display(&sig), "[!]".to_string());

let var = sig.new_var(Some("y".to_string()));
let context_var = Context::Variable(var);
assert_eq!(context_var.display(&sig), "y_".to_string());

let op = sig.new_op(0,Some("S".to_string()));
let args = vec![];
let context_app = Context::Application {op, args};
assert_eq!(context_app.display(&sig), "S".to_string());

let var = sig.new_var(Some("x".to_string()));
let a = sig.new_op(2, Some("A".to_string()));
let example_context = Context::Application {
    op: a,
    args: vec![Context::Hole, Context::Variable(var)],
};
assert_eq!(example_context.display(&sig), "A([!] x_)".to_string());

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

A human-readable serialization of the Context.

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

Every Atom used in self.

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

Every Variable used in self.

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

Every Operator used in self.

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

A list of the Places in self that are holes.

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

The head of the Context.

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

The args of the Context.

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

Every subcontext and its place, starting with the original context itself.

pub fn size(&self) -> usize

The number of distinct Places in self.

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

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

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

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

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

Translate self into a Term, if possible.

Trait Implementations

impl Debug for Context

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

Formats the value using the given formatter.

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

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

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 From<Term> for Context

fn from(t: Term) -> Context

Performs the conversion.