lean ir vs mono

configs.md

1. Milestone Phase Checkpoints (Full Function Dumps)

These dump the entire function representation at major compilation boundaries:

LCNF Phases

• set_option trace.Compiler.init true
  Initial LCNF code directly after conversion from Lean kernel expressions (before optimizations).
• set_option trace.Compiler.saveBase true
  LCNF code at the end of the Base phase (after initial simp, instance pulling, specialization, eager lambda lifting).
• set_option trace.Compiler.saveMono true
  LCNF code at the end of the Mono phase (after monomorphization/lambda lifting/simp, right before closed term extraction).
• set_option trace.Compiler.result true
  Final LCNF code right before emission into Low-level IR (after closed term extraction).

IR Phases (note the lowercase compiler.ir)

• set_option trace.compiler.ir.init true
  Initial Low-level IR converted directly from final LCNF.
• set_option trace.compiler.ir.result true
  Final Low-level IR after all IR optimizations (RC reference-counting, borrow inference @&, boxed wrappers, etc.).

---

2. IR-Level Pass Traces

Inspect specific transformations in the low-level IR backend:

• set_option trace.compiler.ir.rc true — Reference counting (inc / dec) insertion & optimization.
• set_option trace.compiler.ir.borrow true — Borrow inference (@& borrowed parameter markers to avoid RC overhead).
• set_option trace.compiler.ir.boxing true — Unboxed scalar vs boxed object conversions and ._boxed wrapper emission.
• set_option trace.compiler.ir.reset_reuse true & set_option trace.compiler.ir.expand_reset_reuse true — In-place destructive update / memory reuse optimization.
• set_option trace.compiler.ir.simp_case true — Simplification of case branches in IR.
• set_option trace.compiler.ir.elim_dead true — Dead code and variable elimination in IR.
• set_option trace.compiler.ir.push_proj true — Pushing projection operations into branches.

---

3. LCNF Optimization Pass Traces

Detailed diagnostic information for specific LCNF compiler passes:

• set_option trace.Compiler.simp true — Details on simplification and inlining (.inline, .step, .jpCases, .stat).
• set_option trace.Compiler.specialize true — Specialization of polymorphic/higher-order functions (.candidate, .step, .info).
• set_option trace.Compiler.findJoinPoints true / trace.Compiler.jp true — Detection and creation of join points (jp).
• set_option trace.Compiler.extendJoinPointContext true — Join point context propagation.
• set_option trace.Compiler.lambdaLifting true / trace.Compiler.eagerLambdaLifting true — Lambda lifting transformations.
• set_option trace.Compiler.extractClosed true — Extraction of constant subexpressions into auxiliary ._closed_* functions.
• set_option trace.Compiler.cse true — Common subexpression elimination.
• set_option trace.Compiler.elimDeadBranches true — Pruning unreachable match branches.
• set_option trace.Compiler.reduceArity true / trace.Compiler.reduceJpArity true — Unused parameter elimination.
• set_option trace.Compiler.floatLetIn true — Floating let bindings outwards.
• set_option trace.Compiler.toMono true — Monomorphization pass details.

---

4. Broad / Catch-All Traces

• set_option trace.Compiler true — Traces the entry/exit timings and steps of every compiler pass.
• set_option trace.Compiler.trace true — Prints the entire LCNF code after every individual pass checkpoint.
• set_option trace.compiler.ir true — Catch-all for all IR-level logs.

diag.mermaid

diag.txt

Lean 4 Source Code (`.lean`)
                              │
                              ▼
               Elaboration & Kernel Type Checking
                 (Core `Expr` / `ConstantInfo`)
                              │
══════════════════════════════╪════════════════════════════════════════════════════════
 STAGE 1: LCNF Base Phase     │ `toLCNF`
                              ▼
┌──────────────────────────────────────────────────────────────────────────────────────┐
│  init [trace.Compiler.init]                                                          │
│  • A-Normal Form, let-bound expressions, polymorphic types fully present             │
└─────────────────────────────────────┬────────────────────────────────────────────────┘
                                      │
                                      ▼
      ┌──────────────────────────────────────────────────────────────────────────┐
      │  Base Pass Sequence:                                                     │
      │  1. `checkMeta` → `pullInstances` → `cse` → `simp`                       │
      │  2. `floatLetIn` → `findJoinPoints` → `pullFunDecls`                     │
      │  3. `reduceJpArity` → `simp` → `eagerLambdaLifting`                      │
      │  4. `checkTemplateVisibility` → `specialize` → `findJoinPoints`          │
      │  5. `simp` → `cse`                                                       │
      └───────────────────────────────┬──────────────────────────────────────────┘
                                      │
                                      ▼
