[−][src]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 |
TraceNode | A |
TraceNodeIter |
Enums
TraceState | The state of a |