Type Definition kontroli::arc::state::Stack

type Stack<'s> = Stack<RState<'s>>;

Arguments to the abstract machine term.

Implementations

impl<'s> Stack<'s>

pub fn match_rule(
    &self,
    rule: &Rule<'s>,
    sig: &Signature<'s>
) -> Option<Vec<Vec<RState<'s>>>>

impl<'s> Stack<'s>

pub fn match_flatten(
    &self,
    rule: &Rule<'s>,
    sig: &Signature<'s>
) -> Option<Context<'s>>

Determine whether the stack of an abstract machine matches the rule's LHS.

Return a new machine context containing variable assignments in case of a match.

let syms: Symbols = vec!["id", "f", "a"].into_iter().collect();
let sig = Signature::new();

let rule = Rule::from(SRule::parse("[A] id A --> A.\n", &syms)?);
let term = Term::from(STerm::parse("id f a.\n", &syms)?);

let stack = State::new(RTerm::new(term)).whnf(&sig).stack;
let subst = stack.match_flatten(&rule, &sig).unwrap();
let subst = subst.iter().map(|rtt| (**rtt.force()).clone());

let expected = Term::from(STerm::parse("f.\n", &syms)?);
assert_eq!(vec![expected], subst.collect::<Vec<_>>());