Function compile_inductive

crates/compile/src/compile.rs:2163–2234

Compile an Inductive. The inductive type gets its own arena. Each constructor gets its own arena via compile_constructor. No CtorMeta duplication — ConstantMeta::Indc only stores constructor name addresses.

(
  ind: &Ind,
  mut_ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,
)

          typ: rewritten[indices[0]].clone(),
          ctors: new_ctors,
        })
      },
      (MutConstKind::Recr, IxonMutConst::Recr(rec)) => {
        let new_rules: Vec<RecursorRule> = rec
          .rules
          .into_iter()
          .enumerate()
          .map(|(ri, rule)| RecursorRule {
            fields: rule.fields,
            rhs: rewritten[indices[ri + 1]].clone(),
          })
          .collect();
        IxonMutConst::Recr(Recursor {
          k: rec.k,
          is_unsafe: rec.is_unsafe,
          lvls: rec.lvls,
          params: rec.params,
          indices: rec.indices,
          motives: rec.motives,
          minors: rec.minors,
          typ: rewritten[indices[0]].clone(),
          rules: new_rules,
        })
      },
      _ => unreachable!("layout mismatch"),
    };
    new_consts.push(new_mc);
  }

  let constant =
    Constant::with_tables(ConstantInfo::Muts(new_consts), sharing, refs, univs);
  MutualBlockSharingResult { constant, hash_consed_size }
}

/// Helper enum for tracking mutual constant layout during sharing.
#[derive(Clone, Copy)]
enum MutConstKind {
  Defn,
  Indc,
  Recr,
}

// ===========================================================================
// Constant compilation
// ===========================================================================

/// Compile a Definition.
/// Arena persists across type + value within a constant.
pub fn compile_definition(
  def: &Def,
  mut_ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,
) -> Result<(Definition, ConstantMeta), CompileError> {
  cache.compiling = Some(def.name.clone());
  let univ_params = &def.level_params;

  // Compile type expression (arena grows)