Method whnf_core_with_flags

crates/kernel/src/whnf.rs:387–450

Internal flags-threaded core: callers go through [`whnf_core`] or [`whnf_core_for_def_eq`]. Recursive sub-reductions and `try_iota` propagate the same flags so a def-eq structural pass does not accidentally unfold projected values. FULL-mode results are cached in [`KEnv::whnf_core_cache`], mirroring lean4lean's `whnfCoreCache` (TypeChecker.lean:19) and lean4 C++'s `m_whnf_core`. Cheap-mode result

(
    &mut self,
    e: &KExpr<M>,
    flags: WhnfFlags,
  )

        break;
      }

      // Primitive reduction, dispatched by memoized head family — the
      // five recognizers below each collect their own spine and run their
      // own address gauntlet, so probing all of them every iteration was
      // a measurable tax on ordinary (Other-headed) terms. Semantics are
      // unchanged: the families' head-address sets are disjoint, so at
      // most one recognizer could fire anyway. Reference order preserved
      // (native before nat: lean4 `type_checker.cpp:667-672`).
      let family = self.head_prim_family(&cur);
      if family == PrimFamily::Native
        && let Some(reduced) = self.try_reduce_native(&cur)?
      {
        cur = reduced;
        continue;
      }

      // BitVec definitions reduce through Nat comparisons. Keep this before
      // delta so small definitional facts such as `x < 0#w` collapse
      // without unfolding the full Fin-backed representation of BitVec.
      if family == PrimFamily::BitVec
        && let Some(reduced) = self.try_reduce_bitvec(&cur)?
      {
        cur = reduced;
        continue;
      }

      // Nat primitive reduction in main WHNF loop (lean4lean TypeChecker.lean:439).
      // Must run BEFORE delta_unfold_one, so that Nat.sub/Nat.pow/etc. get
      // short-circuited before their bodies (which use Nat.rec) are exposed.
      if family == PrimFamily::Nat
        && let Some(reduced) =
          self.try_reduce_nat_with_succ_mode(&cur, nat_succ_mode)?
      {
        cur = reduced;
        continue;
      }
      // Nat decidability: Nat.decLe/decEq/decLt on literals → Decidable.isTrue/isFalse.
      // Must run BEFORE delta, so the body (which uses dite/Nat.rec) is never exposed.
      if family == PrimFamily::Decidable
        && let Some(reduced) = self.try_reduce_decidable(&cur)?
      {
        cur = reduced;
        continue;
      }

      // String literal primitives (`String.back ""`, literal append,
      // constructor-built strings collapsing to `Str` literals).
      if family == PrimFamily::Str
        && let Some(reduced) = self.try_reduce_string(&cur)?
      {
        cur = reduced;
        continue;
      }

      // Native char values: `Char.ofNat <lit>` with a valid codepoint is
      // a WHNF value. Do not delta-unfold it into its
      // `dite Nat.isValidChar …` body — that grinds through Decidable
      // instance terms and `of_decide_eq_true` proofs per character.