Struct term_rewriting::SignatureChange

pub struct SignatureChange { /* fields omitted */ }

Allows Terms/Rules/TRSs to be reified for use with another Signature. See Signature::merge.

Examples

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

let term = parse_term(&mut sig2, "A B").unwrap();

assert_eq!(term.pretty(), "A B");

let sigchange = sig1.merge(&sig2, MergeStrategy::OperatorsByArityAndName).unwrap();

let ops: Vec<String> = sig1.operators().iter().map(|op| op.display()).collect();

assert_eq!(ops, vec![".", "S", "K", "A", "B"]);

let term = sigchange.reify_term(&sig1, term);

assert_eq!(term.pretty(), "A B");

Methods

impl SignatureChange

pub fn reify_term(&self, sig: &Signature, term: Term) -> Term

Reifies Term for use with another Signature.

Examples

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

let term = parse_term(&mut sig2, "A B").unwrap();

let sigchange = sig1.merge(&sig2, MergeStrategy::DistinctOperators).unwrap();

let term = sigchange.reify_term(&sig1, term);

assert_eq!(term.pretty(), "A B");

pub fn reify_context(&self, sig: &Signature, context: Context) -> Context

Reifies Context for use with another Signature.

Examples

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

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

let sigchange = sig1.merge(&sig2, MergeStrategy::OperatorsByArityAndName).unwrap();

let context = sigchange.reify_context(&sig1, context);

assert_eq!(context.pretty(), "A([!], B)");

pub fn reify_rule(&self, sig: &Signature, rule: Rule) -> Rule

Reifies Rule for use with another Signature.

Examples

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

let rule = parse_rule(&mut sig2, "A = B | C").unwrap();

let sigchange = sig1.merge(&sig2, MergeStrategy::OperatorsByArityAndName).unwrap();

let rule = sigchange.reify_rule(&sig1, rule);

assert_eq!(rule.pretty(), "A = B | C");

pub fn reify_trs(&self, sig: &Signature, trs: TRS) -> TRS

Reifies TRS for use with another Signature.

Examples

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

let trs = parse_trs(&mut sig2,
"A = B;
C = B;").unwrap();

let sigchange = sig1.merge(&sig2, MergeStrategy::OperatorsByArityAndName).unwrap();

let trs = sigchange.reify_trs(&sig1, trs);

assert_eq!(trs.pretty(),
"A = B;
C = B;");