┌──────────────────────────────────────────────────────────────────────────────────────┐
│  saveBase [trace.Compiler.saveBase]                                                  │
│  • Stored in `baseDeclExt` (queryable via `getBaseDecl?`)                            │
└─────────────────────────────────────┬────────────────────────────────────────────────┘
                                      │
                                      ▼ `inferVisibility` → `toMono`
══════════════════════════════════════╪════════════════════════════════════════════════
 STAGE 2: LCNF Mono Phase             │
                                      ▼
      ┌──────────────────────────────────────────────────────────────────────────┐
      │  Mono Pass Sequence (Part 1):                                            │
      │  1. `simp` → `reduceJpArity` → `structProjCases`                         │
      │  2. `extendJoinPointContext` → `floatLetIn`                              │
      │  3. ★ `reduceArity` ★                                                    │
      │     └─ Spawns `._redArg` (strips ghost type/proof params)                │
      │     └─ Turns original declaration into a forwarding stub                 │
      │  4. `commonJoinPointArgs` → `simp` → `floatLetIn` → `lambdaLifting`      │
      │  5. `splitSCC` (topologically separates `._redArg` & caller)             │
      │  6. `extendJoinPointContext` → `simp` → `elimDeadBranches` → `cse`       │
      └───────────────────────────────┬──────────────────────────────────────────┘
                                      │
                                      ▼
┌──────────────────────────────────────────────────────────────────────────────────────┐
│  saveMono [trace.Compiler.saveMono]                                                  │
│  • Stored in `monoDeclExt` (queryable via `getMonoDecl?` / `#print_lcnf_saveMono`)    │
└─────────────────────────────────────┬────────────────────────────────────────────────┘
                                      │
                                      ▼
      ┌──────────────────────────────────────────────────────────────────────────┐
      │  Mono Post-Passes:                                                       │
      │  • `inferVisibility`                                                     │
      │  • `extractClosed` (floats literals into `._closed_0`, `._closed_1`, ...) │
      └───────────────────────────────┬──────────────────────────────────────────┘
                                      │
                                      ▼
┌──────────────────────────────────────────────────────────────────────────────────────┐
│  result [trace.Compiler.result]                                                      │
│  • Final LCNF (closed terms extracted into references)                               │
│  • Ephemeral: discarded after lowering                                               │
└─────────────────────────────────────┬────────────────────────────────────────────────┘
                                      │
                                      ▼ `toLeanIR`
══════════════════════════════════════╪════════════════════════════════════════════════
 STAGE 3: Low-Level IR (Lean.IR)      │
                                      ▼
┌──────────────────────────────────────────────────────────────────────────────────────┐
│  init [trace.compiler.ir.init]                                                       │
│  • Lowers to tagged object pointers (`obj`, `tobj`, `tagged`)                        │
└─────────────────────────────────────┬────────────────────────────────────────────────┘
                                      │
                                      ▼
      ┌──────────────────────────────────────────────────────────────────────────┐
      │  IR Pass Sequence:                                                       │
      │  1. `push_proj` → `reset_reuse` → `elim_dead` → `simp_case`               │
      │  2. `borrow` (infers `@&` borrowed params to avoid reference counting)   │
      │  3. `boxing` (unboxed scalar vs boxed objects, generates `._boxed`)      │
      │  4. `rc` (inserts explicit `inc` and `dec` memory operations)            │
      │  5. `expand_reset_reuse` → `push_proj`                                   │
      └───────────────────────────────┬──────────────────────────────────────────┘
                                      │
                                      ▼
┌──────────────────────────────────────────────────────────────────────────────────────┐
│  result [trace.compiler.ir.result]                                                   │
│  • Stored in `declMapExt` (queryable via `Lean.IR.findEnvDecl` / `#print_ir`)        │
└─────────────────────────────────────┬────────────────────────────────────────────────┘
                                      │
══════════════════════════════════════╪════════════════════════════════════════════════
 STAGE 4: Backend Emission            │
                                      │
         ┌────────────────────────────┴─────────────────────────────┐
         ▼                                                          ▼
   Standard Native Backend:                                   Alternative Backend:
      Emit C Code (`.c`)                                         (e.g., JS Backend)
         │                                                          │
         ▼                                                          ▼
   Clang / GCC                                                JavaScript / TypeScript
         │
         ▼
   Machine Code (`.so` / `.dylib` / native binary)

gistfile1.lean

import Lean
import Lean.Compiler.LCNF

import Lean.Compiler.ClosedTermCache

section
open Lean Lean.Compiler.LCNF

