Method clear_releasing_memory

crates/kernel/src/env.rs:577–601

Clear worker-local state and drop backing allocations. `clear()` preserves `HashMap` capacity, which is useful for reuse but problematic for full-env checking: one very large block can permanently ratchet a worker's retained cache allocation. This variant is for scheduled-block boundaries where memory pressure matters more than preserving buckets for the next unrelated block.

(&mut self)

  /// Computed `is_rec` per inductive, keyed by content address
  pub is_rec_cache: FxHashMap<Address, bool>,
  /// Generated recursors, keyed by inductive Muts block id.
  pub recursor_cache: FxHashMap<KId<M>, Vec<GeneratedRecursor<M>>>,
  /// Nested-auxiliary order expected by stored recursors in this environment.
  pub recursor_aux_order: RecursorAuxOrder,
  /// Maps the set of major inductive KIds to the inductive block id.
  pub rec_majors_cache: FxHashMap<BTreeSet<KId<M>>, KId<M>>,
  /// Mutual-block peer-agreement cache: records block ids whose peers have
  /// already been verified to share the same universe (S3) and parameter
  /// prefix (S3b). Populated by `check_inductive` after the per-peer loop
  /// succeeds; collapses the naturally O(N²) per-peer iteration to O(N)
  /// total work per block across all the peers' individual checks.
  pub block_peer_agreement_cache: FxHashSet<KId<M>>,
  /// Whole-block type-check results. Both successes and failures are cached,
  /// so every member of a bad block reports the same structured failure.
  pub block_check_results: FxHashMap<KId<M>, Result<(), TcError<M>>>,

  /// Primitive-reducer family per head-constant address (see
  /// `whnf.rs::PrimFamily`). Pure function of the address; memoized so
  /// the WHNF loops classify each head with one map probe instead of a
  /// ~30-address compare gauntlet across five recognizers.
  pub prim_family_cache: FxHashMap<Address, super::whnf::PrimFamily>,

  /// Next free-variable id for checker-local binder openings.
  ///
  /// Type-checking caches live on `KEnv`, not on one `TypeChecker`, so FVar
  /// ids must also be allocated from the shared environment. Otherwise two
  /// checker instances could both mint `fv$0` and reuse an `infer(fv$0)` cache
  /// entry under different local contexts.