fix: sanitize build and mimalloc

Reason: we are running the old and new code generators on this branch.

CMakeLists.txt

@@ -20,6 +20,9 @@ foreach(var ${vars})
     elseif("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
+  elseif("${var}" MATCHES "USE_MIMALLOC")
+    list(APPEND CL_ARGS "-D${var}=${${var}}")
+    list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
   elseif(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY"))
     list(APPEND PLATFORM_ARGS "-D${var}=${${var}}")
   endif()

CMakePresets.json

@@ -30,6 +30,7 @@
         "LEANC_EXTRA_CC_FLAGS": "-fsanitize=address,undefined",
         "LEAN_EXTRA_LINKER_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
         "SMALL_ALLOCATOR": "OFF",
+        "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
         "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000"
       },

src/CMakeLists.txt

@@ -175,6 +175,10 @@ string(APPEND LEANC_EXTRA_CC_FLAGS " -fstack-clash-protection")
 string(APPEND CMAKE_CXX_FLAGS " -fwrapv")
 string(APPEND LEANC_EXTRA_CC_FLAGS " -fwrapv")
 
+if(${STAGE} EQUAL 1)
+  string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE=false")
+endif()
+
 if(NOT MULTI_THREAD)
   message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel")
   set(AUTO_THREAD_FINALIZATION OFF)

src/Init/Data/Vector/Extract.lean

@@ -7,6 +7,8 @@ prelude
 import Init.Data.Vector.Lemmas
 import Init.Data.Array.Extract
 
+set_option maxHeartbeats 20000000
+
 /-!
 # Lemmas about `Vector.extract`
 -/

src/Lean/Compiler/IR.lean

@@ -22,6 +22,7 @@ import Lean.Compiler.IR.ElimDeadBranches
 import Lean.Compiler.IR.EmitC
 import Lean.Compiler.IR.CtorLayout
 import Lean.Compiler.IR.Sorry
+import Lean.Compiler.IR.ToIR
 
 namespace Lean.IR
 

src/Lean/Compiler/IR/Basic.lean

@@ -180,7 +180,7 @@ structure CtorInfo where
   size : Nat
   usize : Nat
   ssize : Nat
-  deriving Repr
+  deriving Inhabited, Repr
 
 def CtorInfo.beq : CtorInfo → CtorInfo → Bool
   | ⟨n₁, cidx₁, size₁, usize₁, ssize₁⟩, ⟨n₂, cidx₂, size₂, usize₂, ssize₂⟩ =>
@@ -223,6 +223,7 @@ inductive Expr where
   | lit (v : LitVal)
   /-- Return `1 : uint8` Iff `RC(x) > 1` -/
   | isShared (x : VarId)
+  deriving Inhabited
 
 @[export lean_ir_mk_ctor_expr]  def mkCtorExpr (n : Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : Array Arg) : Expr :=
   Expr.ctor ⟨n, cidx, size, usize, ssize⟩ ys

src/Lean/Compiler/IR/CtorLayout.lean

@@ -15,6 +15,7 @@ inductive CtorFieldInfo where
   | object (i : Nat)
   | usize  (i : Nat)
   | scalar (sz : Nat) (offset : Nat) (type : IRType)
+  deriving Inhabited
 
 namespace CtorFieldInfo
 

src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -165,6 +165,7 @@ structure InterpContext where
 structure InterpState where
   assignments : Array Assignment
   funVals     : PArray Value -- we take snapshots during fixpoint computations
+  visitedJps  : Array (Std.HashSet JoinPointId)
 
 abbrev M := ReaderT InterpContext (StateM InterpState)
 
@@ -239,6 +240,10 @@ def updateJPParamsAssignment (ys : Array Param) (xs : Array Arg) : M Bool := do
       modify fun s => { s with assignments := s.assignments.modify currFnIdx fun a => a.insert y.x newVal }
       pure true
 
+def markJPVisited (j : JoinPointId) : M Bool := do
+  let currFnIdx := (← read).currFnIdx
+  modifyGet fun s => ⟨!(s.visitedJps[currFnIdx]!.contains j), { s with visitedJps := s.visitedJps.modify currFnIdx fun a => a.insert j }⟩
+
 private partial def resetNestedJPParams : FnBody → M Unit
   | FnBody.jdecl _ ys _ k => do
     ys.forM resetParamAssignment
@@ -273,7 +278,8 @@ partial def interpFnBody : FnBody → M Unit
     let ys := (ctx.lctx.getJPParams j).get!
     let b  := (ctx.lctx.getJPBody j).get!
     let updated ← updateJPParamsAssignment ys xs
-    if updated then
+    let isFirstVisit ← markJPVisited j
+    if updated || isFirstVisit then
       -- We must reset the value of nested join-point parameters since they depend on `ys` values
       resetNestedJPParams b
       interpFnBody b
@@ -283,7 +289,7 @@ partial def interpFnBody : FnBody → M Unit
 
 def inferStep : M Bool := do
   let ctx ← read
-  modify fun s => { s with assignments := ctx.decls.map fun _ => {} }
+  modify fun s => { s with assignments := ctx.decls.map fun _ => {}, visitedJps := ctx.decls.map fun _ => {} }
   ctx.decls.size.foldM (init := false) fun idx _ modified => do
     match ctx.decls[idx] with
     | .fdecl (xs := ys) (body := b) .. => do
@@ -295,7 +301,11 @@ def inferStep : M Bool := do
         let s ← get
         let newVals := s.funVals[idx]!
         pure (modified || currVals != newVals)
-    | .extern .. => pure modified
+    | .extern .. => do
+      let currVals := (← get).funVals[idx]!
+      updateCurrFnSummary .top
+      let newVals := (← get).funVals[idx]!
+      pure (modified || currVals != newVals)
 
 partial def inferMain : M Unit := do
   let modified ← inferStep
@@ -332,8 +342,9 @@ def elimDeadBranches (decls : Array Decl) : CompilerM (Array Decl) := do
   let env := s.env
   let assignments : Array Assignment := decls.map fun _ => {}
   let funVals := mkPArray decls.size Value.bot
+  let visitedJps := decls.map fun _ => {}
   let ctx : InterpContext := { decls := decls, env := env }
-  let s : InterpState := { assignments := assignments, funVals := funVals }
+  let s : InterpState := { assignments, funVals, visitedJps }
   let (_, s) := (inferMain ctx).run s
   let funVals := s.funVals
   let assignments := s.assignments

src/Lean/Compiler/IR/ToIR.lean

@@ -0,0 +1,436 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Cameron Zwarich
+-/
+prelude
+import Lean.Compiler.LCNF.Basic
+import Lean.Compiler.LCNF.CompilerM
+import Lean.Compiler.LCNF.PhaseExt
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.CompilerM
+import Lean.Compiler.IR.CtorLayout
+import Lean.CoreM
+import Lean.Environment
+
+namespace Lean.IR
+
+open Lean.Compiler (LCNF.AltCore LCNF.Arg LCNF.Code LCNF.Decl LCNF.DeclValue LCNF.LCtx LCNF.LetDecl
+                    LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.getMonoDecl?)
+
+namespace ToIR
+
+inductive FVarClassification where
+  | var (id : VarId)
+  | joinPoint (id : JoinPointId)
+  | erased
+
+structure BuilderState where
+  fvars : Std.HashMap FVarId FVarClassification := {}
+  nextId : Nat := 1
+
+abbrev M := StateT BuilderState CoreM
+
+def M.run (x : M α) : CoreM α := do
+  x.run' {}
+
+def bindVar (fvarId : FVarId) : M VarId := do
+  modifyGet fun s =>
+    let varId := { idx := s.nextId }
+    ⟨varId, { s with fvars := s.fvars.insertIfNew fvarId (.var varId),
+                     nextId := s.nextId + 1 }⟩
+
+def bindVarToVarId (fvarId : FVarId) (varId : VarId) : M Unit := do
+  modify fun s => { s with fvars := s.fvars.insertIfNew fvarId (.var varId) }
+
+def newVar : M VarId := do
+  modifyGet fun s =>
+    let varId := { idx := s.nextId }
+    ⟨varId, { s with nextId := s.nextId + 1 }⟩
+
+def bindJoinPoint (fvarId : FVarId) : M JoinPointId := do
+  modifyGet fun s =>
+    let joinPointId := { idx := s.nextId }
+    ⟨joinPointId, { s with fvars := s.fvars.insertIfNew fvarId (.joinPoint joinPointId),
+                           nextId := s.nextId + 1 }⟩
+
+def bindErased (fvarId : FVarId) : M Unit := do
+  modify fun s => { s with fvars := s.fvars.insertIfNew fvarId .erased }
+
+def findDecl (n : Name) : M (Option Decl) :=
+  return findEnvDecl (← Lean.getEnv) n
+
+def addDecl (d : Decl) : M Unit :=
+  Lean.modifyEnv fun env => declMapExt.addEntry (env.addExtraName d.name) d
+
+def lowerLitValue (v : LCNF.LitValue) : LitVal :=
+  match v with
+  | .natVal n => .num n
+  | .strVal s => .str s
+
+def lowerEnumToScalarType (name : Name) : M (Option IRType) := do
+  let env ← Lean.getEnv
+  let some (.inductInfo inductiveVal) := env.find? name | return none
+  let ctorNames := inductiveVal.ctors
+  let numCtors := ctorNames.length
+  -- TODO: Use something better here
+  for ctorName in ctorNames do
+    let some (.ctorInfo ctorVal) := env.find? ctorName | panic! "expected valid constructor name"
+    if ctorVal.type.isForall then return none
+  return if numCtors == 1 then
+    none
+  else if numCtors < Nat.pow 2 8 then
+    some .uint8
+  else if numCtors < Nat.pow 2 16 then
+    some .uint16
+  else if numCtors < Nat.pow 2 32 then
+    some .uint32
+  else
+    none
+
+def lowerType (e : Lean.Expr) : M IRType := do
+  match e with
+  | .const name .. =>
+    match name with
+    | ``UInt8 | ``Bool => return .uint8
+    | ``UInt16 => return .uint16
+    | ``UInt32 => return .uint32
+    | ``UInt64 => return .uint64
+    | ``USize => return .usize
+    | ``Float => return .float
+    | ``Float32 => return .float32
+    | ``lcErased => return .irrelevant
+    | _ =>
+      if let some scalarType ← lowerEnumToScalarType name then
+        return scalarType
+      else
+        return .object
+  | .app f _ =>
+    if let .const name _ := f.headBeta then
+      if let some scalarType ← lowerEnumToScalarType name then
+        return scalarType
+      else
+        return .object
+    else
+      return .object
+  | .forallE .. => return .object
+  | _ => panic! "invalid type"
+
+-- TODO: This should be cached.
+def getCtorInfo (name : Name) : M (CtorInfo × (List CtorFieldInfo)) := do
+  match getCtorLayout (← Lean.getEnv) name with
+  | .ok ctorLayout =>
+    return ⟨{
+      name,
+      cidx := ctorLayout.cidx,
+      size := ctorLayout.numObjs,
+      usize := ctorLayout.numUSize,
+      ssize := ctorLayout.scalarSize
+    }, ctorLayout.fieldInfo⟩
+  | .error .. => panic! "unrecognized constructor"
+
+def lowerArg (a : LCNF.Arg) : M Arg := do
+  match a with
+  | .fvar fvarId =>
+    match (← get).fvars[fvarId]? with
+    | some (.var varId) => return .var varId
+    | some .erased => return .irrelevant
+    | some (.joinPoint ..) => panic! "join point used as arg"
+    | none => panic! "unbound fvar arg"
+  | .erased | .type .. => return .irrelevant
+
+inductive TranslatedProj where
+  | expr (e : Expr)
+  | erased
+  deriving Inhabited
+
+def lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo) : TranslatedProj :=
+  match field with
+  | .object i => .expr (.proj i base)
+  | .usize i => .expr (.uproj i base)
+  | .scalar _ offset _ => .expr (.sproj (ctorInfo.size + ctorInfo.usize) offset base)
+  | .irrelevant => .erased
+
+structure ScalarArg where
+  offset : Nat
+  type : IRType
+  arg : Arg
+  deriving Inhabited
+
+inductive TranslatedLetValue where
+  | expr (e : Expr)
+  | var (varId : VarId)
+  | ctor (ctorInfo: CtorInfo) (objArgs : Array Arg) (usizeArgs : Array Arg) (scalarArgs : Array ScalarArg)
+  | apOfExprResult (e : Expr) (restArgs : Array Arg)
+  | natSucc (arg : Arg)
+  | erased
+  | unreachable
+  deriving Inhabited
+
+def lowerLetValue (v : LCNF.LetValue) : M TranslatedLetValue := do
+  match v with
+  | .value litValue =>
+    return .expr (.lit (lowerLitValue litValue))
+  | .proj typeName i fvarId =>
+    match (← get).fvars[fvarId]? with
+    | some (.var varId) =>
+      -- TODO: have better pattern matching here
+      let some (.inductInfo { ctors, .. }) := (← Lean.getEnv).find? typeName | panic! "projection of non-inductive type"
+      let ctorName := ctors[0]!
+      let ⟨ctorInfo, fields⟩ ← getCtorInfo ctorName
+      return match lowerProj varId ctorInfo fields[i]! with
+      | .expr e => .expr e
+      | .erased => .erased
+    | some .erased => return .erased
+    | some (.joinPoint ..) => panic! "expected var or erased value"
+    | none => panic! "reference to unbound variable"
+  | .const ``Nat.succ _ args =>
+    let irArgs ← args.mapM lowerArg
+    return .natSucc irArgs[0]!
+  | .const name _ args =>
+    let irArgs ← args.mapM lowerArg
+    if let some decl ← LCNF.getMonoDecl? name then
+      let numArgs := irArgs.size
+      let numParams := decl.params.size
+      if numArgs < numParams then
+        return .expr (.pap name irArgs)
+      else if numArgs == numParams then
+        return .expr (.fap name irArgs)
+      else
+        let firstArgs := irArgs.extract 0 numParams
+        let restArgs := irArgs.extract numParams irArgs.size
+        return .apOfExprResult (.fap name firstArgs) restArgs
+    else
+      let env ← Lean.getEnv
+      match env.find? name with
+      | some (.ctorInfo ctorVal) =>
+        if isExtern env name then
+          -- TODO: share this
+          if let some irDecl ← findDecl name then
+            let numArgs := irArgs.size
+            let numParams := irDecl.params.size
+            if numArgs < numParams then
+              return .expr (.pap name irArgs)
+            else if numArgs == numParams then
+              return .expr (.fap name irArgs)
+            else
+              let firstArgs := irArgs.extract 0 numParams
+              let restArgs := irArgs.extract numParams irArgs.size
+              return .apOfExprResult (.fap name firstArgs) restArgs
+          else
+              return .expr (.fap name irArgs)
+        else
+          let ⟨ctorInfo, fields⟩ ← getCtorInfo name
+          let mut objArgs := #[]
+          let mut usizeArgs := #[]
+          let mut scalarArgs := #[]
+          for field in fields, arg in args.extract (start := ctorVal.numParams) do
+            match arg with
+            | .fvar fvarId =>
+              match (← get).fvars[fvarId]? with
+              | some (.var varId) =>
+                match field with
+                | .object .. =>
+                  objArgs := objArgs.push (.var varId)
+                | .usize .. =>
+                  usizeArgs := usizeArgs.push (.var varId)
+                | .scalar _ offset argType =>
+                  scalarArgs := scalarArgs.push { offset, type := argType, arg := (.var varId) }
+                | .irrelevant => pure ()
+              | some .erased => pure ()
+              | some (.joinPoint ..) => panic! "join point used as arg"
+              | none => panic! "unbound fvar arg"
+            | .type _ | .erased =>
+              match field with
+              | .object .. =>
+                objArgs := objArgs.push .irrelevant
+              | .irrelevant => pure ()
+              | .usize .. | .scalar .. => panic! "unexpected scalar field"
+          return .ctor ctorInfo objArgs usizeArgs scalarArgs
+      | some (.axiomInfo ..) =>
+        if name == ``Quot.lcInv then
+          match irArgs[2]! with
+          | .var varId => return .var varId
+          | .irrelevant => return .erased
+        else if name == ``lcUnreachable then
+          return .unreachable
+        else
+          throwError f!"axiom '{name}' not supported by code generator; consider marking definition as 'noncomputable'"
+      | some (.quotInfo ..) =>
+        if name == ``Quot.mk then
+          match irArgs[2]! with
+          | .var varId => return .var varId
+          | .irrelevant => return .erased
+        else
+          throwError f!"quot {name} unsupported by code generator"
+      | some (.defnInfo ..) | some (.opaqueInfo ..) =>
+        -- TODO: share this
+        if let some irDecl ← findDecl name then
+          let numArgs := irArgs.size
+          let numParams := irDecl.params.size
+          if numArgs < numParams then
+            return .expr (.pap name irArgs)
+          else if numArgs == numParams then
+            return .expr (.fap name irArgs)
+          else
+            let firstArgs := irArgs.extract 0 numParams
+            let restArgs := irArgs.extract numParams irArgs.size
+            return .apOfExprResult (.fap name firstArgs) restArgs
+        else
+            return .expr (.fap name irArgs)
+      | some (.inductInfo ..) => panic! "induct unsupported by code generator"
+      | some (.recInfo ..) =>
+        throwError f!"code generator does not support recursor '{name}' yet, consider using 'match ... with' and/or structural recursion"
+      | some (.thmInfo ..) => panic! "thm unsupported by code generator"
+      | none => panic! "reference to unbound name"
+  | .fvar fvarId args =>
+    let irArgs ← args.mapM lowerArg
+    match (← get).fvars[fvarId]? with
+    | some (.var id) => return .expr (.ap id irArgs)
+    | some .erased => return .erased
+    | some (.joinPoint ..) => panic! "expected var or erased value"
+    | .none => panic! "reference to unbound variable"
+  | .erased => return .erased
+
+def lowerParam (p : LCNF.Param) : M Param := do
+  let x ← bindVar p.fvarId
+  let ty ← lowerType p.type
+  return { x, borrow := p.borrow, ty }
+
+mutual
+partial def lowerCode (c : LCNF.Code) : M FnBody := do
+  match c with
+  | .let decl k =>
+    let type ← lowerType decl.type
+    match (← lowerLetValue decl.value) with
+    | .expr e =>
+      let var ← bindVar decl.fvarId
+      let type := match e with
+      | .ctor .. | .pap .. | .proj .. => .object
+      | _ => type
+      return .vdecl var type e (← lowerCode k)
+    | .var varId =>
+      bindVarToVarId decl.fvarId varId
+      lowerCode k
+    | .ctor ctorInfo objArgs usizeArgs scalarArgs =>
+      let var ← bindVar decl.fvarId
+      let rec emitScalarArgs (i : Nat) : M FnBody :=
+        if i == scalarArgs.size then
+          lowerCode k
+        else if let ⟨offset, argType, .var argVar⟩ := scalarArgs[i]! then
+          return .sset var (ctorInfo.size + ctorInfo.usize) offset argVar argType (← emitScalarArgs (i + 1))
+        else
+          emitScalarArgs (i + 1)
+      let rec emitUSizeSets (i : Nat) : M FnBody :=
+        if i == usizeArgs.size then
+          emitScalarArgs 0
+        else if let .var argVar := usizeArgs[i]! then
+          return .uset var (ctorInfo.size + i) argVar (← emitUSizeSets (i + 1))
+        else
+          emitUSizeSets (i + 1)
+      return .vdecl var .object (.ctor ctorInfo objArgs) (← emitUSizeSets 0)
+    | .apOfExprResult e restArgs =>
+      let var ← bindVar decl.fvarId
+      let tmpVar ← newVar
+      return .vdecl tmpVar .object e (.vdecl var type (.ap tmpVar restArgs) (← lowerCode k))
+    | .natSucc arg =>
+      let var ← bindVar decl.fvarId
+      let tmpVar ← newVar
+      return .vdecl tmpVar .object (.lit (.num 1)) (.vdecl var type (.fap ``Nat.add #[arg, (.var tmpVar)]) (← lowerCode k))
+    | .erased =>
+      bindErased decl.fvarId
+      lowerCode k
+    | .unreachable => return .unreachable
+  | .jp decl k =>
+    let joinPoint ← bindJoinPoint decl.fvarId
+    let params ← decl.params.mapM lowerParam
+    let body ← lowerCode decl.value
+    return .jdecl joinPoint params body (← lowerCode k)
+  | .jmp fvarId args =>
+    match (← get).fvars[fvarId]? with
+    | some (.joinPoint joinPointId) =>
+      return .jmp joinPointId (← args.mapM lowerArg)
+    | some (.var ..) | some .erased => panic! "expected join point"
+    | none => panic! "reference to unbound variable"
+  | .cases cases =>
+    match (← get).fvars[cases.discr]? with
+    | some (.var varId) =>
+      return .case cases.typeName
+                  varId
+                  (← lowerType cases.resultType)
+                  (← cases.alts.mapM (lowerAlt varId))
+    | some (.joinPoint ..) | some .erased => panic! "expected var"
+    | none => panic! "reference to unbound variable"
+  | .return fvarId =>
+    let arg := match (← get).fvars[fvarId]? with
+    | some (.var varId) => .var varId
+    | some .erased => .irrelevant
+    | some (.joinPoint ..) => panic! "expected var or erased value"
+    | none => panic! "reference to unbound variable"
+    return .ret arg
+  | .unreach .. => return .unreachable
+  | .fun .. => panic! "all local functions should be λ-lifted"
+
+partial def lowerAlt (discr : VarId) (a : LCNF.AltCore LCNF.Code) : M (AltCore FnBody) := do
+  match a with
+  | .alt ctorName params code =>
+    let ⟨ctorInfo, fields⟩ ← getCtorInfo ctorName
+    let rec lowerParams (params : List LCNF.Param) (fields : List CtorFieldInfo) : M FnBody := do
+      match params, fields with
+      | .cons param restParams, .cons field restFields =>
+        match lowerProj discr ctorInfo field with
+        | .expr e =>
+          let loweredType ← match e with
+          | .proj .. => pure .object
+          | _ => lowerType param.type
+          return .vdecl (← bindVar param.fvarId)
+                        loweredType
+                        e
+                        (← lowerParams restParams restFields)
+        | .erased =>
+          bindErased param.fvarId
+          lowerParams restParams restFields
+      | .nil, .nil => lowerCode code
+      | _, _ => panic! "mismatched fieldInfos and fieldTypes"
+    let body ← lowerParams params.toList fields
+    return .ctor ctorInfo body
+  | .default code =>
+    return .default (← lowerCode code)
+end
+
+def lowerResultType (type : Lean.Expr) (arity : Nat) : M IRType :=
+  lowerType (resultTypeForArity type arity)
+where resultTypeForArity (type : Lean.Expr) (arity : Nat) : Lean.Expr :=
+  if arity == 0 then
+    type
+  else
+    match type with
+    | .forallE _ _ b _ => resultTypeForArity b (arity - 1)
+    | .const ``lcErased _ => mkConst ``lcErased
+    | _ => panic! "invalid arity"
+
+def lowerDecl (d : LCNF.Decl) : M (Option Decl) := do
+  let params ← d.params.mapM lowerParam
+  let resultType ← lowerResultType d.type d.params.size
+  match d.value with
+  | .code code =>
+    let body ← lowerCode code
+    pure <| some <| .fdecl d.name params resultType body {}
+  | .extern externAttrData =>
+    if externAttrData.entries.isEmpty then
+      -- This is a complete hack to duplicate the complete hack in the C++ code.
+      addDecl (mkDummyExternDecl d.name params resultType)
+      pure <| none
+    else
+      pure <| some <| .extern d.name params resultType externAttrData
+
+end ToIR
+
+def toIR (decls: Array LCNF.Decl) : CoreM (Array Decl) := do
+  let mut irDecls := #[]
+  for decl in decls do
+    if let some irDecl ← ToIR.lowerDecl decl |>.run then
+      irDecls := irDecls.push irDecl
+  return irDecls
+
+end Lean.IR

src/Lean/Compiler/LCNF/AuxDeclCache.lean

@@ -10,10 +10,7 @@ import Lean.Compiler.LCNF.Internalize
 
 namespace Lean.Compiler.LCNF
 
-abbrev AuxDeclCache := PHashMap Decl Name
-
-builtin_initialize auxDeclCacheExt : EnvExtension AuxDeclCache ←
-  registerEnvExtension (pure {}) (asyncMode := .sync)  -- compilation is non-parallel anyway
+builtin_initialize auxDeclCacheExt : CacheExtension Decl Name ← CacheExtension.register
 
 inductive CacheAuxDeclResult where
   | new
@@ -22,11 +19,11 @@ inductive CacheAuxDeclResult where
 def cacheAuxDecl (decl : Decl) : CompilerM CacheAuxDeclResult := do
   let key := { decl with name := .anonymous }
   let key ← normalizeFVarIds key
-  match auxDeclCacheExt.getState (← getEnv) |>.find? key with
+  match (← auxDeclCacheExt.find? key) with
   | some declName =>
     return .alreadyCached declName
   | none =>
-    modifyEnv fun env => auxDeclCacheExt.modifyState env fun s => s.insert key decl.name
+    auxDeclCacheExt.insert key decl.name
     return .new
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/BaseTypes.lean

@@ -14,21 +14,15 @@ State for the environment extension used to save the LCNF base phase type for de
 that do not have code associated with them.
 Example: constructors, inductive types, foreign functions.
 -/
-structure BaseTypeExtState where
-  /-- The LCNF type for the `base` phase. -/
-  base : PHashMap Name Expr := {}
-  deriving Inhabited
-
-builtin_initialize baseTypeExt : EnvExtension BaseTypeExtState ←
-  registerEnvExtension (pure {}) (asyncMode := .sync)  -- compilation is non-parallel anyway
+builtin_initialize baseTypeExt : CacheExtension Name Expr ← CacheExtension.register
 
 def getOtherDeclBaseType (declName : Name) (us : List Level) : CoreM Expr := do
   let info ← getConstInfo declName
-  let type ← match baseTypeExt.getState (← getEnv) |>.base.find? declName with
+  let type ← match (← baseTypeExt.find? declName) with
     | some type => pure type
     | none =>
       let type ← Meta.MetaM.run' <| toLCNFType info.type
-      modifyEnv fun env => baseTypeExt.modifyState env fun s => { s with base := s.base.insert declName type }
+      baseTypeExt.insert declName type
       pure type
   return type.instantiateLevelParamsNoCache info.levelParams us
 

src/Lean/Compiler/LCNF/Basic.lean

@@ -654,7 +654,8 @@ private partial def collectType (e : Expr) : FVarIdSet → FVarIdSet :=
   | .lam _ d b _     => collectType b ∘ collectType d
   | .app f a         => collectType f ∘ collectType a
   | .fvar fvarId     => fun s => s.insert fvarId
-  | .proj .. | .letE .. | .mdata .. => unreachable!
+  | .mdata _ b       => collectType b
+  | .proj .. | .letE .. => unreachable!
   | _                => id
 
 private def collectArg (arg : Arg) (s : FVarIdSet) : FVarIdSet :=

src/Lean/Compiler/LCNF/CSE.lean

@@ -44,7 +44,7 @@ def replaceFun (decl : FunDecl) (fvarId : FVarId) : M Unit := do
   eraseFunDecl decl
   addFVarSubst decl.fvarId fvarId
 
-partial def _root_.Lean.Compiler.LCNF.Code.cse (code : Code) : CompilerM Code :=
+partial def _root_.Lean.Compiler.LCNF.Code.cse (shouldElimFunDecls : Bool) (code : Code) : CompilerM Code :=
   go code |>.run' {}
 where
   goFunDecl (decl : FunDecl) : M FunDecl := do
@@ -67,14 +67,18 @@ where
         addEntry key decl.fvarId
         return code.updateLet! decl (← go k)
     | .fun decl k =>
-      let decl ← goFunDecl decl
-      let value := decl.toExpr
-      match (← get).map.find? value with
-      | some fvarId' =>
-        replaceFun decl fvarId'
-        go k
-      | none =>
-        addEntry value decl.fvarId
+      if shouldElimFunDecls then
+        let decl ← goFunDecl decl
+        let value := decl.toExpr
+        match (← get).map.find? value with
+        | some fvarId' =>
+          replaceFun decl fvarId'
+          go k
+        | none =>
+          addEntry value decl.fvarId
+          return code.updateFun! decl (← go k)
+      else
+        let decl ← goFunDecl decl
         return code.updateFun! decl (← go k)
     | .jp decl k =>
       let decl ← goFunDecl decl
@@ -101,12 +105,12 @@ end CSE
 /--
 Common sub-expression elimination
 -/
-def Decl.cse (decl : Decl) : CompilerM Decl := do
-  let value ← decl.value.mapCodeM (·.cse)
+def Decl.cse (shouldElimFunDecls : Bool) (decl : Decl) : CompilerM Decl := do
+  let value ← decl.value.mapCodeM (·.cse shouldElimFunDecls)
   return { decl with value }
 
-def cse (phase : Phase := .base) (occurrence := 0) : Pass :=
-  .mkPerDeclaration `cse Decl.cse phase occurrence
+def cse (phase : Phase := .base) (shouldElimFunDecls := false) (occurrence := 0) : Pass :=
+  .mkPerDeclaration `cse (Decl.cse shouldElimFunDecls) phase occurrence
 
 builtin_initialize
   registerTraceClass `Compiler.cse (inherited := true)

src/Lean/Compiler/LCNF/CompatibleTypes.lean

@@ -96,6 +96,8 @@ partial def InferType.compatibleTypesFull (a b : Expr) : InferTypeM Bool := do
           compatibleTypesFull (b₁.instantiate1 x) (b₂.instantiate1 x)
       | .sort u, .sort v => return Level.isEquiv u v
       | .const n us, .const m vs => return n == m && List.isEqv us vs Level.isEquiv
+      | .mdata _ e, _ => compatibleTypesFull e b
+      | _, .mdata _ e => compatibleTypesFull a e
       | _, _ =>
         if a.isLambda then
           let some b ← etaExpand? b | return false

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -483,4 +483,26 @@ def getConfig : CompilerM ConfigOptions :=
 def CompilerM.run (x : CompilerM α) (s : State := {}) (phase : Phase := .base) : CoreM α := do
   x { phase, config := toConfigOptions (← getOptions) } |>.run' s
 
+/-- Environment extension for local caching of key-value pairs, not persisted in .olean files. -/
+structure CacheExtension (α β : Type) [BEq α] [Hashable α] extends EnvExtension (List α × PHashMap α β)
+deriving Inhabited
+
+namespace CacheExtension
+
+def register [BEq α] [Hashable α] [Inhabited β] :
+    IO (CacheExtension α β) :=
+  CacheExtension.mk <$> registerEnvExtension (pure ([], {})) (asyncMode := .sync)  -- compilation is non-parallel anyway
+    (replay? := some fun oldState newState _ s =>
+      let newEntries := newState.1.take (newState.1.length - oldState.1.length)
+      newEntries.foldl (init := s) fun s e =>
+        (e :: s.1, s.2.insert e (newState.2.find! e)))
+
+def insert [BEq α] [Hashable α] [Inhabited β] (ext : CacheExtension α β) (a : α) (b : β) : CoreM Unit := do
+  modifyEnv (ext.modifyState · fun ⟨as, m⟩ => (a :: as, m.insert a b))
+
+def find? [BEq α] [Hashable α] [Inhabited β] (ext : CacheExtension α β) (a : α) : CoreM (Option β) := do
+  return ext.toEnvExtension.getState (← getEnv) |>.2.find? a
+
+end CacheExtension
+
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -249,6 +249,7 @@ builtin_initialize functionSummariesExt : SimplePersistentEnvExtension (Name ×
     addEntryFn := fun s ⟨e, n⟩ => s.insert e n
     toArrayFn := fun s => s.toArray.qsort decLt
     asyncMode := .sync  -- compilation is non-parallel anyway
+    replay? := some <| SimplePersistentEnvExtension.replayOfFilter (!·.contains ·.1) (fun s ⟨e, n⟩ => s.insert e n)
   }
 
 /--
@@ -393,6 +394,16 @@ def updateFunDeclParamsAssignment (params : Array Param) (args : Array Arg) : In
       updateVarAssignment param.fvarId .top
   return ret
 
+def updateFunDeclParamsTop (params : Array Param) : InterpM Bool := do
+  let mut ret := false
+  for param in params do
+    let paramVal ← findVarValue param.fvarId
+    let newVal := .top
+    if newVal != paramVal then
+      modifyAssignment (·.insert param.fvarId newVal)
+      ret := true
+  return ret
+
 private partial def resetNestedFunDeclParams : Code → InterpM Unit
 | .let _ k => resetNestedFunDeclParams k
 | .jp decl k | .fun decl k => do
@@ -488,8 +499,12 @@ where
   -/
   handleFunVar (var : FVarId) : InterpM Unit := do
     if let some funDecl ← findFunDecl? var then
-      funDecl.params.forM (updateVarAssignment ·.fvarId .top)
-      interpFunCall funDecl #[]
+      let updated ← updateFunDeclParamsTop funDecl.params
+      if updated then
+        /- We must reset the value of nested function declaration
+        parameters since they depend on `args` values. -/
+        resetNestedFunDeclParams funDecl.value
+        interpCode funDecl.value
 
   interpFunCall (funDecl : FunDecl) (args : Array Arg) : InterpM Unit := do
     let updated ← updateFunDeclParamsAssignment funDecl.params args

src/Lean/Compiler/LCNF/InferType.lean

@@ -142,7 +142,7 @@ mutual
         fType := instantiateRevRangeArgs fType j i args |>.headBeta
         match fType with
         | .forallE _ _ b _ => j := i; fType := b
-        | _ => return erasedExpr
+        | _ => return anyExpr
     return instantiateRevRangeArgs fType j args.size args |>.headBeta
 
   partial def inferAppType (e : Expr) : InferTypeM Expr := do
@@ -157,7 +157,7 @@ mutual
         fType := fType.instantiateRevRange j i args |>.headBeta
         match fType with
         | .forallE _ _ b _ => j := i; fType := b
-        | _ => return erasedExpr
+        | _ => return anyExpr
     return fType.instantiateRevRange j args.size args |>.headBeta
 
   partial def inferProjType (structName : Name) (idx : Nat) (s : FVarId) : InferTypeM Expr := do
@@ -167,6 +167,8 @@ mutual
     if structType.isErased then
       /- TODO: after we erase universe variables, we can just extract a better type using just `structName` and `idx`. -/
       return erasedExpr
+    else if structType.isAny then
+      return anyExpr
     else
       matchConstStructure structType.getAppFn failed fun structVal structLvls ctorVal =>
         let structTypeArgs := structType.getAppArgs
@@ -179,7 +181,7 @@ mutual
             | .forallE _ _ body _ =>
               if body.hasLooseBVars then
                 -- This can happen when one of the fields is a type or type former.
-                ctorType := body.instantiate1 erasedExpr
+                ctorType := body.instantiate1 anyExpr
               else
                 ctorType := body
             | _ =>

src/Lean/Compiler/LCNF/LambdaLifting.lean

@@ -178,16 +178,8 @@ def eagerLambdaLifting : Pass where
   name       := `eagerLambdaLifting
   run        := fun decls => do
     decls.foldlM (init := #[]) fun decls decl => do
-      if (← Meta.isInstance decl.name) then
-        /-
-        Recall that we lambda lift local functions in instances to control code blowup, and make sure they are cheap to inline.
-        It is not worth to lift tiny ones. TODO: evaluate whether we should add a compiler option to control the min size.
-
-        Recall that when performing eager lambda lifting in instances, we progatate the `[inline]` annotations to the new auxiliary functions.
-
-        Note: we have tried `if decl.inlineable then return decls.push decl`, but it didn't help in our preliminary experiments.
-        -/
-        return decls ++ (← decl.lambdaLifting (liftInstParamOnly := false) (suffix := `_elam) (inheritInlineAttrs := true) (minSize := 3))
+      if decl.inlineAttr || (← Meta.isInstance decl.name) then
+        return decls.push decl
       else
         return decls ++ (← decl.lambdaLifting (liftInstParamOnly := true) (suffix := `_elam))
 

src/Lean/Compiler/LCNF/Main.lean

@@ -6,6 +6,10 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Compiler.Options
 import Lean.Compiler.ExternAttr
+import Lean.Compiler.IR
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.Checker
+import Lean.Compiler.IR.ToIR
 import Lean.Compiler.LCNF.PassManager
 import Lean.Compiler.LCNF.Passes
 import Lean.Compiler.LCNF.PrettyPrinter
@@ -62,7 +66,7 @@ def checkpoint (stepName : Name) (decls : Array Decl) : CompilerM Unit := do
 
 namespace PassManager
 
-def run (declNames : Array Name) : CompilerM (Array Decl) := withAtLeastMaxRecDepth 8192 do
+def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRecDepth 8192 do
   /-
   Note: we need to increase the recursion depth because we currently do to save phase1
   declarations in .olean files. Then, we have to recursively compile all dependencies,
@@ -83,11 +87,21 @@ def run (declNames : Array Name) : CompilerM (Array Decl) := withAtLeastMaxRecDe
       -- We display the declaration saved in the environment because the names have been normalized
       let some decl' ← getDeclAt? decl.name .mono | unreachable!
       Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl'}"
-  return decls
+  let irDecls ← IR.toIR decls
+  let env ← getEnv
+  let opts ← getOptions
+  let ⟨log, res⟩ := IR.compile env opts irDecls
+  for msg in log do
+    addTrace `Compiler.IR m!"{msg}"
+  match res with
+  | .ok env =>
+    setEnv env
+    return irDecls
+  | .error s => throwError s
 
 end PassManager
 
-def compile (declNames : Array Name) : CoreM (Array Decl) :=
+def compile (declNames : Array Name) : CoreM (Array IR.Decl) :=
   CompilerM.run <| PassManager.run declNames
 
 def showDecl (phase : Phase) (declName : Name) : CoreM Format := do

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -81,11 +81,16 @@ partial def toMonoType (type : Expr) : CoreM Expr := do
     | .const ``lcErased _ => return erasedExpr
     | _ => mkArrow (← toMonoType d) monoB
   | .sort _ => return erasedExpr
+  | .mdata _ b => toMonoType b
   | _ => return anyExpr
 where
   visitApp (f : Expr) (args : Array Expr) : CoreM Expr := do
     match f with
-    | .const ``lcErased _ => return erasedExpr
+    | .const ``lcErased _ =>
+      if args.all (·.isErased) then
+        return erasedExpr
+      else
+        return anyExpr
     | .const ``lcAny _ => return anyExpr
     | .const ``Decidable _ => return mkConst ``Bool
     | .const declName us =>
@@ -101,7 +106,7 @@ where
           if d matches .const ``lcErased _ | .sort _ then
             result := mkApp result (← toMonoType arg)
           else
-            result := mkApp result erasedExpr
+            result := mkApp result anyExpr
           type := b.instantiate1 arg
         return result
     | _ => return anyExpr
@@ -111,20 +116,14 @@ State for the environment extension used to save the LCNF mono phase type for de
 that do not have code associated with them.
 Example: constructors, inductive types, foreign functions.
 -/
-structure MonoTypeExtState where
-  /-- The LCNF type for the `mono` phase. -/
-  mono : PHashMap Name Expr := {}
-  deriving Inhabited
-
-builtin_initialize monoTypeExt : EnvExtension MonoTypeExtState ←
-  registerEnvExtension (pure {}) (asyncMode := .sync)  -- compilation is non-parallel anyway
+builtin_initialize monoTypeExt : CacheExtension Name Expr ← CacheExtension.register
 
 def getOtherDeclMonoType (declName : Name) : CoreM Expr := do
-  match monoTypeExt.getState (← getEnv) |>.mono.find? declName with
+  match (← monoTypeExt.find? declName) with
   | some type => return type
   | none =>
     let type ← toMonoType (← getOtherDeclBaseType declName [])
-    modifyEnv fun env => monoTypeExt.modifyState env fun s => { s with mono := s.mono.insert declName type }
+    monoTypeExt.insert declName type
     return type
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/Passes.lean

@@ -61,7 +61,7 @@ def builtinPassManager : PassManager := {
     eagerLambdaLifting,
     specialize,
     simp (occurrence := 2),
-    cse (occurrence := 1),
+    cse (shouldElimFunDecls := false) (occurrence := 1),
     saveBase, -- End of base phase
     toMono,
     simp (occurrence := 3) (phase := .mono),
@@ -94,7 +94,6 @@ builtin_initialize passManagerExt : PersistentEnvExtension Name (Name × PassMan
     addImportedFn := fun ns => return ([], ← ImportM.runCoreM <| runImportedDecls ns)
     addEntryFn := fun (installerDeclNames, _) (installerDeclName, managerNew) => (installerDeclName :: installerDeclNames, managerNew)
     exportEntriesFn := fun s => s.1.reverse.toArray
-    asyncMode := .sync
   }
 
 def getPassManager : CoreM PassManager :=

src/Lean/Compiler/LCNF/PhaseExt.lean

@@ -21,22 +21,21 @@ private abbrev findAtSorted? (decls : Array Decl) (declName : Name) : Option Dec
   let tmpDecl := { tmpDecl with name := declName }
   decls.binSearch tmpDecl declLt
 
-abbrev DeclExt := PersistentEnvExtension Decl Decl DeclExtState
+abbrev DeclExt := SimplePersistentEnvExtension Decl DeclExtState
 
 def mkDeclExt (name : Name := by exact decl_name%) : IO DeclExt := do
-  registerPersistentEnvExtension {
+  registerSimplePersistentEnvExtension {
     name            := name
-    mkInitial       := return {}
-    addImportedFn   := fun _ => return {}
+    addImportedFn   := fun _ => {}
     addEntryFn      := fun decls decl => decls.insert decl.name decl
-    exportEntriesFn := fun s =>
-      let decls := s.foldl (init := #[]) fun decls _ decl => decls.push decl
-      sortDecls decls
+    toArrayFn       := (sortDecls ·.toArray)
     asyncMode       := .sync  -- compilation is non-parallel anyway
+    replay?         := some <| SimplePersistentEnvExtension.replayOfFilter
+      (fun s d => !s.contains d.name) (fun decls decl => decls.insert decl.name decl)
   }
 
-builtin_initialize baseExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt
-builtin_initialize monoExt : PersistentEnvExtension Decl Decl DeclExtState ← mkDeclExt
+builtin_initialize baseExt : DeclExt ← mkDeclExt
+builtin_initialize monoExt : DeclExt ← mkDeclExt
 
 def getDeclCore? (env : Environment) (ext : DeclExt) (declName : Name) : Option Decl :=
   match env.getModuleIdxFor? declName with

src/Lean/Compiler/LCNF/PullLetDecls.lean

@@ -69,9 +69,12 @@ mutual
   partial def pullDecls (code : Code) : PullM Code := do
     match code with
     | .cases c =>
-      withCheckpoint do
-        let alts ← c.alts.mapMonoM pullAlt
-        return code.updateAlts! alts
+      if c.typeName == ``Decidable then
+        return code
+      else
+        withCheckpoint do
+          let alts ← c.alts.mapMonoM pullAlt
+          return code.updateAlts! alts
     | .let decl k =>
       if (← shouldPull decl) then
         pullDecls k

src/Lean/Compiler/LCNF/Simp.lean

@@ -42,30 +42,13 @@ def Decl.simp? (decl : Decl) : SimpM (Option Decl) := do
 partial def Decl.simp (decl : Decl) (config : Config) : CompilerM Decl := do
   let mut config := config
   if (← isTemplateLike decl) then
-    let mut inlineDefs := config.inlineDefs
-    /-
-    At the base phase, we don't inline definitions occurring in instances.
-    Reason: we eagerly lambda lift local functions occurring at instances before saving their code at the end of the base
-    phase. The goal is to make them cheap to inline in actual code. By inlining definitions we would be just generating extra
-    work for the lambda lifter.
-
-    There is an exception: inlineable instances. This is important for auxiliary instances such as
-    ```
-    @[always_inline]
-    instance : Monad TermElabM := let i := inferInstanceAs (Monad TermElabM); { pure := i.pure, bind := i.bind }
-    ```
-    by keeping `inlineDefs := true`, we can pre-compute the `pure` and `bind` methods for `TermElabM`.
-    -/
-    if (← inBasePhase <&&> Meta.isInstance decl.name) then
-      unless decl.inlineable do
-        inlineDefs := false
     /-
     We do not eta-expand or inline partial applications in template like code.
     Recall we don't want to generate code for them.
     Remark: by eta-expanding partial applications in instances, we also make the simplifier
     work harder when inlining instance projections.
     -/
-    config := { config with etaPoly := false, inlinePartial := false, inlineDefs }
+    config := { config with etaPoly := false, inlinePartial := false }
   go decl config
 where
   go (decl : Decl) (config : Config) : CompilerM Decl := do

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -397,7 +397,7 @@ structure FolderOleanEntry where
 structure FolderEntry extends FolderOleanEntry where
   folder : Folder
 
-builtin_initialize folderExt : PersistentEnvExtension FolderOleanEntry FolderEntry (List FolderOleanEntry × SMap Name Folder) ←
+builtin_initialize folderExt : PersistentEnvExtension FolderOleanEntry FolderEntry (List FolderEntry × SMap Name Folder) ←
   registerPersistentEnvExtension {
     mkInitial := return ([], builtinFolders)
     addImportedFn := fun entriesArray => do
@@ -408,9 +408,12 @@ builtin_initialize folderExt : PersistentEnvExtension FolderOleanEntry FolderEnt
           let folder ← IO.ofExcept <| getFolderCore ctx.env ctx.opts folderDeclName
           folders := folders.insert declName folder
       return ([], folders.switch)
-    addEntryFn := fun (entries, map) entry => (entry.toFolderOleanEntry :: entries, map.insert entry.declName entry.folder)
-    exportEntriesFn := fun (entries, _) => entries.reverse.toArray
+    addEntryFn := fun (entries, map) entry => (entry :: entries, map.insert entry.declName entry.folder)
+    exportEntriesFn := fun (entries, _) => entries.reverse.toArray.map (·.toFolderOleanEntry)
     asyncMode := .sync
+    replay? := some fun oldState newState _ s =>
+      let newEntries := newState.1.take (newState.1.length - oldState.1.length)
+      (newEntries ++ s.1, newEntries.foldl (init := s.2) fun s e => s.insert e.declName (newState.2.find! e.declName))
   }
 
 def registerFolder (declName : Name) (folderDeclName : Name) : CoreM Unit := do

src/Lean/Compiler/LCNF/SpecInfo.lean

@@ -86,6 +86,8 @@ builtin_initialize specExtension : SimplePersistentEnvExtension SpecEntry SpecSt
     addImportedFn := fun _ => {}
     toArrayFn     := fun s => sortEntries s.toArray
     asyncMode     := .sync
+    replay?       := some <| SimplePersistentEnvExtension.replayOfFilter
+      (!·.specInfo.contains ·.declName) SpecState.addEntry
   }
 
 /--

src/Lean/Compiler/LCNF/Specialize.lean

@@ -33,6 +33,8 @@ builtin_initialize specCacheExt : SimplePersistentEnvExtension CacheEntry Cache
     addEntryFn    := addEntry
     addImportedFn := fun es => (mkStateFromImportedEntries addEntry {} es).switch
     asyncMode     := .sync
+    replay?       := some <| SimplePersistentEnvExtension.replayOfFilter
+      (!·.contains ·.key) addEntry
   }
 
 def cacheSpec (key : Expr) (declName : Name) : CoreM Unit :=

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Meta.Transform
 import Lean.Meta.Match.MatcherInfo
 import Lean.Compiler.ExternAttr
+import Lean.Compiler.InitAttr
 import Lean.Compiler.ImplementedByAttr
 import Lean.Compiler.LCNF.ToLCNF
 
@@ -99,7 +100,8 @@ def toDecl (declName : Name) : CompilerM Decl := do
   let some info ← getDeclInfo? declName | throwError "declaration `{declName}` not found"
   let safe := !info.isPartial && !info.isUnsafe
   let inlineAttr? := getInlineAttribute? (← getEnv) declName
-  if let some externAttrData := getExternAttrData? (← getEnv) declName then
+  let env ← getEnv
+  if let some externAttrData := getExternAttrData? env declName then
     let paramsFromTypeBinders (expr : Expr) : CompilerM (Array Param) := do
       let mut params := #[]
       let mut currentExpr := expr
@@ -115,6 +117,22 @@ def toDecl (declName : Name) : CompilerM Decl := do
     let type ← Meta.MetaM.run' (toLCNFType info.type)
     let params ← paramsFromTypeBinders type
     return { name := declName, params, type, value := .extern externAttrData, levelParams := info.levelParams, safe, inlineAttr? }
+  else if hasInitAttr env declName then
+    let paramsFromTypeBinders (expr : Expr) : CompilerM (Array Param) := do
+      let mut params := #[]
+      let mut currentExpr := expr
+      repeat
+        match currentExpr with
+        | .forallE binderName type body _ =>
+          let borrow := isMarkedBorrowed type
+          params := params.push (← mkParam binderName type borrow)
+          currentExpr := body
+        | _ => break
+      return params
+
+    let type ← Meta.MetaM.run' (toLCNFType info.type)
+    let params ← paramsFromTypeBinders type
+    return { name := declName, params, type, value := .extern { entries := [] }, levelParams := info.levelParams, safe, inlineAttr? }
   else
     let some value := info.value? (allowOpaque := true) | throwError "declaration `{declName}` does not have a value"
     let (type, value) ← Meta.MetaM.run' do

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -8,6 +8,7 @@ import Lean.ProjFns
 import Lean.Meta.CtorRecognizer
 import Lean.Compiler.BorrowedAnnotation
 import Lean.Compiler.CSimpAttr
+import Lean.Compiler.ImplementedByAttr
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.Bind
 import Lean.Compiler.LCNF.InferType
@@ -302,7 +303,7 @@ are type formers. This can happen when we have a field whose type is, for exampl
 def applyToAny (type : Expr) : M Expr := do
   let toAny := (← get).toAny
   return type.replace fun
-    | .fvar fvarId => if toAny.contains fvarId then some erasedExpr else none
+    | .fvar fvarId => if toAny.contains fvarId then some anyExpr else none
     | _ => none
 
 def toLCNFType (type : Expr) : M Expr := do
@@ -567,6 +568,29 @@ where
           let result := .fvar auxDecl.fvarId
           mkOverApplication result args casesInfo.arity
 
+  visitCasesImplementedBy (casesInfo : CasesInfo) (f : Expr) (args : Array Expr) : M Arg := do
+    let mut args := args
+    let discr := args[casesInfo.discrPos]!
+    if discr matches .fvar _ then
+      let typeName := casesInfo.declName.getPrefix
+      let .inductInfo indVal ← getConstInfo typeName | unreachable!
+      args ← args.mapIdxM fun i arg => do
+        unless casesInfo.altsRange.start <= i && i < casesInfo.altsRange.stop do return arg
+        let altIdx := i - casesInfo.altsRange.start
+        let numParams := casesInfo.altNumParams[altIdx]!
+        let ctorName := indVal.ctors[altIdx]!
+
+        Meta.MetaM.run' <| Meta.lambdaBoundedTelescope arg numParams fun paramExprs body => do
+          let fn := body.getAppFn
+          let args := body.getAppArgs
+          let args := args.map fun arg =>
+            if arg.getAppFn.constName? == some ctorName && arg.getAppArgs == paramExprs then
+              discr
+            else
+              arg
+          Meta.mkLambdaFVars paramExprs (mkAppN fn args)
+    visitAppDefaultConst f args
+
   visitCtor (arity : Nat) (e : Expr) : M Arg :=
     etaIfUnderApplied e arity do
       visitAppDefaultConst e.getAppFn e.getAppArgs
@@ -671,7 +695,7 @@ where
   visitApp (e : Expr) : M Arg := do
     if let some (args, n, t, v, b) := e.letFunAppArgs? then
       visitCore <| mkAppN (.letE n t v b (nonDep := true)) args
-    else if let .const declName _ := CSimp.replaceConstants (← getEnv) e.getAppFn then
+    else if let .const declName us := CSimp.replaceConstants (← getEnv) e.getAppFn then
       if declName == ``Quot.lift then
         visitQuotLift e
       else if declName == ``Quot.mk then
@@ -687,7 +711,10 @@ where
       else if declName == ``False.rec || declName == ``Empty.rec || declName == ``False.casesOn || declName == ``Empty.casesOn then
         visitFalseRec e
       else if let some casesInfo ← getCasesInfo? declName then
-        visitCases casesInfo e
+        if (getImplementedBy? (← getEnv) declName).isSome then
+          e.withApp (visitCasesImplementedBy casesInfo)
+        else
+          visitCases casesInfo e
       else if let some arity ← getCtorArity? declName then
         visitCtor arity e
       else if isNoConfusion (← getEnv) declName then

src/Lean/Compiler/LCNF/ToMono.lean

@@ -101,6 +101,96 @@ partial def decToMono (c : Cases) (_ : c.typeName == ``Decidable) : ToMonoM Code
       return .alt ctorName #[] (← k.toMono)
   return .cases { c with resultType, alts, typeName := ``Bool }
 
+/-- Eliminate `cases` for `Nat`. -/
+partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code := do
+  let resultType ← toMonoType c.resultType
+  let natType := mkConst ``Nat
+  let zeroDecl ← mkLetDecl `zero natType (.value (.natVal 0))
+  let isZeroDecl ← mkLetDecl `isZero (mkConst ``Bool) (.const ``Nat.decEq [] #[.fvar c.discr, .fvar zeroDecl.fvarId])
+  let alts ← c.alts.mapM fun alt => do
+    match alt with
+    | .default k => return alt.updateCode (← k.toMono)
+    | .alt ctorName ps k =>
+      eraseParams ps
+      if ctorName == ``Nat.succ then
+        let p := ps[0]!
+        let oneDecl ← mkLetDecl `one natType (.value (.natVal 1))
+        let subOneDecl := { fvarId := p.fvarId, binderName := p.binderName, type := natType, value := .const ``Nat.sub [] #[.fvar c.discr, .fvar oneDecl.fvarId] }
+        modifyLCtx fun lctx => lctx.addLetDecl subOneDecl
+        return .alt ``Bool.false #[] (.let oneDecl (.let subOneDecl (← k.toMono)))
+      else
+        return .alt ``Bool.true #[] (← k.toMono)
+  return .let zeroDecl (.let isZeroDecl (.cases { discr := isZeroDecl.fvarId, resultType, alts, typeName := ``Bool }))
+
+/-- Eliminate `cases` for `Int`. -/
+partial def casesIntToMono (c: Cases) (_ : c.typeName == ``Int) : ToMonoM Code := do
+  let resultType ← toMonoType c.resultType
+  let natType := mkConst ``Nat
+  let zeroNatDecl ← mkLetDecl `natZero natType (.value (.natVal 0))
+  let zeroIntDecl ← mkLetDecl `intZero (mkConst ``Int) (.const ``Int.ofNat [] #[.fvar zeroNatDecl.fvarId])
+  let isNegDecl ← mkLetDecl `isNeg (mkConst ``Bool) (.const ``Int.decLt [] #[.fvar c.discr, .fvar zeroIntDecl.fvarId])
+  let alts ← c.alts.mapM fun alt => do
+    match alt with
+    | .default k => return alt.updateCode (← k.toMono)
+    | .alt ctorName ps k =>
+      eraseParams ps
+      let p := ps[0]!
+      if ctorName == ``Int.negSucc then
+        let absDecl ← mkLetDecl `abs natType (.const ``Int.natAbs [] #[.fvar c.discr])
+        let oneDecl ← mkLetDecl `one natType (.value (.natVal 1))
+        let subOneDecl := { fvarId := p.fvarId, binderName := p.binderName, type := natType, value := .const ``Nat.sub [] #[.fvar absDecl.fvarId, .fvar oneDecl.fvarId] }
+        modifyLCtx fun lctx => lctx.addLetDecl subOneDecl
+        return .alt ``Bool.true #[] (.let absDecl (.let oneDecl (.let subOneDecl (← k.toMono))))
+      else
+        let absDecl := { fvarId := p.fvarId, binderName := p.binderName, type := natType, value := .const ``Int.natAbs [] #[.fvar c.discr] }
+        modifyLCtx fun lctx => lctx.addLetDecl absDecl
+        return .alt ``Bool.false #[] (.let absDecl (← k.toMono))
+  return .let zeroNatDecl (.let zeroIntDecl (.let isNegDecl (.cases { discr := isNegDecl.fvarId, resultType, alts, typeName := ``Bool })))
+
+/-- Eliminate `cases` for `UInt` types. -/
+partial def casesUIntToMono (c : Cases) (uintName : Name) (_ : c.typeName == uintName) : ToMonoM Code := do
+  assert! c.alts.size == 1
+  let .alt _ ps k := c.alts[0]! | unreachable!
+  eraseParams ps
+  let p := ps[0]!
+  let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const (.str uintName "toBitVec") [] #[.fvar c.discr] }
+  modifyLCtx fun lctx => lctx.addLetDecl decl
+  let k ← k.toMono
+  return .let decl k
+
+/-- Eliminate `cases` for `Array. -/
+partial def casesArrayToMono (c : Cases) (_ : c.typeName == ``Array) : ToMonoM Code := do
+  assert! c.alts.size == 1
+  let .alt _ ps k := c.alts[0]! | unreachable!
+  eraseParams ps
+  let p := ps[0]!
+  let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const ``Array.toList [] #[.erased, .fvar c.discr] }
+  modifyLCtx fun lctx => lctx.addLetDecl decl
+  let k ← k.toMono
+  return .let decl k
+
+/-- Eliminate `cases` for `ByteArray. -/
+partial def casesByteArrayToMono (c : Cases) (_ : c.typeName == ``ByteArray) : ToMonoM Code := do
+  assert! c.alts.size == 1
+  let .alt _ ps k := c.alts[0]! | unreachable!
+  eraseParams ps
+  let p := ps[0]!
+  let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const ``ByteArray.data [] #[.fvar c.discr] }
+  modifyLCtx fun lctx => lctx.addLetDecl decl
+  let k ← k.toMono
+  return .let decl k
+
+/-- Eliminate `cases` for `FloatArray. -/
+partial def casesFloatArrayToMono (c : Cases) (_ : c.typeName == ``FloatArray) : ToMonoM Code := do
+  assert! c.alts.size == 1
+  let .alt _ ps k := c.alts[0]! | unreachable!
+  eraseParams ps
+  let p := ps[0]!
+  let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const ``ByteArray.data [] #[.fvar c.discr] }
+  modifyLCtx fun lctx => lctx.addLetDecl decl
+  let k ← k.toMono
+  return .let decl k
+
 /-- Eliminate `cases` for trivial structure. See `hasTrivialStructure?` -/
 partial def trivialStructToMono (info : TrivialStructureInfo) (c : Cases) : ToMonoM Code := do
   assert! c.alts.size == 1
@@ -124,6 +214,24 @@ partial def Code.toMono (code : Code) : ToMonoM Code := do
   | .cases c =>
     if h : c.typeName == ``Decidable then
       decToMono c h
+    else if h : c.typeName == ``Nat then
+      casesNatToMono c h
+    else if h : c.typeName == ``Int then
+      casesIntToMono c h
+    else if h : c.typeName == ``UInt8 then
+      casesUIntToMono c ``UInt8 h
+    else if h : c.typeName == ``UInt16 then
+      casesUIntToMono c ``UInt16 h
+    else if h : c.typeName == ``UInt32 then
+      casesUIntToMono c ``UInt32 h
+    else if h : c.typeName == ``UInt64 then
+      casesUIntToMono c ``UInt64 h
+    else if h : c.typeName == ``Array then
+      casesArrayToMono c h
+    else if h : c.typeName == ``ByteArray then
+      casesByteArrayToMono c h
+    else if h : c.typeName == ``FloatArray then
+      casesFloatArrayToMono c h
     else if let some info ← hasTrivialStructure? c.typeName then
       trivialStructToMono info c
     else

src/Lean/Compiler/LCNF/Types.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Compiler.BorrowedAnnotation
 import Lean.Meta.InferType
 
 namespace Lean.Compiler
@@ -18,6 +19,9 @@ def anyExpr := mkConst ``lcAny
 def _root_.Lean.Expr.isErased (e : Expr) :=
   e.isAppOf ``lcErased
 
+def _root_.Lean.Expr.isAny (e : Expr) :=
+  e.isAppOf ``lcAny
+
 def isPropFormerTypeQuick : Expr → Bool
   | .forallE _ _ b _ => isPropFormerTypeQuick b
   | .sort .zero => true
@@ -132,7 +136,7 @@ partial def toLCNFType (type : Expr) : MetaM Expr := do
   | .forallE .. => visitForall type #[]
   | .app ..  => type.withApp visitApp
   | .fvar .. => visitApp type #[]
-  | _        => return erasedExpr
+  | _        => return mkConst ``lcAny
 where
   whnfEta (type : Expr) : MetaM Expr := do
     let type ← whnf type
@@ -147,7 +151,10 @@ where
     | .forallE n d b bi =>
       let d := d.instantiateRev xs
       withLocalDecl n bi d fun x => do
-        let d := (← toLCNFType d).abstract xs
+        let isBorrowed := isMarkedBorrowed d
+        let mut d := (← toLCNFType d).abstract xs
+        if isBorrowed then
+          d := markBorrowed d
         return .forallE n d (← visitForall b (xs.push x)) bi
     | _ =>
       let e ← toLCNFType (e.instantiateRev xs)
@@ -156,10 +163,10 @@ where
   visitApp (f : Expr) (args : Array Expr) := do
     let fNew ← match f with
       | .const declName us =>
-        let .inductInfo _ ← getConstInfo declName | return erasedExpr
+        let .inductInfo _ ← getConstInfo declName | return anyExpr
         pure <| .const declName us
       | .fvar .. => pure f
-      | _ => return erasedExpr
+      | _ => return anyExpr
     let mut result := fNew
     for arg in args do
       if (← isProp arg) then
@@ -169,13 +176,13 @@ where
       else if (← isTypeFormer arg) then
         result := mkApp result (← toLCNFType arg)
       else
-        result := mkApp result erasedExpr
+        result := mkApp result (mkConst ``lcAny)
     return result
 
 mutual
 
 partial def joinTypes (a b : Expr) : Expr :=
-  joinTypes? a b |>.getD erasedExpr
+  joinTypes? a b |>.getD (mkConst ``lcAny)
 
 partial def joinTypes? (a b : Expr) : Option Expr := do
   if a.isErased || b.isErased then
@@ -194,16 +201,16 @@ partial def joinTypes? (a b : Expr) : Option Expr := do
       | .app f a, .app g b =>
         (do return .app (← joinTypes? f g) (← joinTypes? a b))
          <|>
-        return erasedExpr
+        return (mkConst ``lcAny)
       | .forallE n d₁ b₁ _, .forallE _ d₂ b₂ _ =>
         (do return .forallE n (← joinTypes? d₁ d₂) (joinTypes b₁ b₂) .default)
         <|>
-        return erasedExpr
+        return (mkConst ``lcAny)
       | .lam n d₁ b₁ _, .lam _ d₂ b₂ _ =>
         (do return .lam n (← joinTypes? d₁ d₂) (joinTypes b₁ b₂) .default)
         <|>
-        return erasedExpr
-      | _, _ => return erasedExpr
+        return (mkConst ``lcAny)
+      | _, _ => return (mkConst ``lcAny)
 
 end
 

src/Lean/CoreM.lean

@@ -543,7 +543,7 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla
     | _ => pure ()
 
 register_builtin_option compiler.enableNew : Bool := {
-  defValue := false
+  defValue := true -- false
   group    := "compiler"
   descr    := "(compiler) enable the new code generator, this should have no significant effect on your code but it does help to test the new code generator; unset to only use the old code generator instead"
 }
@@ -594,20 +594,21 @@ where doCompile := do
     return
   let opts ← getOptions
   if compiler.enableNew.get opts then
-    compileDeclsNew decls
-
-  let res ← withTraceNode `compiler (fun _ => return m!"compiling old: {decls}") do
-    return compileDeclsOld (← getEnv) opts decls
-  match res with
-  | Except.ok env   => setEnv env
-  | Except.error (.other msg) =>
-    if logErrors then
-      if let some decl := ref? then
-        checkUnsupported decl -- Generate nicer error message for unsupported recursors and axioms
-      throwError msg
-  | Except.error ex =>
-    if logErrors then
-      throwKernelException ex
+    try compileDeclsNew decls catch e =>
+      if logErrors then throw e else return ()
+  else
+    let res ← withTraceNode `compiler (fun _ => return m!"compiling old: {decls}") do
+      return compileDeclsOld (← getEnv) opts decls
+    match res with
+    | Except.ok env   => setEnv env
+    | Except.error (.other msg) =>
+      if logErrors then
+        if let some decl := ref? then
+          checkUnsupported decl -- Generate nicer error message for unsupported recursors and axioms
+        throwError msg
+    | Except.error ex =>
+      if logErrors then
+        throwKernelException ex
 
 def compileDecl (decl : Declaration) (logErrors := true) : CoreM Unit := do
   compileDecls (Compiler.getDeclNamesForCodeGen decl) decl logErrors

tests/lean/4089.lean.expected.out

@@ -1,40 +1,38 @@
-
-[reset_reuse]
-def f (x_1 : obj) : obj :=
-  case x_1 : obj of
-  Prod.mk →
-    let x_2 : obj := proj[0] x_1;
-    let x_3 : obj := proj[1] x_1;
-    let x_5 : obj := reset[2] x_1;
-    let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_3 x_2;
-    ret x_4
-
-[reset_reuse]
-def Sigma.toProd._rarg (x_1 : obj) : obj :=
-  case x_1 : obj of
-  Sigma.mk →
-    let x_2 : obj := proj[0] x_1;
-    let x_3 : obj := proj[1] x_1;
-    let x_5 : obj := reset[2] x_1;
-    let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_2 x_3;
-    ret x_4
-def Sigma.toProd (x_1 : ◾) (x_2 : ◾) : obj :=
-  let x_3 : obj := pap Sigma.toProd._rarg;
-  ret x_3
-
-[reset_reuse]
-def foo (x_1 : obj) : obj :=
-  case x_1 : obj of
-  List.nil →
-    let x_2 : obj := ctor_0[List.nil];
-    ret x_2
-  List.cons →
-    let x_3 : obj := proj[0] x_1;
-    case x_3 : obj of
-    Prod.mk →
-      let x_4 : obj := proj[1] x_1;
-      let x_9 : obj := reset[2] x_1;
-      let x_5 : obj := proj[0] x_3;
-      let x_6 : obj := foo x_4;
-      let x_7 : obj := reuse x_9 in ctor_1[List.cons] x_5 x_6;
-      ret x_7
+[Compiler.IR] [reset_reuse]
+    def f (x_1 : obj) : obj :=
+      case x_1 : obj of
+      Prod.mk →
+        let x_2 : obj := proj[0] x_1;
+        let x_3 : obj := proj[1] x_1;
+        let x_5 : obj := reset[2] x_1;
+        let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_3 x_2;
+        ret x_4
+[Compiler.IR] [reset_reuse]
+    def Sigma.toProd._redArg (x_1 : obj) : obj :=
+      case x_1 : obj of
+      Sigma.mk →
+        let x_2 : obj := proj[0] x_1;
+        let x_3 : obj := proj[1] x_1;
+        let x_5 : obj := reset[2] x_1;
+        let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_2 x_3;
+        ret x_4
+    def Sigma.toProd (x_1 : ◾) (x_2 : ◾) (x_3 : obj) : obj :=
+      let x_4 : obj := Sigma.toProd._redArg x_3;
+      ret x_4
+[Compiler.IR] [reset_reuse]
+    def foo (x_1 : obj) : obj :=
+      case x_1 : obj of
+      List.nil →
+        let x_2 : obj := ctor_0[List.nil];
+        ret x_2
+      List.cons →
+        let x_3 : obj := proj[0] x_1;
+        case x_3 : obj of
+        Prod.mk →
+          let x_4 : obj := proj[1] x_1;
+          let x_10 : obj := reset[2] x_1;
+          let x_5 : obj := proj[0] x_3;
+          let x_6 : obj := proj[1] x_3;
+          let x_7 : obj := foo x_4;
+          let x_8 : obj := reuse x_10 in ctor_1[List.cons] x_5 x_7;
+          ret x_8

tests/lean/4240.lean.expected.out

@@ -1,26 +1,28 @@
-
-[result]
-def MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1 (x_1 : @& obj) : u8 :=
-  case x_1 : obj of
-  MyOption.none →
-    let x_2 : u8 := 0;
-    ret x_2
-  MyOption.some →
-    let x_3 : u8 := 1;
-    ret x_3
-def isSomeWithInstanceNat (x_1 : @& obj) : u8 :=
-  let x_2 : usize := 0;
-  let x_3 : obj := Array.uget ◾ x_1 x_2 ◾;
-  let x_4 : u8 := MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1 x_3;
-  dec x_3;
-  ret x_4
-def MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1._boxed (x_1 : obj) : obj :=
-  let x_2 : u8 := MyOption.isSomeWithInstance._at.isSomeWithInstanceNat._spec_1 x_1;
-  dec x_1;
-  let x_3 : obj := box x_2;
-  ret x_3
-def isSomeWithInstanceNat._boxed (x_1 : obj) : obj :=
-  let x_2 : u8 := isSomeWithInstanceNat x_1;
-  dec x_1;
-  let x_3 : obj := box x_2;
-  ret x_3
+[Compiler.IR] [result]
+    def MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 (x_1 : @& obj) : u8 :=
+      case x_1 : obj of
+      MyOption.none →
+        let x_2 : obj := ctor_0[Bool.false];
+        let x_3 : u8 := unbox x_2;
+        ret x_3
+      MyOption.some →
+        let x_4 : obj := ctor_1[Bool.true];
+        let x_5 : u8 := unbox x_4;
+        ret x_5
+    def isSomeWithInstanceNat (x_1 : @& obj) : u8 :=
+      let x_2 : obj := 0;
+      let x_3 : usize := USize.ofNat x_2;
+      let x_4 : obj := Array.uget ◾ x_1 x_3 ◾;
+      let x_5 : u8 := MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 x_4;
+      dec x_4;
+      ret x_5
+    def MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0._boxed (x_1 : obj) : obj :=
+      let x_2 : u8 := MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 x_1;
+      dec x_1;
+      let x_3 : obj := box x_2;
+      ret x_3
+    def isSomeWithInstanceNat._boxed (x_1 : obj) : obj :=
+      let x_2 : u8 := isSomeWithInstanceNat x_1;
+      dec x_1;
+      let x_3 : obj := box x_2;
+      ret x_3

tests/lean/496.lean.expected.out

@@ -1,2 +1,2 @@
-496.lean:3:4-3:8: error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'foo', and it does not have executable code
-496.lean:9:4-9:8: error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'bla1', and it does not have executable code
+496.lean:3:4-3:8: error: axiom 'foo' not supported by code generator; consider marking definition as 'noncomputable'
+496.lean:9:4-9:8: error: failed to compile definition, compiler IR check failed at 'bla2'. Error: depends on declaration 'bla1', which has no executable code; consider marking definition as 'noncomputable'

tests/lean/CompilerConstantFold.lean.expected.out

@@ -16,20 +16,20 @@
       let e1 := UInt64.shiftRight e _x.5;
       let e2 := UInt64.shiftLeft e _x.5;
       let _x.6 := Nat.add a1 a2;
-      let _x.7 := UInt8.val b1;
+      let _x.7 := UInt8.toBitVec b1;
       let _x.8 := Nat.add _x.6 _x.7;
-      let _x.9 := UInt8.val b2;
+      let _x.9 := UInt8.toBitVec b2;
       let _x.10 := Nat.add _x.8 _x.9;
-      let _x.11 := UInt16.val c1;
+      let _x.11 := UInt16.toBitVec c1;
       let _x.12 := Nat.add _x.10 _x.11;
-      let _x.13 := UInt16.val c2;
+      let _x.13 := UInt16.toBitVec c2;
       let _x.14 := Nat.add _x.12 _x.13;
-      let _x.15 := UInt32.val d1;
+      let _x.15 := UInt32.toBitVec d1;
       let _x.16 := Nat.add _x.14 _x.15;
-      let _x.17 := UInt32.val d2;
+      let _x.17 := UInt32.toBitVec d2;
       let _x.18 := Nat.add _x.16 _x.17;
-      let _x.19 := UInt64.val e1;
+      let _x.19 := UInt64.toBitVec e1;
       let _x.20 := Nat.add _x.18 _x.19;
-      let _x.21 := UInt64.val e2;
+      let _x.21 := UInt64.toBitVec e2;
       let _x.22 := Nat.add _x.20 _x.21;
       return _x.22

tests/lean/CompilerElimDeadBranches.lean.expected.out

@@ -1,20 +1,17 @@
-[Compiler.elimDeadBranches] Eliminating addSomeVal._redArg with #[("val.16", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
-      ("_x.37",
+[Compiler.elimDeadBranches] Eliminating addSomeVal with #[("_x.13",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor
          `Option.some
          #[Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]]),
+      ("val.16", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
       ("val.20", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
-      ("_x.35", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("_x.35", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
       ("_x.36",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top])]
-[Compiler.elimDeadBranches] Threw away cases _x.37 branch Option.none
-[Compiler.elimDeadBranches] Threw away cases _x.37 branch Option.none
-[Compiler.elimDeadBranches] Eliminating addSomeVal with #[("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("_x.38",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top])]
+[Compiler.elimDeadBranches] Threw away cases _x.13 branch Option.none
+[Compiler.elimDeadBranches] Threw away cases _x.13 branch Option.none
 [Compiler.elimDeadBranches] size: 11
-    def addSomeVal._redArg : Option Nat :=
-      let _x.1 := someVal._redArg;
+    def addSomeVal x : Option Nat :=
+      let _x.1 := someVal x;
       cases _x.1 : Option Nat
       | Option.none =>
         ⊥
@@ -28,13 +25,9 @@
           let _x.6 := Nat.add _x.3 _x.5;
           let _x.7 := some _ _x.6;
           return _x.7
-[Compiler.elimDeadBranches] size: 1
-    def addSomeVal x : Option Nat :=
-      let _x.1 := addSomeVal._redArg;
-      return _x.1
 [Compiler.result] size: 9
-    def addSomeVal._redArg : Option Nat :=
-      let _x.1 := someVal._redArg;
+    def addSomeVal x : Option Nat :=
+      let _x.1 := someVal x;
       cases _x.1 : Option Nat
       | Option.none =>
         ⊥
@@ -46,37 +39,37 @@
           let _x.4 := 0;
           let _x.5 := some _ _x.4;
           return _x.5
-[Compiler.result] size: 1 def addSomeVal x : Option Nat := let _x.1 := addSomeVal._redArg; return _x.1
-[Compiler.elimDeadBranches] Eliminating monadic with #[("_x.207",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("_x.211",
+[Compiler.elimDeadBranches] Eliminating monadic with #[("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("a.422", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("_x.414",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("a.208", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("a.206", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("_x.205",
+      ("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("_x.423",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("_x.91",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.ok #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("val.200", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("_x.212",
+      ("val.416", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("_x.124", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("a.424", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
+      ("_x.421",
+       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
+      ("_x.61",
        Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("_x.88", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top)]
-[Compiler.elimDeadBranches] Threw away cases _x.211 branch Option.none
-[Compiler.elimDeadBranches] Threw away cases _x.212 branch Option.none
-[Compiler.elimDeadBranches] Threw away cases _x.205 branch Except.ok
+      ("_x.127",
+       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.ok #[Lean.Compiler.LCNF.UnreachableBranches.Value.top])]
+[Compiler.elimDeadBranches] Threw away cases _x.61 branch Option.none
+[Compiler.elimDeadBranches] Threw away cases _x.414 branch Option.none
+[Compiler.elimDeadBranches] Threw away cases _x.421 branch Except.ok
 [Compiler.elimDeadBranches] size: 15
     def monadic x y : Except String Nat :=
       jp _jp.1 : Except String Nat :=
         let _x.2 := Nat.add x y;
         let _x.3 := Except.ok _ _ _x.2;
         return _x.3;
-      let _x.4 := addSomeVal._redArg;
+      let _x.4 := addSomeVal x;
       cases _x.4 : Except String Nat
       | Option.none =>
         ⊥
       | Option.some val.5 =>
-        let _x.6 := addSomeVal._redArg;
+        let _x.6 := addSomeVal y;
         cases _x.6 : Except String Nat
         | Option.none =>
           ⊥
@@ -88,21 +81,22 @@
             return _x.10
           | Except.ok a.11 =>
             ⊥
-[Compiler.result] size: 12
+[Compiler.result] size: 13
     def monadic x y : Except String Nat :=
-      let _x.1 := addSomeVal._redArg;
+      let _x.1 := addSomeVal x;
       cases _x.1 : Except String Nat
       | Option.none =>
         ⊥
       | Option.some val.2 =>
-        cases _x.1 : Except String Nat
+        let _x.3 := addSomeVal y;
+        cases _x.3 : Except String Nat
         | Option.none =>
           ⊥
-        | Option.some val.3 =>
-          let _x.4 := throwMyError val.2 val.3;
-          cases _x.4 : Except String Nat
-          | Except.error a.5 =>
-            let _x.6 := Except.error _ _ a.5;
-            return _x.6
-          | Except.ok a.7 =>
+        | Option.some val.4 =>
+          let _x.5 := throwMyError val.2 val.4;
+          cases _x.5 : Except String Nat
+          | Except.error a.6 =>
+            let _x.7 := Except.error _ _ a.6;
+            return _x.7
+          | Except.ok a.8 =>
             ⊥

tests/lean/CompilerProvokeFloatLet.lean.expected.out

@@ -20,9 +20,9 @@
           return c
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.false 0
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.true 0
-[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.zero 0
-[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.succ 0
-[Compiler.floatLetIn] size: 11
+[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.true 0
+[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.false 0
+[Compiler.floatLetIn] size: 13
     def provokeFloatLet x y cond : Nat :=
       let dual := Nat.mul x y;
       cases cond : Nat
@@ -31,18 +31,20 @@
         let _x.1 := Nat.add b dual;
         return _x.1
       | Bool.true =>
-        cases dual : Nat
-        | Nat.zero =>
+        let zero := 0;
+        let isZero := Nat.decEq dual zero;
+        cases isZero : Nat
+        | Bool.true =>
           let a := Nat.pow x y;
           return a
-        | Nat.succ n.2 =>
+        | Bool.false =>
           let c := Nat.sub x y;
           return c
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.false 0
 [Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.true 0
-[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.zero 0
-[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Nat.succ 0
-[Compiler.floatLetIn] size: 11
+[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.true 0
+[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.false 0
+[Compiler.floatLetIn] size: 13
     def provokeFloatLet x y cond : Nat :=
       let dual := Nat.mul x y;
       cases cond : Nat
@@ -51,10 +53,12 @@
         let _x.1 := Nat.add b dual;
         return _x.1
       | Bool.true =>
-        cases dual : Nat
-        | Nat.zero =>
+        let zero := 0;
+        let isZero := Nat.decEq dual zero;
+        cases isZero : Nat
+        | Bool.true =>
           let a := Nat.pow x y;
           return a
-        | Nat.succ n.2 =>
+        | Bool.false =>
           let c := Nat.sub x y;
           return c

tests/lean/computedFieldsCode.lean.expected.out

@@ -1,191 +1,236 @@
-
-[result]
-def Exp.casesOn._override._rarg (x_1 : obj) (x_2 : obj) (x_3 : obj) (x_4 : @& obj) (x_5 : @& obj) (x_6 : @& obj) (x_7 : @& obj) (x_8 : @& obj) : obj :=
-  case x_1 : obj of
-  Exp.var._impl →
-    dec x_3;
-    let x_9 : u32 := sproj[0, 8] x_1;
-    dec x_1;
-    let x_10 : obj := box x_9;
-    let x_11 : obj := app x_2 x_10;
-    ret x_11
-  Exp.app._impl →
-    dec x_2;
-    let x_12 : obj := proj[0] x_1;
-    inc x_12;
-    let x_13 : obj := proj[1] x_1;
-    inc x_13;
-    dec x_1;
-    let x_14 : obj := app x_3 x_12 x_13;
-    ret x_14
-  Exp.a1._impl →
-    dec x_3;
-    dec x_2;
-    inc x_4;
-    ret x_4
-  Exp.a2._impl →
-    dec x_3;
-    dec x_2;
-    inc x_5;
-    ret x_5
-  Exp.a3._impl →
-    dec x_3;
-    dec x_2;
-    inc x_6;
-    ret x_6
-  Exp.a4._impl →
-    dec x_3;
-    dec x_2;
-    inc x_7;
-    ret x_7
-  Exp.a5._impl →
-    dec x_3;
-    dec x_2;
-    inc x_8;
-    ret x_8
-def Exp.casesOn._override (x_1 : ◾) : obj :=
-  let x_2 : obj := pap Exp.casesOn._override._rarg._boxed;
-  ret x_2
-def Exp.casesOn._override._rarg._boxed (x_1 : obj) (x_2 : obj) (x_3 : obj) (x_4 : obj) (x_5 : obj) (x_6 : obj) (x_7 : obj) (x_8 : obj) : obj :=
-  let x_9 : obj := Exp.casesOn._override._rarg x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8;
-  dec x_8;
-  dec x_7;
-  dec x_6;
-  dec x_5;
-  dec x_4;
-  ret x_9
-
-[result]
-def Exp.var._override (x_1 : u32) : obj :=
-  let x_2 : u64 := UInt32.toUInt64 x_1;
-  let x_3 : u64 := 1000;
-  let x_4 : u64 := UInt64.add x_2 x_3;
-  let x_5 : obj := ctor_0.0.12[Exp.var._impl];
-  sset x_5[0, 0] : u64 := x_4;
-  sset x_5[0, 8] : u32 := x_1;
-  ret x_5
-def Exp.app._override (x_1 : obj) (x_2 : obj) : obj :=
-  let x_3 : u64 := Exp.hash._override x_1;
-  let x_4 : u64 := Exp.hash._override x_2;
-  let x_5 : u64 := mixHash x_3 x_4;
-  let x_6 : obj := ctor_1.0.8[Exp.app._impl] x_1 x_2;
-  sset x_6[2, 0] : u64 := x_5;
-  ret x_6
-def Exp.a1._override : obj :=
-  let x_1 : obj := ctor_2[Exp.a1._impl];
-  ret x_1
-def Exp.a2._override : obj :=
-  let x_1 : obj := ctor_3[Exp.a2._impl];
-  ret x_1
-def Exp.a3._override : obj :=
-  let x_1 : obj := ctor_4[Exp.a3._impl];
-  ret x_1
-def Exp.a4._override : obj :=
-  let x_1 : obj := ctor_5[Exp.a4._impl];
-  ret x_1
-def Exp.a5._override : obj :=
-  let x_1 : obj := ctor_6[Exp.a5._impl];
-  ret x_1
-def Exp.hash._override (x_1 : @& obj) : u64 :=
-  case x_1 : obj of
-  Exp.var._impl →
-    let x_2 : u64 := sproj[0, 0] x_1;
-    ret x_2
-  Exp.app._impl →
-    let x_3 : u64 := sproj[2, 0] x_1;
-    ret x_3
-  default →
-    let x_4 : u64 := 42;
-    ret x_4
-def Exp.var._override._boxed (x_1 : obj) : obj :=
-  let x_2 : u32 := unbox x_1;
-  dec x_1;
-  let x_3 : obj := Exp.var._override x_2;
-  ret x_3
-def Exp.hash._override._boxed (x_1 : obj) : obj :=
-  let x_2 : u64 := Exp.hash._override x_1;
-  dec x_1;
-  let x_3 : obj := box x_2;
-  ret x_3
-
-[result]
-def f._closed_1 : obj :=
-  let x_1 : u32 := 10;
-  let x_2 : obj := Exp.var._override x_1;
-  ret x_2
-def f._closed_2 : obj :=
-  let x_1 : obj := f._closed_1;
-  let x_2 : obj := ctor_5[Exp.a4._impl];
-  let x_3 : obj := Exp.app._override x_1 x_2;
-  ret x_3
-def f._closed_3 : u64 :=
-  let x_1 : obj := f._closed_2;
-  let x_2 : u64 := Exp.hash._override x_1;
-  dec x_1;
-  ret x_2
-def f : u64 :=
-  let x_1 : u64 := f._closed_3;
-  ret x_1
-
-[result]
-def g (x_1 : @& obj) : u8 :=
-  case x_1 : obj of
-  Exp.a3._impl →
-    let x_2 : u8 := 1;
-    ret x_2
-  default →
-    let x_3 : u8 := 0;
-    ret x_3
-def g._boxed (x_1 : obj) : obj :=
-  let x_2 : u8 := g x_1;
-  dec x_1;
-  let x_3 : obj := box x_2;
-  ret x_3
-
-[result]
-def hash' (x_1 : @& obj) : obj :=
-  case x_1 : obj of
-  Exp.var._impl →
-    let x_2 : u32 := sproj[0, 8] x_1;
-    let x_3 : obj := UInt32.toNat x_2;
-    ret x_3
-  Exp.app._impl →
-    let x_4 : obj := proj[0] x_1;
-    let x_5 : obj := proj[1] x_1;
-    let x_6 : obj := hash' x_4;
-    let x_7 : obj := hash' x_5;
-    let x_8 : obj := Nat.add x_6 x_7;
-    dec x_7;
-    dec x_6;
-    ret x_8
-  default →
-    let x_9 : obj := 42;
-    ret x_9
-def hash'._boxed (x_1 : obj) : obj :=
-  let x_2 : obj := hash' x_1;
-  dec x_1;
-  ret x_2
-
-[result]
-def getAppFn (x_1 : @& obj) : obj :=
-  case x_1 : obj of
-  Exp.app._impl →
-    let x_2 : obj := proj[0] x_1;
-    let x_3 : obj := getAppFn x_2;
-    ret x_3
-  default →
-    inc x_1;
-    ret x_1
-def getAppFn._boxed (x_1 : obj) : obj :=
-  let x_2 : obj := getAppFn x_1;
-  dec x_1;
-  ret x_2
-
-[result]
-def Exp.f (x_1 : @& obj) : obj :=
-  let x_2 : obj := getAppFn x_1;
-  ret x_2
-def Exp.f._boxed (x_1 : obj) : obj :=
-  let x_2 : obj := Exp.f x_1;
-  dec x_1;
-  ret x_2
+[Compiler.IR] [result]
+    def Exp.casesOn._override._redArg (x_1 : obj) (x_2 : obj) (x_3 : obj) (x_4 : @& obj) (x_5 : @& obj) (x_6 : @& obj) (x_7 : @& obj) (x_8 : @& obj) : obj :=
+      case x_1 : obj of
+      Exp.var._impl →
+        dec x_3;
+        let x_9 : u32 := sproj[0, 8] x_1;
+        dec x_1;
+        let x_10 : obj := box x_9;
+        let x_11 : obj := app x_2 x_10;
+        ret x_11
+      Exp.app._impl →
+        dec x_2;
+        let x_12 : obj := proj[0] x_1;
+        inc x_12;
+        let x_13 : obj := proj[1] x_1;
+        inc x_13;
+        dec x_1;
+        let x_14 : obj := app x_3 x_12 x_13;
+        ret x_14
+      Exp.a1._impl →
+        dec x_3;
+        dec x_2;
+        inc x_4;
+        ret x_4
+      Exp.a2._impl →
+        dec x_3;
+        dec x_2;
+        inc x_5;
+        ret x_5
+      Exp.a3._impl →
+        dec x_3;
+        dec x_2;
+        inc x_6;
+        ret x_6
+      Exp.a4._impl →
+        dec x_3;
+        dec x_2;
+        inc x_7;
+        ret x_7
+      Exp.a5._impl →
+        dec x_3;
+        dec x_2;
+        inc x_8;
+        ret x_8
+    def Exp.casesOn._override (x_1 : ◾) (x_2 : obj) (x_3 : obj) (x_4 : obj) (x_5 : @& obj) (x_6 : @& obj) (x_7 : @& obj) (x_8 : @& obj) (x_9 : @& obj) : obj :=
+      case x_2 : obj of
+      Exp.var._impl →
+        dec x_4;
+        let x_10 : u32 := sproj[0, 8] x_2;
+        dec x_2;
+        let x_11 : obj := box x_10;
+        let x_12 : obj := app x_3 x_11;
+        ret x_12
+      Exp.app._impl →
+        dec x_3;
+        let x_13 : obj := proj[0] x_2;
+        inc x_13;
+        let x_14 : obj := proj[1] x_2;
+        inc x_14;
+        dec x_2;
+        let x_15 : obj := app x_4 x_13 x_14;
+        ret x_15
+      Exp.a1._impl →
+        dec x_4;
+        dec x_3;
+        inc x_5;
+        ret x_5
+      Exp.a2._impl →
+        dec x_4;
+        dec x_3;
+        inc x_6;
+        ret x_6
+      Exp.a3._impl →
+        dec x_4;
+        dec x_3;
+        inc x_7;
+        ret x_7
+      Exp.a4._impl →
+        dec x_4;
+        dec x_3;
+        inc x_8;
+        ret x_8
+      Exp.a5._impl →
+        dec x_4;
+        dec x_3;
+        inc x_9;
+        ret x_9
+    def Exp.casesOn._override._redArg._boxed (x_1 : obj) (x_2 : obj) (x_3 : obj) (x_4 : obj) (x_5 : obj) (x_6 : obj) (x_7 : obj) (x_8 : obj) : obj :=
+      let x_9 : obj := Exp.casesOn._override._redArg x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8;
+      dec x_8;
+      dec x_7;
+      dec x_6;
+      dec x_5;
+      dec x_4;
+      ret x_9
+    def Exp.casesOn._override._boxed (x_1 : obj) (x_2 : obj) (x_3 : obj) (x_4 : obj) (x_5 : obj) (x_6 : obj) (x_7 : obj) (x_8 : obj) (x_9 : obj) : obj :=
+      let x_10 : obj := Exp.casesOn._override x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9;
+      dec x_9;
+      dec x_8;
+      dec x_7;
+      dec x_6;
+      dec x_5;
+      ret x_10
+[Compiler.IR] [result]
+    def Exp.var._override (x_1 : u32) : obj :=
+      let x_2 : u64 := UInt32.toUInt64 x_1;
+      let x_3 : obj := 1000;
+      let x_4 : u64 := UInt64.ofNat x_3;
+      let x_5 : u64 := UInt64.add x_2 x_4;
+      let x_6 : obj := ctor_0.0.12[Exp.var._impl];
+      sset x_6[0, 0] : u64 := x_5;
+      sset x_6[0, 8] : u32 := x_1;
+      ret x_6
+    def Exp.app._override (x_1 : obj) (x_2 : obj) : obj :=
+      let x_3 : u64 := Exp.hash._override x_1;
+      let x_4 : u64 := Exp.hash._override x_2;
+      let x_5 : u64 := mixHash x_3 x_4;
+      let x_6 : obj := ctor_1.0.8[Exp.app._impl] x_1 x_2;
+      sset x_6[2, 0] : u64 := x_5;
+      ret x_6
+    def Exp.a1._override : obj :=
+      let x_1 : obj := ctor_2[Exp.a1._impl];
+      ret x_1
+    def Exp.a2._override : obj :=
+      let x_1 : obj := ctor_3[Exp.a2._impl];
+      ret x_1
+    def Exp.a3._override : obj :=
+      let x_1 : obj := ctor_4[Exp.a3._impl];
+      ret x_1
+    def Exp.a4._override : obj :=
+      let x_1 : obj := ctor_5[Exp.a4._impl];
+      ret x_1
+    def Exp.a5._override : obj :=
+      let x_1 : obj := ctor_6[Exp.a5._impl];
+      ret x_1
+    def Exp.hash._override (x_1 : @& obj) : u64 :=
+      case x_1 : obj of
+      Exp.var._impl →
+        let x_2 : u64 := sproj[0, 0] x_1;
+        ret x_2
+      Exp.app._impl →
+        let x_3 : u64 := sproj[2, 0] x_1;
+        ret x_3
+      default →
+        let x_4 : obj := 42;
+        let x_5 : u64 := UInt64.ofNat x_4;
+        ret x_5
+    def Exp.var._override._boxed (x_1 : obj) : obj :=
+      let x_2 : u32 := unbox x_1;
+      dec x_1;
+      let x_3 : obj := Exp.var._override x_2;
+      ret x_3
+    def Exp.hash._override._boxed (x_1 : obj) : obj :=
+      let x_2 : u64 := Exp.hash._override x_1;
+      dec x_1;
+      let x_3 : obj := box x_2;
+      ret x_3
+[Compiler.IR] [result]
+    def f : u64 :=
+      let x_1 : obj := 10;
+      let x_2 : u32 := UInt32.ofNat x_1;
+      let x_3 : obj := Exp.var._override x_2;
+      let x_4 : obj := ctor_5[Exp.a4._impl];
+      let x_5 : obj := Exp.app._override x_3 x_4;
+      let x_6 : u64 := Exp.hash._override x_5;
+      dec x_5;
+      ret x_6
+[Compiler.IR] [result]
+    def g (x_1 : @& obj) : u8 :=
+      let x_2 : obj := ctor_0[Bool.false];
+      case x_1 : obj of
+      Exp.var._impl →
+        let x_3 : u8 := unbox x_2;
+        ret x_3
+      Exp.app._impl →
+        let x_4 : u8 := unbox x_2;
+        ret x_4
+      Exp.a3._impl →
+        let x_5 : obj := ctor_1[Bool.true];
+        let x_6 : u8 := unbox x_5;
+        ret x_6
+      default →
+        let x_7 : u8 := unbox x_2;
+        ret x_7
+    def g._boxed (x_1 : obj) : obj :=
+      let x_2 : u8 := g x_1;
+      dec x_1;
+      let x_3 : obj := box x_2;
+      ret x_3
+[Compiler.IR] [result]
+    def hash' (x_1 : @& obj) : obj :=
+      case x_1 : obj of
+      Exp.var._impl →
+        let x_2 : u32 := sproj[0, 8] x_1;
+        let x_3 : obj := UInt32.toNat x_2;
+        ret x_3
+      Exp.app._impl →
+        let x_4 : obj := proj[0] x_1;
+        let x_5 : obj := proj[1] x_1;
+        let x_6 : obj := hash' x_4;
+        let x_7 : obj := hash' x_5;
+        let x_8 : obj := Nat.add x_6 x_7;
+        dec x_7;
+        dec x_6;
+        ret x_8
+      default →
+        let x_9 : obj := 42;
+        ret x_9
+    def hash'._boxed (x_1 : obj) : obj :=
+      let x_2 : obj := hash' x_1;
+      dec x_1;
+      ret x_2
+[Compiler.IR] [result]
+    def getAppFn (x_1 : @& obj) : obj :=
+      case x_1 : obj of
+      Exp.app._impl →
+        let x_2 : obj := proj[0] x_1;
+        let x_3 : obj := getAppFn x_2;
+        ret x_3
+      default →
+        inc x_1;
+        ret x_1
+    def getAppFn._boxed (x_1 : obj) : obj :=
+      let x_2 : obj := getAppFn x_1;
+      dec x_1;
+      ret x_2
+[Compiler.IR] [result]
+    def Exp.f (x_1 : obj) : obj :=
+      inc x_1;
+      let x_2 : obj := Exp.app._override x_1 x_1;
+      let x_3 : obj := proj[0] x_2;
+      inc x_3;
+      dec x_2;
+      let x_4 : obj := getAppFn x_3;
+      dec x_3;
+      ret x_4

tests/lean/csimpAttr.lean.expected.out

@@ -1,7 +1,6 @@
 csimpAttr.lean:7:2-7:7: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.
-
-[init]
-def f (x_1 : obj) : obj :=
-  let x_2 : obj := Nat.add x_1 x_1;
-  let x_3 : obj := Nat.add x_2 x_2;
-  ret x_3
+[Compiler.IR] [init]
+    def f (x_1 : obj) : obj :=
+      let x_2 : obj := Nat.add x_1 x_1;
+      let x_3 : obj := Nat.add x_2 x_2;
+      ret x_3

tests/lean/csimpAttrAppend.lean.expected.out

@@ -1,6 +1,5 @@
-
-[init]
-def f (x_1 : obj) (x_2 : obj) (x_3 : obj) : obj :=
-  let x_4 : obj := List.appendTR._rarg x_1 x_2;
-  let x_5 : obj := List.appendTR._rarg x_4 x_3;
-  ret x_5
+[Compiler.IR] [init]
+    def f (x_1 : obj) (x_2 : obj) (x_3 : obj) : obj :=
+      let x_4 : obj := List.appendTR._redArg x_1 x_2;
+      let x_5 : obj := List.appendTR._redArg x_4 x_3;
+      ret x_5

tests/lean/doubleReset.lean.expected.out

@@ -1,37 +1,33 @@
-
-[reset_reuse]
-def Array.mapMUnsafe.map._at.applyProjectionRules._spec_1._rarg (x_1 : obj) (x_2 : usize) (x_3 : usize) (x_4 : obj) : obj :=
-  let x_5 : u8 := USize.decLt x_3 x_2;
-  case x_5 : obj of
-  Bool.false →
-    ret x_4
-  Bool.true →
-    let x_6 : obj := Array.uget ◾ x_4 x_3 ◾;
-    let x_7 : obj := 0;
-    let x_8 : obj := Array.uset ◾ x_4 x_3 x_7 ◾;
-    let x_9 : obj := proj[0] x_6;
-    case x_9 : obj of
-    Prod.mk →
-      case x_9 : obj of
-      Prod.mk →
+[Compiler.IR] [reset_reuse]
+    def Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg (x_1 : obj) (x_2 : usize) (x_3 : usize) (x_4 : obj) : obj :=
+      let x_5 : u8 := USize.decLt x_3 x_2;
+      case x_5 : obj of
+      Bool.false →
+        ret x_4
+      Bool.true →
+        let x_6 : obj := Array.uget ◾ x_4 x_3 ◾;
+        let x_7 : obj := ctor_0[Nat.zero];
+        let x_8 : obj := Array.uset ◾ x_4 x_3 x_7 ◾;
+        let x_9 : obj := proj[0] x_6;
         let x_10 : obj := proj[0] x_9;
         let x_11 : obj := proj[1] x_9;
-        let x_18 : obj := reset[2] x_9;
-        let x_12 : obj := reuse x_18 in ctor_0[Prod.mk] x_10 x_11;
+        let x_12 : obj := ctor_0[Prod.mk] x_10 x_11;
         let x_13 : obj := ctor_0[Prod.mk] x_12 x_1;
-        let x_14 : usize := 1;
-        let x_15 : usize := USize.add x_3 x_14;
-        let x_16 : obj := Array.uset ◾ x_8 x_3 x_13 ◾;
-        let x_17 : obj := Array.mapMUnsafe.map._at.applyProjectionRules._spec_1._rarg x_1 x_2 x_15 x_16;
-        ret x_17
-def Array.mapMUnsafe.map._at.applyProjectionRules._spec_1 (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) : obj :=
-  let x_4 : obj := pap Array.mapMUnsafe.map._at.applyProjectionRules._spec_1._rarg;
-  ret x_4
-def applyProjectionRules._rarg (x_1 : obj) (x_2 : obj) : obj :=
-  let x_3 : usize := Array.usize ◾ x_1;
-  let x_4 : usize := 0;
-  let x_5 : obj := Array.mapMUnsafe.map._at.applyProjectionRules._spec_1._rarg x_2 x_3 x_4 x_1;
-  ret x_5
-def applyProjectionRules (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) : obj :=
-  let x_4 : obj := pap applyProjectionRules._rarg;
-  ret x_4
+        let x_14 : obj := 1;
+        let x_15 : usize := USize.ofNat x_14;
+        let x_16 : usize := USize.add x_3 x_15;
+        let x_17 : obj := Array.uset ◾ x_8 x_3 x_13 ◾;
+        let x_18 : obj := Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_1 x_2 x_16 x_17;
+        ret x_18
+    def Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0 (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) (x_4 : obj) (x_5 : usize) (x_6 : usize) (x_7 : obj) : obj :=
+      let x_8 : obj := Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_4 x_5 x_6 x_7;
+      ret x_8
+    def applyProjectionRules._redArg (x_1 : obj) (x_2 : obj) : obj :=
+      let x_3 : usize := Array.usize ◾ x_1;
+      let x_4 : obj := 0;
+      let x_5 : usize := USize.ofNat x_4;
+      let x_6 : obj := Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_2 x_3 x_5 x_1;
+      ret x_6
+    def applyProjectionRules (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) (x_4 : obj) (x_5 : obj) : obj :=
+      let x_6 : obj := applyProjectionRules._redArg x_4 x_5;
+      ret x_6

tests/lean/lambdaLiftCache.lean.expected.out

@@ -2,13 +2,9 @@
     def foo._lam_0 x x.1 : Nat :=
       let _x.2 := Nat.add x.1 x;
       return _x.2
-[Compiler.saveMono] size: 2
-    def foo x xs : List Nat :=
-      let _f.1 := foo._lam_0 x;
-      let _x.2 := List.map._at_.map.spec_0 _f.1 xs;
-      return _x.2
+[Compiler.saveMono] size: 2 def foo x xs : List Nat := let _f.1 := foo._lam_0 x; let _x.2 := map _f.1 xs; return _x.2
 [Compiler.saveMono] size: 2
     def boo x xs : List Nat :=
       let _f.1 := foo._lam_0 x;
-      let _x.2 := List.map._at_.map.spec_0 _f.1 xs;
+      let _x.2 := map _f.1 xs;
       return _x.2

tests/lean/lcnfTypes.lean.expected.out

@@ -1,20 +1,20 @@
-Vec.zip : {α : Type u_1} → {n : Nat} → {β : Type u_2} → Vec α ◾ → Vec β ◾ → Vec (α × β) ◾
-mkConstTuple : {α : Type u_1} → α → Nat → ◾
-Fin.add : {n : Nat} → Fin ◾ → Fin ◾ → Fin ◾
-Vec.cons : {α : Type u} → {n : Nat} → α → Vec α ◾ → Vec α ◾
-Eq.rec : {α : Sort u_1} → {a : α} → {motive : α → ◾ → Sort u} → motive ◾ ◾ → {a : α} → ◾ → motive ◾ ◾
+Vec.zip : {α : Type u_1} → {n : Nat} → {β : Type u_2} → Vec α lcAny → Vec β lcAny → Vec (α × β) lcAny
+mkConstTuple : {α : Type u_1} → α → Nat → lcAny
+Fin.add : {n : Nat} → Fin lcAny → Fin lcAny → Fin lcAny
+Vec.cons : {α : Type u} → {n : Nat} → α → Vec α lcAny → Vec α lcAny
+Eq.rec : {α : Sort u_1} → {a : α} → {motive : α → ◾ → Sort u} → motive lcAny lcAny → {a : α} → ◾ → motive lcAny lcAny
 GetElem.getElem : {coll : Type u} →
   {idx : Type v} →
     {elem : Type w} → {valid : coll → idx → Prop} → [self : GetElem coll idx elem ◾] → coll → idx → ◾ → elem
-Term.constFold : {ctx : List Ty} → {ty : Ty} → _root_.Term ◾ ◾ → _root_.Term ◾ ◾
-Term.denote : {ctx : List Ty} → {ty : Ty} → _root_.Term ◾ ◾ → HList ◾ ◾ → ◾
-HList.get : {α : Type u_1} → {β : α → Type u_2} → {is : List α} → {i : α} → HList β ◾ → Member ◾ ◾ → β ◾
-Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member ◾ ◾
+Term.constFold : {ctx : List Ty} → {ty : Ty} → _root_.Term lcAny lcAny → _root_.Term lcAny lcAny
+Term.denote : {ctx : List Ty} → {ty : Ty} → _root_.Term lcAny lcAny → HList lcAny lcAny → lcAny
+HList.get : {α : Type u_1} → {β : α → Type u_2} → {is : List α} → {i : α} → HList β lcAny → Member lcAny lcAny → β lcAny
+Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member lcAny lcAny
 Ty.denote : Ty → Type
 MonadControl.liftWith : {m : Type u → Type v} →
-  {n : Type u → Type w} → [self : MonadControl m n] → {α : Type u} → (({β : Type u} → n β → m ◾) → m α) → n α
-MonadControl.restoreM : {m : Type u → Type v} → {n : Type u → Type w} → [self : MonadControl m n] → {α : Type u} → m ◾ → n α
-Decidable.casesOn : {p : Prop} → {motive : Decidable ◾ → Sort u} → Decidable ◾ → (◾ → motive ◾) → (◾ → motive ◾) → motive ◾
+  {n : Type u → Type w} → [self : MonadControl m n] → {α : Type u} → (({β : Type u} → n β → m lcAny) → m α) → n α
+MonadControl.restoreM : {m : Type u → Type v} → {n : Type u → Type w} → [self : MonadControl m n] → {α : Type u} → m lcAny → n α
+Decidable.casesOn : {p : Prop} → {motive : Decidable ◾ → Sort u} → Decidable ◾ → (◾ → motive lcAny) → (◾ → motive lcAny) → motive lcAny
 Lean.getConstInfo : {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m ConstantInfo
 Lean.Meta.instMonadMetaM : Monad fun α =>
   Context → ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit α
@@ -29,26 +29,25 @@ Lean.Elab.Term.elabTerm : Syntax →
             Context →
               ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit Expr
 Nat.add : Nat → Nat → Nat
-Magma.mul : Magma → ◾ → ◾ → ◾
-weird1 : Bool → ◾
-lamAny₁ : Bool → Monad ◾
-lamAny₂ : Bool → Monad ◾
-Term.constFold : List Ty → Ty → _root_.Term lcErased lcErased → _root_.Term lcErased lcErased
-Term.denote : lcErased
-HList.get : lcErased → lcErased → List lcAny → lcAny → HList lcAny lcErased lcErased → Member lcAny lcErased lcErased → lcAny
-Member.head : lcErased → lcAny → List lcAny → Member lcAny lcErased lcErased
+Magma.mul : Magma → lcAny → lcAny → lcAny
+weird1 : Bool → lcAny
+lamAny₁ : Bool → Monad fun α => lcAny
+lamAny₂ : Bool → Monad lcAny
+Term.constFold : List Ty → Ty → _root_.Term lcAny lcAny → _root_.Term lcAny lcAny
+Term.denote : List Ty → Ty → _root_.Term lcAny lcAny → HList Ty lcAny lcAny → lcAny
+HList.get : lcErased → lcErased → List lcAny → lcAny → HList lcAny lcAny lcAny → Member lcAny lcAny lcAny → lcAny
+Member.head : lcErased → lcAny → List lcAny → Member lcAny lcAny lcAny
 Ty.denote : lcErased
-MonadControl.liftWith : lcErased → lcErased → MonadControl lcErased lcErased → lcErased → ((lcErased → lcAny → lcAny) → lcAny) → lcAny
-MonadControl.restoreM : lcErased → lcErased → MonadControl lcErased lcErased → lcErased → lcAny → lcAny
+MonadControl.liftWith : lcErased → lcErased → MonadControl lcAny lcAny → lcErased → ((lcErased → lcAny → lcAny) → lcAny) → lcAny
+MonadControl.restoreM : lcErased → lcErased → MonadControl lcAny lcAny → lcErased → lcAny → lcAny
 Decidable.casesOn : lcErased → lcErased → Bool → (lcErased → lcAny) → (lcErased → lcAny) → lcAny
-Lean.getConstInfo : lcErased → Monad lcErased → MonadEnv lcErased → MonadError lcErased → Name → lcAny
-Lean.Meta.instMonadMetaM : Monad lcErased
-Lean.Meta.inferType : Expr → Context → lcErased → Core.Context → lcErased → PUnit → EStateM.Result Exception PUnit Expr
+Lean.getConstInfo : lcErased → Monad lcAny → MonadEnv lcAny → MonadError lcAny → Name → lcAny
+Lean.Meta.instMonadMetaM : Monad lcAny
+Lean.Meta.inferType : Expr → Context → lcAny → Core.Context → lcAny → PUnit → EStateM.Result Exception PUnit Expr
 Lean.Elab.Term.elabTerm : Syntax →
   Option Expr →
     Bool →
       Bool →
-        Elab.Term.Context →
-          lcErased → Context → lcErased → Core.Context → lcErased → PUnit → EStateM.Result Exception PUnit Expr
+        Elab.Term.Context → lcAny → Context → lcAny → Core.Context → lcAny → PUnit → EStateM.Result Exception PUnit Expr
 Nat.add : Nat → Nat → Nat
 Fin.add : Nat → Nat → Nat → Nat

tests/lean/listLength.lean.expected.out

@@ -1,8 +1,6 @@
-
-[init]
-def f (x_1 : obj) : obj :=
-  let x_2 : obj := 0;
-  let x_3 : obj := List.lengthTRAux._rarg x_1 x_2;
-  let x_4 : obj := 2;
-  let x_5 : obj := Nat.mul x_4 x_3;
-  ret x_5
+[Compiler.IR] [init]
+    def f (x_1 : obj) : obj :=
+      let x_2 : obj := List.lengthTR._redArg x_1;
+      let x_3 : obj := 1;
+      let x_4 : obj := Nat.shiftLeft x_2 x_3;
+      ret x_4

tests/lean/new-compiler/README.md

@@ -1,2 +0,0 @@
-This folder contains test files for the new compiler.
-They are currently disabled while development on the compiler is paused and `compiler.enableNew` is deactivated.

tests/lean/new-compiler/unhygienicCode.lean

@@ -1,10 +0,0 @@
-import Lean.Hygiene
-open Lean
-
-set_option trace.Compiler.result true
-set_option trace.compiler.ir.result true
-
--- The following function should not allocate any closures,
--- nor any heap object that doesn't appear in the result:
-def foo (n : Nat) : Syntax.Term :=
-  Unhygienic.run `(a + $(quote n))

tests/lean/new-compiler/unhygienicCode.lean.expected.out

@@ -1,86 +0,0 @@
-
-[result]
-def foo._closed_1 : obj :=
-  let x_1 : obj := ctor_0[Lean.Syntax.missing];
-  let x_2 : u8 := 0;
-  let x_3 : obj := Lean.SourceInfo.fromRef x_1 x_2;
-  ret x_3
-def foo._closed_2 : obj :=
-  let x_1 : obj := "UnhygienicMain";
-  ret x_1
-def foo._closed_3 : obj :=
-  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
-  let x_2 : obj := foo._closed_2;
-  let x_3 : obj := Lean.Name.str._override x_1 x_2;
-  ret x_3
-def foo._closed_4 : obj :=
-  let x_1 : obj := "term_+_";
-  ret x_1
-def foo._closed_5 : obj :=
-  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
-  let x_2 : obj := foo._closed_4;
-  let x_3 : obj := Lean.Name.str._override x_1 x_2;
-  ret x_3
-def foo._closed_6 : obj :=
-  let x_1 : obj := "a";
-  ret x_1
-def foo._closed_7 : obj :=
-  let x_1 : obj := foo._closed_6;
-  let x_2 : obj := String.toSubstring' x_1;
-  ret x_2
-def foo._closed_8 : obj :=
-  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
-  let x_2 : obj := foo._closed_6;
-  let x_3 : obj := Lean.Name.str._override x_1 x_2;
-  ret x_3
-def foo._closed_9 : obj :=
-  let x_1 : obj := foo._closed_3;
-  let x_2 : obj := foo._closed_8;
-  let x_3 : obj := Lean.firstFrontendMacroScope;
-  let x_4 : obj := Lean.addMacroScope x_1 x_2 x_3;
-  ret x_4
-def foo._closed_10 : obj :=
-  let x_1 : obj := ctor_0[List.nil];
-  let x_2 : obj := foo._closed_1;
-  let x_3 : obj := foo._closed_7;
-  let x_4 : obj := foo._closed_9;
-  let x_5 : obj := ctor_3[Lean.Syntax.ident] x_2 x_3 x_4 x_1;
-  ret x_5
-def foo._closed_11 : obj :=
-  let x_1 : obj := "+";
-  ret x_1
-def foo._closed_12 : obj :=
-  let x_1 : obj := foo._closed_1;
-  let x_2 : obj := foo._closed_11;
-  let x_3 : obj := ctor_2[Lean.Syntax.atom] x_1 x_2;
-  ret x_3
-def foo (x_1 : obj) : obj :=
-  let x_2 : obj := Nat.repr x_1;
-  let x_3 : obj := ctor_2[Lean.SourceInfo.none];
-  let x_4 : obj := Lean.Syntax.mkNumLit x_2 x_3;
-  let x_5 : obj := foo._closed_1;
-  let x_6 : obj := foo._closed_5;
-  let x_7 : obj := foo._closed_10;
-  let x_8 : obj := foo._closed_12;
-  let x_9 : obj := Lean.Syntax.node3 x_5 x_6 x_7 x_8 x_4;
-  ret x_9[Compiler.result] size: 18
-    def foo n : Syntax :=
-      let _x.1 := Syntax.missing;
-      let _x.2 := 1;
-      let _x.3 := false;
-      let _x.4 := SourceInfo.fromRef _x.1 _x.3;
-      let _x.5 := "UnhygienicMain";
-      let _x.6 := Name.mkStr1 _x.5;
-      let _x.7 := "term_+_";
-      let _x.8 := Name.mkStr1 _x.7;
-      let _x.9 := "a";
-      let _x.10 := String.toSubstring' _x.9;
-      let _x.11 := Name.mkStr1 _x.9;
-      let _x.12 := addMacroScope _x.6 _x.11 _x.2;
-      let _x.13 := [] _;
-      let _x.14 := Syntax.ident _x.4 _x.10 _x.12 _x.13;
-      let _x.15 := "+";
-      let _x.16 := Syntax.atom _x.4 _x.15;
-      let _x.17 := Lean.instQuoteNatNumLitKind._elam_0 n;
-      let _x.18 := Syntax.node3 _x.4 _x.8 _x.14 _x.16 _x.17;
-      return _x.18

tests/lean/noncompSection.lean.expected.out

@@ -1,2 +1,2 @@
 1
-noncompSection.lean:35:4-35:5: error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.choose', and it does not have executable code
+noncompSection.lean:35:4-35:5: error: failed to compile definition, compiler IR check failed at 'i'. Error: depends on declaration 'Classical.choose', which has no executable code; consider marking definition as 'noncomputable'

tests/lean/reduceArity.lean.expected.out

@@ -1,14 +1,18 @@
-[Compiler.result] size: 5
-    def g._redArg (n : Nat) (a : ◾) (f : ◾ → ◾) : ◾ :=
-      cases n : ◾
-      | Nat.zero =>
+[Compiler.result] size: 9
+    def g._redArg (n : Nat) (a : lcAny) (f : lcAny → lcAny) : lcAny :=
+      let zero := 0;
+      let isZero := Nat.decEq n zero;
+      cases isZero : lcAny
+      | Bool.true =>
         return a
-      | Nat.succ (n.1 : Nat) =>
+      | Bool.false =>
+        let one := 1;
+        let n.1 := Nat.sub n one;
         let _x.2 := g._redArg n.1 a f;
         let _x.3 := f _x.2;
         return _x.3
 [Compiler.result] size: 1
-    def g (α : ◾) (n : Nat) (a : ◾) (b : ◾) (f : ◾ → ◾) : ◾ :=
+    def g (α : ◾) (n : Nat) (a : lcAny) (b : lcAny) (f : lcAny → lcAny) : lcAny :=
       let _x.1 := g._redArg n a f;
       return _x.1
 [Compiler.result] size: 4

tests/lean/run/1785.lean

@@ -11,8 +11,8 @@ noncomputable
 def char (R : Type) [∀ n, OfNat R n] : Nat := 0
 
 /--
-error: failed to compile definition, compiler IR check failed at 'bug._rarg'. Error: depends on
-declaration 'char', which has no executable code; consider marking definition as 'noncomputable'
+error: failed to compile definition, compiler IR check failed at 'bug._redArg'. Error: depends
+on declaration 'char', which has no executable code; consider marking definition as 'noncomputable'
 -/
 #guard_msgs in
 def bug (R : Type) [∀ n, OfNat R n] : R :=

tests/lean/run/2291.lean

@@ -6,107 +6,193 @@ Issue #2291
 The following example would cause the pretty printer to panic.
 -/
 
-set_option trace.compiler.simp true in
+set_option trace.Compiler.simp true in
 /--
 info: [0]
 ---
-info: [compiler.simp] >> _eval
-let _x_21 := `Nat;
-let _x_22 := [];
-let _x_23 := Lean.Expr.const _x_21 _x_22;
-let _x_24 := `List.nil;
-let _x_25 := Lean.Level.zero :: _x_22;
-let _x_26 := Lean.Expr.const _x_24 _x_25;
-let _x_27 := _x_26.app _x_23;
-let _x_28 := `List.cons;
-let _x_29 := Lean.Expr.const _x_28 _x_25;
-let _x_30 := _x_29.app _x_23;
-let _x_31 := [];
-let _x_32 := 0 :: _x_31;
-let _x_33 := Lean.List.toExprAux✝ _x_27 _x_30 _x_32;
-Lean.MessageData.ofExpr _x_33
-[compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
-fun nilFn consFn x =>
-  List.casesOn fun head tail =>
-    let _x_1 := Lean.mkNatLit head;
-    let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail;
-    Lean.mkAppB consFn _x_1 _x_2
->> _eval
-let _x_14 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat";
-let _x_15 := List.nil _neutral;
-let _x_16 := Lean.Expr.const._override _x_14 _x_15;
-let _x_17 := `List.nil;
-let _x_18 := List.cons _neutral Lean.Level.zero._impl _x_15;
-let _x_19 := Lean.Expr.const._override _x_17 _x_18;
-let _x_20 := Lean.Expr.app._override _x_19 _x_16;
-let _x_21 := `List.cons;
-let _x_22 := Lean.Expr.const._override _x_21 _x_18;
-let _x_23 := Lean.Expr.app._override _x_22 _x_16;
-let _x_24 := List.cons _neutral 0 _x_15;
-let _x_25 := Lean.List.toExprAux._at._eval._spec_1✝ _x_20 _x_23 _x_24;
-Lean.MessageData.ofExpr _x_25
-[compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
-fun nilFn consFn x =>
-  List.casesOn fun head tail =>
-    let _x_1 := Lean.mkNatLit head;
-    let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail;
-    Lean.mkAppB consFn _x_1 _x_2
->> _eval
-let _x_1 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat";
-let _x_2 := List.nil _neutral;
-let _x_3 := Lean.Expr.const._override _x_1 _x_2;
-let _x_4 := `List.nil;
-let _x_5 := List.cons _neutral Lean.Level.zero._impl _x_2;
-let _x_6 := Lean.Expr.const._override _x_4 _x_5;
-let _x_7 := Lean.Expr.app._override _x_6 _x_3;
-let _x_8 := `List.cons;
-let _x_9 := Lean.Expr.const._override _x_8 _x_5;
-let _x_10 := Lean.Expr.app._override _x_9 _x_3;
-let _x_11 := List.cons _neutral 0 _x_2;
-let _x_12 := Lean.List.toExprAux._at._eval._spec_1✝ _x_7 _x_10 _x_11;
-Lean.MessageData.ofExpr _x_12
-[compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
-fun nilFn consFn x =>
-  List.casesOn fun head tail =>
-    let _x_1 := Lean.mkNatLit head;
-    let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail;
-    Lean.mkAppB consFn _x_1 _x_2
->> _eval._closed_1
-"Nat"
->> _eval._closed_2
-Lean.Name.str._override Lean.Name.anonymous._impl _eval._closed_1
->> _eval._closed_3
-let _x_1 := List.nil _neutral;
-Lean.Expr.const._override _eval._closed_2 _x_1
->> _eval._closed_4
-"List"
->> _eval._closed_5
-"nil"
->> _eval._closed_6
-Lean.Name.mkStr2 _eval._closed_4 _eval._closed_5
->> _eval._closed_7
-let _x_1 := List.nil _neutral;
-List.cons _neutral Lean.Level.zero._impl _x_1
->> _eval._closed_8
-Lean.Expr.const._override _eval._closed_6 _eval._closed_7
->> _eval._closed_9
-Lean.Expr.app._override _eval._closed_8 _eval._closed_3
->> _eval._closed_10
-"cons"
->> _eval._closed_11
-Lean.Name.mkStr2 _eval._closed_4 _eval._closed_10
->> _eval._closed_12
-Lean.Expr.const._override _eval._closed_11 _eval._closed_7
->> _eval._closed_13
-Lean.Expr.app._override _eval._closed_12 _eval._closed_3
->> _eval._closed_14
-let _x_1 := List.nil _neutral;
-List.cons _neutral 0 _x_1
->> _eval
-let _x_1 :=
-  Lean.List.toExprAux._at._eval._spec_1✝ _eval._closed_9 _eval._closed_13
-    _eval._closed_14;
-Lean.MessageData.ofExpr _x_1
+info: [Compiler.simp] size: 22
+    def _eval : Lean.MessageData :=
+      let _x.1 := Lean.instToExprNat;
+      let _x.2 := "Nat";
+      let _x.3 := Lean.Name.mkStr1 _x.2;
+      let _x.4 := @List.nil _;
+      let type := Lean.Expr.const._override _x.3 _x.4;
+      let _x.5 := "List";
+      let _x.6 := "nil";
+      let _x.7 := Lean.Name.mkStr2 _x.5 _x.6;
+      let _x.8 := Lean.Level.zero._impl;
+      let _x.9 := @List.nil _;
+      let _x.10 := @List.cons _ _x.8 _x.9;
+      let _x.11 := Lean.Expr.const._override _x.7 _x.10;
+      let nil := Lean.Expr.app._override _x.11 type;
+      let _x.12 := "cons";
+      let _x.13 := Lean.Name.mkStr2 _x.5 _x.12;
+      let _x.14 := Lean.Expr.const._override _x.13 _x.10;
+      let cons := Lean.Expr.app._override _x.14 type;
+      let _x.15 := 0;
+      let _x.16 := @List.nil _;
+      let _x.17 := @List.cons _ _x.15 _x.16;
+      let _x.18 := @Lean.List.toExprAux.0 _ _x.1 nil cons _x.17;
+      let _x.19 := Lean.MessageData.ofExpr _x.18;
+      return _x.19
+[Compiler.simp] size: 22
+    def _eval : Lean.MessageData :=
+      let _x.1 := Lean.instToExprNat;
+      let _x.2 := "Nat";
+      let _x.3 := Lean.Name.mkStr1 _x.2;
+      let _x.4 := @List.nil _;
+      let type := Lean.Expr.const._override _x.3 _x.4;
+      let _x.5 := "List";
+      let _x.6 := "nil";
+      let _x.7 := Lean.Name.mkStr2 _x.5 _x.6;
+      let _x.8 := Lean.Level.zero._impl;
+      let _x.9 := @List.nil _;
+      let _x.10 := @List.cons _ _x.8 _x.9;
+      let _x.11 := Lean.Expr.const._override _x.7 _x.10;
+      let nil := Lean.Expr.app._override _x.11 type;
+      let _x.12 := "cons";
+      let _x.13 := Lean.Name.mkStr2 _x.5 _x.12;
+      let _x.14 := Lean.Expr.const._override _x.13 _x.10;
+      let cons := Lean.Expr.app._override _x.14 type;
+      let _x.15 := 0;
+      let _x.16 := @List.nil _;
+      let _x.17 := @List.cons _ _x.15 _x.16;
+      let _x.18 := @Lean.List.toExprAux.0 _ _x.1 nil cons _x.17;
+      let _x.19 := Lean.MessageData.ofExpr _x.18;
+      return _x.19
+[Compiler.simp] size: 6
+    def _private.Lean.ToExpr.0.Lean.List.toExprAux._at_._eval.spec_0 nilFn consFn x.1 : Lean.Expr :=
+      cases x.1 : Lean.Expr
+      | List.nil =>
+        return nilFn
+      | List.cons head.2 tail.3 =>
+        let _x.4 := Lean.mkNatLit head.2;
+        let _x.5 := Lean.List.toExprAux._at_._eval.spec_0.0 nilFn consFn tail.3;
+        let _x.6 := Lean.mkAppB consFn _x.4 _x.5;
+        return _x.6
+[Compiler.simp] size: 21
+    def _eval : Lean.MessageData :=
+      let _x.1 := "Nat";
+      let _x.2 := Lean.Name.mkStr1 _x.1;
+      let _x.3 := @List.nil _;
+      let type := Lean.Expr.const._override _x.2 _x.3;
+      let _x.4 := "List";
+      let _x.5 := "nil";
+      let _x.6 := Lean.Name.mkStr2 _x.4 _x.5;
+      let _x.7 := Lean.Level.zero._impl;
+      let _x.8 := @List.nil _;
+      let _x.9 := @List.cons _ _x.7 _x.8;
+      let _x.10 := Lean.Expr.const._override _x.6 _x.9;
+      let nil := Lean.Expr.app._override _x.10 type;
+      let _x.11 := "cons";
+      let _x.12 := Lean.Name.mkStr2 _x.4 _x.11;
+      let _x.13 := Lean.Expr.const._override _x.12 _x.9;
+      let cons := Lean.Expr.app._override _x.13 type;
+      let _x.14 := 0;
+      let _x.15 := @List.nil _;
+      let _x.16 := @List.cons _ _x.14 _x.15;
+      let _x.17 := Lean.List.toExprAux._at_._eval.spec_0.0 nil cons _x.16;
+      let _x.18 := Lean.MessageData.ofExpr _x.17;
+      return _x.18
+[Compiler.simp] size: 6
+    def _private.Lean.ToExpr.0.Lean.List.toExprAux._at_._eval.spec_0 nilFn consFn x.1 : Lean.Expr :=
+      cases x.1 : Lean.Expr
+      | List.nil =>
+        return nilFn
+      | List.cons head.2 tail.3 =>
+        let _x.4 := Lean.mkNatLit head.2;
+        let _x.5 := Lean.List.toExprAux._at_._eval.spec_0.0 nilFn consFn tail.3;
+        let _x.6 := Lean.mkAppB consFn _x.4 _x.5;
+        return _x.6
+[Compiler.simp] size: 20
+    def _eval : Lean.MessageData :=
+      let _x.1 := "Nat";
+      let _x.2 := Lean.Name.mkStr1 _x.1;
+      let _x.3 := [] _;
+      let type := Lean.Expr.const._override _x.2 _x.3;
+      let _x.4 := "List";
+      let _x.5 := "nil";
+      let _x.6 := Lean.Name.mkStr2 _x.4 _x.5;
+      let _x.7 := Lean.Level.zero._impl;
+      let _x.8 := List.cons _ _x.7 _x.3;
+      let _x.9 := Lean.Expr.const._override _x.6 _x.8;
+      let nil := Lean.Expr.app._override _x.9 type;
+      let _x.10 := "cons";
+      let _x.11 := Lean.Name.mkStr2 _x.4 _x.10;
+      let _x.12 := Lean.Expr.const._override _x.11 _x.8;
+      let cons := Lean.Expr.app._override _x.12 type;
+      let _x.13 := 0;
+      let _x.14 := [] _;
+      let _x.15 := List.cons _ _x.13 _x.14;
+      let _x.16 := Lean.List.toExprAux._at_._eval.spec_0.0 nil cons _x.15;
+      let _x.17 := Lean.MessageData.ofExpr _x.16;
+      return _x.17
+[Compiler.simp] size: 6
+    def _private.Lean.ToExpr.0.Lean.List.toExprAux._at_._eval.spec_0 nilFn consFn x.1 : Lean.Expr :=
+      cases x.1 : Lean.Expr
+      | List.nil =>
+        return nilFn
+      | List.cons head.2 tail.3 =>
+        let _x.4 := Lean.mkNatLit head.2;
+        let _x.5 := Lean.List.toExprAux._at_._eval.spec_0.0 nilFn consFn tail.3;
+        let _x.6 := Lean.mkAppB consFn _x.4 _x.5;
+        return _x.6
+[Compiler.simp] size: 20
+    def _eval : Lean.MessageData :=
+      let _x.1 := "Nat";
+      let _x.2 := Lean.Name.mkStr1 _x.1;
+      let _x.3 := [] _;
+      let type := Lean.Expr.const._override _x.2 _x.3;
+      let _x.4 := "List";
+      let _x.5 := "nil";
+      let _x.6 := Lean.Name.mkStr2 _x.4 _x.5;
+      let _x.7 := Lean.Level.zero._impl;
+      let _x.8 := List.cons _ _x.7 _x.3;
+      let _x.9 := Lean.Expr.const._override _x.6 _x.8;
+      let nil := Lean.Expr.app._override _x.9 type;
+      let _x.10 := "cons";
+      let _x.11 := Lean.Name.mkStr2 _x.4 _x.10;
+      let _x.12 := Lean.Expr.const._override _x.11 _x.8;
+      let cons := Lean.Expr.app._override _x.12 type;
+      let _x.13 := 0;
+      let _x.14 := [] _;
+      let _x.15 := List.cons _ _x.13 _x.14;
+      let _x.16 := Lean.List.toExprAux._at_._eval.spec_0.0 nil cons _x.15;
+      let _x.17 := Lean.MessageData.ofExpr _x.16;
+      return _x.17
+[Compiler.simp] size: 6
+    def _private.Lean.ToExpr.0.Lean.List.toExprAux._at_._eval.spec_0 nilFn consFn x.1 : Lean.Expr :=
+      cases x.1 : Lean.Expr
+      | List.nil =>
+        return nilFn
+      | List.cons head.2 tail.3 =>
+        let _x.4 := Lean.mkNatLit head.2;
+        let _x.5 := Lean.List.toExprAux._at_._eval.spec_0.0 nilFn consFn tail.3;
+        let _x.6 := Lean.mkAppB consFn _x.4 _x.5;
+        return _x.6
+[Compiler.simp] size: 20
+    def _eval : Lean.MessageData :=
+      let _x.1 := "Nat";
+      let _x.2 := Lean.Name.mkStr1 _x.1;
+      let _x.3 := [] _;
+      let type := Lean.Expr.const._override _x.2 _x.3;
+      let _x.4 := "List";
+      let _x.5 := "nil";
+      let _x.6 := Lean.Name.mkStr2 _x.4 _x.5;
+      let _x.7 := Lean.Level.zero._impl;
+      let _x.8 := List.cons _ _x.7 _x.3;
+      let _x.9 := Lean.Expr.const._override _x.6 _x.8;
+      let nil := Lean.Expr.app._override _x.9 type;
+      let _x.10 := "cons";
+      let _x.11 := Lean.Name.mkStr2 _x.4 _x.10;
+      let _x.12 := Lean.Expr.const._override _x.11 _x.8;
+      let cons := Lean.Expr.app._override _x.12 type;
+      let _x.13 := 0;
+      let _x.14 := [] _;
+      let _x.15 := List.cons _ _x.13 _x.14;
+      let _x.16 := Lean.List.toExprAux._at_._eval.spec_0.0 nil cons _x.15;
+      let _x.17 := Lean.MessageData.ofExpr _x.16;
+      return _x.17
 -/
 #guard_msgs in
 #eval [0]

tests/lean/run/CompilerCSE.lean

@@ -27,6 +27,19 @@ info: [Compiler.test] Starting wrapper test cseSizeLeq for cse occurrence 0
 [Compiler.test] Wrapper test cseSizeLeq for cse occurrence 2 successful
 [Compiler.test] Starting post condition test cseFix for cse occurrence 2
 [Compiler.test] Post condition test cseFix for cse occurrence 2 successful
+---
+info: [Compiler.test] Starting wrapper test cseSizeLeq for cse occurrence 0
+[Compiler.test] Wrapper test cseSizeLeq for cse occurrence 0 successful
+[Compiler.test] Starting post condition test cseFix for cse occurrence 0
+[Compiler.test] Post condition test cseFix for cse occurrence 0 successful
+[Compiler.test] Starting wrapper test cseSizeLeq for cse occurrence 1
+[Compiler.test] Wrapper test cseSizeLeq for cse occurrence 1 successful
+[Compiler.test] Starting post condition test cseFix for cse occurrence 1
+[Compiler.test] Post condition test cseFix for cse occurrence 1 successful
+[Compiler.test] Starting wrapper test cseSizeLeq for cse occurrence 2
+[Compiler.test] Wrapper test cseSizeLeq for cse occurrence 2 successful
+[Compiler.test] Starting post condition test cseFix for cse occurrence 2
+[Compiler.test] Post condition test cseFix for cse occurrence 2 successful
 -/
 #guard_msgs in
 run_meta Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo]

tests/lean/run/CompilerFindJoinPoints.lean

@@ -19,6 +19,11 @@ info: [Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPo
 [Compiler.test] Wrapper test findJoinPointsSizeLeq for findJoinPoints occurrence 0 successful
 [Compiler.test] Starting post condition test findJoinPointsFix for findJoinPoints occurrence 0
 [Compiler.test] Post condition test findJoinPointsFix for findJoinPoints occurrence 0 successful
+---
+info: [Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPoints occurrence 0
+[Compiler.test] Wrapper test findJoinPointsSizeLeq for findJoinPoints occurrence 0 successful
+[Compiler.test] Starting post condition test findJoinPointsFix for findJoinPoints occurrence 0
+[Compiler.test] Post condition test findJoinPointsFix for findJoinPoints occurrence 0 successful
 -/
 #guard_msgs in
 run_meta Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo, ``Lean.MetavarContext.MkBinding.collectForwardDeps]

tests/lean/run/CompilerFloatLetIn.lean

@@ -22,6 +22,13 @@ info: [Compiler.test] Starting wrapper test floatLetInSizeEq for floatLetIn occu
 [Compiler.test] Wrapper test floatLetInSizeEq for floatLetIn occurrence 1 successful
 [Compiler.test] Starting wrapper test floatLetInSizeEq for floatLetIn occurrence 2
 [Compiler.test] Wrapper test floatLetInSizeEq for floatLetIn occurrence 2 successful
+---
+info: [Compiler.test] Starting wrapper test floatLetInSizeEq for floatLetIn occurrence 0
+[Compiler.test] Wrapper test floatLetInSizeEq for floatLetIn occurrence 0 successful
+[Compiler.test] Starting wrapper test floatLetInSizeEq for floatLetIn occurrence 1
+[Compiler.test] Wrapper test floatLetInSizeEq for floatLetIn occurrence 1 successful
+[Compiler.test] Starting wrapper test floatLetInSizeEq for floatLetIn occurrence 2
+[Compiler.test] Wrapper test floatLetInSizeEq for floatLetIn occurrence 2 successful
 -/
 #guard_msgs in
 run_meta Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo]

tests/lean/run/CompilerProbe.lean

@@ -5,7 +5,40 @@ open Lean.Compiler.LCNF
 -- Note: 2024-05-15: At the time of adding #guard_msgs here, the tests seem to all be failing.
 
 -- Find functions that have jps which take a lambda
-/-- info: #[] -/
+/-- info: #["_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.elimMVar",
+  "Array.foldlMUnsafe.fold._at_._private.Lean.Data.PersistentArray.0.Lean.PersistentArray.foldlMAux._at_._private.Lean.Data.PersistentArray.0.Lean.PersistentArray.foldlFromMAux._at_.Lean.PersistentArray.foldlM._at_.Lean.LocalContext.foldlM._at_.Lean.MetavarContext.MkBinding.collectForwardDeps.spec_3.spec_3.spec_3.spec_3.spec_4._redArg",
+  "Lean.MessageData.formatAux",
+  "_private.Lean.Data.Lsp.Diagnostics.0.Lean.Lsp.DiagnosticWith.ordUserVisible._redArg._@.Lean.Data.Lsp.Diagnostics._hyg.2056",
+  "IO.FS.withIsolatedStreams._at_.Lean.Core.wrapAsyncAsSnapshot.spec_28._redArg",
+  "IO.FS.withIsolatedStreams._at_.Lean.Meta.realizeConst.realizeAndReport.spec_10._redArg",
+  "Lean.Meta.withRestoreOrSaveFull._redArg", "Lean.addDecl", "Lean.IR.EmitC.emitDeclAux",
+  "Lean.computeStructureResolutionOrder.selectParent._redArg._lam_6",
+  "Lean.computeStructureResolutionOrder._redArg._lam_16", "Lean.Meta.evalNat",
+  "_private.Lean.Meta.WHNF.0.Lean.Meta.toCtorWhenK", "Lean.IR.ToIR.lowerLetValue",
+  "Lean.Compiler.LCNF.toMonoType.visitApp", "Lean.Compiler.LCNF.Simp.inlineApp?", "Lean.Compiler.LCNF.Simp.simp",
+  "Lean.Compiler.LCNF.Specialize.specializeApp?", "Lean.Compiler.LCNF.Decl.reduceArity",
+  "Lean.Compiler.LCNF.UnreachableBranches.Value.getLiteral.go", "Lean.Parser.registerBuiltinParserAttribute",
+  "Lean.Elab.elabTerminationHints._redArg._lam_3", "Lean.Elab.Term.isLetRecAuxMVar",
+  "Lean.Elab.mkDeclName._at_.Lean.Elab.expandDeclId._at_.Lean.Elab.Term.expandDeclId.spec_0.spec_1._lam_3",
+  "_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabForallBinders",
+  "Lean.PrettyPrinter.Delaborator.delabAppExplicitCore._lam_2", "Lean.PrettyPrinter.Delaborator.delabLetFun._lam_1",
+  "Lean.PrettyPrinter.Delaborator.delabAppImplicitCore", "Lean.Elab.Tactic.withRestoreOrSaveFull._redArg",
+  "Lean.Elab.Tactic.evalTactic.expandEval._lam_2",
+  "Lean.Elab.Term.withNarrowedTacticReuse._at_.Lean.Elab.Term.withNarrowedArgTacticReuse._at_.Lean.Elab.Term.runTactic.spec_9.spec_9._redArg",
+  "_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.resumePostponed._lam_1",
+  "Lean.Elab.Command.elabCommandTopLevel._lam_3",
+  "IO.FS.withIsolatedStreams._at_.Lean.Elab.Command.wrapAsyncAsSnapshot.spec_9._redArg",
+  "Lean.Elab.Term.ElabElim.finalize", "_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.finalize",
+  "_private.Lean.Elab.App.0.Lean.Elab.Term.resolveDotName.go", "Lean.Elab.Command.elabSyntax",
+  "Lean.Meta.mkCongrSimpCore?.mk?.go", "Lean.Linter.MissingDocs.initFn._lam_2._@.Lean.Linter.MissingDocs._hyg.802",
+  "Lean.Elab.elabTerminationHints._at_._private.Lean.Elab.LetRec.0.Lean.Elab.Term.mkLetRecDeclView.spec_4._lam_2",
+  "Lean.Language.Lean.process.doElab", "Lean.Language.Lean.processCommands",
+  "IO.FS.withIsolatedStreams._at_.Lean.Language.Lean.process.doElab.spec_0._redArg",
+  "Lean.Language.Lean.process.parseCmd", "Lean.Elab.Term.elabSubst._lam_6",
+  "Lean.Meta.Simp.Arith.Nat.ToLinear.toLinearExpr",
+  "Array.forIn'Unsafe.loop._at_.Array.forIn'Unsafe.loop._at_.Lean.Meta.Simp.trySimpCongrTheorem?.spec_0.spec_0",
+  "Lean.Meta.Simp.simpForall", "Array.forIn'Unsafe.loop._at_.Lean.Meta.Simp.trySimpCongrTheorem?.spec_0", ⋯]
+-/
 #guard_msgs in
 #eval
   Probe.runGlobally (phase := .mono) <|
@@ -24,21 +57,20 @@ def lambdaCounter : Probe Decl Nat :=
   Probe.count
 
 -- Run everywhere
-/-- info: #[0] -/
-#guard_msgs in
-#eval
-  Probe.runGlobally (phase := .mono) <|
-  lambdaCounter
+#eval do
+  let probeResult ← Probe.runGlobally (phase := .mono) <| lambdaCounter
+  let #[numLiftedFunctions] := probeResult | panic! "unexpected probe result"
+  assert! numLiftedFunctions ≥ 7000
 
 -- Run limited
-/-- info: #[0] -/
+/-- info: #[18] -/
 #guard_msgs in
 #eval
   Probe.runOnModule `Lean.Compiler.LCNF.JoinPoints (phase := .mono) <|
   lambdaCounter
 
 -- Find most commonly used function with threshold
-/-- info: #[] -/
+/-- info: #[("USize.ofNat", 111), ("EStateM.Result.ok", 141)] -/
 #guard_msgs in
 #eval
   Probe.runOnModule `Lean.Compiler.LCNF.JoinPoints (phase := .mono) <|

tests/lean/run/CompilerPullInstances.lean

@@ -19,6 +19,11 @@ info: [Compiler.test] Starting wrapper test pullInstancesSizeEq for pullInstance
 [Compiler.test] Wrapper test pullInstancesSizeEq for pullInstances occurrence 0 successful
 [Compiler.test] Starting post condition test pullInstancesFix for pullInstances occurrence 0
 [Compiler.test] Post condition test pullInstancesFix for pullInstances occurrence 0 successful
+---
+info: [Compiler.test] Starting wrapper test pullInstancesSizeEq for pullInstances occurrence 0
+[Compiler.test] Wrapper test pullInstancesSizeEq for pullInstances occurrence 0 successful
+[Compiler.test] Starting post condition test pullInstancesFix for pullInstances occurrence 0
+[Compiler.test] Post condition test pullInstancesFix for pullInstances occurrence 0 successful
 -/
 #guard_msgs in
 run_meta Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo]

tests/lean/run/CompilerSimp.lean

@@ -39,6 +39,30 @@ info: [Compiler.test] Starting post condition test simpInlinesBinds for simp occ
 [Compiler.test] Post condition test simpInlinesBinds for simp occurrence 5 successful
 [Compiler.test] Starting post condition test simpFix for simp occurrence 5
 [Compiler.test] Post condition test simpFix for simp occurrence 5 successful
--/
+---
+info: [Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 0
+[Compiler.test] Post condition test simpInlinesBinds for simp occurrence 0 successful
+[Compiler.test] Starting post condition test simpFix for simp occurrence 0
+[Compiler.test] Post condition test simpFix for simp occurrence 0 successful
+[Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 1
+[Compiler.test] Post condition test simpInlinesBinds for simp occurrence 1 successful
+[Compiler.test] Starting post condition test simpFix for simp occurrence 1
+[Compiler.test] Post condition test simpFix for simp occurrence 1 successful
+[Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 2
+[Compiler.test] Post condition test simpInlinesBinds for simp occurrence 2 successful
+[Compiler.test] Starting post condition test simpFix for simp occurrence 2
+[Compiler.test] Post condition test simpFix for simp occurrence 2 successful
+[Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 3
+[Compiler.test] Post condition test simpInlinesBinds for simp occurrence 3 successful
+[Compiler.test] Starting post condition test simpFix for simp occurrence 3
+[Compiler.test] Post condition test simpFix for simp occurrence 3 successful
+[Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 4
+[Compiler.test] Post condition test simpInlinesBinds for simp occurrence 4 successful
+[Compiler.test] Starting post condition test simpFix for simp occurrence 4
+[Compiler.test] Post condition test simpFix for simp occurrence 4 successful
+[Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 5
+[Compiler.test] Post condition test simpInlinesBinds for simp occurrence 5 successful
+[Compiler.test] Starting post condition test simpFix for simp occurrence 5
+[Compiler.test] Post condition test simpFix for simp occurrence 5 successful-/
 #guard_msgs in
 run_meta Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo]

tests/lean/run/emptyLcnf.lean

@@ -10,6 +10,27 @@ set_option trace.Compiler.result true
 info: [Compiler.result] size: 0
     def f x : Nat :=
       ⊥
+---
+info: [Compiler.result] size: 5
+    def _eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EStateM.Result Lean.Exception PUnit PUnit :=
+      let _x.10 := Lean.Compiler.compile _x.1 _y.7 _y.8 _y.9;
+      cases _x.10 : EStateM.Result Lean.Exception PUnit PUnit
+      | EStateM.Result.ok a.11 a.12 =>
+        let _x.13 := EStateM.Result.ok _ _ _ _x.2 a.12;
+        return _x.13
+      | EStateM.Result.error a.14 a.15 =>
+        return _x.10
+[Compiler.result] size: 8
+    def _eval a.1 a.2 a.3 : EStateM.Result Lean.Exception PUnit PUnit :=
+      let _x.4 := "f";
+      let _x.5 := Lean.Name.mkStr1 _x.4;
+      let _x.6 := 1;
+      let _x.7 := Array.mkEmpty ◾ _x.6;
+      let _x.8 := Array.push ◾ _x.7 _x.5;
+      let _x.9 := PUnit.unit;
+      let _f.10 := _eval._lam_0 _x.8 _x.9;
+      let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
+      return _x.11
 -/
 #guard_msgs in
 run_meta Lean.Compiler.compile #[``f]

tests/lean/run/erased.lean

@@ -21,9 +21,39 @@ set_option pp.letVarTypes true
 set_option trace.Compiler.result true
 /--
 info: [Compiler.result] size: 1
-    def Erased.mk (α : lcErased) (a : lcAny) : PSigma lcErased lcErased :=
-      let _x.1 : PSigma lcErased lcErased := PSigma.mk lcErased ◾ ◾ ◾;
+    def Erased.mk (α : lcErased) (a : lcAny) : PSigma lcErased lcAny :=
+      let _x.1 : PSigma lcErased lcAny := PSigma.mk lcErased ◾ ◾ ◾;
       return _x.1
+---
+info: [Compiler.result] size: 5
+    def _eval._lam_0 (_x.1 : Array
+       Lean.Name) (_x.2 : PUnit) (_y.3 : Lean.Elab.Term.Context) (_y.4 : lcAny) (_y.5 : Lean.Meta.Context) (_y.6 : lcAny) (_y.7 : Lean.Core.Context) (_y.8 : lcAny) (_y.9 : PUnit) : EStateM.Result
+      Lean.Exception PUnit PUnit :=
+      let _x.10 : EStateM.Result Lean.Exception PUnit PUnit := compile _x.1 _y.7 _y.8 _y.9;
+      cases _x.10 : EStateM.Result Lean.Exception PUnit PUnit
+      | EStateM.Result.ok (a.11 : PUnit) (a.12 : PUnit) =>
+        let _x.13 : EStateM.Result Lean.Exception PUnit PUnit := EStateM.Result.ok Lean.Exception PUnit PUnit _x.2 a.12;
+        return _x.13
+      | EStateM.Result.error (a.14 : Lean.Exception) (a.15 : PUnit) =>
+        return _x.10
+[Compiler.result] size: 9
+    def _eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : PUnit) : EStateM.Result Lean.Exception PUnit
+      PUnit :=
+      let _x.4 : String := "Erased";
+      let _x.5 : String := "mk";
+      let _x.6 : Lean.Name := Lean.Name.mkStr2 _x.4 _x.5;
+      let _x.7 : Nat := 1;
+      let _x.8 : Array Lean.Name := Array.mkEmpty ◾ _x.7;
+      let _x.9 : Array Lean.Name := Array.push ◾ _x.8 _x.6;
+      let _x.10 : PUnit := PUnit.unit;
+      let _f.11 : Lean.Elab.Term.Context →
+        lcAny →
+          Lean.Meta.Context →
+            lcAny →
+              Lean.Core.Context → lcAny → PUnit → EStateM.Result Lean.Exception PUnit PUnit := _eval._lam_0 _x.9 _x.10;
+      let _x.12 : EStateM.Result Lean.Exception PUnit
+        lcAny := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 a.3;
+      return _x.12
 -/
 #guard_msgs in
 run_meta Lean.Compiler.compile #[``Erased.mk]

tests/lean/run/isDefEqProjIssue.lean

@@ -83,7 +83,7 @@ instance g (x : Nat) : Foo :=
   { x, y := ack 10 11 }
 
 open Lean Meta
-set_option maxHeartbeats 400 in
+set_option maxHeartbeats 800 in
 run_meta do
   withLocalDeclD `x (mkConst ``Nat) fun x => do
     let lhs := Expr.proj ``Foo 0 <| mkApp (mkConst ``f) x

tests/lean/sint_basic.lean.expected.out

@@ -72,16 +72,15 @@ true
 true
 true
 true
-
-[result]
-def myId8 (x_1 : u8) : u8 :=
-  ret x_1
-def myId8._boxed (x_1 : obj) : obj :=
-  let x_2 : u8 := unbox x_1;
-  dec x_1;
-  let x_3 : u8 := myId8 x_2;
-  let x_4 : obj := box x_3;
-  ret x_4
+[Compiler.IR] [result]
+    def myId8 (x_1 : u8) : u8 :=
+      ret x_1
+    def myId8._boxed (x_1 : obj) : obj :=
+      let x_2 : u8 := unbox x_1;
+      dec x_1;
+      let x_3 : u8 := myId8 x_2;
+      let x_4 : obj := box x_3;
+      ret x_4
 Int16 : Type
 20
 -20
@@ -156,16 +155,15 @@ true
 true
 true
 true
-
-[result]
-def myId16 (x_1 : u16) : u16 :=
-  ret x_1
-def myId16._boxed (x_1 : obj) : obj :=
-  let x_2 : u16 := unbox x_1;
-  dec x_1;
-  let x_3 : u16 := myId16 x_2;
-  let x_4 : obj := box x_3;
-  ret x_4
+[Compiler.IR] [result]
+    def myId16 (x_1 : u16) : u16 :=
+      ret x_1
+    def myId16._boxed (x_1 : obj) : obj :=
+      let x_2 : u16 := unbox x_1;
+      dec x_1;
+      let x_3 : u16 := myId16 x_2;
+      let x_4 : obj := box x_3;
+      ret x_4
 Int32 : Type
 20
 -20
@@ -240,16 +238,15 @@ true
 true
 true
 true
-
-[result]
-def myId32 (x_1 : u32) : u32 :=
-  ret x_1
-def myId32._boxed (x_1 : obj) : obj :=
-  let x_2 : u32 := unbox x_1;
-  dec x_1;
-  let x_3 : u32 := myId32 x_2;
-  let x_4 : obj := box x_3;
-  ret x_4
+[Compiler.IR] [result]
+    def myId32 (x_1 : u32) : u32 :=
+      ret x_1
+    def myId32._boxed (x_1 : obj) : obj :=
+      let x_2 : u32 := unbox x_1;
+      dec x_1;
+      let x_3 : u32 := myId32 x_2;
+      let x_4 : obj := box x_3;
+      ret x_4
 Int64 : Type
 20
 -20
@@ -324,16 +321,15 @@ true
 true
 true
 true
-
-[result]
-def myId64 (x_1 : u64) : u64 :=
-  ret x_1
-def myId64._boxed (x_1 : obj) : obj :=
-  let x_2 : u64 := unbox x_1;
-  dec x_1;
-  let x_3 : u64 := myId64 x_2;
-  let x_4 : obj := box x_3;
-  ret x_4
+[Compiler.IR] [result]
+    def myId64 (x_1 : u64) : u64 :=
+      ret x_1
+    def myId64._boxed (x_1 : obj) : obj :=
+      let x_2 : u64 := unbox x_1;
+      dec x_1;
+      let x_3 : u64 := myId64 x_2;
+      let x_4 : obj := box x_3;
+      ret x_4
 ISize : Type
 20
 -20
@@ -408,13 +404,12 @@ true
 true
 true
 true
-
-[result]
-def myIdSize (x_1 : usize) : usize :=
-  ret x_1
-def myIdSize._boxed (x_1 : obj) : obj :=
-  let x_2 : usize := unbox x_1;
-  dec x_1;
-  let x_3 : usize := myIdSize x_2;
-  let x_4 : obj := box x_3;
-  ret x_4
+[Compiler.IR] [result]
+    def myIdSize (x_1 : usize) : usize :=
+      ret x_1
+    def myIdSize._boxed (x_1 : obj) : obj :=
+      let x_2 : usize := unbox x_1;
+      dec x_1;
+      let x_3 : usize := myIdSize x_2;
+      let x_4 : obj := box x_3;
+      ret x_4

tests/lean/unboxStruct.lean.expected.out

@@ -1,10 +1,9 @@
-
-[result]
-def test2 (x_1 : u32) (x_2 : obj) : obj :=
-  let x_3 : obj := foo x_1 x_2;
-  ret x_3
-def test2._boxed (x_1 : obj) (x_2 : obj) : obj :=
-  let x_3 : u32 := unbox x_1;
-  dec x_1;
-  let x_4 : obj := test2 x_3 x_2;
-  ret x_4
+[Compiler.IR] [result]
+    def test2 (x_1 : u32) (x_2 : obj) : obj :=
+      let x_3 : obj := foo x_1 x_2;
+      ret x_3
+    def test2._boxed (x_1 : obj) (x_2 : obj) : obj :=
+      let x_3 : u32 := unbox x_1;
+      dec x_1;
+      let x_4 : obj := test2 x_3 x_2;
+      ret x_4

tests/lean/unhygienicCode.lean.expected.out

@@ -0,0 +1,23 @@
+[Compiler.result] size: 20
+    def foo n : Syntax :=
+      let _x.1 := Syntax.missing;
+      let _x.2 := 1;
+      let _x.3 := false;
+      let _x.4 := @SourceInfo.fromRef _x.1 _x.3;
+      let _x.5 := "UnhygienicMain";
+      let _x.6 := Name.mkStr1 _x.5;
+      let _x.7 := "term_+_";
+      let _x.8 := Name.mkStr1 _x.7;
+      let _x.9 := "a";
+      let _x.10 := String.toSubstring' _x.9;
+      let _x.11 := Name.mkStr1 _x.9;
+      let _x.12 := addMacroScope _x.6 _x.11 _x.2;
+      let _x.13 := [] _;
+      let _x.14 := Syntax.ident _x.4 _x.10 _x.12 _x.13;
+      let _x.15 := "+";
+      let _x.16 := Syntax.atom _x.4 _x.15;
+      let _x.17 := Nat.reprFast.0 n;
+      let _x.18 := SourceInfo.none;
+      let _x.19 := @Syntax.mkNumLit _x.17 _x.18;
+      let _x.20 := Syntax.node3 _x.4 _x.8 _x.14 _x.16 _x.19;
+      return _x.20

tests/lean/updateExprIssue.lean.expected.out

@@ -1,45 +1,26 @@
-
-[init]
-def sefFn (x_1 : obj) (x_2 : obj) : obj :=
-  case x_1 : obj of
-  Lean.Expr.bvar._impl →
-    ret x_1
-  Lean.Expr.fvar._impl →
-    ret x_1
-  Lean.Expr.mvar._impl →
-    ret x_1
-  Lean.Expr.sort._impl →
-    ret x_1
-  Lean.Expr.const._impl →
-    ret x_1
-  Lean.Expr.app._impl →
-    let x_3 : obj := proj[0] x_1;
-    let x_4 : obj := proj[1] x_1;
-    let x_5 : usize := ptrAddrUnsafe ◾ x_3;
-    let x_6 : usize := ptrAddrUnsafe ◾ x_2;
-    let x_7 : u8 := USize.decEq x_5 x_6;
-    case x_7 : obj of
-    Bool.false →
-      let x_8 : obj := Lean.Expr.app._override x_2 x_4;
-      ret x_8
-    Bool.true →
-      let x_9 : usize := ptrAddrUnsafe ◾ x_4;
-      let x_10 : u8 := USize.decEq x_9 x_9;
-      case x_10 : obj of
-      Bool.false →
-        let x_11 : obj := Lean.Expr.app._override x_2 x_4;
-        ret x_11
-      Bool.true →
+[Compiler.IR] [init]
+    def sefFn (x_1 : obj) (x_2 : obj) : obj :=
+      case x_1 : obj of
+      Lean.Expr.app._impl →
+        let x_3 : u64 := sproj[2, 0] x_1;
+        let x_4 : obj := proj[0] x_1;
+        let x_5 : obj := proj[1] x_1;
+        block_6 (x_7 : u8) :=
+          case x_7 : obj of
+          Bool.false →
+            let x_8 : obj := Lean.Expr.app._override x_2 x_5;
+            ret x_8
+          Bool.true →
+            ret x_1;
+        let x_9 : usize := ptrAddrUnsafe ◾ x_4;
+        let x_10 : usize := ptrAddrUnsafe ◾ x_2;
+        let x_11 : u8 := USize.decEq x_9 x_10;
+        case x_11 : obj of
+        Bool.false →
+          jmp block_6 x_11
+        Bool.true →
+          let x_12 : usize := ptrAddrUnsafe ◾ x_5;
+          let x_13 : u8 := USize.decEq x_12 x_12;
+          jmp block_6 x_13
+      default →
         ret x_1
-  Lean.Expr.lam._impl →
-    ret x_1
-  Lean.Expr.forallE._impl →
-    ret x_1
-  Lean.Expr.letE._impl →
-    ret x_1
-  Lean.Expr.lit._impl →
-    ret x_1
-  Lean.Expr.mdata._impl →
-    ret x_1
-  Lean.Expr.proj._impl →
-    ret x_1