Reset thread-local state between constants. Global caches in `KEnv` are NOT cleared — they grow monotonically and are shared across all TCs.
(&mut self)
| 815 | let b2 = self.subst_univ(b, us)?; |
| 816 | Ok(KUniv::imax(a2, b2)) |
| 817 | }, |
| 818 | } |
| 819 | } |
| 820 | |
| 821 | // ----------------------------------------------------------------------- |
| 822 | // Per-constant reset (thread-local state only) |
| 823 | // ----------------------------------------------------------------------- |
| 824 | |
| 825 | /// Reset thread-local state between constants. Global caches in `KEnv` are |
| 826 | /// NOT cleared — they grow monotonically and are shared across all TCs. |
| 827 | pub fn reset(&mut self) { |
| 828 | self.ctx.clear(); |
| 829 | self.let_vals.clear(); |
| 830 | self.num_let_bindings = 0; |
| 831 | self.ctx_id = empty_ctx_addr(); |
| 832 | self.ctx_id_stack.clear(); |
| 833 | self.equiv_manager.clear(); |
| 834 | self.infer_only = false; |
| 835 | self.in_native_reduce = false; |
| 836 | self.cheap_recursion_depth = 0; |
| 837 | self.eager_reduce = false; |
| 838 | self.def_eq_depth = 0; |
| 839 | self.def_eq_peak = 0; |
| 840 | // Record fuel consumed by the *previous* constant check (if any) before |
| 841 | // wiping it. `Drop` records the final check in a TypeChecker's lifetime. |
| 842 | self.record_current_fuel_used(); |
| 843 | // Per-constant cache isolation for sound/faithful profile recording: clear |
| 844 | // the cross-constant reduction memo so the next constant re-executes every |
| 845 | // delta-unfold and its heartbeats reflect in-circuit (un-memoized) cost. |
| 846 | if self.env.profile_sink.as_ref().is_some_and(|s| s.isolate) { |
| 847 | self.env.clear_reduction_caches(); |
| 848 | } |
| 849 | self.rec_fuel = max_rec_fuel(); |