Struct TermStore 

pub struct TermStore { /* private fields */ }

A hash-consed term store: maximal structural sharing, O(1) equality, O(1) annotations.

Every mk_* and intern call goes through one dedup table, so two structurally identical subterms are ONE node with ONE id. Nothing in this type recurses natively, and its Drop is a flat Vec drop.

Implementations

impl TermStore

pub fn new() -> Self

An empty store, with the empty name set pre-interned at NameSetId 0 and the identity substitution at SubstId::EMPTY.

pub fn len(&self) -> usize

How many DISTINCT nodes the store holds.

pub fn is_empty(&self) -> bool

Whether the store holds no nodes at all.

pub fn clear_caches(&mut self)

Drop every memo table. Ids stay valid; only cached derived results are discarded.

pub fn rename_risk(&self) -> bool

Whether any substitution this store has performed could have RENAMED a binder.

It is set when substitute is asked to push a value into a body that BINDS one of the value’s free names — the exact condition under which a capture-avoiding pass has to invent a name — and it is a hard false otherwise.

Why a caller comparing two substitutions needs it

type_checker::substitute_avoiding renames a binder when replacement_fvs.contains(param) and this store renames on the same criterion, so on a term where the condition never arises the two are the SAME FUNCTION and their answers are equal, not merely α-equivalent. Where it does arise they can still differ, because the two passes visit different binders: this store descends only where the substitution is live, while substitute_avoiding descends the whole body and renames a binder whose name is a free variable of the replacement even in a subtree the substituted variable never reaches. So the flag is the precondition beta_zeta_normal_form needs to promise an EQUAL answer rather than an α-equivalent one.

pub fn symbol(&mut self, name: &str) -> Symbol

Intern a name, returning its symbol.

pub fn lookup_symbol(&self, name: &str) -> Option<Symbol>

An already-interned name’s symbol, without creating one.

pub fn name(&self, sym: Symbol) -> &str

The string a symbol denotes.

pub fn node(&self, id: TermId) -> &Node

The node behind an id.

pub fn level_view(&self, id: LevelId) -> LevelView<'_>

Borrow one universe node without materializing its recursive tree.

As with node(), the handle must have come from this store.

pub fn add(&mut self, node: Node) -> TermId

Add a node, returning the existing id if an identical node is already stored.

This is the ONE place a TermId is minted, which is what makes the store maximally shared by construction rather than by a later pass.

pub fn mk_sort(&mut self, u: &Universe) -> TermId

Term::Sort(u).

pub fn mk_var(&mut self, name: &str) -> TermId

Term::Var(name).

pub fn mk_var_sym(&mut self, s: Symbol) -> TermId

Term::Var from an already-interned name.

pub fn mk_global(&mut self, name: &str) -> TermId

Term::Global(name).

pub fn mk_app(&mut self, f: TermId, a: TermId) -> TermId

Term::App(f, a).

pub fn mk_lambda( &mut self, param: &str, param_type: TermId, body: TermId, ) -> TermId

Term::Lambda.

pub fn mk_pi( &mut self, param: &str, param_type: TermId, body_type: TermId, ) -> TermId

Term::Pi.

pub fn mk_let( &mut self, name: &str, ty: TermId, value: TermId, body: TermId, ) -> TermId

Term::Let.

pub fn mk_fix(&mut self, name: &str, body: TermId) -> TermId

Term::Fix.

pub fn mk_lit(&mut self, lit: &Literal) -> TermId

Term::Lit.

pub fn mk_hole(&mut self) -> TermId

Term::Hole.

pub fn mk_const(&mut self, name: &str, levels: &[Universe]) -> TermId

Term::Const — a universe-polymorphic global at explicit levels.

pub fn mk_match( &mut self, discriminant: TermId, motive: TermId, cases: &[TermId], ) -> TermId

Term::Match.

pub fn mk_mutual_fix(&mut self, defs: &[(&str, TermId)], index: usize) -> TermId

Term::MutualFix — every name in defs is bound in EVERY body.

pub fn level_of(&mut self, u: &Universe) -> LevelId

