Function compile_expr

crates/compile/src/compile.rs:619–1453

Compile a Lean expression to an Ixon expression. Builds arena-based metadata in cache.arena with bottom-up allocation.

(
  expr: &LeanExpr,
  univ_params: &[Name],
  mut_ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,
)

pub fn collect_mut_const_exprs<'a>(
  cnst: &'a MutConst,
  exprs: &mut Vec<(&'a LeanExpr, &'a [Name])>,
) {
  match cnst {
    MutConst::Defn(def) => {
      let lvls = def.level_params.as_slice();
      exprs.push((&def.typ, lvls));
      exprs.push((&def.value, lvls));
    },
    MutConst::Indc(ind) => {
      exprs.push((&ind.ind.cnst.typ, ind.ind.cnst.level_params.as_slice()));
      for ctor in &ind.ctors {
        exprs.push((&ctor.cnst.typ, ctor.cnst.level_params.as_slice()));
      }
    },
    MutConst::Recr(rec) => {
      let lvls = rec.cnst.level_params.as_slice();
      exprs.push((&rec.cnst.typ, lvls));
      for rule in &rec.rules {
        exprs.push((&rule.rhs, lvls));
      }
    },
  }
}

// ===========================================================================
// Expression compilation
// ===========================================================================

/// Compile a Lean expression to an Ixon expression.
/// Builds arena-based metadata in cache.arena with bottom-up allocation.
pub fn compile_expr(
  expr: &LeanExpr,
  univ_params: &[Name],
  mut_ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,
) -> Result<Arc<Expr>, CompileError> {
  use ixon::metadata::CallSiteEntry;

  // Stack-based iterative compilation to avoid stack overflow
  enum Frame {
    Compile(LeanExpr),
    BuildApp,
    BuildLam(Address, BinderInfo),
    BuildAll(Address, BinderInfo),
    BuildLet(Address, bool),
    BuildProj(u64, u64, Address), // type_ref_idx, field_idx, struct_name_addr
    WrapMdata(Vec<KVMap>),
    Cache(LeanExpr),
    /// Build a surgered call-site from compiled head + canonical args + collapsed args.
    BuildCallSite {
      name_addr: Address,
      /// Source-order entries. `meta` fields are placeholder 0 — filled during build.
      entries: Vec<CallSiteEntry>,
      /// Number of canonical (kept) args on the results stack.
      n_canonical: usize,
      /// Number of collapsed args on the results stack (after canonical args).