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,
)

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

/// Handle `imax(u, imax(v, w))` = `max(imax(u, w), imax(v, w))`.
fn normalize_imax_imax<M: KernelMode>(
  u: &KUniv<M>,
  v: &KUniv<M>,
  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);