Intern a universe level, for a caller building a Node::Const by hand.

pub fn literal_payload_bytes(&self, id: LitId) -> usize

Borrow the heap payload size needed when extracting a literal. This excludes the Term/enum headers and allocator overhead. The handle must belong to this store, as with node() and level_view().

pub fn depth(&self, id: TermId) -> u32

Maximum height — 1 for a leaf. O(1): computed when the node was built.

pub fn tree_size(&self, id: TermId) -> u64

The node count an unfolding tree walk would report, saturating at u64::MAX. O(1).

pub fn structural_hash(&self, id: TermId) -> u64

O(1) structural hash. Equal ids have equal hashes.

pub fn float_free(&self, id: TermId) -> bool

Whether the subterm contains no Literal::Float.

The most conservative GUARD on using id equality as Term equality. Literal equality compares floats by bit identity, so id equality is faithful everywhere; this guard was correct under the old IEEE rule, when NaN and ±0.0 made the two part company, and stays correct under the current one. On a float_free term, same(a, b) and extract(a) == extract(b) agree EXACTLY.

pub fn eq_faithful(&self, id: TermId) -> bool

Whether id equality is a FAITHFUL decision procedure for Term equality on this subterm: for any two eq_faithful ids, same(a, b) and extract(a) == extract(b) agree in BOTH directions.

This is the precise condition; float_free is the conservative one. A float that is neither a NaN nor a zero compares the same way under IEEE == and under bit equality, so a term may hold as many 1.5s and infinities as it likes and still be safe to compare by identity under either rule; NaN and ±0.0 are the literals on which the two rules differ.

It is SUFFICIENT rather than necessary: Literal’s equality is bit identity (the rule literal_identity_eq models independently), so id equality is faithful everywhere and this predicate is conservative. store.same(a, b) && store.eq_faithful(a) is correct under both rules.

pub fn shapes(&self, id: TermId) -> ShapeMask

Which NodeShapes occur anywhere in a subterm. O(1).

This is Lean’s Expr.Data has* bits widened to one per node kind — see ShapeMask for the citation and the trade-off. A reducer that does not implement ι can ask !store.shapes(id).contains(NodeShape::Match) without walking anything.

pub fn constants(&self, id: TermId) -> Vec<&str>

Every Global and Const NAME occurring anywhere in a subterm, sorted and without duplicates — the δ SURFACE. O(1) to reach, O(k) to hand back.

It is the question a caller with no Context cannot answer for itself: whether a term still holds a δ redex depends on what those names MEAN here, and only the caller knows.

pub fn binder_names(&self, id: TermId) -> Vec<&str>

Every BINDER name occurring anywhere in a subterm, sorted. O(1) to reach.

The use is a guard rather than a query: a substitution pass that has to FRESHEN a binder mints a name this store chose, and a caller comparing its answer against another implementation’s needs to know that no such name leaked into the result.

pub fn binders_within(&self, inner: TermId, outer: TermId) -> bool

Whether every binder name in inner also occurs as a binder in outer — the test that says a reduction invented no name of its own. O(k), over two sorted hash-consed sets.

pub fn is_beta_zeta_pure( &self, id: TermId, inert: &dyn Fn(&str) -> bool, ) -> bool

Whether the only redexes this subterm can hold are β and ζ — so a reducer that implements exactly those two rules computes the same normal form as the full kernel.

Two conditions, and the split between them is the point. The SHAPE condition is decided here, in O(1), from shapes: Match carries ι, Fix and MutualFix carry unrolling, Const carries δ plus a level well-formedness test, Lit is what the arithmetic primitives key their argument on, Hole is not a term, and Bound cannot be reached from a Term at all. The NAME condition belongs to the caller: whether a Global still has a δ body, or is one of the names a rule is keyed on rather than a shape, is a fact about the Context this store has never seen.

pub fn free_vars(&self, id: TermId) -> Vec<&str>

The free variable names of a subterm, sorted. Resolves and collects O(k) names, where k is the number of free names; the underlying symbol set is cached.

