Function ingress_standalone

crates/kernel/src/ingress.rs:1629–1780

(
  const_name: &Name,
  addr: &Address,
  constant: &Constant,
  meta: &ConstantMeta,
  ixon_env: &IxonEnv,
  names: &FxHashMap<Address, Name>,
  name_to_addr: &FxHashMap<Name, Address>,
  intern: &m

  )?;
  let value = ingress_expr(
    &def.value,
    value_root,
    &ctx,
    intern,
    ixon_env,
    &mut cache,
    &mut univ_cache,
    stats,
  )?;
  let lean_all = resolve_all(&all_addrs, names, name_to_addr)?;

  let name = resolve_name(
    match &meta.info {
      ConstantMetaInfo::Def { name, .. } => name,
      _ => &self_id.addr,
    },
    names,
  );

  Ok(vec![(
    self_id,
    KConst::Defn {
      name: M::meta_field(name),
      level_params: M::meta_field(level_params),
      kind: def.kind,
      safety,
      hints,
      lvls: def.lvls,
      ty: typ,
      val: value,
      lean_all: M::meta_field(lean_all),
      block,
    },
  )])
}

#[allow(clippy::too_many_arguments)]
fn ingress_recursor<M: KernelMode>(
  rec: &ixon::constant::Recursor,
  self_id: KId<M>,
  meta: &ConstantMeta,
  ixon_env: &IxonEnv,
  names: &FxHashMap<Address, Name>,
  name_to_addr: &FxHashMap<Name, Address>,
  sharing: &[Arc<IxonExpr>],
  refs: &[Address],
  univs: &[Arc<IxonUniv>],
  block: KId<M>,
  intern: &mut InternTable<M>,
  stats: &mut ConvertStats,
  // Anon callers compute `mut_ctx` structurally; Meta callers pass
  // `None` to fall back to the metadata-derived `build_mut_ctx`.
  mut_ctx_override: Option<Vec<KId<M>>>,
) -> Result<Vec<(KId<M>, KConst<M>)>, String> {
  let mut cache: ExprCache<M> = FxHashMap::default();
  let mut univ_cache: UnivCache<M> = FxHashMap::default();
  let (level_params, arena, type_root, rule_roots, rule_ctor_addrs, all_addrs) =
    match &meta.info {