Struct term_rewriting::Signature

pub struct Signature { /* fields omitted */ }

Records a universe of symbols.

Use Signature::default for a blank signature, or Signature::new to initialize a signature with given operators.

Methods

impl Signature

pub fn new(
    operator_spec: Vec<(u32, Option<String>)>
) -> (Signature, Vec<Operator>)

Construct a signature with the given operators.

Each operator is specified in the form of (arity, Some(name)) or (arity, None), where arity is the number of arguments a term takes (for example, an arity of 0 gives a "constant" operator). A name for the operator is unnecessary, but may be supplied for more readable formatting.

The returned vector of Operators corresponds to the supplied spec.

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

Returns every Operator known to the signature, in the order they were created.

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

Returns every Variable known to the signature, in the order they were created.

pub fn new_op(&mut self, arity: u32, name: Option<String>) -> Operator

Create a new Operator distinct from all existing operators.

pub fn new_var(&mut self, name: Option<String>) -> Variable

Create a new Variable distinct from all existing variables.

pub fn merge(
    &mut self,
    other: Signature,
    strategy: MergeStrategy
) -> SignatureChange

Merge two signatures. All terms, contexts, rules, and TRSs associated with the other signature should be reified using methods provided by the returned SignatureChange.

Examples

let (mut sig1, _ops) = Signature::new(vec![
    (2, Some(".".to_string())),
    (0, Some("S".to_string())),
    (0, Some("K".to_string())),
]);
let mut sig2 = sig1.clone();

let s1 = "S K K";
let term = parse_term(&mut sig1, s1).unwrap();
let s2 = "S x_ y_ z_ = (x_ z_) (y_ z_);";
let trs = parse_trs(&mut sig2, s2).unwrap();

let sigchange = sig1.merge(sig2, MergeStrategy::SameOperators);
// we only reify terms/rules/TRSs associated with sig2
let trs = sigchange.reify_trs(trs);
// now term and rule both exist with symbols according to sig1.

Trait Implementations

impl Clone for Signature

fn clone(&self) -> Signature

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Signature

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

Formats the value using the given formatter.

impl Default for Signature

fn default() -> Signature

Returns the "default value" for a type.

impl PartialEq for Signature

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

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

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

This method tests for !=.