-- 1. Print IR
elab "#print_ir " id:ident : command => do
  let n := id.getId
  Lean.Elab.Command.liftCoreM do
    if let some d := Lean.IR.findEnvDecl (← getEnv) n then
      IO.println s!"IR for {n}:\n{format d}"
    else
      IO.println s!"No IR found for {n}"
      
elab "#print_lcnf_saveBase " id:ident : command => do
  let n := id.getId
  Lean.Elab.Command.liftCoreM do
    if let some d ← getBaseDecl? n then
      IO.println s!"LCNF (saveBase) for {n}:\n{← ppDecl' d}"
    else
      IO.println s!"No LCNF (saveBase) found for {n}"

-- 2. Print LCNF right after monomorphization (saveMono phase)
elab "#print_lcnf_saveMono " id:ident : command => do
  let n := id.getId
  Lean.Elab.Command.liftCoreM do
    if let some d ← getMonoDecl? n then
      IO.println s!"LCNF (saveMono) for {n}:\n{← ppDecl' d}"
    else
      IO.println s!"No LCNF (saveMono) found for {n}"

-- 3. Print final LCNF (result phase, after post-mono passes like extractClosed)
elab "#print_lcnf_result " id:ident : command => do
  let n := id.getId
  Lean.Elab.Command.liftCoreM do
    let some d ← getMonoDecl? n | do
      IO.println s!"No LCNF found for {n}"
      return

    let decls ← if isClosedTermName (← getEnv) n then
      pure #[d]
    else
      let pm ← getPassManager

      -- Find passes in `monoPassesNoLambda` after `saveMono` (e.g. inferVisibility, extractClosed)
      let mut afterSaveMono := false
      let mut postPasses : Array Pass := #[]
      for pass in pm.monoPassesNoLambda do
        if afterSaveMono then
          postPasses := postPasses.push pass
        else if pass.name == `saveMono then
          afterSaveMono := true

      -- Collect any auxiliary closed declarations already generated for `n`
      let mut closedDecls : Array Decl := #[]
      let mut i := 0
      repeat
        let closedName := n ++ (`_closed).appendIndexAfter i
        if let some cdecl ← getMonoDecl? closedName then
          closedDecls := closedDecls.push cdecl
          i := i + 1
        else
          break

      -- Run the post-mono passes (inferVisibility, extractClosed)
      let resDecls ← CompilerM.run (phase := .mono) do
        let mut decls := #[d]
        for pass in postPasses do
          decls ← withPhase pass.phase <| pass.run decls
        return decls

      pure (closedDecls ++ resDecls)

    -- Print all declarations produced (test1 and its extracted ._closed_* terms)
    for decl in decls do
      let decl ← CompilerM.run (phase := .mono) <| normalizeFVarIds decl
      IO.println s!"LCNF (result) for {decl.name}:\n{← ppDecl' decl}\n"

end
set_option trace.Compiler true   -- print all
set_option trace.Compiler.saveBase true   -- print all
set_option trace.Compiler.saveMono true   -- mono LCNF phase
set_option trace.Compiler.result true     -- final LCNF result

-- @js_export: Expr, instToStringExpr, test1
inductive Expr where
  | add (a : Expr) (b : Expr)
  | mul (a : Expr) (b : Expr)
  | succ (a : Expr)
  | zero


def renderExpr : Expr → String
  | .add a b => "Add(" ++ renderExpr a ++ " " ++ renderExpr b ++ ")"
  | .mul a b => "Mul(" ++ renderExpr a ++ " " ++ renderExpr b ++ ")"
  | .succ a => "Succ(" ++ renderExpr a ++ ")"
  | .zero => "Zero"

instance : ToString Expr where
  toString a := renderExpr a -- will be inlined

-- #print instToStringExpr

def test1 : Expr → String
  | .add .zero .zero => "e1"
  | .mul .zero x => "e2: " ++ toString x -- though toString is used - will use renderExpr anyway, tnx to optimization
  | .add (.succ x) y => "e3: " ++ toString x ++ " " ++ toString y
  | .mul x .zero => "e4: " ++ toString x
  | .mul (.add x y) z => "e5: " ++ toString x ++ " " ++ toString y ++ " " ++ toString z
  | .add x .zero => "e6: " ++ toString x
  | x => "e7: " ++ toString x
#print_lcnf_saveMono renderExpr
#print_lcnf_saveMono test1
#print_lcnf_saveMono test1._closed_0
#print_lcnf_result renderExpr
#print_lcnf_result test1
#print_lcnf_result test1._closed_0
#print_ir renderExpr
#print_ir test1
#print_ir test1._closed_0