Struct kontroli::Stack

pub struct Stack<A>(_);

A Vec that is iterated from the last to the first pushed element.

The motivation for this data structure is the translation of algorithms using (immutable) linked lists. These algorithms usually assume that the nth element of a list is the nth-last consed element, whereas the nth element of a Vec is the nth-first pushed element. This data structure uses a Vec inside, but the nth element of a Stack is the nth-last pushed element, that is, the nth element counted from the end of the underlying Vec.

This behaviour is convenient e.g. when dealing with de Bruijn indices.

Implementations

impl<'s> Stack<RState<'s>>

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

impl<'s> Stack<RState<'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<_>>());

impl<'s> Stack<RState<'s>>

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

impl<'s> Stack<RState<'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<_>>());

impl<A> Stack<A>

pub fn new() -> Self

Create an empty stack.

pub fn push(&mut self, x: A)

Add an element to the top of the stack.

pub fn pop(&mut self) -> Option<A>

Remove and return an element from the top of the stack.

pub fn pop_many(&mut self, n: usize)

Remove n elements from the top of the stack.

pub fn clear(&mut self)

Remove all elements from the stack.

pub fn len(&self) -> usize

Return the number of elements on the stack.

pub fn is_empty(&self) -> bool

Return true if the stack contains no elements.

pub fn get(&self, n: usize) -> Option<&A>

Obtain the nth element counted from the top of the stack.

pub fn with_pushed<F, Y, E>(&mut self, x: A, f: F) -> Result<Y, E> where
    F: FnOnce(&mut Stack<A>) -> Result<Y, E>, 

Push an element on the stack, run a function on it, then pop the element.

This is to simulate function calls like f(Cons(x, l)), which assume that l is not changed in this call. If with_pushed is used consistently, then l at the end will contain the same elements as at the beginning.

pub fn iter(&self) -> impl Iterator<Item = &A>

Iterate through the elements of the stack starting from the top.

Trait Implementations

impl<A: Clone> Clone for Stack<A>

fn clone(&self) -> Stack<A>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<A: Debug> Debug for Stack<A>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<A> Default for Stack<A>

fn default() -> Self

Returns the "default value" for a type.

impl<'s> Display for Stack<RTerm<'s>>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'s> Display for Stack<RTerm<'s>>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<A> From<Vec<A>> for Stack<A>

fn from(v: Vec<A>) -> Self

Performs the conversion.

impl<A> FromIterator<A> for Stack<A>

fn from_iter<I: IntoIterator<Item = A>>(iter: I) -> Self

Creates a value from an iterator.

impl<A> IntoIterator for Stack<A>

type Item = A

The type of the elements being iterated over.

type IntoIter = Rev<IntoIter<Self::Item>>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.