Function lean_expr_to_zexpr_raw

crates/kernel/src/ingress.rs:2291–2529

(
  expr: &LeanExpr,
  pn: &[Name],
  binder_names: &mut Vec<Name>,
  intern: &mut InternTable<Meta>,
  n2a: Option<&DashMap<Name, Address>>,
  aux_n2a: Option<&DashMap<Name, Address>>,
  mut cache: O

pub fn lean_level_to_kuniv(lvl: &Level, param_names: &[Name]) -> KUniv<Meta> {
  match lvl.as_data() {
    LevelData::Succ(l, _) => KUniv::succ(lean_level_to_kuniv(l, param_names)),
    LevelData::Max(a, b, _) => KUniv::max(
      lean_level_to_kuniv(a, param_names),
      lean_level_to_kuniv(b, param_names),
    ),
    LevelData::Imax(a, b, _) => KUniv::imax(
      lean_level_to_kuniv(a, param_names),
      lean_level_to_kuniv(b, param_names),
    ),
    LevelData::Param(name, _) => {
      let idx =
        param_names.iter().position(|n| n == name).unwrap_or_else(|| {
          panic!(
            "unknown level param `{}` not found in param_names {:?}",
            name.pretty(),
            param_names.iter().map(|n| n.pretty()).collect::<Vec<_>>()
          )
        }) as u64;
      KUniv::param(idx, name.clone())
    },
    LevelData::Zero(_) => KUniv::zero(),
    LevelData::Mvar(name, _) => {
      panic!(
        "unexpected level metavariable `{}` in elaborated kernel term",
        name.pretty()
      );
    },
  }
}

/// Resolve a Lean Name to an Address, using real Ixon address if available.
///
/// Checks `name_to_ixon_addr` first (real compiled address), falls back to
/// `Address::from_blake3_hash(*name.get_hash())` for constants not yet compiled.
pub fn resolve_lean_name_addr(
  name: &Name,
  name_to_ixon_addr: Option<&DashMap<Name, Address>>,
  aux_n2a: Option<&DashMap<Name, Address>>,
) -> Address {
  if let Some(map) = name_to_ixon_addr
    && let Some(entry) = map.get(name)
  {
    return entry.value().clone();
  }
  if let Some(map) = aux_n2a
    && let Some(entry) = map.get(name)
  {
    return entry.value().clone();
  }
  Address::from_blake3_hash(*name.get_hash())
}

/// Convert a LeanExpr to KExpr<Meta>.
///
/// `param_names` provides the positional mapping for universe level params.
/// `name_to_ixon_addr` maps Lean names to real Ixon addresses for already-compiled
/// constants. Falls back to name hash for constants not yet compiled.
/// Compute a stable hash for a `param_names` slice, used as part of the