Function decompile_const

crates/compile/src/decompile.rs:1795–1891

Decompile a single constant (non-mutual).

(
  name: &Name,
  named: &Named,
  stt: &CompileState,
  dstt: &DecompileState,
)

    cnst,
    induct: induct_name,
    cidx: Nat::from(ctor.cidx),
    num_params: Nat::from(ctor.params),
    num_fields: Nat::from(ctor.fields),
    is_unsafe: ctor.is_unsafe,
  })
}

/// Decompile an Inductive.
/// Constructor metadata is resolved from Named entries, not from CtorMeta.
fn decompile_inductive(
  ind: &Inductive,
  meta: &ConstantMeta,
  cache: &mut BlockCache,
  stt: &CompileState,
  dstt: &DecompileState,
) -> Result<(InductiveVal, Vec<ConstructorVal>), DecompileError> {
  let name = decompile_name_from_meta(meta, stt)?;
  let level_params = decompile_level_names_from_meta(meta, stt)?;

  let (arena, type_root) = get_arena_and_type_root(meta);
  let typ = decompile_expr(
    &ind.typ,
    arena,
    type_root,
    &level_params,
    cache,
    stt,
    dstt,
  )?;

  // Extract constructor name addresses and all from metadata. The
  // non-Indc arm should be unreachable — `decompile_inductive` is only
  // called when the meta is an Indc variant. If we ever get here with
  // a different variant shape, that's structural corruption, not a
  // silently recoverable condition.
  let (ctor_name_addrs, all) = match &meta.info {
    ConstantMetaInfo::Indc { ctors, all: all_addrs, .. } => {
      let all = all_addrs
        .iter()
        .map(|a| decompile_name(a, stt))
        .collect::<Result<Vec<_>, _>>()?;
      (ctors.as_slice(), all)
    },
    other => {
      return Err(DecompileError::BadConstantFormat {
        msg: format!(
          "decompile_inductive for '{}': expected ConstantMetaInfo::Indc, \
           got variant with discriminant {:?}",
          name.pretty(),
          std::mem::discriminant(other),
        ),
      });
    },
  };

  let mut ctors = Vec::with_capacity(ind.ctors.len());
  let mut ctor_names = Vec::new();