Method try_proj_reduce

crates/kernel/src/whnf.rs:1390–1443

(
    &mut self,
    id: &KId<M>,
    field: u64,
    wval: &KExpr<M>,
  )

          log::info!(
            "[nat_iota_trace] rec={} major_bits={} spine={} major_idx={}",
            rec_id,
            val.0.bits(),
            spine.len(),
            recr.major_idx
          );
        }
      }
      major_was_nat_lit = true;
      major_whnf = self.nat_to_constructor(&val.clone());
    }
    if let Some(cleaned) = self.cleanup_nat_offset_major(&major_whnf)? {
      major_whnf = cleaned;
    }
    // String literal → constructor form (matching lean4lean
    // Reduce.lean:71 / C++ inductive.h:95). The expansion takes one
    // delta step past `String.ofList` (see `str_lit_to_ctor_app`) so the
    // native collapse rule in `try_reduce_string` can't fold it straight
    // back into the literal; constructor fields stay lazy.
    if let ExprData::Str(val, _, _) = major_whnf.data() {
      let val = val.clone();
      major_whnf = self.str_lit_to_ctor_app(&val)?;
    }
    // Native char values are kept stuck by whnf (they never unfold to
    // their `dite`-validity body on their own). A recursor that
    // genuinely scrutinizes a char pays for the structural expansion
    // here, once — exactly what pre-native reduction did on every whnf.
    // Cheap mode leaves the major stuck, as it did before the fast path
    // (`Char.ofNat` is a Defn head that cheap whnf never delta-unfolds).
    if !flags.cheap_rec
      && self.char_lit_value(&major_whnf).is_some()
      && let Some(unfolded) = self.delta_unfold_one(&major_whnf)?
    {
      major_whnf = self.whnf(&unfolded)?;
    }

    // Check if major is a constructor application
    let (ctor_head, ctor_args) = collect_app_spine(&major_whnf);
    let is_ctor = match ctor_head.data() {
      ExprData::Const(id, _, _) => {
        matches!(self.try_get_const(id)?, Some(KConst::Ctor { .. }))
      },
      _ => false,
    };

    // Diagnostic: when the major doesn't reduce to a ctor, iota is stuck.
    // Surface which recursor + major shape we got \u2014 the major's head
    // tells us which downstream reduction (delta, iota, nat, int) failed
    // to complete.
    if !is_ctor && let Some(filter) = IX_IOTA_STUCK.as_ref() {
      let rec_name = format!("{rec_id}");
      if filter.is_empty() || rec_name.contains(filter) {
        log::info!("[iota stuck] rec={rec_name}");
        log::info!("[iota stuck]   major:      {major}");
        log::info!("[iota stuck]   major whnf: {major_whnf}");
      }
    }