Function roundtrip_block

crates/compile/src/decompile.rs:2406–2943

Compile a batch of regenerated `MutConst`s as a mutual block (mirroring `compile_aux_block`), then decompile each member with original metadata from `named.original` to restore binder names. Returns a map from constant name to decompiled `LeanConstantInfo`. Constructor entries from inductives are included under their own names. `orig_env` is the immutable original Lean environment from the compi

(
  consts: &[LeanMutConst],
  generated_consts: &FxHashMap<Name, LeanConstantInfo>,
  orig_env: Option<&LeanEnv>,
  stt: &CompileState,
  dstt: &DecompileState,
)

/// Convert a `BRecOnDef` to a `LeanConstantInfo`.
///
/// Replicates Lean's `Lean/Meta/Constructions/BRecOn.lean` per-kind decisions:
///
/// | Shape                 | Emits                    | Hints    |
/// |-----------------------|--------------------------|----------|
/// | `.brecOn` (Prop, safe)   | `ThmInfo`                   | —        |
/// | `.brecOn` (Prop, unsafe) | `DefnInfo` (`Unsafe`)       | `Opaque` |
/// | `.brecOn` (Type)         | `DefnInfo` (`Safe`/`Unsafe`) | `Abbrev` |
/// | `.brecOn.go`             | `DefnInfo` (`Safe`/`Unsafe`) | `Abbrev` |
/// | `.brecOn.eq` (safe)      | `ThmInfo`                   | —        |
/// | `.brecOn.eq` (unsafe)    | `DefnInfo` (`Unsafe`)       | `Opaque` |
///
/// The unsafe-`.eq` flip mirrors Lean's `mkThmOrUnsafeDef`
/// (`Lean/Environment.lean:2797`), which replaces a theorem with an unsafe
/// definition whenever `env.hasUnsafe` fires on the type or value.
fn brecon_def_to_lean(
  def: &crate::compile::aux_gen::brecon::BRecOnDef,
) -> LeanConstantInfo {
  let cnst = ConstantVal {
    name: def.name.clone(),
    level_params: def.level_params.clone(),
    typ: def.typ.clone(),
  };

  let is_eq = def.name.last_str() == Some("eq");
  // Emit `ThmInfo` when Lean would have emitted `.thmDecl`: Prop-level
  // `.brecOn` or safe Type-level `.brecOn.eq`. Unsafe cases always flatten
  // into an unsafe `DefnInfo` with opaque reducibility.
  let as_theorem = (def.is_prop || is_eq) && !def.is_unsafe;

  if as_theorem {
    LeanConstantInfo::ThmInfo(TheoremVal {
      cnst,
      value: def.value.clone(),
      all: vec![def.name.clone()],
    })
  } else {
    // Hints: `.opaque` matches Lean's `mkThmOrUnsafeDef` for the unsafe-eq
    // flip (and unsafe Prop-level `.brecOn`, which in practice never
    // happens — Lean forbids `unsafe` in Prop — but we honor the flag).
    // `.abbrev` matches `mkDefinitionValInferringUnsafe … .abbrev` for
    // `.brecOn` / `.brecOn.go`.
    let hints = if def.is_unsafe && (def.is_prop || is_eq) {
      ReducibilityHints::Opaque
    } else {
      ReducibilityHints::Abbrev
    };
    LeanConstantInfo::DefnInfo(DefinitionVal {
      cnst,
      value: def.value.clone(),
      hints,
      safety: def_safety(def.is_unsafe),
      all: vec![def.name.clone()],
    })
  }
}

fn ci_kind(ci: &LeanConstantInfo) -> &'static str {