pub fn free_names_are_empty(&self, id: TermId) -> bool

Whether the exact free-name set is empty, including annotations and all binder scopes. O(1): the full free-symbol set was cached at construction. This says nothing about internal de Bruijn Bound nodes.

pub fn occurs_free(&self, id: TermId, name: &str) -> bool

Whether name occurs free. O(1) mask test, then a binary search.

pub fn occurs_free_sym(&self, id: TermId, s: Symbol) -> bool

Whether name occurs free, by symbol.

pub fn dag_size(&self, id: TermId) -> usize

How many DISTINCT nodes id reaches — the DAG size, which is what a checker keyed on identity actually pays.

pub fn same(&self, a: TermId, b: TermId) -> bool

Whether two ids denote the same term — ONE integer compare.

pub fn env(&mut self, entries: &[(Symbol, TermId)]) -> EnvId

Intern a local typing environment — (name, type) pairs, sorted by name.

Two Contexts that assign the same types to the same names get the same EnvId, whatever order they were built in and whatever else they contain.

Panics

Panics if a name appears twice. An environment is a FUNCTION from names to types; two entries for one name is a caller that has not decided which scope it is in, and silently keeping one of them is how a cache starts answering for the wrong context.

pub fn env_for( &mut self, id: TermId, lookup: &mut impl FnMut(&str) -> Option<TermId>, ) -> EnvId

The environment fragment that DECIDES id’s type: the types lookup assigns to exactly the free variables of id, and nothing else.

This is the key half that makes an inferType cache sound over a NAMED term representation, and it is O(|free variables|) rather than O(|context|) because the free set was computed at construction and is itself hash-consed.

Two properties make it the RIGHT key rather than merely a safe one:

• A closed subterm gets EnvId::EMPTY under every context, so it is checked ONCE for the whole call however many scopes it occurs under. That is where the win is.
• A variable the context does not bind is OMITTED, not defaulted, so “x is unbound” and “x : Nat” are different keys and the cached refusal cannot leak into a scope that binds it.

pub fn env_entries(&self, e: EnvId) -> &[(Symbol, TermId)]

The entries of an interned environment, sorted by name.

pub fn env_count(&self) -> usize

How many environments have been interned — the measure that says a descent is reusing its scopes rather than minting a new one per binder.

pub fn intern(&mut self, term: &Term) -> TermId

Intern a Term. Iterative: a term the native stack could not walk still interns.

pub fn extract(&self, id: TermId) -> Term

Materialise a Term from an id. Iterative — but note that the Term it returns is a TREE, so DROPPING it is native recursion again, and unfolding a DAG can be exponentially larger than the DAG. extract_bounded is the guarded form.

pub fn extract_bounded(&self, id: TermId, limit: u64) -> Result<Term, TooLarge>

extract, refusing an unfolding bigger than limit nodes instead of trying to allocate it.

pub fn fold<V: Clone>( &self, root: TermId, cache: &mut IdCache<V>, f: &mut dyn FnMut(&TermStore, TermId, &Node, &[V]) -> V, ) -> V

Fold over the DAG, children before parents, visiting every DISTINCT node EXACTLY ONCE and remembering the answer in cache.

This is the shape infer_type has to take for a shared subterm to be checked once instead of once per occurrence. Iterative, so depth costs heap and not stack.

pub fn occurrence_count(&mut self, id: TermId, name: Symbol) -> u32

How many FREE occurrences of name a subterm has, saturating at u32::MAX.

Memoised on node identity, so a shared subterm is counted once. This is the measure an occurrence-gated ζ rule needs: a let whose name occurs at most once can be expanded for free, and one that occurs more must KEEP the let as its sharing node.

pub fn occurrences(&mut self, id: TermId, name: Symbol) -> Occurrences

occurrence_count, classified — all an occurrence gate needs to decide.

pub fn substitute( &mut self, body: TermId, name: Symbol, value: TermId, ) -> TermId

Capture-avoiding substitution of ONE name.

