Function normalize_aux

crates/kernel/src/level.rs:367–437

Recursively flatten a level into canonical form, accumulating into `acc`. `path` tracks the imax-conditioning chain, `k` is the accumulated succ offset.

(
  l: &KUniv<M>,
  path: &[u64],
  k: u64,
  acc: &mut NormLevel,
)

    Err(pos) => {
      let mut result = list.to_vec();
      result.insert(pos, a);
      Some(result)
    },
  }
}

/// Recursively flatten a level into canonical form, accumulating into `acc`.
/// `path` tracks the imax-conditioning chain, `k` is the accumulated succ offset.
fn normalize_aux<M: KernelMode>(
  l: &KUniv<M>,
  path: &[u64],
  k: u64,
  acc: &mut NormLevel,
) {
  match l.data() {
    UnivData::Zero(_) => {
      norm_add_const(acc, k, path);
    },
    UnivData::Succ(inner, _) => {
      normalize_aux(inner, path, k + 1, acc);
    },
    UnivData::Max(a, b, _) => {
      normalize_aux(a, path, k, acc);
      normalize_aux(b, path, k, acc);
    },
    UnivData::IMax(_, b, _) if b.is_zero() => {
      norm_add_const(acc, k, path);
    },
    UnivData::IMax(u, b, _) if matches!(b.data(), UnivData::Succ(..)) => {
      if let UnivData::Succ(v, _) = b.data() {
        normalize_aux(u, path, k, acc);
        normalize_aux(v, path, k + 1, acc);
      }
    },
    UnivData::IMax(u, b, _) if matches!(b.data(), UnivData::Max(..)) => {
      if let UnivData::Max(v, w, _) = b.data() {
        normalize_imax_max(u, v, w, path, k, acc);
      }
    },
    UnivData::IMax(u, b, _) if matches!(b.data(), UnivData::IMax(..)) => {
      if let UnivData::IMax(v, w, _) = b.data() {
        normalize_imax_imax(u, v, w, path, k, acc);
      }
    },
    UnivData::IMax(u, b, _) if matches!(b.data(), UnivData::Param(..)) => {
      if let UnivData::Param(idx, _, _) = b.data() {
        let idx = *idx;
        if let Some(new_path) = ordered_insert(idx, path) {
          // When param(idx) = 0, imax(u, 0) = 0, contributing k from outer succs.
          norm_add_const(acc, k, path);
          norm_add_node(acc, idx, k, &new_path);
          normalize_aux(u, &new_path, k, acc);
        } else {
          // Param(idx) is already in path (so we're in an `imax(u, v)` where
          // v = Param(idx) and idx is fixed > 0 by the enclosing chain).
          // The outer k Succ's still contribute when idx > 0, which it is
          // along this path. Matches Lean4Lean's `acc.addVar v k path`.
          if k != 0 {