Module term_rewriting::trace

Record sequences of rewrites.

Examples

A TRS with mutually exclusive rules gives a straightfoward linear record of rewrites:

use term_rewriting::{parse, trace::Trace, Signature, Strategy};

let mut sig = Signature::default();
let inp = "
    PLUS(SUCC(x_) y_) = PLUS(x_ SUCC(y_));
    PLUS(ZERO x_) = x_;

    PLUS(SUCC(SUCC(SUCC(ZERO))) SUCC(ZERO));"
    .trim();
let (trs, mut terms) = parse(&mut sig, inp).unwrap();
let mut term = terms.pop().unwrap();
let mut trace = Trace::new(&trs, &term, 0.5, 1.0, None, Strategy::Normal);

let expected = vec!["PLUS(3, 1)", "PLUS(2, 2)", "PLUS(1, 3)", "PLUS(0, 4)", "4"];
let got = trace
    .by_ref()
    .take(5)
    .map(|n| n.term().pretty())
    .collect::<Vec<_>>();
assert_eq!(got, expected);
assert!(trace.next().is_none());

Structs

Trace	A Trace provides first-class control over Term rewriting.
TraceNode	A TraceNode describes a specific evaluation step in the Trace.
TraceNodeIter

Enums

TraceState

The state of a Term at a particular evaluation step in a Trace.