Struct Arena 

pub struct Arena { /* private fields */ }

All values of a checking session, their memos, and the tables that intern them.

Implementations

impl Arena

pub fn new() -> Arena

pub fn reset(&mut self)

Drops every value (the end of a session), keeping the storage for the next session.

pub fn len(&self) -> usize

pub fn is_empty(&self) -> bool

pub fn get(&self, v: V) -> Val

pub fn is_open(&self, v: V) -> bool

pub fn head(&self, h: HeadId) -> Head

pub fn whnf_memo(&self, v: V) -> Option<V>

pub fn set_whnf_memo(&mut self, v: V, r: V)

pub fn whnf_core_memo(&self, v: V) -> Option<V>

pub fn set_whnf_core_memo(&mut self, v: V, r: V)

pub fn delta_memo(&self, v: V) -> Option<V>

pub fn set_delta_memo(&mut self, v: V, r: V)

pub fn type_memo(&self, v: V) -> Option<V>

pub fn set_type_memo(&mut self, v: V, r: V)

pub fn proof_memo(&self, v: V) -> Option<bool>

Whether the value is a proof, once decided.

pub fn set_proof_memo(&mut self, v: V, proof: bool)

pub fn dom_memo(&self, v: V) -> Option<V>

A lambda’s evaluated domain.

pub fn set_dom_memo(&mut self, v: V, r: V)

pub fn find_head(&self, h: &Head) -> Option<V>

pub fn head_value(&mut self, kind: Kind, h: Head) -> V

The bare value of a head (no arguments).

pub fn neutral_app(&mut self, f: V, a: V) -> V

The neutral f a for a neutral f.

pub fn sort(&mut self, l: LevelId) -> V

pub fn nat(&mut self, n: NatId) -> V

pub fn str(&mut self, s: StrId) -> V

pub fn lam(&mut self, dom: ExprId, env: EnvId, body: ExprId) -> V

pub fn pi(&mut self, dom: V, env: EnvId, body: ExprId) -> V

pub fn pi_lam(&mut self, dom: V, env: EnvId, ctx: CtxId, body: ExprId) -> V

pub fn spine_node(&self, s: Sp) -> SpNode

pub fn spine_len(&self, s: Sp) -> usize

pub fn args(&self, s: Sp) -> SmallVec<[V; 8]>

The arguments of a spine, first to last.

pub fn arg(&self, s: Sp, i: usize) -> Option<V>

The i-th argument (0-based, first to last) of a spine.

pub fn env(&self, e: EnvId) -> EnvNode

pub fn last_prune(&self, e: EnvId, mask: u64) -> Option<EnvId>

The environment e was last pruned to with mask, if that was the last pruning asked of it.

pub fn note_prune(&mut self, e: EnvId, mask: u64, r: EnvId)

pub fn env_open(&self, e: EnvId) -> bool

pub fn lsub_of(&self, e: EnvId) -> SubstId

The universe substitution e’s terms are read under.

pub fn lsub_base(&mut self, s: SubstId) -> EnvId

The empty environment of the substitution s (for s the identity, EnvId::EMPTY).

pub fn same_shape(&self, a: EnvId, b: EnvId) -> bool

Whether two environments have the same length and substitution: all that tells them apart besides their entries.

pub fn extend(&mut self, parent: EnvId, val: V) -> EnvId

pub fn frame_slot_count(&self) -> usize

Entries stored in frames so far this session: what pruning has copied.

pub fn lookup(&self, e: EnvId, i: u32) -> Option<V>

The value of de Bruijn index i.

pub fn entries(&self, e: EnvId) -> impl Iterator<Item = V> + '_

The entries of an environment, innermost first (DEAD for those pruned away), in one walk.

pub fn select(&self, e: EnvId, mask: u64, out: &mut SmallVec<[V; 16]>)

The values at the positions mask marks (innermost first), in one walk.

pub fn select_indices( &self, e: EnvId, indices: &[u32], out: &mut SmallVec<[V; 16]>, )

The values at indices (ascending, innermost first), in one walk.

pub fn frame(&mut self, len: u32, mask: u64, vals: &[V], lsub: SubstId) -> EnvId

The frame of len entries whose live entries are vals at the positions mask marks (innermost first), read under the substitution lsub, interned by content.

pub fn wide_frame( &mut self, len: u32, indices: &[u32], vals: &[V], lsub: SubstId, ) -> EnvId

The frame of len entries whose live entries are vals at indices (ascending, some of them 64 or more), read under the substitution lsub, interned by content.

pub fn ctx_extend(&mut self, parent: CtxId, ty: V) -> CtxId

pub fn ctx_lookup(&self, c: CtxId, i: u32) -> Option<V>

pub fn memory_report(&self) -> Vec<(&'static str, usize)>

Bytes held by each part of the arena (capacity: what the process pays).

pub fn bytes(&self) -> usize

Trait Implementations

impl Clone for Arena

fn clone(&self) -> Arena

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Default for Arena

fn default() -> Self

Returns the “default value” for a type.