Struct kontroli::rc::state::State

pub struct State<'s> {
    pub ctx: Context<'s>,
    pub term: RTerm<'s>,
    pub stack: Stack<'s>,
}

An abstract machine representing arguments applied to a substituted term.

This representation allows for the lazy evaluation of terms.

See section 5.1 of the following reference: Asperti, A.; Ricciotti, W.; Sacerdoti Coen, C.; Tassi, E. (2009). "A compact kernel for the calculus of inductive constructions". Sadhana. 34: 71–144. doi: 10.1007/s12046-009-0003-3.

Fields

ctx: Context<'s>

term: RTerm<'s>

stack: Stack<'s>

Implementations

impl<'s> State<'s>

pub fn whnf(self, sig: &Signature<'s>) -> Self

Evaluate the state to its weak head normal form.

let sig = Signature::new();
let syms = Symbols::new();

let term = Term::from(STerm::parse(r"(x => x) (x => x).", &syms)?);
let whnf = State::new(RTerm::new(term)).whnf(&sig);

let expected = Term::from(STerm::parse(r"(x => x).", &syms)?);
assert!(whnf.ctx.is_empty());
assert!(whnf.stack.is_empty());
assert_eq!(*whnf.term, expected);

impl<'s> State<'s>

pub fn new(term: RTerm<'s>) -> Self

Construct a new state from a reference to a term.

This does not yet evaluate anything, as can be seen from following example:

let syms = Symbols::new();

let term = Term::from(STerm::parse(r"(x => x) (x => x).", &syms)?);
let rterm = RTerm::new(term);

let state = State::new(rterm.clone());
assert!(RTerm::ptr_eq(&RTerm::from(state), &rterm));

Trait Implementations

impl<'s> Clone for State<'s>

fn clone(&self) -> State<'s>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'s> Default for State<'s>

fn default() -> State<'s>

Returns the "default value" for a type.

impl<'s> From<State<'s>> for RTerm<'s>

fn from(state: State<'s>) -> Self

Performs the conversion.