Method clear

crates/kernel/src/env.rs:509–539

Clear all worker-local kernel state before checking another scheduled block or when a caller needs a fresh environment.

(&mut self)

  /// Cheap def-eq cache: same key as `def_eq_cache`, but only for comparisons
  /// performed inside cheap projection reductions. Cheap `false` can be a
  /// full-mode false negative, so those entries must not be visible to full
  /// callers.
  pub def_eq_cheap_cache: FxHashMap<(Addr, Addr, CtxAddr), bool>,
  /// Failed def-eq pairs in lazy delta: canonical ordering by hash.
  pub def_eq_failure: FxHashSet<(Addr, Addr, CtxAddr)>,
  /// Constant-instantiation cache: caches the result of
  /// `instantiate_univ_params(val, us)` for each `Const(id, us)` head encountered
  /// during delta unfolding. Keyed by the head expression's content hash, which
  /// already content-addresses `(id, us)` (the head's address derives from id +
  /// universe args). Mirrors lean4 C++ `m_unfold` cache. Cross-call sharing of
  /// universe-substituted bodies eliminates O(body) walks on every unfold.
  pub unfold_cache: FxHashMap<Addr, KExpr<M>>,
  /// Memo of `try_reduce_nat_succ_iter` STUCK outcomes: succ-chain args
  /// whose base never collapses to a literal. Keyed like `whnf_cache`
  /// ((expr_hash, ctx_hash)). The succ-collapse loop runs its inner WHNF
  /// in `NatSuccMode::Stuck`, which bypasses the WHNF caches, so without
  /// this memo a stuck `Nat.succ^k(x)` chain is re-peeled from every
  /// depth it is encountered at — O(k²) fuel for symbolic-plus-literal
  /// Nat arithmetic (e.g. `x + 0xC0` in the UTF-8 codec proofs).
  pub nat_succ_stuck: FxHashSet<(Addr, CtxAddr)>,
  /// Ingress cache: LeanExpr → KExpr conversion results.
  /// Keyed by (expr_hash, param_names_hash) to account for different
  /// level param bindings producing different KExprs from the same LeanExpr.
  pub ingress_cache: FxHashMap<(CtxAddr, CtxAddr), KExpr<M>>,
  /// "Is this type Prop?" cache, keyed by (type_hash, ctx_hash).
  ///
  /// `try_proof_irrel` is called on essentially every `is_def_eq`
  /// invocation, and its uncached path costs `infer ∘ infer ∘ whnf` —
  /// two type-inference runs and one full WHNF — to decide whether the
  /// term's type is `Prop`. Because the answer depends only on the
  /// *type* (not on the term whose type was inferred), caching by the
  /// type's content hash + suffix-aware context lets every subsequent
  /// proof-irrelevance probe skip those three calls. Empirically this
  /// is the dominant cost on mathlib proof-heavy blocks, where the same