Struct TypeCache 

pub struct TypeCache<'call, V> { /* private fields */ }

inferType, memoised on (environment, term) — the cache Lean has and we do not, with the half Lean does not need because its Expr is de Bruijn.

Why the environment is in the key, and what happens to a cache without it

Term names its variables. Var("x") interns to ONE TermId whatever scope it occurs in, and Context::extend SHADOWS — so under x : Nat that id’s type is Nat and under x : Bool it is Bool. A cache keyed on the term ALONE hands the second scope the first scope’s answer: the kernel certifying a type the term does not have, from an optimisation. W_perf_extra::a_type_cache_keyed_on_the_term_alone_would_certify_the_wrong_type builds exactly that and watches it happen, and the same test watches this key refuse to.

Lean is not exposed to it: its Expr uses de Bruijn indices for bound variables and globally unique FVarIds for free ones, so two occurrences under different binders are DIFFERENT expressions, and inferType may cache on the expression alone. Porting that design across without porting the representation is the mistake this type exists to make unavailable.

What it costs, and why it still pays

The invariant the key does NOT carry, and why it does not have to. A term’s type also depends on the GLOBAL environment — definitions, inductives, constructors, structures. That is not in the key because it cannot change: every kernel entry point takes &Context, and a shared reference can be neither displaced, nor extended in place, nor popped. One cache must therefore be threaded only through calls that share one &Context’s globals, which is exactly one outermost kernel call — the lifetime KernelCall gives it.

TermStore::env_for restricts the environment to a term’s FREE VARIABLES, which the store already knows in O(1) and hash-conses, so the key costs O(|free vars|) and not O(|context|). A CLOSED subterm — every type, every literal, every global’s body — keys on EnvId::EMPTY under every scope, so it is checked once for the whole call however many scopes it appears under. That is a_shared_subterm_is_checked_once_and_not_once_per_occurrence on the CHECKING side, by construction rather than by a special case.

Implementations

impl<'call, V: Clone + Debug> TypeCache<'call, V>

pub fn new(_call: &'call KernelCall) -> Self

An empty cache, borrowing the call it may not outlive.

pub fn get(&mut self, env: EnvId, id: TermId) -> Option<&V>

The type decided for this term under this environment, if it has been asked.

pub fn insert(&mut self, env: EnvId, id: TermId, ty: V)

Record a decision.

Recording the same key twice with a DIFFERENT answer is a bug in the caller — one environment, one term, one type — and it is the empirical tripwire for a cache that has outlived the environment it decided under. It is a debug_assert because it compares through Debug, which every kernel answer has and not every one has PartialEq; the test suite runs in debug, which is where a stale cache would be caught.

pub fn len(&self) -> usize

How many judgements are cached.

pub fn is_empty(&self) -> bool

Whether nothing has been decided.

pub fn hits(&self) -> u64

Lookups answered from the cache — the number that says a shared subterm was checked once.

pub fn misses(&self) -> u64

Lookups that had to be decided.

pub fn clear(&mut self)

Forget every decision.