Freshening is STORE-SCOPED: a binder that has to be renamed takes the next name from this store’s counter, so the same substitution asked for twice returns the identical id (the memo answers the second time), while the same substitution in a fresh store — or after clear_caches — can pick a different fresh name and return an α-equivalent answer with a different id. Compare such answers with alpha_same, never with ==.

pub fn instantiate( &mut self, body: TermId, pairs: &[(Symbol, TermId)], ) -> TermId

SIMULTANEOUS capture-avoiding substitution — Lean’s instantiateRev shape.

A whole telescope’s arguments go in together, in ONE pass, so instantiating an n-binder telescope costs one walk and not n. pairs is treated as a simultaneous map: no to term is ever re-scanned for another pair’s name.

pub fn alpha_id(&mut self, root: TermId) -> TermId

The α-CANONICAL form of a term: every binder name replaced by one reserved name and every bound occurrence by its de Bruijn LEVEL, so two terms are α-equivalent exactly when their canonical forms are the SAME id.

This is what makes the store useful to a NAMED kernel. same(a, b) is structural equality, and the kernel’s conversion checker does not want structural equality — it wants α. type_checker::is_subtype opens with an alpha_eq(a, b) fast path that walks both trees on EVERY conversion, which is the hottest path in the kernel; against a canonical id it is one integer compare plus a memo hit.

Free variables keep their names, so λx. y and λx. z stay distinct — α renames BOUND names only.

Levels rather than indices: a level-canonical subterm depends on how deep it sits, so λx. x canonicalises differently under one binder than under two, and the memo holds one entry per (environment, level, node). De Bruijn INDICES would make a closed subterm’s canonical form position-independent and therefore shared everywhere it occurs — strictly more sharing, at the price of an abstraction pass that shifts. Recorded rather than done.

pub fn alpha_same(&mut self, a: TermId, b: TermId) -> bool

Whether two terms are α-equivalent — ONE integer compare, after each side’s canonical form has been computed once.

pub fn is_alpha_canonical(&mut self, id: TermId) -> bool

Whether a term is already its own α-canonical form — that is, whether canonicalising changes nothing. True for anything that binds nothing, and also for a term whose binders already carry the reserved name and bind no occurrence.

pub fn zeta_expand_head(&mut self, id: TermId) -> Option<TermId>

ζ-expand a Let at the head, whatever its occurrence count — what a conversion check must be able to do on demand once a Let is allowed to survive into a normal form.

pub fn beta_zeta_normalize( &mut self, root: TermId, budget: u64, ) -> StoreNormalForm

β/ζ normal form, with ζ OCCURRENCE-GATED: a let whose name occurs at most once in the normalised body is expanded, and one that occurs more KEEPS the let as its sharing node.

The gate is re-evaluated AFTER the body is normalised, because reduction can erase occurrences — a body with three uses of n before reduction and one after must still expand.

The rule is zeta_or_share_opt’s, all three cases of it

The occurrence count is only two of the three. The third is the SPECULATION: nothing inside a held binding stepping is not the same as the binding having no redex, because ζ is always available and firing it can unblock a rule that could not see past the binder. let x := λz. y in x x is stuck as long as the binding is held and reduces to y the moment it is expanded. So a held binding whose parts are all normal is EXPANDED SPECULATIVELY and kept only when its expansion is itself a normal form — which is the corpus’s quad b b b b, whose head is a declaration with no body.

The speculation is not re-entered while one is running, exactly as zeta_or_share_opt’s Speculating guard does it: a nest of k shared bindings would otherwise be 2^k probes rather than a walk.

Why the rebuild is re-examined

Normalising a node’s children can put a redex AT the node: (let b := λu. u in e) arg holds its binding while e mentions b twice, and if normalising e drops that to one the binding expands to a λ — and the application above it, already past its own weak-head pass, is a β-redex nobody would look at again. So a rebuild whose head can move is sent back through the loop rather than accepted.

NOT A KERNEL TIER: β and ζ only. No δ, no ι, no η, no Fix, no universe algebra.

Trait Implementations

impl Default for TermStore

fn default() -> Self

Returns the “default value” for a type.