Struct DefEqCache 

pub struct DefEqCache { /* private fields */ }

A cache of decided conversions, keyed on a PAIR of node identities.

IdCache answers “what is this node’s type” once per node. This answers “are these two nodes convertible” once per pair, which is the other thing Lean’s kernel has and ours does not: is_subtype today has exactly one shortcut (alpha_eq) and then normalises BOTH sides to a FULL normal form before comparing, with nothing remembered afterwards.

MEASURED on this box: 100 repetitions of one convertible-but-not-α-equal pair cost 0.662 s against 0.00655 s for one — 6.55, 6.57 and 6.62 ms per call at 1, 10 and 100 repeats. The per-call cost is FLAT, which is the measurement that says there is no cache anywhere. tests/W_perf_extra.rs::w_perf_measure_what_the_missing_conversion_cache_costs prints it.

Conversion is SYMMETRIC, so (a, b) and (b, a) are one entry: the key is ordered.

NEGATIVE ENTRIES ARE KEPT, deliberately. They are the expensive half — deciding that two terms are NOT convertible is what costs a full normalisation of both sides — and Lean caches them for the same reason.

Two rules this cache cannot enforce for itself, and a soundness trap in the second

1. Identity is not Term equality on floats. Settled: Literal’s PartialEq compares f64::to_bits(), so the store’s interning key IS the kernel’s equality and the two agree everywhere. eq_faithful remains the conservative guard, and a caller that writes store.same(a, b) && store.eq_faithful(a) is correct under the old rule as well as the new one.

2. A cache may not outlive the environment it decided under. Adding a definition can only ADD conversions, so a stale NEGATIVE is merely incomplete. A stale POSITIVE is the kernel certifying a conversion that no longer holds.

   Wave 2 named the wrong mechanism, and the correction matters. Context::pop_scope does NOT remove definitions: it reverts the four ATTRIBUTE databases — instances, coercions, simp rules, hints — and its own doc says “NEVER a declaration”; a def written inside a section survives its end. The call that genuinely removes one is Context::displace, which add_inductive/declare run on the name they are about to bind, so re-declaring a name deletes the previous definition of it — and a positive decided against that body is then stale.

   The reason a per-call cache needs nothing else: every kernel entry takes &Context, and a shared reference cannot be displaced, extended in place or popped. Within one outermost kernel call the global environment is FIXED. Only the LOCAL bindings vary, by Context::extend, which returns a new Context and may SHADOW — and locals are what EnvId keys. So: hold the cache for exactly one outermost call, and let KernelCall make that a borrow rather than a comment — see DefEqCache::scoped.

Implementations

impl DefEqCache

pub fn new() -> Self

An empty cache.

pub fn get(&mut self, a: TermId, b: TermId) -> Option<bool>

What was decided about this pair, in either order, or None if it has not been asked.

pub fn insert(&mut self, a: TermId, b: TermId, equal: bool)

Record a decision. Recording the same pair twice with DIFFERENT verdicts is a bug in the caller — one Context, one answer — and is caught here rather than propagated.

pub fn len(&self) -> usize

How many pairs have been decided.

pub fn is_empty(&self) -> bool

Whether nothing has been decided.

pub fn hits(&self) -> u64

Lookups that were answered from the cache.

pub fn misses(&self) -> u64

Lookups that had to be decided.

pub fn clear(&mut self)

Forget every decision — what a Context change requires, and what dropping the cache at the end of a kernel call does for free.

pub fn scoped(_call: &KernelCall) -> ScopedDefEqCache<'_>

The same cache with a LIFETIME it cannot escape — the enforceable form of rule 2 above.

use logicaffeine_kernel::term_store::{DefEqCache, KernelCall};

let call = KernelCall::begin();
let conv = DefEqCache::scoped(&call);
assert!(conv.is_empty() && conv.hits() == 0 && conv.misses() == 0);

Returning it past its call does not compile:

use logicaffeine_kernel::term_store::{DefEqCache, KernelCall, ScopedDefEqCache};

fn escape() -> ScopedDefEqCache<'static> {
    let call = KernelCall::begin();
    DefEqCache::scoped(&call)
}

ScopedDefEqCache<'call> borrows the KernelCall, so it cannot reach a static (that needs 'static) and cannot be stored in a Context without giving Context a lifetime parameter — a change every call site would see. KernelCall is neither Send nor Sync, so it cannot be smuggled into a global through a Mutex either.

Trait Implementations

impl Default for DefEqCache

fn default() -> Self

Returns the “default value” for a type.