Struct Store 

pub struct Store {
    pub names: Names,
    pub levels: Levels,
    /* private fields */
}

Fields

names: Names

levels: Levels

Implementations

impl Store

pub fn new() -> Store

pub fn expr_count(&self) -> usize

pub fn persistent_count(&self) -> usize

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

Bytes held by each part of the store (capacity, not length: what the process pays).

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

Room for n more persistent nodes without growing (a reader that knows its input size avoids rehashing a table of millions of entries several times over).

pub fn begin_scratch(&mut self)

Everything interned from now on is transient until Store::end_scratch.

pub fn end_scratch(&mut self)

pub fn in_scratch(&self) -> bool

pub fn with_persistent<T>( &mut self, f: impl FnOnce(&mut Store) -> T, ) -> (T, bool)

Runs f, a computation over persistent terms only, interning what it builds persistently so the result can be cached across declarations. Returns the result and whether it is persistent.

A structure is only ever created when it is in neither region, so each structure has one id at any time. If f meets a node that already lives in scratch (built earlier in this declaration), the computation continues in scratch with that node rather than duplicate it, and the result is reported as not persistent — correct for this declaration, not cacheable.

pub fn intern(&mut self, node: Node) -> ExprId

pub fn node(&self, e: ExprId) -> Node

pub fn loose_bvar_range(&self, e: ExprId) -> u32

One more than the largest loose de Bruijn index (0 when closed).

pub fn loose_bvars(&self, e: ExprId) -> (u32, Option<u64>)

Store::loose_bvar_range and Store::loose_bvar_mask in one read.

pub fn scope_of(&self, e: ExprId) -> (u32, Option<u64>, bool)

Store::loose_bvars and Store::has_lparam in one read: everything outside a term that its meaning can depend on.

pub fn loose_bvar_mask(&self, e: ExprId) -> Option<u64>

Which loose de Bruijn indices occur — bit i for BVar(i) — when that is known exactly: None if a bound variable with index 64 or more occurs anywhere in e (its bit could not be recorded, and may have come into range under binders).

pub fn has_loose_bvars(&self, e: ExprId) -> bool

pub fn has_fvar(&self, e: ExprId) -> bool

pub fn has_lparam(&self, e: ExprId) -> bool

pub fn bvar(&mut self, i: u32) -> ExprId

pub fn fvar(&mut self, i: u32) -> ExprId

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

pub fn prop(&mut self) -> ExprId

pub fn cnst(&mut self, n: NameId, ls: LevelsId) -> ExprId

pub fn cnst_levels(&mut self, n: NameId, ls: &[LevelId]) -> ExprId

pub fn app(&mut self, f: ExprId, a: ExprId) -> ExprId

pub fn lam(&mut self, t: ExprId, b: ExprId) -> ExprId

pub fn pi(&mut self, t: ExprId, b: ExprId) -> ExprId

pub fn let_(&mut self, t: ExprId, v: ExprId, b: ExprId) -> ExprId

pub fn proj(&mut self, s: NameId, i: u32, e: ExprId) -> ExprId

pub fn nat_lit(&mut self, n: Nat) -> ExprId

pub fn nat_id(&mut self, n: Nat) -> NatId

The interned id of a natural number (the table is append-only: ids never go stale).

pub fn str_lit(&mut self, s: &str) -> ExprId

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

pub fn lit(&mut self, l: Lit) -> ExprId

pub fn lit_value(&self, l: LitId) -> &Lit

pub fn seq(&mut self, items: &[ExprId]) -> ExprId

pub fn seq_items(&self, e: ExprId) -> Args

The elements of a Node::Seq chain, first to last.

pub fn match_( &mut self, disc: ExprId, motive: ExprId, cases: &[ExprId], ) -> ExprId

pub fn fix(&mut self, body: ExprId) -> ExprId

pub fn mutual_fix(&mut self, defs: &[ExprId], index: u32) -> ExprId

pub fn string(&self, s: StrId) -> Rc<str>

pub fn mk_app_n(&mut self, f: ExprId, args: &[ExprId]) -> ExprId

pub fn app_fn(&self, e: ExprId) -> ExprId

The head of an application spine.

pub fn app_args(&self, e: ExprId) -> (ExprId, Args)

Head and arguments (in application order), filled last to first into a buffer of the recorded spine length.

pub fn app_num_args(&self, e: ExprId) -> usize

pub fn const_head(&self, e: ExprId) -> Option<(NameId, LevelsId)>

pub fn instantiate_core( &mut self, e: ExprId, subst: &[ExprId], rev: bool, ) -> ExprId

Replaces loose BVar(i), i < subst.len(), by subst[i] (rev = false) or by subst[len - 1 - i] (rev = true), and lowers the remaining loose indices by len.

pub fn instantiate(&mut self, e: ExprId, subst: &[ExprId]) -> ExprId

pub fn instantiate_rev(&mut self, e: ExprId, subst: &[ExprId]) -> ExprId

pub fn instantiate1(&mut self, e: ExprId, v: ExprId) -> ExprId

pub fn lift_loose(&mut self, e: ExprId, s: u32, d: u32) -> ExprId

Adds d to every loose index ≥ s.

pub fn abstract_fvars(&mut self, e: ExprId, fvars: &[u32]) -> ExprId

Replaces FVar(fvars[i]) by the bound variable of the i-th of fvars.len() enclosing binders (the last free variable becomes BVar(0)), as mkForall/mkLambda require.

pub fn instantiate_lparams( &mut self, e: ExprId, ps: &[NameId], us: &[LevelId], ) -> ExprId

Substitutes universe parameters ps[i] := us[i] throughout e.

pub fn any_node( &self, e: ExprId, pred: &mut dyn FnMut(&Store, ExprId) -> bool, ) -> bool

Does any subterm satisfy pred? Each distinct node is visited once.

pub fn mentions_const(&self, e: ExprId, names: &[NameId]) -> bool

Does e mention constant n?

Trait Implementations

impl Clone for Store

fn clone(&self) -> Store

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Default for Store

fn default() -> Self

Returns the “default value” for a type.