Function normalize_imax_dispatch

crates/kernel/src/level.rs:466–503

Dispatch `imax(a, b)` normalization based on `b`'s shape.

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

  w: &KUniv<M>,
  path: &[u64],
  k: u64,
  acc: &mut NormLevel,
) {
  normalize_imax_dispatch(u, w, path, k, acc);
  normalize_imax_dispatch(v, w, path, k, acc);
}

/// Dispatch `imax(a, b)` normalization based on `b`'s shape.
fn normalize_imax_dispatch<M: KernelMode>(
  a: &KUniv<M>,
  b: &KUniv<M>,
  path: &[u64],
  k: u64,
  acc: &mut NormLevel,
) {
  if b.is_zero() {
    norm_add_const(acc, k, path);
  } else if let UnivData::Succ(v, _) = b.data() {
    normalize_aux(a, path, k, acc);
    normalize_aux(v, path, k + 1, acc);
  } else if let UnivData::Max(v, w, _) = b.data() {
    normalize_imax_max(a, v, w, path, k, acc);
  } else if let UnivData::IMax(v, w, _) = b.data() {
    normalize_imax_imax(a, v, w, path, k, acc);
  } else if let UnivData::Param(idx, _, _) = b.data() {
    let idx = *idx;
    if let Some(new_path) = ordered_insert(idx, path) {
      // When param(idx) = 0, imax(a, 0) = 0, contributing k from outer succs.
      norm_add_const(acc, k, path);
      norm_add_node(acc, idx, k, &new_path);
      normalize_aux(a, &new_path, k, acc);
    } else {
      // idx is already in path; outer k Succ's still contribute.
      // Matches Lean4Lean's `acc.addVar v k path`.
      if k != 0 {
        norm_add_var(acc, idx, k, path);
      }
      normalize_aux(a, path, k, acc);
    }
  } else {
    // All UnivData variants for `b` are covered above.