final tweaks

src/Lean/Compiler/IR/AddExtern.lean

@@ -9,6 +9,9 @@ module
 prelude
 public import Lean.Compiler.IR.Boxing
 import Lean.Compiler.IR.RC
+import Lean.Compiler.LCNF.ToImpureType
+import Lean.Compiler.LCNF.ToImpure
+import Lean.Compiler.LCNF.ToImpureType
 
 public section
 
@@ -16,23 +19,60 @@ namespace Lean.IR
 
 @[export lean_add_extern]
 def addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit := do
-  let mut type ← Compiler.LCNF.getOtherDeclMonoType declName
-  let mut params := #[]
-  let mut nextVarIndex := 0
-  repeat
-    let .forallE _ d b _ := type | break
-    let borrow := isMarkedBorrowed d
-    let ty ← toIRType d
-    params := params.push { x := ⟨nextVarIndex⟩, borrow, ty }
-    type := b
-    nextVarIndex := nextVarIndex + 1
-  let irType ← toIRType type
-  let decls := #[.extern declName params irType externAttrData]
   if !isPrivateName declName then
     modifyEnv (Compiler.LCNF.setDeclPublic · declName)
-  let decls := ExplicitBoxing.addBoxedVersions (← Lean.getEnv) decls
-  let decls ← explicitRC decls
-  logDecls `result decls
-  addDecls decls
+  let monoDecl ← addMono declName
+  let impureDecl ← addImpure monoDecl
+  addIr impureDecl
+where
+  addMono (declName : Name) : CoreM (Compiler.LCNF.Decl .pure) := do
+    let type ← Compiler.LCNF.getOtherDeclMonoType declName
+    let mut typeIter := type
+    let mut params := #[]
+    repeat
+      let .forallE binderName ty b _ := typeIter | break
+      let borrow := isMarkedBorrowed ty
+      params := params.push {
+        fvarId := (← mkFreshFVarId)
+        type := ty,
+        binderName,
+        borrow
+      }
+      typeIter := b
+    let decl := {
+      name := declName,
+      levelParams := [],
+      value := .extern externAttrData,
+      inlineAttr? := some .noinline,
+      type,
+      params,
+    }
+    decl.saveMono
+    return decl
+
+  addImpure (decl : Compiler.LCNF.Decl .pure) : CoreM (Compiler.LCNF.Decl .impure) := do
+    let type ← Compiler.LCNF.lowerResultType decl.type decl.params.size
+    let params ← decl.params.mapM fun param =>
+      return { param with type := ← Compiler.LCNF.toImpureType param.type }
+    let decl := {
+      name := decl.name,
+      levelParams := decl.levelParams,
+      value := .extern externAttrData
+      inlineAttr? := some .noinline,
+      type,
+      params
+    }
+    decl.saveImpure
+    return decl
+
+  addIr (decl : Compiler.LCNF.Decl .impure) : CoreM Unit := do
+    let params := decl.params.mapIdx fun idx param =>
+      { x := ⟨idx⟩, borrow := param.borrow, ty := toIRType param.type  }
+    let type := toIRType decl.type
+    let decls := #[.extern declName params type externAttrData]
+    let decls := ExplicitBoxing.addBoxedVersions (← Lean.getEnv) decls
+    let decls ← explicitRC decls
+    logDecls `result decls
+    addDecls decls
 
 end Lean.IR

src/Lean/Compiler/IR/ToIR.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Lean.Compiler.IR.CompilerM
-public import Lean.Compiler.IR.ToIRType
+import Lean.Compiler.IR.ToIRType
 
 public section
 
@@ -15,48 +15,22 @@ namespace Lean.IR
 
 open Lean.Compiler (LCNF.Alt LCNF.Arg LCNF.Code LCNF.Decl LCNF.DeclValue LCNF.LCtx LCNF.LetDecl
   LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.getMonoDecl? LCNF.FVarSubst LCNF.MonadFVarSubst
-  LCNF.MonadFVarSubstState LCNF.addSubst LCNF.normLetValue LCNF.normFVar)
+  LCNF.MonadFVarSubstState LCNF.addSubst LCNF.normLetValue LCNF.normFVar LCNF.getType LCNF.CtorInfo)
 
 namespace ToIR
 
-/--
-Marks an extern definition to be guaranteed to always return tagged values.
-This information is used to optimize reference counting in the compiler.
--/
-@[builtin_doc]
-builtin_initialize taggedReturnAttr : TagAttribute ←
-  registerTagAttribute `tagged_return "mark extern definition to always return tagged values"
-
 structure BuilderState where
   vars : Std.HashMap FVarId Arg := {}
   joinPoints : Std.HashMap FVarId JoinPointId := {}
   nextId : Nat := 1
-  /--
-  We keep around a substitution here because we run a second trivial structure elimination when
-  converting to IR. This elimination is aware of the fact that `Void` is irrelevant while the first
-  one in LCNF isn't because LCNF is still pure. However, IR does not allow us to have bindings of
-  the form `let x := y` which might occur when for example projecting out of a trivial structure
-  where previously a binding would've been `let x := proj y i` and now becomes `let x := y`.
-  For this reason we carry around these kinds of bindings in this substitution and apply it whenever
-  we access an fvar in the conversion.
-  -/
-  subst : LCNF.FVarSubst .pure := {}
 
 abbrev M := StateRefT BuilderState CoreM
 
-instance : LCNF.MonadFVarSubst M .pure false where
-  getSubst := return (← get).subst
-
-instance : LCNF.MonadFVarSubstState M .pure where
-  modifySubst f := modify fun s => { s with subst := f s.subst }
-
 def M.run (x : M α) : CoreM α := do
   x.run' {}
 
 def getFVarValue (fvarId : FVarId) : M Arg := do
-  match ← LCNF.normFVar fvarId with
-  | .fvar fvarId => return (← get).vars.get! fvarId
-  | .erased => return .erased
+  return (← get).vars.get! fvarId
 
 def getJoinPointValue (fvarId : FVarId) : M JoinPointId := do
   return (← get).joinPoints.get! fvarId
@@ -67,14 +41,6 @@ def bindVar (fvarId : FVarId) : M VarId := do
     ⟨varId, { s with vars := s.vars.insertIfNew fvarId (.var varId),
                      nextId := s.nextId + 1 }⟩
 
-def bindVarToVarId (fvarId : FVarId) (varId : VarId) : M Unit := do
-  modify fun s => { s with vars := s.vars.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 }
@@ -84,9 +50,6 @@ def bindJoinPoint (fvarId : FVarId) : M JoinPointId := do
 def bindErased (fvarId : FVarId) : M Unit := do
   modify fun s => { s with vars := s.vars.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 d
 
@@ -102,34 +65,22 @@ def lowerLitValue (v : LCNF.LitValue) : LitVal × IRType :=
   | .uint64 v => ⟨.num (UInt64.toNat v), .uint64⟩
   | .usize v => ⟨.num (UInt64.toNat v), .usize⟩
 
-def lowerArg (a : LCNF.Arg .pure) : M Arg := do
+def lowerArg (a : LCNF.Arg .impure) : M Arg := do
   match a with
   | .fvar fvarId => getFVarValue fvarId
-  | .erased | .type .. => return .erased
+  | .erased => return .erased
 
-inductive TranslatedProj where
-  | expr (e : Expr)
-  | erased
-  deriving Inhabited
-
-def lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo)
-    : TranslatedProj × IRType :=
-  match field with
-  | .object i irType => ⟨.expr (.proj i base), irType⟩
-  | .usize i => ⟨.expr (.uproj i base), .usize⟩
-  | .scalar _ offset irType => ⟨.expr (.sproj (ctorInfo.size + ctorInfo.usize) offset base), irType⟩
-  | .erased => ⟨.erased, .erased⟩
-  | .void => ⟨.erased, .void⟩
-
-def lowerParam (p : LCNF.Param .pure) : M Param := do
+def lowerParam (p : LCNF.Param .impure) : M Param := do
   let x ← bindVar p.fvarId
-  let ty ← toIRType p.type
-  if ty.isVoid || ty.isErased then
-    Compiler.LCNF.addSubst p.fvarId (.erased : LCNF.Arg .pure)
+  let ty := toIRType p.type
   return { x, borrow := p.borrow, ty }
 
+@[inline]
+def lowerCtorInfo (i : LCNF.CtorInfo) : CtorInfo :=
+  ⟨i.name, i.cidx, i.size, i.usize, i.ssize⟩
+
 mutual
-partial def lowerCode (c : LCNF.Code .pure) : M FnBody := do
+partial def lowerCode (c : LCNF.Code .impure) : M FnBody := do
   match c with
   | .let decl k => lowerLet decl k
   | .jp decl k =>
@@ -141,222 +92,75 @@ partial def lowerCode (c : LCNF.Code .pure) : M FnBody := do
     let joinPointId ← getJoinPointValue fvarId
     return .jmp joinPointId (← args.mapM lowerArg)
   | .cases cases =>
-    if let some info ← hasTrivialStructure? cases.typeName then
-      assert! cases.alts.size == 1
-      let .alt ctorName ps k := cases.alts[0]! | unreachable!
-      assert! ctorName == info.ctorName
-      assert! info.fieldIdx < ps.size
-      for idx in 0...ps.size do
-        let p := ps[idx]!
-        if idx == info.fieldIdx then
-          LCNF.addSubst p.fvarId (.fvar cases.discr : LCNF.Arg .pure)
-        else
-          bindErased p.fvarId
-      lowerCode k
-    else
-      -- `casesOn` for inductive predicates should have already been expanded.
-      let .var varId := (← getFVarValue cases.discr) | unreachable!
-      return .case cases.typeName
-                   varId
-                   (← nameToIRType cases.typeName)
-                   (← cases.alts.mapM (lowerAlt varId))
+    let .var varId := (← getFVarValue cases.discr) | unreachable!
+    return .case cases.typeName
+                 varId
+                 (nameToIRType cases.typeName)
+                 (← cases.alts.mapM (lowerAlt))
   | .return fvarId =>
-    return .ret (← getFVarValue fvarId)
+    let ret ← getFVarValue fvarId
+    return .ret ret
   | .unreach .. => return .unreachable
+  | .sset var i offset y type k _ =>
+    let .var y ← getFVarValue y | unreachable!
+    let .var var ← getFVarValue var | unreachable!
+    return .sset var i offset y (toIRType type) (← lowerCode k)
+  | .uset var i y k _ =>
+    let .var y ← getFVarValue y | unreachable!
+    let .var var ← getFVarValue var | unreachable!
+    return .uset var i y (← lowerCode k)
   | .fun .. => panic! "all local functions should be λ-lifted"
 
-partial def lowerLet (decl : LCNF.LetDecl .pure) (k : LCNF.Code .pure) : M FnBody := do
-  let value ← LCNF.normLetValue decl.value
-  match value with
+partial def lowerLet (decl : LCNF.LetDecl .impure) (k : LCNF.Code .impure) : M FnBody := do
+  let type := toIRType decl.type
+  let continueLet (e : Expr) : M FnBody := do
+    let letVar ← bindVar decl.fvarId
+    return .vdecl letVar type e (← lowerCode k)
+  match decl.value with
   | .lit litValue =>
-    let var ← bindVar decl.fvarId
-    let ⟨litValue, type⟩ := lowerLitValue litValue
-    return .vdecl var type (.lit litValue) (← lowerCode k)
-  | .proj typeName i fvarId =>
-    if let some info ← hasTrivialStructure? typeName then
-      if info.fieldIdx == i then
-        LCNF.addSubst decl.fvarId (.fvar fvarId : LCNF.Arg .pure)
-      else
-        bindErased decl.fvarId
-      lowerCode k
-    else
-      match (← getFVarValue fvarId) with
-      | .var varId =>
-        let some (.inductInfo { ctors := [ctorName], .. }) := (← Lean.getEnv).find? typeName
-          | panic! "projection of non-structure type"
-        let ⟨ctorInfo, fields⟩ ← getCtorLayout ctorName
-        let ⟨result, type⟩ := lowerProj varId ctorInfo fields[i]!
-        match result with
-        | .expr e =>
-          let var ← bindVar decl.fvarId
-          return .vdecl var type e (← lowerCode k)
-        | .erased =>
-          bindErased decl.fvarId
-          lowerCode k
-      | .erased =>
-        bindErased decl.fvarId
-        lowerCode k
-  | .const name _ args =>
-    let irArgs ← args.mapM lowerArg
-    if let some decl ← findDecl name then
-      return (← mkApplication name decl.params.size irArgs)
-    if let some decl ← LCNF.getMonoDecl? name then
-      return (← mkApplication name decl.params.size irArgs)
-    let env ← Lean.getEnv
-    match env.find? name with
-    | some (.ctorInfo ctorVal) =>
-      if let some info ← hasTrivialStructure? ctorVal.induct then
-        let arg := args[info.numParams + info.fieldIdx]!
-        LCNF.addSubst decl.fvarId arg
-        lowerCode k
-      else
-        let type ← nameToIRType ctorVal.induct
-        if type.isScalar then
-          let var ← bindVar decl.fvarId
-          return .vdecl var type (.lit (.num ctorVal.cidx)) (← lowerCode k)
-
-        let ⟨ctorInfo, fields⟩ ← getCtorLayout name
-        let irArgs := irArgs.extract (start := ctorVal.numParams)
-        if irArgs.size != fields.size then
-          -- An overapplied constructor arises from compiler
-          -- transformations on unreachable code
-          return .unreachable
-
-        let objArgs : Array Arg ← do
-          let mut result : Array Arg := #[]
-          for h : i in *...fields.size do
-            match fields[i] with
-            | .object .. =>
-              result := result.push irArgs[i]!
-            | .usize .. | .scalar .. | .erased | .void => pure ()
-          pure result
-        let objVar ← bindVar decl.fvarId
-        let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
-          let rec loop (i : Nat) : M FnBody := do
-            match irArgs[i]? with
-            | some (.var varId) =>
-              match fields[i]! with
-              | .usize usizeIdx =>
-                let k ← loop (i + 1)
-                return .uset objVar usizeIdx varId k
-              | .scalar _ offset argType =>
-                let k ← loop (i + 1)
-                return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
-              | .object .. | .erased | .void => loop (i + 1)
-            | some .erased => loop (i + 1)
-            | none => lowerCode k
-          loop 0
-        return .vdecl objVar ctorInfo.type (.ctor ctorInfo objArgs) (← lowerNonObjectFields ())
-    | some (.defnInfo ..) | some (.opaqueInfo ..) =>
-      mkFap name irArgs
-    | some (.axiomInfo ..) | .some (.quotInfo ..) | .some (.inductInfo ..) | .some (.thmInfo ..) =>
-      -- Should have been caught by `ToLCNF`
-      throwError f!"ToIR: unexpected use of noncomputable declaration `{name}`; please report this issue"
-    | some (.recInfo ..) =>
-      throwError f!"code generator does not support recursor `{name}` yet, consider using 'match ... with' and/or structural recursion"
-    | none => panic! "reference to unbound name"
+    let ⟨litValue, _⟩ := lowerLitValue litValue
+    continueLet (.lit litValue)
+  | .oproj i var _ =>
+    withGetFVarValue var fun var =>
+      continueLet (.proj i var)
+  | .uproj i var _ =>
+    withGetFVarValue var fun var =>
+      continueLet (.uproj i var)
+  | .sproj i offset var _ =>
+    withGetFVarValue var fun var =>
+      continueLet (.sproj i offset var)
+  | .ctor info args _ => continueLet (.ctor (lowerCtorInfo info) (← args.mapM lowerArg))
+  | .fap fn args => continueLet (.fap fn (← args.mapM lowerArg))
+  | .pap fn args => continueLet (.pap fn (← args.mapM lowerArg))
   | .fvar fvarId args =>
-    match (← getFVarValue fvarId) with
-    | .var id =>
+    withGetFVarValue fvarId fun id => do
       let irArgs ← args.mapM lowerArg
-      mkAp id irArgs
-    | .erased => mkErased ()
+      continueLet (.ap id irArgs)
   | .erased => mkErased ()
 where
-  mkVar (v : VarId) : M FnBody := do
-    bindVarToVarId decl.fvarId v
-    lowerCode k
-
   mkErased (_ : Unit) : M FnBody := do
     bindErased decl.fvarId
     lowerCode k
 
-  mkFap (name : Name) (args : Array Arg) : M FnBody := do
-    let var ← bindVar decl.fvarId
-    let type ← toIRType decl.type
-    return .vdecl var type (.fap name args) (← lowerCode k)
+  withGetFVarValue (fvarId : FVarId) (f : VarId → M FnBody) : M FnBody := do
+    match (← getFVarValue fvarId) with
+    | .var id => f id
+    | .erased => mkErased ()
 
-  mkPap (name : Name) (args : Array Arg) : M FnBody := do
-    let var ← bindVar decl.fvarId
-    return .vdecl var .object (.pap name args) (← lowerCode k)
-
-  mkAp (fnVar : VarId) (args : Array Arg) : M FnBody := do
-    let var ← bindVar decl.fvarId
-    let type := (← toIRType decl.type).boxed
-    return .vdecl var type (.ap fnVar args) (← lowerCode k)
-
-  mkOverApplication (name : Name) (numParams : Nat) (args : Array Arg) : M FnBody := do
-    let var ← bindVar decl.fvarId
-    let type := (← toIRType decl.type).boxed
-    let tmpVar ← newVar
-    let firstArgs := args.extract 0 numParams
-    let restArgs := args.extract numParams args.size
-    return .vdecl tmpVar .object (.fap name firstArgs) <|
-           .vdecl var type (.ap tmpVar restArgs) (← lowerCode k)
-
-  mkApplication (name : Name) (numParams : Nat) (args : Array Arg) : M FnBody := do
-    let numArgs := args.size
-    if numArgs < numParams then
-      mkPap name args
-    else if numArgs == numParams then
-      mkFap name args
-    else
-      mkOverApplication name numParams args
-
-partial def lowerAlt (discr : VarId) (a : LCNF.Alt .pure) : M Alt := do
+partial def lowerAlt (a : LCNF.Alt .impure) : M Alt := do
   match a with
-  | .alt ctorName params code =>
-    let ⟨ctorInfo, fields⟩ ← getCtorLayout ctorName
-    let lowerParams (params : Array (LCNF.Param .pure)) (fields : Array CtorFieldInfo) : M FnBody := do
-      let rec loop (i : Nat) : M FnBody := do
-        match params[i]?, fields[i]? with
-        | some param, some field =>
-          let ⟨result, type⟩ := lowerProj discr ctorInfo field
-          match result with
-          | .expr e =>
-            return .vdecl (← bindVar param.fvarId)
-                          type
-                          e
-                          (← loop (i + 1))
-          | .erased =>
-            bindErased param.fvarId
-            loop (i + 1)
-        | none, none => lowerCode code
-        | _, _ => panic! "mismatched fields and params"
-      loop 0
-    let body ← lowerParams params fields
-    return .ctor ctorInfo body
-  | .default code =>
-    return .default (← lowerCode code)
+  | .ctorAlt info k => return .ctor (lowerCtorInfo info) (← lowerCode k)
+  | .default code => return .default (← lowerCode code)
 end
 
-def lowerResultType (type : Lean.Expr) (arity : Nat) : M IRType :=
-  toIRType (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 .pure) : M (Option Decl) := do
+def lowerDecl (d : LCNF.Decl .impure) : M (Option Decl) := do
   let params ← d.params.mapM lowerParam
-  let mut resultType ← lowerResultType d.type d.params.size
-  let taggedReturn := taggedReturnAttr.hasTag (← getEnv) d.name
+  let resultType := toIRType d.type
   match d.value with
   | .code code =>
-    if taggedReturn then
-      throwError m!"Error while compiling function '{d.name}': @[tagged_return] is only valid for extern declarations"
     let body ← lowerCode code
     pure <| some <| .fdecl d.name params resultType body {}
   | .extern externAttrData =>
-    if taggedReturn then
-      if resultType.isScalar then
-        throwError m!"@[tagged_return] on function '{d.name}' with scalar return type {resultType}"
-      else
-        resultType := .tagged
     if externAttrData.entries.isEmpty then
       -- TODO: This matches the behavior of the old compiler, but we should
       -- find a better way to handle this.
@@ -367,7 +171,7 @@ def lowerDecl (d : LCNF.Decl .pure) : M (Option Decl) := do
 
 end ToIR
 
-def toIR (decls: Array (LCNF.Decl .pure)) : CoreM (Array Decl) := do
+def toIR (decls: Array (LCNF.Decl .impure)) : CoreM (Array Decl) := do
   let mut irDecls := #[]
   for decl in decls do
     if let some irDecl ← ToIR.lowerDecl decl |>.run then

src/Lean/Compiler/IR/ToIRType.lean

@@ -14,237 +14,39 @@ public section
 namespace Lean
 namespace IR
 
-open Lean.Compiler (LCNF.CacheExtension LCNF.isTypeFormerType LCNF.toLCNFType LCNF.toMonoType
-  LCNF.TrivialStructureInfo LCNF.getOtherDeclBaseType LCNF.getParamTypes LCNF.instantiateForall
-  LCNF.Irrelevant.hasTrivialStructure?)
+open Lean.Compiler
 
-def irTypeForEnum (numCtors : Nat) : IRType :=
-  if numCtors == 1 then
-    .tagged
-  else if numCtors < Nat.pow 2 8 then
-    .uint8
-  else if numCtors < Nat.pow 2 16 then
-    .uint16
-  else if numCtors < Nat.pow 2 32 then
-    .uint32
-  else
-    .tagged
-
-builtin_initialize irTypeExt : LCNF.CacheExtension Name IRType ←
-  LCNF.CacheExtension.register
-
-builtin_initialize trivialStructureInfoExt :
-    LCNF.CacheExtension Name (Option LCNF.TrivialStructureInfo) ←
-  LCNF.CacheExtension.register
-
-/--
-The idea of this function is the same as in `ToMono`, however the notion of "irrelevancy" has
-changed because we now have the `void` type which can only be erased in impure context and thus at
-earliest at the conversion from mono to IR.
--/
-def hasTrivialStructure? (declName : Name) : CoreM (Option LCNF.TrivialStructureInfo) := do
-  let isVoidType type := do
-    let type ← Meta.whnfD type
-    return type matches .proj ``Subtype 0 (.app (.const ``Void.nonemptyType []) _)
-  let irrelevantType type :=
-    Meta.isProp type <||> Meta.isTypeFormerType type <||> isVoidType type
-  LCNF.Irrelevant.hasTrivialStructure? trivialStructureInfoExt irrelevantType declName
-
-def nameToIRType (name : Name) : CoreM IRType := do
-  match (← irTypeExt.find? name) with
-  | some type => return type
-  | none =>
-    let type ← fillCache
-    irTypeExt.insert name type
-    return type
-where fillCache : CoreM IRType := do
-    match name with
-    | ``UInt8 => return .uint8
-    | ``UInt16 => return .uint16
-    | ``UInt32 => return .uint32
-    | ``UInt64 => return .uint64
-    | ``USize => return .usize
-    | ``Float => return .float
-    | ``Float32 => return .float32
-    | ``lcErased => return .erased
-    -- `Int` is specified as an inductive type with two constructors that have relevant arguments,
-    -- but it has the same runtime representation as `Nat` and thus needs to be special-cased here.
-    | ``Int => return .tobject
-    | ``lcVoid => return .void
-    | _ =>
-      let env ← Lean.getEnv
-      let some (.inductInfo inductiveVal) := env.find? name | return .tobject
-      let ctorNames := inductiveVal.ctors
-      let numCtors := ctorNames.length
-      let mut numScalarCtors := 0
-      for ctorName in ctorNames do
-        let some (.ctorInfo ctorInfo) := env.find? ctorName | unreachable!
-        let hasRelevantField ← Meta.MetaM.run' <|
-                               Meta.forallTelescope ctorInfo.type fun params _ => do
-          for field in params[ctorInfo.numParams...*] do
-            let fieldType ← field.fvarId!.getType
-            let lcnfFieldType ← LCNF.toLCNFType fieldType
-            let monoFieldType ← LCNF.toMonoType lcnfFieldType
-            if !monoFieldType.isErased then return true
-          return false
-        if !hasRelevantField then
-          numScalarCtors := numScalarCtors + 1
-      if numScalarCtors == numCtors then
-        return irTypeForEnum numCtors
-      else if numScalarCtors == 0 then
-        return .object
-      else
-        return .tobject
-
-private def isAnyProducingType (type : Lean.Expr) : Bool :=
-  match type with
-  | .const ``lcAny _ => true
-  | .forallE _ _ b _ => isAnyProducingType b
-  | _ => false
-
-partial def toIRType (type : Lean.Expr) : CoreM IRType := do
-  match type with
-  | .const name _ => visitApp name #[]
-  | .app .. =>
-    -- All mono types are in headBeta form.
-    let .const name _ := type.getAppFn | unreachable!
-    visitApp name type.getAppArgs
-  | .forallE _ _ b _ =>
-    -- Type formers are erased, but can be used polymorphically as
-    -- an arrow type producing `lcAny`. The runtime representation of
-    -- erased values is a tagged scalar, so this means that any such
-    -- polymorphic type must be represented as `.tobject`.
-    if isAnyProducingType b then
-      return .tobject
-    else
-      return .object
-  | .mdata _ b => toIRType b
+def nameToIRType (n : Name) : IRType :=
+  match n with
+  | ``Float => .float
+  | ``Float32 => .float32
+  | ``UInt8 => .uint8
+  | ``UInt16 => .uint16
+  | ``UInt32 => .uint32
+  | ``UInt64 => .uint64
+  | ``lcErased => .erased
+  | `obj => .object
+  | `tobj => .tobject
+  | `tagged => .tagged
+  | ``lcVoid => .void
   | _ => unreachable!
-where
-  visitApp (declName : Name) (args : Array Lean.Expr) : CoreM IRType := do
-    if let some info ← hasTrivialStructure? declName then
-      let ctorType ← LCNF.getOtherDeclBaseType info.ctorName []
-      let monoType ← LCNF.toMonoType (LCNF.getParamTypes (← LCNF.instantiateForall ctorType args[*...info.numParams]))[info.fieldIdx]!
-      toIRType monoType
-    else
-      nameToIRType declName
 
-inductive CtorFieldInfo where
-  | erased
-  | object (i : Nat) (type : IRType)
-  | usize  (i : Nat)
-  | scalar (sz : Nat) (offset : Nat) (type : IRType)
-  | void
-  deriving Inhabited
 
-namespace CtorFieldInfo
-
-def format : CtorFieldInfo → Format
-  | erased => "◾"
-  | void => "void"
-  | object i type => f!"obj@{i}:{type}"
-  | usize i    => f!"usize@{i}"
-  | scalar sz offset type => f!"scalar#{sz}@{offset}:{type}"
-
-instance : ToFormat CtorFieldInfo := ⟨format⟩
-
-end CtorFieldInfo
-
-structure CtorLayout where
-  ctorInfo : CtorInfo
-  fieldInfo : Array CtorFieldInfo
-  deriving Inhabited
-
-builtin_initialize ctorLayoutExt : LCNF.CacheExtension Name CtorLayout ←
-  LCNF.CacheExtension.register
-
-def getCtorLayout (ctorName : Name) : CoreM CtorLayout := do
-  match (← ctorLayoutExt.find? ctorName) with
-  | some info => return info
-  | none =>
-    let info ← fillCache
-    ctorLayoutExt.insert ctorName info
-    return info
-where fillCache := do
-  let .some (.ctorInfo ctorInfo) := (← getEnv).find? ctorName | unreachable!
-  Meta.MetaM.run' <| Meta.forallTelescopeReducing ctorInfo.type fun params _ => do
-    let mut fields : Array CtorFieldInfo := .emptyWithCapacity ctorInfo.numFields
-    let mut nextIdx := 0
-    let mut has1BScalar := false
-    let mut has2BScalar := false
-    let mut has4BScalar := false
-    let mut has8BScalar := false
-    for field in params[ctorInfo.numParams...(ctorInfo.numParams + ctorInfo.numFields)] do
-      let fieldType ← field.fvarId!.getType
-      let lcnfFieldType ← LCNF.toLCNFType fieldType
-      let monoFieldType ← LCNF.toMonoType lcnfFieldType
-      let irFieldType ← toIRType monoFieldType
-      let ctorField ← match irFieldType with
-      | .object | .tagged | .tobject => do
-        let i := nextIdx
-        nextIdx := nextIdx + 1
-        pure <| .object i irFieldType
-      | .usize => pure <| .usize 0
-      | .erased => .pure <| .erased
-      | .void => .pure <| .void
-      | .uint8 =>
-        has1BScalar := true
-        .pure <| .scalar 1 0 .uint8
-      | .uint16 =>
-        has2BScalar := true
-        .pure <| .scalar 2 0 .uint16
-      | .uint32 =>
-        has4BScalar := true
-        .pure <| .scalar 4 0 .uint32
-      | .uint64 =>
-        has8BScalar := true
-        .pure <| .scalar 8 0 .uint64
-      | .float32 =>
-        has4BScalar := true
-        .pure <| .scalar 4 0 .float32
-      | .float =>
-        has8BScalar := true
-        .pure <| .scalar 8 0 .float
-      | .struct .. | .union .. => unreachable!
-      fields := fields.push ctorField
-    let numObjs := nextIdx
-    ⟨fields, nextIdx⟩ := Id.run <| StateT.run (s := nextIdx) <| fields.mapM fun field => do
-      match field with
-      | .usize _ => do
-        let i ← modifyGet fun nextIdx => (nextIdx, nextIdx + 1)
-        return .usize i
-      | .object .. | .scalar .. | .erased | .void => return field
-    let numUSize := nextIdx - numObjs
-    let adjustScalarsForSize (fields : Array CtorFieldInfo) (size : Nat) (nextOffset : Nat)
-        : Array CtorFieldInfo × Nat :=
-      Id.run <| StateT.run (s := nextOffset) <| fields.mapM fun field => do
-        match field with
-        | .scalar sz _ type => do
-          if sz == size then
-            let offset ← modifyGet fun nextOffset => (nextOffset, nextOffset + sz)
-            return .scalar sz offset type
-          else
-            return field
-        | .object .. | .usize _ | .erased | .void => return field
-    let mut nextOffset := 0
-    if has8BScalar then
-      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 8 nextOffset
-    if has4BScalar then
-      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 4 nextOffset
-    if has2BScalar then
-      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 2 nextOffset
-    if has1BScalar then
-      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 1 nextOffset
-    return {
-      ctorInfo := {
-        name := ctorName
-        cidx := ctorInfo.cidx
-        size := numObjs
-        usize := numUSize
-        ssize := nextOffset
-      }
-      fieldInfo := fields
-    }
+def toIRType (type : Lean.Expr) : IRType :=
+  match type with
+  | LCNF.ImpureType.float => .float
+  | LCNF.ImpureType.float32 => .float32
+  | LCNF.ImpureType.uint8 => .uint8
+  | LCNF.ImpureType.uint16 => .uint16
+  | LCNF.ImpureType.uint32 => .uint32
+  | LCNF.ImpureType.uint64 => .uint64
+  | LCNF.ImpureType.usize => .usize
+  | LCNF.ImpureType.erased => .erased
+  | LCNF.ImpureType.object => .object
+  | LCNF.ImpureType.tobject => .tobject
+  | LCNF.ImpureType.tagged => .tagged
+  | LCNF.ImpureType.void => .void
+  | _ => unreachable!
 
 end IR
 end Lean

src/Lean/Compiler/LCNF/Basic.lean

@@ -60,6 +60,140 @@ def Purity.withAssertPurity [Inhabited α] (is : Purity) (should : Purity)
 
 scoped macro "purity_tac" : tactic => `(tactic| first | with_reducible rfl | assumption)
 
+namespace ImpureType
+
+/-!
+This section defines the low level IR types used in the impure phase of LCNF.
+-/
+
+/--
+`float` is a 64-bit floating point number.
+-/
+@[inline, expose, match_pattern]
+def float : Expr := .const ``Float []
+
+
+/--
+`float32` is a 32-bit floating point number.
+-/
+@[inline, expose, match_pattern]
+def float32 : Expr := .const ``Float32 []
+
+/--
+`uint8` is an 8-bit unsigned integer.
+-/
+@[inline, expose, match_pattern]
+def uint8 : Expr := .const ``UInt8 []
+
+/--
+`uint16` is a 16-bit unsigned integer.
+-/
+@[inline, expose, match_pattern]
+def uint16 : Expr := .const ``UInt16 []
+
+/--
+`uint32` is a 32-bit unsigned integer.
+-/
+@[inline, expose, match_pattern]
+def uint32 : Expr := .const ``UInt32 []
+
+/--
+`uint64` is a 64-bit unsigned integer.
+-/
+@[inline, expose, match_pattern]
+def uint64 : Expr := .const ``UInt64 []
+
+/--
+`usize` represents the C `size_t` type. It has a separate representation because depending on the
+target architecture it has a different width and we try to generate platform independent C code.
+
+We generally assume that `sizeof(size_t) == sizeof(void)`.
+-/
+@[inline, expose, match_pattern]
+def usize : Expr := .const ``USize []
+
+/--
+`erased` represents type arguments, propositions and proofs which are no longer relevant at this
+point in time.
+-/
+@[inline, expose, match_pattern]
+def erased : Expr := .const ``lcErased []
+
+/-
+`object` is a pointer to a value in the heap.
+-/
+@[inline, expose, match_pattern]
+def object : Expr := .const `obj []
+
+/--
+`tobject` is either an `object` or a `tagged` pointer.
+
+Crucially the RC the RC operations for `tobject` are slightly more expensive because we
+first need to test whether the `tobject` is really a pointer or not.
+-/
+@[inline, expose, match_pattern]
+def tobject : Expr := .const `tobj []
+
+/--
+tagged` is a tagged pointer (i.e., the least significant bit is 1) storing a scalar value.
+-/
+@[inline, expose, match_pattern]
+def tagged : Expr := .const `tagged []
+
+/--
+`void` is used to identify uses of the state token from `BaseIO` which do no longer need
+to be passed around etc. at this point in the pipeline.
+-/
+@[inline, expose, match_pattern]
+def void : Expr := .const ``lcVoid []
+
+/--
+Whether the type is a scalar as opposed to a pointer (or a value disguised as a pointer).
+-/
+def Lean.Expr.isScalar : Expr → Bool
+  | ImpureType.float    => true
+  | ImpureType.float32  => true
+  | ImpureType.uint8    => true
+  | ImpureType.uint16   => true
+  | ImpureType.uint32   => true
+  | ImpureType.uint64   => true
+  | ImpureType.usize    => true
+  | _        => false
+
+/--
+Whether the type is an object which is to say a pointer or a value disguised as a pointer.
+-/
+def Lean.Expr.isObj : Expr → Bool
+  | ImpureType.object  => true
+  | ImpureType.tagged  => true
+  | ImpureType.tobject => true
+  | ImpureType.void    => true
+  | _       => false
+
+/--
+Whether the type might be an actual pointer (crucially this excludes `tagged`).
+-/
+def Lean.Expr.isPossibleRef : Expr → Bool
+  | ImpureType.object | ImpureType.tobject => true
+  | _ => false
+
+/--
+Whether the type is a pointer for sure.
+-/
+def Lean.Expr.isDefiniteRef : Expr → Bool
+  | ImpureType.object => true
+  | _ => false
+
+/--
+The boxed version of types.
+-/
+def Lean.Expr.boxed : Expr → Expr
+  | ImpureType.object | ImpureType.float | ImpureType.float32 => ImpureType.object
+  | ImpureType.void | ImpureType.tagged | ImpureType.uint8 | ImpureType.uint16 => ImpureType.tagged
+  | _ => ImpureType.tobject
+
+end ImpureType
+
 structure Param (pu : Purity) where
   fvarId     : FVarId
   binderName : Name
@@ -91,6 +225,15 @@ def LitValue.toExpr : LitValue → Expr
   | .uint64 v => .app (.const ``UInt64.ofNat []) (.lit (.natVal (UInt64.toNat v)))
   | .usize v => .app (.const ``USize.ofNat []) (.lit (.natVal (UInt64.toNat v)))
 
+def LitValue.impureTypeScalarNumLit (e : Expr) (n : Nat) : LitValue :=
+  match e with
+  | ImpureType.uint8 => .uint8 n.toUInt8
+  | ImpureType.uint16 => .uint16 n.toUInt16
+  | ImpureType.uint32 => .uint32 n.toUInt32
+  | ImpureType.uint64 => .uint64 n.toUInt64
+  | ImpureType.usize => .usize n.toUInt64
+  | _ => panic! s!"Provided invalid type to impureTypeScalarNumLit: {e}"
+
 inductive Arg (pu : Purity) where
   | erased
   | fvar (fvarId : FVarId)
@@ -120,12 +263,79 @@ private unsafe def Arg.updateFVarImp (arg : Arg pu) (fvarId' : FVarId) : Arg pu
 
 @[implemented_by Arg.updateFVarImp] opaque Arg.updateFVar! (arg : Arg pu) (fvarId' : FVarId) : Arg pu
 
+/-- Constructor information.
+
+   - `name` is the Name of the Constructor in Lean.
+   - `cidx` is the Constructor index (aka tag).
+   - `size` is the number of arguments of type `object/tobject`.
+   - `usize` is the number of arguments of type `usize`.
+   - `ssize` is the number of bytes used to store scalar values.
+
+Recall that a Constructor object contains a header, then a sequence of
+pointers to other Lean objects, a sequence of `USize` (i.e., `size_t`)
+scalar values, and a sequence of other scalar values. -/
+structure CtorInfo where
+  name : Name
+  cidx : Nat
+  size : Nat
+  usize : Nat
+  ssize : Nat
+  deriving Inhabited, BEq, Repr, Hashable
+
+def CtorInfo.isRef (info : CtorInfo) : Bool :=
+  info.size > 0 || info.usize > 0 || info.ssize > 0
+
+def CtorInfo.isScalar (info : CtorInfo) : Bool :=
+  !info.isRef
+
+def CtorInfo.type (info : CtorInfo) : Expr :=
+  if info.isRef then ImpureType.object else ImpureType.tagged
+
 inductive LetValue (pu : Purity) where
+  /--
+  A literal value.
+  -/
   | lit (value : LitValue)
+  /--
+  An erased value that is irrelevant for computation.
+  -/
   | erased
+  /--
+  A projection from a pure LCNF value.
+  -/
   | proj (typeName : Name) (idx : Nat) (struct : FVarId) (h : pu = .pure := by purity_tac)
+  /--
+  A pure application of a constant.
+  -/
   | const (declName : Name) (us : List Level) (args : Array (Arg pu)) (h : pu = .pure := by purity_tac)
+  /--
+  An application of a free variable
+  -/
   | fvar (fvarId : FVarId) (args : Array (Arg pu))
+  /--
+  Allocating a constructor.
+  -/
+  | ctor (i : CtorInfo) (args : Array (Arg pu)) (h : pu = .impure := by purity_tac)
+  /--
+  Projecting objects out of a value.
+  -/
+  | oproj (i : Nat) (var : FVarId) (h : pu = .impure := by purity_tac)
+  /--
+  Projecting USize scalars out of a value.
+  -/
+  | uproj (i : Nat) (var : FVarId) (h : pu = .impure := by purity_tac)
+  /--
+  Projecting non-USize scalars out of a value
+  -/
+  | sproj (n : Nat) (offset : Nat) (var : FVarId) (h : pu = .impure := by purity_tac)
+  /--
+  Full, impure, application of a function.
+  -/
+  | fap (fn : Name) (args : Array (Arg pu)) (h : pu = .impure := by purity_tac)
+  /--
+  Partial application of a function.
+  -/
+  | pap (fn : Name) (args : Array (Arg pu)) (h : pu = .impure := by purity_tac)
   deriving Inhabited, BEq, Hashable
 
 def Arg.toLetValue (arg : Arg pu) : LetValue pu :=
@@ -136,6 +346,9 @@ def Arg.toLetValue (arg : Arg pu) : LetValue pu :=
 private unsafe def LetValue.updateProjImp (e : LetValue pu) (fvarId' : FVarId) : LetValue pu :=
   match e with
   | .proj s i fvarId _ => if fvarId == fvarId' then e else .proj s i fvarId'
+  | .sproj i offset fvarId _ => if fvarId == fvarId' then e else .sproj i offset fvarId'
+  | .uproj i fvarId _ => if fvarId == fvarId' then e else .uproj i fvarId'
+  | .oproj i fvarId _ => if fvarId == fvarId' then e else .oproj i fvarId'
   | _ => unreachable!
 
 @[implemented_by LetValue.updateProjImp] opaque LetValue.updateProj! (e : LetValue pu) (fvarId' : FVarId) : LetValue pu
@@ -158,6 +371,9 @@ private unsafe def LetValue.updateArgsImp (e : LetValue pu) (args' : Array (Arg
   match e with
   | .const declName us args h => if ptrEq args args' then e else .const declName us args'
   | .fvar fvarId args => if ptrEq args args' then e else .fvar fvarId args'
+  | .pap declName args _  => if ptrEq args args' then e else .pap declName args'
+  | .fap declName args _  => if ptrEq args args' then e else .fap declName args'
+  | .ctor info args _  => if ptrEq args args' then e else .ctor info args'
   | _ => unreachable!
 
 @[implemented_by LetValue.updateArgsImp] opaque LetValue.updateArgs! (e : LetValue pu) (args' : Array (Arg pu)) : LetValue pu
@@ -169,6 +385,11 @@ def LetValue.toExpr (e : LetValue pu) : Expr :=
   | .proj n i s _ => .proj n i (.fvar s)
   | .const n us as _ => mkAppN (.const n us) (as.map Arg.toExpr)
   | .fvar fvarId as => mkAppN (.fvar fvarId) (as.map Arg.toExpr)
+  | .ctor i as _ => mkAppN (.const i.name []) (as.map Arg.toExpr)
+  | .fap fn as _ | .pap fn as _ => mkAppN (.const fn []) (as.map Arg.toExpr)
+  | .oproj i var _ => mkApp2 (.const `oproj []) (ToExpr.toExpr i) (.fvar var)
+  | .uproj i var _ => mkApp2 (.const `uproj []) (ToExpr.toExpr i) (.fvar var)
+  | .sproj i offset var _ => mkApp3 (.const `sproj []) (ToExpr.toExpr i) (ToExpr.toExpr offset) (.fvar var)
 
 structure LetDecl (pu : Purity) where
   fvarId : FVarId
@@ -181,6 +402,7 @@ mutual
 
 inductive Alt (pu : Purity) where
   | alt (ctorName : Name) (params : Array (Param pu)) (code : Code pu) (h : pu = .pure := by purity_tac)
+  | ctorAlt (info : CtorInfo) (code : Code pu) (h : pu = .impure := by purity_tac)
   | default (code : Code pu)
 
 inductive FunDecl (pu : Purity) where
@@ -198,6 +420,8 @@ inductive Code (pu : Purity) where
   | cases (cases : Cases pu)
   | return (fvarId : FVarId)
   | unreach (type : Expr)
+  | uset (var : FVarId) (i : Nat) (y : FVarId) (k : Code pu) (h : pu = .impure := by purity_tac)
+  | sset (var : FVarId) (i : Nat) (offset : Nat) (y : FVarId)  (ty : Expr) (k : Code pu) (h : pu = .impure := by purity_tac)
   deriving Inhabited
 
 end
@@ -267,6 +491,7 @@ def Cases.getCtorNames (c : Cases pu) : NameSet :=
     match alt with
     | .default _ => ctorNames
     | .alt ctorName .. => ctorNames.insert ctorName
+    | .ctorAlt info .. => ctorNames.insert info.name
 
 inductive CodeDecl (pu : Purity) where
   | let (decl : LetDecl pu)
@@ -335,8 +560,9 @@ instance : BEq (FunDecl pu) where
 def Alt.getCode : Alt pu → Code pu
   | .default k => k
   | .alt _ _ k _ => k
+  | .ctorAlt _ k _ => k
 
-def Alt.getParams : Alt pu → Array (Param pu)
+def Alt.getParams : Alt .pure → Array (Param .pure)
   | .default _ => #[]
   | .alt _ ps _ _ => ps
 
@@ -344,11 +570,13 @@ def Alt.forCodeM [Monad m] (alt : Alt pu) (f : Code pu → m Unit) : m Unit := d
   match alt with
   | .default k => f k
   | .alt _ _ k _ => f k
+  | .ctorAlt _ k _ => f k
 
 private unsafe def updateAltCodeImp (alt : Alt pu) (k' : Code pu) : Alt pu :=
   match alt with
   | .default k => if ptrEq k k' then alt else .default k'
   | .alt ctorName ps k _ => if ptrEq k k' then alt else .alt ctorName ps k'
+  | .ctorAlt info k _ => if ptrEq k k' then alt else .ctorAlt info k'
 
 @[implemented_by updateAltCodeImp] opaque Alt.updateCode (alt : Alt pu) (c : Code pu) : Alt pu
 
@@ -389,6 +617,8 @@ private unsafe def updateAltImp (alt : Alt pu) (ps' : Array (Param pu)) (k' : Co
   | .let decl k => if ptrEq k k' then c else .let decl k'
   | .fun decl k _ => if ptrEq k k' then c else .fun decl k'
   | .jp decl k => if ptrEq k k' then c else .jp decl k'
+  | .sset fvarId i offset y ty k _ => if ptrEq k k' then c else .sset fvarId i offset y ty k'
+  | .uset fvarId offset y k _ => if ptrEq k k' then c else .uset fvarId offset y k'
   | _ => unreachable!
 
 @[implemented_by updateContImp] opaque Code.updateCont! (c : Code pu) (k' : Code pu) : Code pu
@@ -422,6 +652,32 @@ private unsafe def updateAltImp (alt : Alt pu) (ps' : Array (Param pu)) (k' : Co
 
 @[implemented_by updateUnreachImp] opaque Code.updateUnreach! (c : Code pu) (type' : Expr) : Code pu
 
+@[inline] private unsafe def updateSsetImp (c : Code pu) (fvarId' : FVarId) (i' : Nat)
+    (offset' : Nat) (y' : FVarId) (ty' : Expr) (k' : Code pu) : Code pu :=
+  match c with
+  | .sset fvarId i offset y ty k _ =>
+    if ptrEq fvarId fvarId' && i == i' && offset == offset' && ptrEq y y' && ptrEq ty ty' && ptrEq k k' then
+      c
+    else
+      .sset fvarId' i' offset' y' ty' k'
+  | _ => unreachable!
+
+@[implemented_by updateSsetImp] opaque Code.updateSset! (c : Code pu) (fvarId' : FVarId) (i' : Nat)
+    (offset' : Nat) (y' : FVarId) (ty' : Expr) (k' : Code pu) : Code pu
+
+@[inline] private unsafe def updateUsetImp (c : Code pu) (fvarId' : FVarId)
+    (offset' : Nat) (y' : FVarId) (k' : Code pu) : Code pu :=
+  match c with
+  | .sset fvarId i offset y ty k _ =>
+    if ptrEq fvarId fvarId' && offset == offset' && ptrEq y y' && ptrEq k k' then
+      c
+    else
+      .uset fvarId' offset' y' k'
+  | _ => unreachable!
+
+@[implemented_by updateUsetImp] opaque Code.updateUset! (c : Code pu) (fvarId' : FVarId)
+    (offset' : Nat) (y' : FVarId) (k' : Code pu) : Code pu
+
 private unsafe def updateParamCoreImp (p : Param pu) (type : Expr) : Param pu :=
   if ptrEq type p.type then
     p
@@ -490,7 +746,7 @@ partial def Code.size (c : Code pu) : Nat :=
 where
   go (c : Code pu) (n : Nat) : Nat :=
     match c with
-    | .let _ k => go k (n+1)
+    | .let _ k | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k (n + 1)
     | .jp decl k | .fun decl k _ => go k <| go decl.value n
     | .cases c => c.alts.foldl (init := n+1) fun n alt => go alt.getCode (n+1)
     | .jmp .. => n+1
@@ -508,7 +764,7 @@ where
 
   go (c : Code pu) : EStateM Unit Nat Unit := do
     match c with
-    | .let _ k => inc; go k
+    | .let _ k | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => inc; go k
     | .jp decl k | .fun decl k _ => inc; go decl.value; go k
     | .cases c => inc; c.alts.forM fun alt => go alt.getCode
     | .jmp .. => inc
@@ -520,7 +776,7 @@ where
   go (c : Code pu) : m Unit := do
     f c
     match c with
-    | .let _ k => go k
+    | .let _ k | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
     | .fun decl k _ | .jp decl k => go decl.value; go k
     | .cases c => c.alts.forM fun alt => go alt.getCode
     | .unreach .. | .return .. | .jmp .. => return ()
@@ -600,13 +856,13 @@ def DeclValue.isCodeAndM [Monad m] (v : DeclValue pu) (f : Code pu → m Bool) :
   | .extern .. => pure false
 
 /--
-Declaration being processed by the Lean to Lean compiler passes.
+The signature of a declaration being processed by the Lean to Lean compiler passes.
 -/
-structure Decl (pu : Purity) where
+structure Signature (pu : Purity) where
   /--
   The name of the declaration from the `Environment` it came from
   -/
-  name  : Name
+  name : Name
   /--
   Universe level parameter names.
   -/
@@ -614,7 +870,8 @@ structure Decl (pu : Purity) where
   /--
   The type of the declaration. Note that this is an erased LCNF type
   instead of the fully dependent one that might have been the original
-  type of the declaration in the `Environment`.
+  type of the declaration in the `Environment`. Furthermore, once in the
+  impure staged of LCNF this type is only the return type.
   -/
   type  : Expr
   /--
@@ -622,21 +879,6 @@ structure Decl (pu : Purity) where
   -/
   params : Array (Param pu)
   /--
-  The body of the declaration, usually changes as it progresses
-  through compiler passes.
-  -/
-  value : DeclValue pu
-  /--
-  We set this flag to true during LCNF conversion. When we receive
-  a block of functions to be compiled, we set this flag to `true`
-  if there is an application to the function in the block containing
-  it. This is an approximation, but it should be good enough because
-  in the frontend, we invoke the compiler with blocks of strongly connected
-  components only.
-  We use this information to control inlining.
-  -/
-  recursive : Bool := false
-  /--
   We set this flag to false during LCNF conversion if the Lean function
   associated with this function was tagged as partial or unsafe. This
   information affects how static analyzers treat function applications
@@ -660,6 +902,27 @@ structure Decl (pu : Purity) where
   exhaust resources or output a looping computation.
   -/
   safe : Bool := true
+  deriving Inhabited, BEq
+
+/--
+Declaration being processed by the Lean to Lean compiler passes.
+-/
+structure Decl (pu : Purity) extends Signature pu where
+  /--
+  The body of the declaration, usually changes as it progresses
+  through compiler passes.
+  -/
+  value : DeclValue pu
+  /--
+  We set this flag to true during LCNF conversion. When we receive
+  a block of functions to be compiled, we set this flag to `true`
+  if there is an application to the function in the block containing
+  it. This is an approximation, but it should be good enough because
+  in the frontend, we invoke the compiler with blocks of strongly connected
+  components only.
+  We use this information to control inlining.
+  -/
+  recursive : Bool := false
   /--
   We store the inline attribute at LCNF declarations to make sure we can set them for
   auxiliary declarations created during compilation.
@@ -775,8 +1038,8 @@ private def collectArgs (args : Array (Arg pu)) (s : FVarIdHashSet) : FVarIdHash
 private def collectLetValue (e : LetValue pu) (s : FVarIdHashSet) : FVarIdHashSet :=
   match e with
   | .fvar fvarId args => collectArgs args <| s.insert fvarId
-  | .const _ _ args _ => collectArgs args s
-  | .proj _ _ fvarId _ => s.insert fvarId
+  | .const _ _ args _ | .pap _ args _ | .fap _ args _ | .ctor _ args _  => collectArgs args s
+  | .proj _ _ fvarId _ | .sproj _ _ fvarId _ | .uproj _ fvarId _ | .oproj _ fvarId _ => s.insert fvarId
   | .lit .. | .erased => s
 
 private partial def collectParams (ps : Array (Param pu)) (s : FVarIdHashSet) : FVarIdHashSet :=
@@ -795,11 +1058,15 @@ partial def Code.collectUsed (code : Code pu) (s : FVarIdHashSet := {}) : FVarId
     let s := collectType c.resultType s
     c.alts.foldl (init := s) fun s alt =>
       match alt with
-      | .default k => k.collectUsed s
+      | .default k | .ctorAlt _ k _  => k.collectUsed s
       | .alt _ ps k _ => k.collectUsed <| collectParams ps s
   | .return fvarId => s.insert fvarId
   | .unreach type => collectType type s
   | .jmp fvarId args => collectArgs args <| s.insert fvarId
+  | .sset var _ _ y _ k _ | .uset var _ y k _ =>
+    let s := s.insert var
+    let s := s.insert y
+    k.collectUsed s
 end
 
 @[inline] def collectUsedAtExpr (s : FVarIdHashSet) (e : Expr) : FVarIdHashSet :=
@@ -827,10 +1094,13 @@ where
     | .cases c => c.alts.forM fun alt => visit alt.getCode
     | .unreach .. | .jmp .. | .return .. => return ()
     | .let decl k =>
-      if let .const declName _ _ _ := decl.value then
+      match decl.value with
+      | .const declName .. | .fap declName .. | .pap declName .. =>
         if decls.any (·.name == declName) then
           modify fun s => s.insert declName
+      | _ => pure ()
       visit k
+    | .uset _ _ _ k _ | .sset _ _ _ _ _ k _ => visit k
 
   go : StateM NameSet Unit :=
     decls.forM (·.value.forCodeM visit)

src/Lean/Compiler/LCNF/Bind.lean

@@ -46,6 +46,7 @@ where
       let alts ← c.alts.mapM fun
         | .alt ctorName params k _ => return .alt ctorName params (← go k)
         | .default k => return .default (← go k)
+        | .ctorAlt info k _ => return .ctorAlt info (← go k)
       if alts.isEmpty then
         throwError "`Code.bind` failed, empty `cases` found"
       let resultType ← mkCasesResultType alts
@@ -67,6 +68,8 @@ where
       eraseCode k
       eraseParam auxParam
       return .unreach typeNew
+    | .sset fvarId i offset y ty k _ => return .sset fvarId i offset y ty (← go k)
+    | .uset fvarId offset y k _ => return .uset fvarId offset y (← go k)
 
 instance : MonadCodeBind CompilerM where
   codeBind := CompilerM.codeBind

src/Lean/Compiler/LCNF/Check.lean

@@ -260,6 +260,6 @@ end Check
 def Decl.check (decl : Decl pu) : CompilerM Unit := do
   match pu with
   | .pure => Check.Pure.run do decl.value.forCodeM (Check.Pure.checkFunDeclCore decl.name decl.params decl.type)
-  | .impure => panic! "Check for impure unimplemented" -- TODO
+  | .impure => return () -- TODO: port the IR check once it actually makes sense to
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -274,10 +274,12 @@ See `normExprImp`
 private partial def normLetValueImp (s : FVarSubst pu) (e : LetValue pu) (translator : Bool) : LetValue pu :=
   match e with
   | .erased | .lit .. => e
-  | .proj _ _ fvarId _ => match normFVarImp s fvarId translator with
+  | .proj _ _ fvarId _ | .sproj _ _ fvarId _ | .uproj _ fvarId _ | .oproj _ fvarId _  =>
+    match normFVarImp s fvarId translator with
     | .fvar fvarId' => e.updateProj! fvarId'
     | .erased => .erased
-  | .const _ _ args _ => e.updateArgs! (normArgsImp s args translator)
+  | .const _ _ args _ | .ctor _ args _ | .fap _ args _ | .pap _ args _ =>
+    e.updateArgs! (normArgsImp s args translator)
   | .fvar fvarId args => match normFVarImp s fvarId translator with
     | .fvar fvarId' => e.updateFVar! fvarId' (normArgsImp s args translator)
     | .erased => .erased
@@ -462,8 +464,16 @@ mutual
         let alts ← c.alts.mapMonoM fun alt =>
           match alt with
           | .alt _ params k _ => return alt.updateAlt! (← normParams params) (← normCodeImp k)
-          | .default k => return alt.updateCode (← normCodeImp k)
+          | .default k | .ctorAlt _ k _ => return alt.updateCode (← normCodeImp k)
         return code.updateCases! resultType discr alts
+    | .sset fvarId i offset y ty k _ =>
+      withNormFVarResult (← normFVar fvarId) fun fvarId => do
+      withNormFVarResult (← normFVar y) fun y => do
+        return code.updateSset! fvarId i offset y (← normExpr ty) (← normCodeImp k)
+    | .uset fvarId offset y k _ =>
+      withNormFVarResult (← normFVar fvarId) fun fvarId => do
+      withNormFVarResult (← normFVar y) fun y => do
+        return code.updateUset! fvarId offset y (← normCodeImp k)
 end
 
 @[inline] def normFunDecl [MonadLiftT CompilerM m] [Monad m] [MonadFVarSubst m pu t] (decl : FunDecl pu) : m (FunDecl pu) := do

src/Lean/Compiler/LCNF/DeclHash.lean

@@ -23,6 +23,7 @@ partial def hashAlt (alt : Alt pu) : UInt64 :=
   match alt with
   | .alt ctorName ps k _ => mixHash (mixHash (hash ctorName) (hash ps)) (hashCode k)
   | .default k => hashCode k
+  | .ctorAlt info k _ => mixHash (hash info) (hashCode k)
 
 partial def hashAlts (alts : Array (Alt pu)) : UInt64 :=
   alts.foldl (fun r a => mixHash r (hashAlt a)) 7
@@ -36,6 +37,10 @@ partial def hashCode (code : Code pu) : UInt64 :=
   | .unreach type => hash type
   | .jmp fvarId args => mixHash (hash fvarId) (hash args)
   | .cases c => mixHash (mixHash (hash c.discr) (hash c.resultType)) (hashAlts c.alts)
+  | .sset fvarId i offset y ty k _ =>
+    mixHash (mixHash (hash fvarId) (hash i)) (mixHash (mixHash (hash offset) (hash y)) (mixHash (hash ty) (hashCode k)))
+  | .uset fvarId offset y k _ =>
+    mixHash (mixHash (hash fvarId) (hash offset)) (mixHash (hash y) (hashCode k))
 
 end
 
@@ -43,6 +48,7 @@ instance : Hashable (Code pu) where
   hash c := hashCode c
 
 deriving instance Hashable for DeclValue
+deriving instance Hashable for Signature
 deriving instance Hashable for Decl
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/DependsOn.lean

@@ -30,9 +30,9 @@ private def argDepOn (a : Arg pu) : M Bool := do
 private def letValueDepOn (e : LetValue pu) : M Bool :=
   match e with
   | .erased | .lit .. => return false
-  | .proj _ _ fvarId _ => fvarDepOn fvarId
+  | .proj _ _ fvarId _ | .oproj _ fvarId _ | .uproj _ fvarId _ | .sproj _ _ fvarId _ => fvarDepOn fvarId
   | .fvar fvarId args => fvarDepOn fvarId <||> args.anyM argDepOn
-  | .const _ _ args _ => args.anyM argDepOn
+  | .const _ _ args _ | .ctor _ args _ | .fap _ args _ | .pap _ args _ => args.anyM argDepOn
 
 private def LetDecl.depOn (decl : LetDecl pu) : M Bool :=
   typeDepOn decl.type <||> letValueDepOn decl.value
@@ -45,6 +45,7 @@ private partial def depOn (c : Code pu) : M Bool :=
   | .jmp fvarId args => fvarDepOn fvarId <||> args.anyM argDepOn
   | .return fvarId => fvarDepOn fvarId
   | .unreach _ => return false
+  | .sset fv1 _ _ fv2 _ k _ | .uset fv1 _ fv2 k _ => fvarDepOn fv1 <||> fvarDepOn fv2 <||> depOn k
 
 @[inline] def LetDecl.dependsOn (decl : LetDecl pu) (s : FVarIdSet) :  Bool :=
   decl.depOn s

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -678,7 +678,7 @@ def Decl.elimDeadBranches (decls : Array (Decl .pure)) : CompilerM (Array (Decl
   decls.mapIdxM fun i decl => if decl.safe then elimDead assignments[i]! decl else return decl
 
 def elimDeadBranches : Pass :=
-  { name := `elimDeadBranches, run := Decl.elimDeadBranches, phase := .mono }
+  { name := `elimDeadBranches, run := Decl.elimDeadBranches, phase := .mono, phaseOut := .mono }
 
 builtin_initialize
   registerTraceClass `Compiler.elimDeadBranches (inherited := true)

src/Lean/Compiler/LCNF/FVarUtil.lean

@@ -67,15 +67,18 @@ instance : TraverseFVar (Arg pu) where
 def LetValue.mapFVarM [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (e : LetValue pu) : m (LetValue pu) := do
   match e with
   | .lit .. | .erased => return e
-  | .proj _ _ fvarId _ => return e.updateProj! (← f fvarId)
-  | .const _ _ args _ => return e.updateArgs! (← args.mapM (TraverseFVar.mapFVarM f))
+  | .proj _ _ fvarId _ | .oproj _ fvarId _ | .sproj _ _ fvarId _ | .uproj _ fvarId _ =>
+    return e.updateProj! (← f fvarId)
+  | .const _ _ args _ | .pap _ args _ | .fap _ args _ | .ctor _ args _ =>
+    return e.updateArgs! (← args.mapM (TraverseFVar.mapFVarM f))
   | .fvar fvarId args => return e.updateFVar! (← f fvarId) (← args.mapM (TraverseFVar.mapFVarM f))
 
 def LetValue.forFVarM [Monad m] (f : FVarId → m Unit) (e : LetValue pu) : m Unit := do
   match e with
   | .lit .. | .erased => return ()
-  | .proj _ _ fvarId _ => f fvarId
-  | .const _ _ args _ => args.forM (TraverseFVar.forFVarM f)
+  | .proj _ _ fvarId _ | .oproj _ fvarId _ | .sproj _ _ fvarId _ | .uproj _ fvarId _ => f fvarId
+  | .const _ _ args _ | .pap _ args _ | .fap _ args _ | .ctor _ args _ =>
+    args.forM (TraverseFVar.forFVarM f)
   | .fvar fvarId args => f fvarId; args.forM (TraverseFVar.forFVarM f)
 
 instance : TraverseFVar (LetValue pu) where
@@ -124,6 +127,10 @@ partial def Code.mapFVarM [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m F
     return Code.updateReturn! c (← f var)
   | .unreach typ =>
     return Code.updateUnreach! c (← Expr.mapFVarM f typ)
+  | .sset fvarId i offset y ty k _ =>
+    return Code.updateSset! c (← f fvarId) i offset (← f y) (← Expr.mapFVarM f ty) (← mapFVarM f k)
+  | .uset fvarId offset y k _ =>
+    return Code.updateUset! c (← f fvarId) offset (← f y) (← mapFVarM f k)
 
 partial def Code.forFVarM [Monad m] (f : FVarId → m Unit) (c : Code pu) : m Unit := do
   match c with
@@ -150,6 +157,15 @@ partial def Code.forFVarM [Monad m] (f : FVarId → m Unit) (c : Code pu) : m Un
   | .return var => f var
   | .unreach typ =>
     Expr.forFVarM f typ
+  | .sset fvarId _ _ y ty k _ =>
+    f fvarId
+    f y
+    Expr.forFVarM f ty
+    forFVarM f k
+  | .uset fvarId _ y k _ =>
+    f fvarId
+    f y
+    forFVarM f k
 
 instance : TraverseFVar (Code pu) where
   mapFVarM := Code.mapFVarM
@@ -187,12 +203,14 @@ instance : TraverseFVar (Alt pu) where
       let params ← params.mapM (Param.mapFVarM f)
       return .alt ctor params (← Code.mapFVarM f c)
     | .default c => return .default (← Code.mapFVarM f c)
+    | .ctorAlt i c _ => return .ctorAlt i (← Code.mapFVarM f c)
   forFVarM f alt := do
     match alt with
     | .alt _ params c _ =>
       params.forM (Param.forFVarM f)
       Code.forFVarM f c
     | .default c => Code.forFVarM f c
+    | .ctorAlt i c _ => Code.forFVarM f c
 
 def anyFVarM [Monad m] [TraverseFVar α] (f : FVarId → m Bool) (x : α) : m Bool := do
   return (← TraverseFVar.forFVarM go x |>.run) matches none

src/Lean/Compiler/LCNF/Internalize.lean

@@ -95,10 +95,12 @@ def internalizeArgs (args : Array (Arg pu)) : InternalizeM pu (Array (Arg pu)) :
 private partial def internalizeLetValue (e : LetValue pu) : InternalizeM pu (LetValue pu) := do
   match e with
   | .erased | .lit .. => return e
-  | .proj _ _ fvarId _ => match (← normFVar fvarId) with
+  | .proj _ _ fvarId _ | .oproj _ fvarId _ | .sproj _ _ fvarId _ | .uproj _ fvarId _ =>
+    match (← normFVar fvarId) with
     | .fvar fvarId' => return e.updateProj! fvarId'
     | .erased => return .erased
-  | .const _ _ args _ => return e.updateArgs! (← internalizeArgs args)
+  | .const _ _ args _ | .fap _ args _ | .pap _ args _ | .ctor _ args _ =>
+    return e.updateArgs! (← internalizeArgs args)
   | .fvar fvarId args => match (← normFVar fvarId) with
     | .fvar fvarId' => return e.updateFVar! fvarId' (← internalizeArgs args)
     | .erased => return .erased
@@ -135,12 +137,19 @@ partial def internalizeCode (code : Code pu) : InternalizeM pu (Code pu) := do
   | .cases c =>
     withNormFVarResult (← normFVar c.discr) fun discr => do
       let resultType ← internalizeExpr c.resultType
-      let internalizeAltCode (k : Code pu) : InternalizeM pu (Code pu) :=
-        internalizeCode k
       let alts ← c.alts.mapM fun
-        | .alt ctorName params k _ => return .alt ctorName (← params.mapM internalizeParam) (← internalizeAltCode k)
-        | .default k => return .default (← internalizeAltCode k)
+        | .alt ctorName params k _ => return .alt ctorName (← params.mapM internalizeParam) (← internalizeCode k)
+        | .default k => return .default (← internalizeCode k)
+        | .ctorAlt i k _ => return .default (← internalizeCode k)
       return .cases ⟨c.typeName, resultType, discr, alts⟩
+  | .sset fvarId i offset y ty k _ =>
+    withNormFVarResult (← normFVar fvarId) fun fvarId => do
+    withNormFVarResult (← normFVar y) fun y => do
+      return .sset fvarId i offset y (← internalizeExpr ty) (← internalizeCode k)
+  | .uset fvarId offset y k _ =>
+    withNormFVarResult (← normFVar fvarId) fun fvarId => do
+    withNormFVarResult (← normFVar y) fun y => do
+      return .uset fvarId offset y (← internalizeCode k)
 
 end
 

src/Lean/Compiler/LCNF/LCtx.lean

@@ -70,6 +70,7 @@ mutual
       match alt with
       | .default k => eraseCode k lctx
       | .alt _ ps k _ => eraseCode k <| eraseParams lctx ps
+      | .ctorAlt _ k _ => eraseCode k lctx
 
   partial def LCtx.eraseCode (code : Code pu) (lctx : LCtx) : LCtx :=
     match code with

src/Lean/Compiler/LCNF/LambdaLifting.lean

@@ -198,6 +198,7 @@ Eliminate all local function declarations.
 -/
 def lambdaLifting : Pass where
   phase      := .mono
+  phaseOut   := .mono
   name       := `lambdaLifting
   run        := fun decls => do
     decls.foldlM (init := #[]) fun decls decl =>
@@ -211,6 +212,7 @@ their body to ensure they are specialized.
 -/
 def eagerLambdaLifting : Pass where
   phase      := .base
+  phaseOut   := .base
   name       := `eagerLambdaLifting
   run        := fun decls => do
     decls.foldlM (init := #[]) fun decls decl => do

src/Lean/Compiler/LCNF/Main.lean

@@ -57,7 +57,7 @@ def checkpoint (stepName : Name) (decls : Array (Decl pu)) (shouldCheck : Bool)
     withOptions (fun opts => opts.set `pp.motives.pi false) do
       let clsName := `Compiler ++ stepName
       if (← Lean.isTracingEnabledFor clsName) then
-        Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl' decl}"
+        Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl' decl (← getPhase)}"
       if shouldCheck then
         decl.check
 
@@ -91,6 +91,8 @@ def run (declNames : Array Name) : CompilerM (Array (Array IR.Decl)) := withAtLe
           LCNF.markDeclPublicRec .base decl
           if let some decl ← getLocalDeclAt? fnName .mono then
             LCNF.markDeclPublicRec .mono decl
+            if let some decl ← getLocalDeclAt? fnName .impure then
+              LCNF.markDeclPublicRec .impure decl
   let declNames ← declNames.filterM (shouldGenerateCode ·)
   if declNames.isEmpty then return #[]
   for declName in declNames do
@@ -107,14 +109,20 @@ def run (declNames : Array Name) : CompilerM (Array (Array IR.Decl)) := withAtLe
   let sccs ← withTraceNode `Compiler.splitSCC (fun _ => return m!"Splitting up SCC") do
     splitScc decls
   sccs.mapM fun decls => do
-    let decls ← runPassManagerPart .pure .pure "compilation (LCNF mono)" manager.monoPassesNoLambda decls isCheckEnabled
-    if (← Lean.isTracingEnabledFor `Compiler.result) then
-      for decl in decls do
-        let decl ← normalizeFVarIds decl
-        Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl}"
-    profileitM Exception "compilation (IR)" (← getOptions) do
-      let irDecls ← IR.toIR decls
-      IR.compile irDecls
+    let decls ← runPassManagerPart .pure .impure "compilation (LCNF mono)" manager.monoPassesNoLambda decls isCheckEnabled
+    withPhase .impure do
+      let decls ← runPassManagerPart .impure .impure "compilation (LCNF impure)" manager.impurePasses decls isCheckEnabled
+
+      if (← Lean.isTracingEnabledFor `Compiler.result) then
+        for decl in decls do
+          let decl ← normalizeFVarIds decl
+          Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl (← getPhase)}"
+
+      -- TODO consider doing this in one go afterwards in a separate mapM and running clearPure to save memory
+      -- or consider running clear? unclear
+      profileitM Exception "compilation (IR)" (← getOptions) do
+        let irDecls ← IR.toIR decls
+        IR.compile irDecls
 where
   runPassManagerPart (inPhase outPhase : Purity) (profilerName : String)
       (passes : Array Pass) (decls : Array (Decl inPhase)) (isCheckEnabled : Bool) :
@@ -136,10 +144,6 @@ end PassManager
 def compile (declNames : Array Name) : CoreM (Array (Array IR.Decl)) :=
   CompilerM.run <| PassManager.run declNames
 
-def showDecl (phase : Phase) (declName : Name) : CoreM Format := do
-  let some decl ← getDeclAt? declName phase | return "<not-available>"
-  ppDecl' decl
-
 def main (declNames : Array Name) : CoreM Unit := do
   withTraceNode `Compiler (fun _ => return m!"compiling: {declNames}") do
     CompilerM.run <| discard <| PassManager.run declNames

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -99,7 +99,4 @@ def getOtherDeclMonoType (declName : Name) : CoreM Expr := do
     monoTypeExt.insert declName type
     return type
 
-def getOtherDeclImpureType (_declName : Name) : CoreM Expr := do
-  panic! "Other decl impure type unimplemented" -- TODO
-
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/OtherDecl.lean

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Compiler.LCNF.MonoTypes
+public import Lean.Compiler.LCNF.CompilerM
+import Lean.Compiler.LCNF.MonoTypes
+import Lean.Compiler.LCNF.ToImpureType
 
 public section
 

src/Lean/Compiler/LCNF/PassManager.lean

@@ -74,7 +74,7 @@ structure Pass where
   /--
   The actual pass function, operating on the `Decl`s.
   -/
-  run : Array (Decl phase.toPurity) → CompilerM (Array (Decl phase.toPurity))
+  run : Array (Decl phase.toPurity) → CompilerM (Array (Decl phaseOut.toPurity))
 
 instance : Inhabited Pass where
   default := { phase := .base, name := default, run := fun decls => return decls }
@@ -102,6 +102,7 @@ structure PassManager where
   basePasses : Array Pass
   monoPasses : Array Pass
   monoPassesNoLambda : Array Pass
+  impurePasses : Array Pass
   deriving Inhabited
 
 namespace Pass
@@ -200,7 +201,8 @@ def run (manager : PassManager) (installer : PassInstaller) : CoreM PassManager
     return { manager with basePasses := (← installer.install manager.basePasses) }
   | .mono =>
     return { manager with monoPasses := (← installer.install manager.monoPasses) }
-  | .impure => panic! "Pass manager support for impure unimplemented" -- TODO
+  | .impure =>
+    return { manager with impurePasses := (← installer.install manager.monoPasses) }
 
 private unsafe def getPassInstallerUnsafe (declName : Name) : CoreM PassInstaller := do
   ofExcept <| (← getEnv).evalConstCheck PassInstaller (← getOptions) ``PassInstaller declName

src/Lean/Compiler/LCNF/Passes.lean

@@ -19,6 +19,7 @@ public import Lean.Compiler.LCNF.StructProjCases
 public import Lean.Compiler.LCNF.ExtractClosed
 public import Lean.Compiler.LCNF.Visibility
 public import Lean.Compiler.LCNF.Simp
+public import Lean.Compiler.LCNF.ToImpure
 
 public section
 
@@ -52,6 +53,7 @@ def trace (phase := Phase.base) : Pass where
 def saveBase : Pass where
   occurrence := 0
   phase := .base
+  phaseOut := .base
   name := `saveBase
   run decls := decls.mapM fun decl => do
     (← normalizeFVarIds decl).saveBase
@@ -61,12 +63,23 @@ def saveBase : Pass where
 def saveMono : Pass where
   occurrence := 0
   phase := .mono
+  phaseOut := .mono
   name := `saveMono
   run decls := decls.mapM fun decl => do
     (← normalizeFVarIds decl).saveMono
     return decl
   shouldAlwaysRunCheck := true
 
+def saveImpure : Pass where
+  occurrence := 0
+  phase := .impure
+  phaseOut := .impure
+  name := `saveImpure
+  run decls := decls.mapM fun decl => do
+    (← normalizeFVarIds decl).saveImpure
+    return decl
+  shouldAlwaysRunCheck := true
+
 end Pass
 
 open Pass
@@ -124,6 +137,11 @@ def builtinPassManager : PassManager := {
     saveMono,  -- End of mono phase
     inferVisibility (phase := .mono),
     extractClosed,
+    toImpure,
+  ]
+  impurePasses := #[
+    saveImpure, -- End of impure phase
+    inferVisibility (phase := .impure),
   ]
 }
 
@@ -169,6 +187,7 @@ builtin_initialize
 builtin_initialize
   registerTraceClass `Compiler.saveBase (inherited := true)
   registerTraceClass `Compiler.saveMono (inherited := true)
+  registerTraceClass `Compiler.saveImpure (inherited := true)
   registerTraceClass `Compiler.trace (inherited := true)
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/PhaseExt.lean

@@ -86,16 +86,30 @@ def setDeclTransparent (env : Environment) (phase : Phase) (declName : Name) : E
     getTransparencyExt phase |>.modifyState env fun s =>
       (declName :: s.1, s.2.insert declName)
 
-abbrev DeclExtState (pu : Purity) := PHashMap Name (Decl pu)
+abbrev AbstractDeclExtState (pu : Purity) (β : Purity → Type) := PHashMap Name (β pu)
+
+private def sortedEntries (s : AbstractDeclExtState pu β) (lt : β pu → β pu → Bool) : Array (β pu) :=
+  let decls := s.foldl (init := #[]) fun ps _ v => ps.push v
+  decls.qsort lt
+
+private def replayFn (phase : Phase) : ReplayFn (AbstractDeclExtState phase.toPurity β) :=
+  fun oldState newState _ otherState =>
+    newState.foldl (init := otherState) fun otherState k v =>
+      if oldState.contains k then
+        otherState
+      else
+        otherState.insert k v
+
+private def statsFn (state : AbstractDeclExtState pu β) : Format :=
+  let numEntries := state.foldl (init := 0) (fun count _ _ => count + 1)
+  format "number of local entries: " ++ format numEntries
+
+abbrev DeclExtState (pu : Purity) := AbstractDeclExtState pu Decl
 
 private abbrev declLt (a b : Decl pu) :=
   Name.quickLt a.name b.name
 
-private def sortedDecls (s : DeclExtState pu) : Array (Decl pu) :=
-  let decls := s.foldl (init := #[]) fun ps _ v => ps.push v
-  decls.qsort declLt
-
-private abbrev findAtSorted? (decls : Array (Decl pu)) (declName : Name) : Option (Decl pu) :=
+private abbrev findDeclAtSorted? (decls : Array (Decl pu)) (declName : Name) : Option (Decl pu) :=
   let tmpDecl : Decl pu := default
   let tmpDecl := { tmpDecl with name := declName }
   decls.binSearch tmpDecl declLt
@@ -114,7 +128,7 @@ def mkDeclExt (phase : Phase) (name : Name := by exact decl_name%) :
     addImportedFn := fun _ => pure {},
     addEntryFn := fun s decl => s.insert decl.name decl
     exportEntriesFnEx env s level := Id.run do
-      let mut entries := sortedDecls s
+      let mut entries := sortedEntries s declLt
       if level != .private then
         entries := entries.filterMap fun decl => do
           guard <| isDeclPublic env decl.name
@@ -123,25 +137,63 @@ def mkDeclExt (phase : Phase) (name : Name := by exact decl_name%) :
           else
             some { decl with value := .extern { entries := [.opaque] } }
       return entries
-    statsFn := fun s =>
-      let numEntries := s.foldl (init := 0) (fun count _ _ => count + 1)
-      format "number of local entries: " ++ format numEntries
+    statsFn := statsFn,
     asyncMode := .sync,
-    replay? := some <| fun oldState newState _ otherState =>
-      newState.foldl (init := otherState) fun otherState k v =>
-        if oldState.contains k then
-          otherState
-        else
-          otherState.insert k v
+    replay? := some (replayFn phase)
   }
 
+
 builtin_initialize baseExt : DeclExt .pure ← mkDeclExt .base
 builtin_initialize monoExt : DeclExt .pure ← mkDeclExt .mono
-builtin_initialize impureExt : DeclExt .impure ← mkDeclExt .impure
+builtin_initialize impureExt : EnvExtension (DeclExtState .impure) ←
+  registerEnvExtension (mkInitial := pure {}) (asyncMode := .sync) (replay? := some (replayFn .impure))
+
+
+abbrev SigExtState (pu : Purity) := AbstractDeclExtState pu Signature
+
+@[expose] def SigExt (pu : Purity) :=
+   PersistentEnvExtension (Signature pu) (Signature pu) (SigExtState pu)
+
+instance : Inhabited (SigExt pu) :=
+  inferInstanceAs (Inhabited (PersistentEnvExtension (Signature pu) (Signature pu) (SigExtState pu)))
+
+private abbrev sigLt (a b : Signature pu) :=
+  Name.quickLt a.name b.name
+
+private abbrev findSigAtSorted? (sigs : Array (Signature pu)) (declName : Name) : Option (Signature pu) :=
+  let tmpSig : Signature pu := default
+  let tmpSig := { tmpSig with name := declName }
+  sigs.binSearch tmpSig sigLt
+
+def mkSigDeclExt (phase : Phase) (name : Name := by exact decl_name%) :
+    IO (SigExt phase.toPurity) :=
+  registerPersistentEnvExtension {
+    name,
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun s sig => s.insert sig.name sig
+    exportEntriesFnEx env s level := Id.run do
+      let mut entries := sortedEntries s sigLt
+      if level != .private then
+        entries := entries.filterMap fun sig => do
+          guard <| isDeclPublic env sig.name
+          some sig
+      return entries
+    statsFn := statsFn,
+    asyncMode := .sync,
+    replay? := some (replayFn phase)
+  }
+
+builtin_initialize impureSigExt : SigExt .impure ← mkSigDeclExt .impure
 
 def getDeclCore? (env : Environment) (ext : DeclExt pu) (declName : Name) : Option (Decl pu) :=
   match env.getModuleIdxFor? declName with
-  | some modIdx => findAtSorted? (ext.getModuleEntries env modIdx) declName
+  | some modIdx => findDeclAtSorted? (ext.getModuleEntries env modIdx) declName
+  | none        => ext.getState env |>.find? declName
+
+def getSigCore? (env : Environment) (ext : SigExt pu) (declName : Name) : Option (Signature pu) :=
+  match env.getModuleIdxFor? declName with
+  | some modIdx => findSigAtSorted? (ext.getModuleEntries env modIdx) declName
   | none        => ext.getState env |>.find? declName
 
 def getBaseDecl? (declName : Name) : CoreM (Option (Decl .pure)) := do
@@ -150,8 +202,11 @@ def getBaseDecl? (declName : Name) : CoreM (Option (Decl .pure)) := do
 def getMonoDecl? (declName : Name) : CoreM (Option (Decl .pure)) := do
   return getDeclCore? (← getEnv) monoExt declName
 
-def getImpureDecl? (declName : Name) : CoreM (Option (Decl .impure)) := do
-  return getDeclCore? (← getEnv) impureExt declName
+def getLocalImpureDecl? (declName : Name) : CoreM (Option (Decl .impure)) := do
+  return impureExt.getState (← getEnv) |>.find? declName
+
+def getImpureSignature? (declName : Name) : CoreM (Option (Signature .impure)) := do
+  return impureSigExt.getState (← getEnv) |>.find? declName
 
 def saveBaseDeclCore (env : Environment) (decl : Decl .pure) : Environment :=
   baseExt.addEntry env decl
@@ -160,7 +215,8 @@ def saveMonoDeclCore (env : Environment) (decl : Decl .pure) : Environment :=
   monoExt.addEntry env decl
 
 def saveImpureDeclCore (env : Environment) (decl : Decl .impure) : Environment :=
-  impureExt.addEntry env decl
+  let env := impureExt.modifyState env (fun s => s.insert decl.name decl)
+  impureSigExt.addEntry env decl.toSignature
 
 def Decl.saveBase (decl : Decl .pure) : CoreM Unit :=
   modifyEnv (saveBaseDeclCore · decl)
@@ -184,7 +240,7 @@ def getDeclAt? (declName : Name) (phase : Phase) : CoreM (Option (Decl phase.toP
   match phase with
   | .base => getBaseDecl? declName
   | .mono => getMonoDecl? declName
-  | .impure => getImpureDecl? declName
+  | .impure => throwError "Internal compiler error: getDecl? on impure is unuspported for now"
 
 @[inline]
 def getDecl? (declName : Name) : CompilerM (Option ((pu : Purity) × Decl pu)) := do
@@ -202,10 +258,4 @@ def getLocalDecl? (declName : Name) : CompilerM (Option ((pu : Purity) × Decl p
   let some decl ← getLocalDeclAt? declName (← getPhase) | return none
   return some ⟨_, decl⟩
 
-def getExt (phase : Phase) : DeclExt phase.toPurity :=
-  match phase with
-  | .base => baseExt
-  | .mono => monoExt
-  | .impure => impureExt
-
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -64,6 +64,17 @@ def ppLitValue (lit : LitValue) : M Format := do
   | .nat v | .uint8 v | .uint16 v | .uint32 v | .uint64 v | .usize v => return format v
   | .str v => return format (repr v)
 
+private def formatCtorInfo : CtorInfo → Format
+  | { name := name, cidx := cidx, usize := usize, ssize := ssize, .. } => Id.run do
+    let mut r := f!"ctor_{cidx}"
+    if usize > 0 || ssize > 0 then
+      r := f!"{r}.{usize}.{ssize}"
+    if name != Name.anonymous then
+      r := f!"{r}[{name}]"
+    r
+
+instance : ToFormat CtorInfo := ⟨private_decl% formatCtorInfo⟩
+
 def ppLetValue (e : LetValue pu) : M Format := do
   match e with
   | .erased => return "◾"
@@ -71,6 +82,12 @@ def ppLetValue (e : LetValue pu) : M Format := do
   | .proj _ i fvarId _ => return f!"{← ppFVar fvarId} # {i}"
   | .fvar fvarId args => return f!"{← ppFVar fvarId}{← ppArgs args}"
   | .const declName us args _ => return f!"{← ppExpr (.const declName us)}{← ppArgs args}"
+  | .ctor i args _ => return f!"{i} {← ppArgs args}"
+  | .fap declName args _ => return f!"{declName}{← ppArgs args}"
+  | .pap declName args _ => return f!"pap {declName}{← ppArgs args}"
+  | .oproj i fvarId _ => return f!"proj[{i}] {← ppFVar fvarId}"
+  | .uproj i fvarId _ => return f!"uproj[{i}] {← ppFVar fvarId}"
+  | .sproj i offset fvarId _ => return f!"sproj[{i}, {offset}] {← ppFVar fvarId}"
 
 def ppParam (param : Param pu) : M Format := do
   let borrow := if param.borrow then "@&" else ""
@@ -92,7 +109,9 @@ def getFunType (ps : Array (Param pu)) (type : Expr) : CoreM Expr :=
   if type.isErased then
     pure type
   else
-    instantiateForall type (ps.map (mkFVar ·.fvarId))
+    match pu with
+    | .pure => instantiateForall type (ps.map (mkFVar ·.fvarId))
+    | .impure => return type
 
 mutual
   partial def ppFunDecl (funDecl : FunDecl pu) : M Format := do
@@ -102,6 +121,7 @@ mutual
     match alt with
     | .default k => return f!"| _ =>{indentD (← ppCode k)}"
     | .alt ctorName params k _ => return f!"| {ctorName}{← ppParams params} =>{indentD (← ppCode k)}"
+    | .ctorAlt info k _ => return f!"| {info.name} =>{indentD (← ppCode k)}"
 
   partial def ppCode (c : Code pu) : M Format := do
     match c with
@@ -116,6 +136,14 @@ mutual
         return f!"⊥ : {← ppExpr type}"
       else
         return "⊥"
+    | .sset fvarId i offset y ty k _ =>
+      if pp.letVarTypes.get (← getOptions) then
+        return f!"sset {← ppFVar fvarId} [{i}, {offset}] : {← ppExpr ty} := {← ppFVar y} " ++ ";" ++ .line ++ (← ppCode k)
+      else
+        return f!"sset {← ppFVar fvarId} [{i}, {offset}] := {← ppFVar y} " ++ ";" ++ .line ++ (← ppCode k)
+    | .uset fvarId i y k _ =>
+      return f!"uset {← ppFVar fvarId} [{i}] := {← ppFVar y} " ++ ";" ++ .line ++ (← ppCode k)
+
 
   partial def ppDeclValue (b : DeclValue pu) : M Format := do
     match b with
@@ -147,10 +175,10 @@ def ppFunDecl (decl : FunDecl pu) : CompilerM Format :=
 Execute `x` in `CoreM` without modifying `Core`s state.
 This is useful if we want make sure we do not affect the next free variable id.
 -/
-def runCompilerWithoutModifyingState (x : CompilerM α) : CoreM α := do
+def runCompilerWithoutModifyingState (phase : Phase) (x : CompilerM α) : CoreM α := do
   let s ← get
   try
-    x |>.run {}
+    x |>.run (phase := phase)
   finally
     set s
 
@@ -159,16 +187,16 @@ Similar to `ppDecl`, but in `CoreM`, and it does not assume
 `decl` has already been internalized.
 This function is used for debugging purposes.
 -/
-def ppDecl' (decl : Decl pu) : CoreM Format := do
-  runCompilerWithoutModifyingState do
+def ppDecl' (decl : Decl pu) (phase : Phase) : CoreM Format := do
+  runCompilerWithoutModifyingState phase do
     ppDecl (← decl.internalize)
 
 /--
 Similar to `ppCode`, but in `CoreM`, and it does not assume
 `code` has already been internalized.
 -/
-def ppCode' (code : Code pu) : CoreM Format := do
-  runCompilerWithoutModifyingState do
+def ppCode' (code : Code pu) (phase : Phase) : CoreM Format := do
+  runCompilerWithoutModifyingState phase do
     ppCode (← code.internalize)
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/Probing.lean

@@ -58,6 +58,7 @@ where
       go k
     | .cases cs => cs.alts.forM (go ·.getCode)
     | .jmp .. | .return .. | .unreach .. => return ()
+    | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
   start (decls : Array (Decl pu)) : StateRefT (Array (LetValue pu)) CompilerM Unit :=
     decls.forM (·.value.forCodeM go)
 
@@ -72,6 +73,7 @@ where
     | .jp decl k => modify (·.push decl); go decl.value; go k
     | .cases cs => cs.alts.forM (go ·.getCode)
     | .jmp .. | .return .. | .unreach .. => return ()
+    | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
 
   start (decls : Array (Decl pu)) : StateRefT (Array (FunDecl pu)) CompilerM Unit :=
     decls.forM (·.value.forCodeM go)
@@ -84,6 +86,7 @@ where
   | .fun decl k _ | .jp decl k => go decl.value <||> go k
   | .cases cs => cs.alts.anyM (go ·.getCode)
   | .jmp .. | .return .. | .unreach .. => return false
+  | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
 
 partial def filterByFun (pu : Purity) (f : FunDecl pu → CompilerM Bool) : Probe (Decl pu) (Decl pu) :=
   filter (·.value.isCodeAndM go)
@@ -93,6 +96,7 @@ where
   | .fun decl k _ => do if (← f decl) then return true else go decl.value <||> go k
   | .cases cs => cs.alts.anyM (go ·.getCode)
   | .jmp .. | .return .. | .unreach .. => return false
+  | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
 
 partial def filterByJp (pu : Purity) (f : FunDecl pu → CompilerM Bool) : Probe (Decl pu) (Decl pu) :=
   filter (·.value.isCodeAndM go)
@@ -103,6 +107,7 @@ where
   | .jp decl k => do if (← f decl) then return true else go decl.value <||> go k
   | .cases cs => cs.alts.anyM (go ·.getCode)
   | .jmp .. | .return .. | .unreach .. => return false
+  | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
 
 partial def filterByFunDecl (pu : Purity) (f : FunDecl pu → CompilerM Bool) :
     Probe (Decl pu) (Decl pu):=
@@ -113,6 +118,7 @@ where
   | .fun decl k _ | .jp decl k => do if (← f decl) then return true else go decl.value <||> go k
   | .cases cs => cs.alts.anyM (go ·.getCode)
   | .jmp .. | .return .. | .unreach .. => return false
+  | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
 
 partial def filterByCases (pu : Purity) (f : Cases pu → CompilerM Bool) : Probe (Decl pu) (Decl pu) :=
   filter (·.value.isCodeAndM go)
@@ -122,6 +128,7 @@ where
   | .fun decl k _ | .jp decl k => go decl.value <||> go k
   | .cases cs => do if (← f cs) then return true else cs.alts.anyM (go ·.getCode)
   | .jmp .. | .return .. | .unreach .. => return false
+  | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
 
 partial def filterByJmp (pu : Purity) (f : FVarId → Array (Arg pu) → CompilerM Bool) :
     Probe (Decl pu) (Decl pu) :=
@@ -133,6 +140,7 @@ where
   | .cases cs => cs.alts.anyM (go ·.getCode)
   | .jmp fn var => f fn var
   | .return .. | .unreach .. => return false
+  | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
 
 partial def filterByReturn (pu : Purity) (f : FVarId → CompilerM Bool) : Probe (Decl pu) (Decl pu) :=
   filter (·.value.isCodeAndM go)
@@ -143,6 +151,7 @@ where
   | .cases cs => cs.alts.anyM (go ·.getCode)
   | .jmp .. | .unreach .. => return false
   | .return var  => f var
+  | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
 
 partial def filterByUnreach (pu : Purity) (f : Expr → CompilerM Bool) : Probe (Decl pu) (Decl pu) :=
   filter (·.value.isCodeAndM go)
@@ -153,6 +162,7 @@ where
   | .cases cs => cs.alts.anyM (go ·.getCode)
   | .jmp .. | .return .. => return false
   | .unreach typ  => f typ
+  | .sset _ _ _ _ _ k _ | .uset _ _ _ k _ => go k
 
 @[inline]
 def declNames (pu : Purity) : Probe (Decl pu) Name :=
@@ -174,31 +184,6 @@ def tail (n : Nat) : Probe α α := fun data => return data[(data.size - n)...*]
 @[inline]
 def head (n : Nat) : Probe α α := fun data => return data[*...n]
 
-def runOnDeclsNamed (declNames : Array Name) (phase : Phase := Phase.base)
-    (probe : Probe (Decl phase.toPurity) β) : CoreM (Array β) := do
-  let ext := getExt phase
-  let env ← getEnv
-  let decls ← declNames.mapM fun name => do
-    let some decl := getDeclCore? env ext name | throwError "decl `{name}` not found"
-    return decl
-  probe decls |>.run (phase := phase)
-
-def runOnModule (moduleName : Name) (phase : Phase := Phase.base)
-    (probe : Probe (Decl phase.toPurity) β) : CoreM (Array β) := do
-  let ext := getExt phase
-  let env ← getEnv
-  let some modIdx := env.getModuleIdx? moduleName | throwError "module `{moduleName}` not found"
-  let decls := ext.getModuleEntries env modIdx
-  probe decls |>.run (phase := phase)
-
-def runGlobally  (phase : Phase := Phase.base) (probe : Probe (Decl phase.toPurity) β) : CoreM (Array β) := do
-  let ext := getExt phase
-  let env ← getEnv
-  let mut decls := #[]
-  for modIdx in *...env.allImportedModuleNames.size do
-    decls := decls.append <| ext.getModuleEntries env modIdx
-  probe decls |>.run (phase := phase)
-
 def toPass [ToString β] (phase : Phase) (probe : Probe (Decl phase.toPurity) β) : Pass where
   phase := phase
   name := `probe

src/Lean/Compiler/LCNF/ReduceArity.lean

@@ -188,6 +188,7 @@ def Decl.reduceArity (decl : Decl .pure) : CompilerM (Array (Decl .pure)) := do
 
 def reduceArity : Pass where
   phase := .mono
+  phaseOut := .mono
   name  := `reduceArity
   run   := fun decls => do
     decls.foldlM (init := #[]) fun decls decl => return decls ++ (← decl.reduceArity)

src/Lean/Compiler/LCNF/Renaming.lean

@@ -50,8 +50,13 @@ partial def Code.applyRenaming (code : Code pu) (r : Renaming) : CompilerM (Code
       match alt with
       | .default k => return alt.updateCode (← k.applyRenaming r)
       | .alt _ ps k _ => return alt.updateAlt! (← ps.mapMonoM (·.applyRenaming r)) (← k.applyRenaming r)
+      | .ctorAlt _ k _ => return alt.updateCode (← k.applyRenaming r)
     return code.updateAlts! alts
   | .jmp .. | .unreach .. | .return .. => return code
+  | .sset fvarId i offset y ty k _ =>
+    return code.updateSset! fvarId i offset y ty (← k.applyRenaming r)
+  | .uset fvarId offset y k _ =>
+    return code.updateUset! fvarId offset y (← k.applyRenaming r)
 end
 
 def Decl.applyRenaming (decl : Decl pu) (r : Renaming) : CompilerM (Decl pu) := do

src/Lean/Compiler/LCNF/Specialize.lean

@@ -556,9 +556,10 @@ def main (decls : Array (Decl .pure)) : CompilerM (Array (Decl .pure)) := do
 end Specialize
 
 public def specialize : Pass where
-  phase := .base
-  name  := `specialize
-  run   := Specialize.main
+  phase    := .base
+  phaseOut := .base
+  name     := `specialize
+  run      := Specialize.main
 
 builtin_initialize
   registerTraceClass `Compiler.specialize (inherited := true)

src/Lean/Compiler/LCNF/SplitSCC.lean

@@ -23,15 +23,18 @@ where
   goCode (c : Code pu) : StateRefT (Std.HashSet Name) BaseIO Unit := do
     match c with
     | .let decl k =>
-      if let .const name .. := decl.value then
+      match decl.value with
+      | .const name .. | .fap name .. | .pap name .. =>
         if scc.contains name then
           modify fun s => s.insert name
+      | _ => pure ()
       goCode k
     | .fun decl k _ | .jp decl k =>
       goCode decl.value
       goCode k
     | .cases cases => cases.alts.forM (·.forCodeM goCode)
     | .jmp .. | .return .. | .unreach .. => return ()
+    | .uset _ _ _ k _ | .sset _ _ _ _ _ k _ => goCode k
 
 end SplitScc
 

src/Lean/Compiler/LCNF/StructProjCases.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Compiler.LCNF.PrettyPrinter
+import Lean.Compiler.LCNF.MonoTypes
 
 public section
 

src/Lean/Compiler/LCNF/ToExpr.lean

@@ -107,7 +107,18 @@ partial def Code.toExprM (code : Code pu) : ToExprM Expr := do
         let body ← withParams params do mkLambdaM params (← k.toExprM)
         return mkApp (mkConst ctorName) body
       | .default k => k.toExprM
+      | .ctorAlt i k _ => do
+        let body ← k.toExprM
+        return mkApp (mkConst i.name) body
     return mkAppN (mkConst `cases) (#[← c.discr.toExprM] ++ alts)
+  | .sset fvarId i offset y ty k _ =>
+    let value := mkApp5 (mkConst `sset) (.fvar fvarId) (toExpr i) (toExpr offset) (.fvar y) ty
+    let body ← withFVar fvarId k.toExprM
+    return .letE `dummy (mkConst ``Unit) value body true
+  | .uset fvarId offset y k _ =>
+    let value := mkApp3 (mkConst `uset) (.fvar fvarId) (toExpr offset) (.fvar y)
+    let body ← withFVar fvarId k.toExprM
+    return .letE `dummy (mkConst ``Unit) value body true
 end
 
 public def Code.toExpr (code : Code pu) (xs : Array FVarId := #[]) : Expr :=

src/Lean/Compiler/LCNF/ToImpure.lean

@@ -0,0 +1,326 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving, Cameron Zwarich
+-/
+module
+
+prelude
+public import Lean.Compiler.LCNF.CompilerM
+import Lean.Compiler.LCNF.ToImpureType
+public import Lean.Compiler.LCNF.PassManager
+import Lean.Compiler.LCNF.PhaseExt
+
+namespace Lean.Compiler.LCNF
+
+open ImpureType
+
+/--
+Marks an extern definition to be guaranteed to always return tagged values.
+This information is used to optimize reference counting in the compiler.
+-/
+@[builtin_doc]
+builtin_initialize taggedReturnAttr : TagAttribute ←
+  registerTagAttribute `tagged_return "mark extern definition to always return tagged values"
+
+structure BuilderState where
+  /--
+  We keep around a substitution here because we run a second trivial structure elimination when
+  converting to impure. This elimination is aware of the fact that `Void` is irrelevant while the first
+  one in isn't because we are still pure. However, impure does not allow us to have bindings of
+  the form `let x := y` which might occur when for example projecting out of a trivial structure
+  where previously a binding would've been `let x := proj y i` and now becomes `let x := y`.
+  For this reason we carry around these kinds of bindings in this substitution and apply it whenever
+  we access an fvar in the conversion.
+  -/
+  subst : LCNF.FVarSubst .pure := {}
+
+abbrev ToImpureM := StateRefT BuilderState CompilerM
+
+instance : MonadFVarSubst ToImpureM .pure true where
+  getSubst := return (← get).subst
+
+instance : MonadFVarSubstState ToImpureM .pure where
+  modifySubst f := modify fun s => { s with subst := f s.subst }
+
+def Param.toImpure (p : Param .pure) : ToImpureM (Param .impure) := do
+  let type ← toImpureType p.type
+  if type.isVoid || type.isErased then
+    addSubst p.fvarId .erased
+
+  let p := { p with type }
+  modifyLCtx fun lctx => lctx.addParam p
+  return p
+
+def lowerProj (base : FVarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo) :
+    LetValue .impure × Expr :=
+  match field with
+  | .object i irType => ⟨.oproj i base, irType⟩
+  | .usize i => ⟨.uproj i base, ImpureType.usize⟩
+  | .scalar _ offset irType => ⟨.sproj (ctorInfo.size + ctorInfo.usize) offset base, irType⟩
+  | .erased => ⟨.erased, ImpureType.erased⟩
+  | .void => ⟨.erased, ImpureType.void⟩
+
+def Arg.toImpure (arg : Arg .pure) : ToImpureM (Arg .impure) := do
+  let arg ← normArg arg
+  match arg with
+  | .fvar fvarId => return .fvar fvarId
+  | .erased | .type .. => return .erased
+
+public def lowerResultType (type : Expr) (arity : Nat) : CoreM Expr :=
+  toImpureType (resultTypeForArity type arity)
+where resultTypeForArity (type : Lean.Expr) (arity : Nat) : Expr :=
+  if arity == 0 then
+    type
+  else
+    match type with
+    | .forallE _ _ b _ => resultTypeForArity b (arity - 1)
+    | .const ``lcErased _ => mkConst ``lcErased
+    | _ => panic! "invalid arity"
+
+def litValueImpureType (v : LCNF.LitValue) : Expr :=
+  match v with
+  | .nat n =>
+    if n < UInt32.size then ImpureType.tagged else ImpureType.tobject
+  | .str .. => ImpureType.object
+  | .uint8 .. => ImpureType.uint8
+  | .uint16 .. => ImpureType.uint16
+  | .uint32 .. => ImpureType.uint32
+  | .uint64 .. => ImpureType.uint64
+  | .usize .. => ImpureType.usize
+
+mutual
+
+partial def lowerLet (decl : LetDecl .pure) (k : Code .pure) : ToImpureM (Code .impure) := do
+  let value ← normLetValue decl.value
+  match value with
+  | .lit litValue =>
+    let type := litValueImpureType litValue
+    let decl := ⟨decl.fvarId, decl.binderName, type, .lit litValue⟩
+    continueLet decl
+  | .proj typeName i fvarId =>
+    if let some info ← hasTrivialImpureStructure? typeName then
+      if info.fieldIdx == i then
+        addSubst decl.fvarId (.fvar fvarId)
+      else
+        addSubst decl.fvarId .erased
+      k.toImpure
+    else
+      match (← normFVar fvarId) with
+      | .fvar fvarId =>
+        let some (.inductInfo { ctors := [ctorName], .. }) := (← Lean.getEnv).find? typeName
+          | panic! "projection of non-structure type"
+        let ⟨ctorInfo, fields⟩ ← getCtorLayout ctorName
+        let ⟨result, type⟩ := lowerProj fvarId ctorInfo fields[i]!
+        match result with
+        | .erased => continueErased decl.fvarId
+        | _ => continueLet ⟨decl.fvarId, decl.binderName, type, result⟩
+      | .erased =>
+        addSubst decl.fvarId .erased
+        k.toImpure
+  | .const name _ args =>
+    let irArgs ← args.mapM (·.toImpure)
+    if let some sig ← getImpureSignature? name then
+      return (← mkApplication name sig.params.size irArgs)
+    if let some decl ← getMonoDecl? name then
+      return (← mkApplication name decl.params.size irArgs)
+
+    let env ← Lean.getEnv
+    match env.find? name with
+    | some (.ctorInfo ctorVal) =>
+      if let some info ← hasTrivialImpureStructure? ctorVal.induct then
+        let arg := args[info.numParams + info.fieldIdx]!
+        LCNF.addSubst decl.fvarId arg
+        k.toImpure
+      else
+        let type ← nameToImpureType ctorVal.induct
+        if type.isScalar then
+          let decl := ⟨decl.fvarId, decl.binderName, type, .lit (.impureTypeScalarNumLit type ctorVal.cidx)⟩
+          let res ← continueLet decl
+          return res
+
+        let ⟨ctorInfo, fields⟩ ← getCtorLayout name
+        let irArgs := irArgs.extract (start := ctorVal.numParams)
+        if irArgs.size != fields.size then
+          -- An overapplied constructor arises from compiler
+          -- transformations on unreachable code
+          return .unreach (ImpureType.tobject) -- TODO: need a more precise type for this
+
+        let objArgs : Array (Arg .impure) ← do
+          let mut result : Array (Arg .impure) := #[]
+          for h : i in *...fields.size do
+            match fields[i] with
+            | .object .. =>
+              result := result.push irArgs[i]!
+            | .usize .. | .scalar .. | .erased | .void => pure ()
+          pure result
+        let rec lowerNonObjectFields : ToImpureM (Code .impure) :=
+          let rec loop (i : Nat) : ToImpureM (Code .impure) := do
+            match irArgs[i]? with
+            | some (.fvar fvarId) =>
+              match fields[i]! with
+              | .usize usizeIdx =>
+                let k ← loop (i + 1)
+                return .uset decl.fvarId usizeIdx fvarId k
+              | .scalar _ offset argType =>
+                let k ← loop (i + 1)
+                return .sset decl.fvarId (ctorInfo.size + ctorInfo.usize) offset fvarId argType k
+              | .object .. | .erased | .void => loop (i + 1)
+            | some .erased => loop (i + 1)
+            | none => k.toImpure
+          loop 0
+        let decl := ⟨decl.fvarId, decl.binderName, ctorInfo.type, .ctor ctorInfo objArgs⟩
+        modifyLCtx fun lctx => lctx.addLetDecl decl
+        return .let decl (← lowerNonObjectFields)
+    | some (.defnInfo ..) | some (.opaqueInfo ..) => mkFap name irArgs
+    | some (.axiomInfo ..) | .some (.quotInfo ..) | .some (.inductInfo ..) | .some (.thmInfo ..) =>
+      -- Should have been caught by `ToLCNF`
+      throwError f!"ToImpure: unexpected use of noncomputable declaration `{name}`; please report this issue"
+    | some (.recInfo ..) =>
+      throwError f!"code generator does not support recursor `{name}` yet, consider using 'match ... with' and/or structural recursion"
+    | none => panic! "reference to unbound name"
+  | .fvar fvarId irArgs =>
+    let irArgs ← irArgs.mapM (·.toImpure)
+    let type := (← toImpureType decl.type).boxed
+    let decl := ⟨decl.fvarId, decl.binderName, type, .fvar fvarId irArgs⟩
+    continueLet decl
+  | .erased =>
+    continueErased decl.fvarId
+where
+  continueLet (decl : LetDecl .impure) : ToImpureM (Code .impure) := do
+    modifyLCtx fun lctx => lctx.addLetDecl decl
+    let k ← k.toImpure
+    return .let decl k
+
+  continueErased (fvarId : FVarId) : ToImpureM (Code .impure) := do
+    addSubst fvarId .erased
+    k.toImpure
+
+  mkFap (name : Name) (args : Array (Arg .impure)) : ToImpureM (Code .impure) := do
+    continueLet ⟨decl.fvarId, decl.binderName, ← toImpureType decl.type, .fap name args⟩
+
+  mkPap (name : Name) (args : Array (Arg .impure)) : ToImpureM (Code .impure) := do
+    continueLet ⟨decl.fvarId, decl.binderName, ImpureType.object, .pap name args⟩
+
+  mkOverApplication (name : Name) (numParams : Nat) (args : Array (Arg .impure)) :
+      ToImpureM (Code .impure) := do
+    let type := (← toImpureType decl.type).boxed
+    let firstArgs := args.extract 0 numParams
+    let restArgs := args.extract numParams args.size
+    let auxDecl ← mkLetDecl (.str decl.binderName "overap") ImpureType.object (.fap name firstArgs)
+    let resDecl := ⟨decl.fvarId, decl.binderName, type, .fvar auxDecl.fvarId restArgs⟩
+    modifyLCtx fun lctx => lctx.addLetDecl resDecl
+    return .let auxDecl (.let resDecl (← k.toImpure))
+
+  mkApplication (name : Name) (numParams : Nat) (args : Array (Arg .impure)) :
+      ToImpureM (Code .impure) := do
+    let numArgs := args.size
+    if numArgs < numParams then
+      mkPap name args
+    else if numArgs == numParams then
+      mkFap name args
+    else
+      mkOverApplication name numParams args
+
+partial def Code.toImpure (c : Code .pure) : ToImpureM (Code .impure) := do
+  match c with
+  | .let decl k => lowerLet decl k
+  | .jp decl k =>
+    let params ← decl.params.mapM (·.toImpure)
+    let value ← decl.value.toImpure
+    let k ← k.toImpure
+    let type ← lowerResultType decl.type params.size
+    let decl := ⟨decl.fvarId, decl.binderName, params, type, value⟩
+    modifyLCtx fun lctx => lctx.addFunDecl decl
+    return .jp decl k
+  | .jmp fvarId args => return .jmp fvarId (← args.mapM (·.toImpure))
+  | .cases c =>
+    if let some info ← hasTrivialImpureStructure? c.typeName then
+      assert! c.alts.size == 1
+      let .alt ctorName ps k := c.alts[0]! | unreachable!
+      assert! ctorName == info.ctorName
+      assert! info.fieldIdx < ps.size
+      for idx in 0...ps.size do
+        let p := ps[idx]!
+        if idx == info.fieldIdx then
+          addSubst p.fvarId (.fvar c.discr)
+        else
+          addSubst p.fvarId .erased
+      k.toImpure
+    else
+      -- `casesOn` for inductive predicates should have already been expanded.
+      withNormFVarResult (← normFVar c.discr) fun discr => do
+        let resultType ← toImpureType c.resultType
+        let alts ← c.alts.mapM (·.toImpure discr)
+        return .cases ⟨(← nameToImpureType c.typeName).getAppFn.constName!, resultType, discr, alts⟩
+  | .return fvarId =>
+    withNormFVarResult (← normFVar fvarId) fun fvarId => do
+      return .return fvarId
+  | .unreach type => return .unreach (← toImpureType type)
+  | .fun .. => panic! "all local functions should be λ-lifted"
+
+partial def Alt.toImpure (discr : FVarId) (alt : Alt .pure) : ToImpureM (Alt .impure) := do
+  match alt with
+  | .alt ctorName params k =>
+    let ⟨ctorInfo, fields⟩ ← getCtorLayout ctorName
+    let lowerParams (params : Array (LCNF.Param .pure)) (fields : Array CtorFieldInfo) :
+        ToImpureM (Code .impure) := do
+      let rec loop (i : Nat) : ToImpureM (Code .impure) := do
+        match params[i]?, fields[i]? with
+        | some param, some field =>
+          let ⟨result, type⟩ := lowerProj discr ctorInfo field
+          match result with
+          | .erased =>
+            addSubst param.fvarId .erased
+            loop (i + 1)
+          | _ =>
+            let decl := ⟨param.fvarId, param.binderName, type, result⟩
+            modifyLCtx fun lctx => lctx.addLetDecl decl
+            return .let decl (← loop (i + 1))
+        | none, none => k.toImpure
+        | _, _ => panic! "mismatched fields and params"
+      loop 0
+    let body ← lowerParams params fields
+    return .ctorAlt ctorInfo body
+  | .default k => return .default (← k.toImpure)
+
+end
+
+def Decl.toImpure (decl : Decl .pure) : CompilerM (Decl .impure) := do
+  go |>.run' {}
+where
+  go : ToImpureM (Decl .impure) := do
+    let decl ← lowerDecl
+    decl.saveImpure
+    return decl
+
+  lowerDecl : ToImpureM (Decl .impure) := do
+    let params ← decl.params.mapM (·.toImpure)
+    let mut resultType ← lowerResultType decl.type decl.params.size
+    let taggedReturn := taggedReturnAttr.hasTag (← getEnv) decl.name
+    match decl.value with
+    | .code code =>
+      if taggedReturn then
+        throwError m!"Error while compiling function '{decl.name}': @[tagged_return] is only valid for extern declarations"
+      let value ← code.toImpure
+      return { decl with type := resultType, params, value := .code value }
+    | .extern externAttrData =>
+      if taggedReturn then
+        if resultType.isScalar then
+          throwError m!"@[tagged_return] on function '{decl.name}' with scalar return type {resultType}"
+        else
+          resultType := ImpureType.tagged
+
+      return { decl with type := resultType, params, value := .extern externAttrData }
+
+public def toImpure : Pass where
+  name     := `toImpure
+  run      := (·.mapM (·.toImpure))
+  phase    := .mono
+  phaseOut := .impure
+  shouldAlwaysRunCheck := true
+
+builtin_initialize
+  registerTraceClass `Compiler.toImpure (inherited := true)
+
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ToImpureType.lean

@@ -0,0 +1,251 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Cameron Zwarich, Henrik Böving
+-/
+module
+
+prelude
+public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.Irrelevant
+import Lean.Compiler.LCNF.MonoTypes
+
+namespace Lean.Compiler.LCNF
+
+def impureTypeForEnum (numCtors : Nat) : Expr :=
+  if numCtors == 1 then
+    ImpureType.tagged
+  else if numCtors < Nat.pow 2 8 then
+    ImpureType.uint8
+  else if numCtors < Nat.pow 2 16 then
+    ImpureType.uint16
+  else if numCtors < Nat.pow 2 32 then
+    ImpureType.uint32
+  else
+    ImpureType.tagged
+
+builtin_initialize impureTypeExt : CacheExtension Name Expr ←
+  CacheExtension.register
+
+builtin_initialize impureTrivialStructureInfoExt :
+    CacheExtension Name (Option TrivialStructureInfo) ←
+  CacheExtension.register
+
+/--
+The idea of this function is the same as in `ToMono`, however the notion of "irrelevancy" has
+changed because we now have the `void` type which can only be erased in impure context and thus at
+earliest at the conversion from mono to impure.
+-/
+public def hasTrivialImpureStructure? (declName : Name) : CoreM (Option TrivialStructureInfo) := do
+  let isVoidType type := do
+    let type ← Meta.whnfD type
+    return type matches .proj ``Subtype 0 (.app (.const ``Void.nonemptyType []) _)
+  let irrelevantType type :=
+    Meta.isProp type <||> Meta.isTypeFormerType type <||> isVoidType type
+  Irrelevant.hasTrivialStructure? impureTrivialStructureInfoExt irrelevantType declName
+
+public def nameToImpureType (name : Name) : CoreM Expr := do
+  match (← impureTypeExt.find? name) with
+  | some type => return type
+  | none =>
+    let type ← fillCache
+    impureTypeExt.insert name type
+    return type
+where fillCache : CoreM Expr := do
+    match name with
+    | ``UInt8 => return ImpureType.uint8
+    | ``UInt16 => return ImpureType.uint16
+    | ``UInt32 => return ImpureType.uint32
+    | ``UInt64 => return ImpureType.uint64
+    | ``USize => return ImpureType.usize
+    | ``Float => return ImpureType.float
+    | ``Float32 => return ImpureType.float32
+    | ``lcErased => return ImpureType.erased
+    -- `Int` is specified as an inductive type with two constructors that have relevant arguments,
+    -- but it has the same runtime representation as `Nat` and thus needs to be special-cased here.
+    | ``Int => return ImpureType.tobject
+    | ``lcVoid => return ImpureType.void
+    | _ =>
+      let env ← Lean.getEnv
+      let some (.inductInfo inductiveVal) := env.find? name | return ImpureType.tobject
+      let ctorNames := inductiveVal.ctors
+      let numCtors := ctorNames.length
+      let mut numScalarCtors := 0
+      for ctorName in ctorNames do
+        let some (.ctorInfo ctorInfo) := env.find? ctorName | unreachable!
+        let hasRelevantField ← Meta.MetaM.run' <|
+                               Meta.forallTelescope ctorInfo.type fun params _ => do
+          for field in params[ctorInfo.numParams...*] do
+            let fieldType ← field.fvarId!.getType
+            let lcnfFieldType ← toLCNFType fieldType
+            let monoFieldType ← toMonoType lcnfFieldType
+            if !monoFieldType.isErased then return true
+          return false
+        if !hasRelevantField then
+          numScalarCtors := numScalarCtors + 1
+      if numScalarCtors == numCtors then
+        return impureTypeForEnum numCtors
+      else if numScalarCtors == 0 then
+        return ImpureType.object
+      else
+        return ImpureType.tobject
+
+def isAnyProducingType (type : Expr) : Bool :=
+  match type with
+  | .const ``lcAny _ => true
+  | .forallE _ _ b _ => isAnyProducingType b
+  | _ => false
+
+public partial def toImpureType (type : Expr) : CoreM Expr := do
+  match type with
+  | .const name _ => visitApp name #[]
+  | .app .. =>
+    -- All mono types are in headBeta form.
+    let .const name _ := type.getAppFn | unreachable!
+    visitApp name type.getAppArgs
+  | .forallE _ _ b _ =>
+    -- Type formers are erased, but can be used polymorphically as
+    -- an arrow type producing `lcAny`. The runtime representation of
+    -- erased values is a tagged scalar, so this means that any such
+    -- polymorphic type must be represented as `.tobject`.
+    if isAnyProducingType b then
+      return ImpureType.tobject
+    else
+      return ImpureType.object
+  | .mdata _ b => toImpureType b
+  | _ => unreachable!
+where
+  visitApp (declName : Name) (args : Array Lean.Expr) : CoreM Expr := do
+    if let some info ← hasTrivialImpureStructure? declName then
+      let ctorType ← getOtherDeclBaseType info.ctorName []
+      let monoType ← toMonoType (getParamTypes (← instantiateForall ctorType args[*...info.numParams]))[info.fieldIdx]!
+      toImpureType monoType
+    else
+      nameToImpureType declName
+
+public inductive CtorFieldInfo where
+  | erased
+  | object (i : Nat) (type : Expr)
+  | usize  (i : Nat)
+  | scalar (sz : Nat) (offset : Nat) (type : Expr)
+  | void
+  deriving Inhabited
+
+namespace CtorFieldInfo
+
+def format : CtorFieldInfo → Format
+  | erased => "◾"
+  | void => "void"
+  | object i type => f!"obj@{i}:{type}"
+  | usize i    => f!"usize@{i}"
+  | scalar sz offset type => f!"scalar#{sz}@{offset}:{type}"
+
+instance : ToFormat CtorFieldInfo := ⟨format⟩
+
+end CtorFieldInfo
+
+public structure CtorLayout where
+  ctorInfo : CtorInfo
+  fieldInfo : Array CtorFieldInfo
+  deriving Inhabited
+
+builtin_initialize ctorLayoutExt : CacheExtension Name CtorLayout ←
+  CacheExtension.register
+
+public def getCtorLayout (ctorName : Name) : CoreM CtorLayout := do
+  match (← ctorLayoutExt.find? ctorName) with
+  | some info => return info
+  | none =>
+    let info ← fillCache
+    ctorLayoutExt.insert ctorName info
+    return info
+where fillCache := do
+  let .some (.ctorInfo ctorInfo) := (← getEnv).find? ctorName | unreachable!
+  Meta.MetaM.run' <| Meta.forallTelescopeReducing ctorInfo.type fun params _ => do
+    let mut fields : Array CtorFieldInfo := .emptyWithCapacity ctorInfo.numFields
+    let mut nextIdx := 0
+    let mut has1BScalar := false
+    let mut has2BScalar := false
+    let mut has4BScalar := false
+    let mut has8BScalar := false
+    for field in params[ctorInfo.numParams...(ctorInfo.numParams + ctorInfo.numFields)] do
+      let fieldType ← field.fvarId!.getType
+      let lcnfFieldType ← LCNF.toLCNFType fieldType
+      let monoFieldType ← LCNF.toMonoType lcnfFieldType
+      let irFieldType ← toImpureType monoFieldType
+      let ctorField ← match irFieldType with
+      | ImpureType.object | ImpureType.tagged | ImpureType.tobject => do
+        let i := nextIdx
+        nextIdx := nextIdx + 1
+        pure <| .object i irFieldType
+      | ImpureType.usize => pure <| .usize 0
+      | ImpureType.erased => .pure <| .erased
+      | ImpureType.void => .pure <| .void
+      | ImpureType.uint8 =>
+        has1BScalar := true
+        .pure <| .scalar 1 0 ImpureType.uint8
+      | ImpureType.uint16 =>
+        has2BScalar := true
+        .pure <| .scalar 2 0 ImpureType.uint16
+      | ImpureType.uint32 =>
+        has4BScalar := true
+        .pure <| .scalar 4 0 ImpureType.uint32
+      | ImpureType.uint64 =>
+        has8BScalar := true
+        .pure <| .scalar 8 0 ImpureType.uint64
+      | ImpureType.float32 =>
+        has4BScalar := true
+        .pure <| .scalar 4 0 ImpureType.float32
+      | ImpureType.float =>
+        has8BScalar := true
+        .pure <| .scalar 8 0 ImpureType.float
+      | _ => unreachable!
+      fields := fields.push ctorField
+    let numObjs := nextIdx
+    ⟨fields, nextIdx⟩ := Id.run <| StateT.run (s := nextIdx) <| fields.mapM fun field => do
+      match field with
+      | .usize _ => do
+        let i ← modifyGet fun nextIdx => (nextIdx, nextIdx + 1)
+        return .usize i
+      | .object .. | .scalar .. | .erased | .void => return field
+    let numUSize := nextIdx - numObjs
+    let adjustScalarsForSize (fields : Array CtorFieldInfo) (size : Nat) (nextOffset : Nat)
+        : Array CtorFieldInfo × Nat :=
+      Id.run <| StateT.run (s := nextOffset) <| fields.mapM fun field => do
+        match field with
+        | .scalar sz _ type => do
+          if sz == size then
+            let offset ← modifyGet fun nextOffset => (nextOffset, nextOffset + sz)
+            return .scalar sz offset type
+          else
+            return field
+        | .object .. | .usize _ | .erased | .void => return field
+    let mut nextOffset := 0
+    if has8BScalar then
+      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 8 nextOffset
+    if has4BScalar then
+      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 4 nextOffset
+    if has2BScalar then
+      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 2 nextOffset
+    if has1BScalar then
+      ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 1 nextOffset
+    return {
+      ctorInfo := {
+        name := ctorName
+        cidx := ctorInfo.cidx
+        size := numObjs
+        usize := numUSize
+        ssize := nextOffset
+      }
+      fieldInfo := fields
+    }
+
+public def getOtherDeclImpureType (declName : Name) : CoreM Expr := do
+  match (← impureTypeExt.find? declName) with
+  | some type => return type
+  | none =>
+    let type ← toImpureType (← getOtherDeclMonoType declName)
+    monoTypeExt.insert declName type
+    return type
+
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -14,6 +14,8 @@ import Lean.Meta.CasesInfo
 import Lean.Meta.WHNF
 import Lean.Compiler.NoncomputableAttr
 import Lean.AddDecl
+import Lean.Compiler.LCNF.Util
+
 public section
 namespace Lean.Compiler.LCNF
 namespace ToLCNF

src/Lean/Compiler/LCNF/ToMono.lean

@@ -9,6 +9,8 @@ prelude
 public import Lean.Compiler.ImplementedByAttr
 public import Lean.Compiler.LCNF.InferType
 public import Lean.Compiler.NoncomputableAttr
+import Lean.Compiler.LCNF.MonoTypes
+public import Lean.Compiler.LCNF.Irrelevant
 
 public section
 

src/Lean/Compiler/LCNF/Types.lean

@@ -21,6 +21,9 @@ namespace LCNF
 def erasedExpr := mkConst ``lcErased
 def anyExpr := mkConst ``lcAny
 
+def _root_.Lean.Expr.isVoid (e : Expr) :=
+  e.isAppOf ``lcVoid
+
 def _root_.Lean.Expr.isErased (e : Expr) :=
   e.isAppOf ``lcErased
 

src/Lean/Compiler/LCNF/Visibility.lean

@@ -23,13 +23,12 @@ private partial def collectUsedDecls (code : Code pu) (s : NameSet := {}) : Name
   | .cases c =>
     c.alts.foldl (init := s) fun s alt =>
       match alt with
-      | .default k => collectUsedDecls k s
-      | .alt _ _ k _ => collectUsedDecls k s
+      | .default k | .alt _ _ k _ | .ctorAlt _ k _ => collectUsedDecls k s
   | _ => s
 where
   collectLetValue (e : LetValue pu) (s : NameSet) : NameSet :=
     match e with
-    | .const declName .. => s.insert declName
+    | .const declName .. | .fap declName .. | .pap declName .. => s.insert declName
     | _ => s
 
 private def shouldExportBody (decl : Decl pu) : CompilerM Bool := do

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// update thy!
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/ctor_layout.lean

@@ -4,10 +4,10 @@ open Lean
 open Lean.IR
 
 def test : CoreM Unit := do
-   let ctorLayout ← getCtorLayout ``Lean.IR.Expr.reuse;
+   let ctorLayout ← Compiler.LCNF.getCtorLayout ``Lean.IR.Expr.reuse;
    ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
    IO.println "---";
-   let ctorLayout ← getCtorLayout ``Subtype.mk;
+   let ctorLayout ← Compiler.LCNF.getCtorLayout ``Subtype.mk;
    ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
    pure ()
 

tests/lean/ctor_layout.lean.expected.out

@@ -1,6 +1,6 @@
 obj@0:tobj
 obj@1:obj
-scalar#1@0:u8
+scalar#1@0:UInt8
 obj@2:obj
 ---
 obj@0:tobj

tests/lean/reduceArity.lean

@@ -3,12 +3,12 @@ open Lean Compiler LCNF
 @[noinline] def double (x : Nat) := x + x
 
 set_option pp.funBinderTypes true
-set_option trace.Compiler.result true in
+set_option trace.Compiler.saveMono true in
 def g (n : Nat) (a b : α) (f : α → α) :=
   match n with
   | 0 => a
   | n+1 => f (g n a b f)
 
-set_option trace.Compiler.result true in
+set_option trace.Compiler.saveMono true in
 def h (n : Nat) (a : Nat) :=
   g n a a double + g a n n double

tests/lean/reduceArity.lean.expected.out

@@ -1,4 +1,4 @@
-[Compiler.result] size: 9
+[Compiler.saveMono] size: 9
     def g._redArg (n : Nat) (a : lcAny) (f : lcAny → lcAny) : lcAny :=
       let zero := 0;
       let isZero := Nat.decEq n zero;
@@ -11,17 +11,13 @@
         let _x.2 := g._redArg n.1 a f;
         let _x.3 := f _x.2;
         return _x.3
-[Compiler.result] size: 1
+[Compiler.saveMono] size: 1
     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: 1
-    def h._closed_0 : Nat → Nat :=
-      let _x.1 := double;
-      return _x.1
-[Compiler.result] size: 4
+[Compiler.saveMono] size: 4
     def h (n : Nat) (a : Nat) : Nat :=
-      let _x.1 := h._closed_0;
+      let _x.1 := double;
       let _x.2 := g._redArg n a _x.1;
       let _x.3 := g._redArg a n _x.1;
       let _x.4 := Nat.add _x.2 _x.3;

tests/lean/run/Decidable-decide-erasure.lean

@@ -3,21 +3,21 @@ import Lean.Compiler.LCNF.Probing
 
 open Lean.Compiler.LCNF
 
+/--
+trace: [Compiler.saveBase] size: 3
+    def f a : Bool :=
+      let _x.1 := 1;
+      let _x.2 := instDecidableEqNat a _x.1;
+      let _x.3 := decide ◾ _x.2;
+      return _x.3
+[Compiler.saveMono] size: 2
+    def f a : Bool :=
+      let _x.1 := 1;
+      let _x.2 := Nat.decEq a _x.1;
+      return _x.2
+-/
+#guard_msgs in
+set_option trace.Compiler.saveBase true in
+set_option trace.Compiler.saveMono true in
 def f (a : Nat) : Bool :=
   decide (a = 1)
-
--- This is only required until the new code generator is enabled.
-run_meta Lean.Compiler.compile #[``f]
-
-def countCalls : Probe (Decl .pure) Nat :=
-  Probe.getLetValues .pure >=>
-  Probe.filter (fun e => return e matches .const `Decidable.decide ..) >=>
-  Probe.count
-
-#eval do
-  let numCalls <- Probe.runOnDeclsNamed #[`f] (phase := .base) <| countCalls
-  assert! numCalls == #[1]
-
-#eval do
-  let numCalls <- Probe.runOnDeclsNamed #[`f] (phase := .mono) <| countCalls
-  assert! numCalls == #[0]

tests/lean/run/emptyLcnf.lean

@@ -5,13 +5,13 @@ inductive MyEmpty
 def f (x : MyEmpty) : Nat :=
   MyEmpty.casesOn _ x
 
-set_option trace.Compiler.result true
+set_option trace.Compiler.saveMono true
 /--
-trace: [Compiler.result] size: 0
+trace: [Compiler.saveMono] size: 0
     def f x : Nat :=
       ⊥
 ---
-trace: [Compiler.result] size: 5
+trace: [Compiler.saveMono] size: 5
     def _private.lean.run.emptyLcnf.0._eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EST.Out Lean.Exception
       lcAny PUnit :=
       let _x.10 := Lean.Compiler.compile _x.1 _y.7 _y.8 _y.9;
@@ -21,42 +21,15 @@ trace: [Compiler.result] size: 5
         return _x.13
       | EST.Out.error a.14 a.15 =>
         return _x.10
-[Compiler.result] size: 1
-    def _private.lean.run.emptyLcnf.0._eval._closed_0 : String :=
-      let _x.1 := "f";
-      return _x.1
-[Compiler.result] size: 2
-    def _private.lean.run.emptyLcnf.0._eval._closed_1 : Lean.Name :=
-      let _x.1 := _eval._closed_0.2;
-      let _x.2 := Lean.Name.mkStr1 _x.1;
-      return _x.2
-[Compiler.result] size: 2
-    def _private.lean.run.emptyLcnf.0._eval._closed_2 : Array Lean.Name :=
-      let _x.1 := 1;
-      let _x.2 := Array.mkEmpty ◾ _x.1;
-      return _x.2
-[Compiler.result] size: 3
-    def _private.lean.run.emptyLcnf.0._eval._closed_3 : Array Lean.Name :=
-      let _x.1 := _eval._closed_1.2;
-      let _x.2 := _eval._closed_2.2;
-      let _x.3 := Array.push ◾ _x.2 _x.1;
-      return _x.3
-[Compiler.result] size: 3
-    def _private.lean.run.emptyLcnf.0._eval._closed_4 : Lean.Elab.Term.Context →
-      lcAny → Lean.Meta.Context → lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit :=
-      let _x.1 := PUnit.unit;
-      let _x.2 := _eval._closed_3.2;
-      let _f.3 := _eval._lam_0.2 _x.2 _x.1;
-      return _f.3
-[Compiler.result] size: 8
+[Compiler.saveMono] size: 8
     def _private.lean.run.emptyLcnf.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
-      let _x.4 := _eval._closed_0.2;
-      let _x.5 := _eval._closed_1.2;
+      let _x.4 := "f";
+      let _x.5 := Lean.Name.mkStr1 _x.4;
       let _x.6 := 1;
-      let _x.7 := _eval._closed_2.2;
-      let _x.8 := _eval._closed_3.2;
+      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._closed_4.2;
+      let _f.10 := _eval._lam_0.2 _x.8 _x.9;
       let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
       return _x.11
 -/

tests/lean/run/erased.lean

@@ -18,14 +18,14 @@ open Lean.Compiler
 set_option pp.explicit true
 set_option pp.funBinderTypes true
 set_option pp.letVarTypes true
-set_option trace.Compiler.result true
+set_option trace.Compiler.saveMono true
 /--
-trace: [Compiler.result] size: 1
+trace: [Compiler.saveMono] size: 1
     def Erased.mk (α : lcErased) (a : lcAny) : PSigma lcErased lcAny :=
       let _x.1 : PSigma lcErased lcAny := PSigma.mk ◾ ◾ ◾ ◾;
       return _x.1
 ---
-trace: [Compiler.result] size: 5
+trace: [Compiler.saveMono] size: 5
     def _private.lean.run.erased.0._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 : lcVoid) : EST.Out
       Lean.Exception lcAny PUnit :=
@@ -36,55 +36,21 @@ trace: [Compiler.result] size: 5
         return _x.13
       | EST.Out.error (a.14 : Lean.Exception) (a.15 : lcVoid) =>
         return _x.10
-[Compiler.result] size: 1
-    def _private.lean.run.erased.0._eval._closed_0 : String :=
-      let _x.1 : String := "Erased";
-      return _x.1
-[Compiler.result] size: 1
-    def _private.lean.run.erased.0._eval._closed_1 : String :=
-      let _x.1 : String := "mk";
-      return _x.1
-[Compiler.result] size: 3
-    def _private.lean.run.erased.0._eval._closed_2 : Lean.Name :=
-      let _x.1 : String := _eval._closed_1.2;
-      let _x.2 : String := _eval._closed_0.2;
-      let _x.3 : Lean.Name := Lean.Name.mkStr2 _x.2 _x.1;
-      return _x.3
-[Compiler.result] size: 2
-    def _private.lean.run.erased.0._eval._closed_3 : Array Lean.Name :=
-      let _x.1 : Nat := 1;
-      let _x.2 : Array Lean.Name := Array.mkEmpty ◾ _x.1;
-      return _x.2
-[Compiler.result] size: 3
-    def _private.lean.run.erased.0._eval._closed_4 : Array Lean.Name :=
-      let _x.1 : Lean.Name := _eval._closed_2.2;
-      let _x.2 : Array Lean.Name := _eval._closed_3.2;
-      let _x.3 : Array Lean.Name := Array.push ◾ _x.2 _x.1;
-      return _x.3
-[Compiler.result] size: 3
-    def _private.lean.run.erased.0._eval._closed_5 : Lean.Elab.Term.Context →
-      lcAny → Lean.Meta.Context → lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit :=
-      let _x.1 : PUnit := PUnit.unit;
-      let _x.2 : Array Lean.Name := _eval._closed_4.2;
-      let _f.3 : Lean.Elab.Term.Context →
-        lcAny →
-          Lean.Meta.Context →
-            lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._lam_0.2 _x.2 _x.1;
-      return _f.3
-[Compiler.result] size: 9
+[Compiler.saveMono] size: 9
     def _private.lean.run.erased.0._eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcVoid) : EST.Out
       Lean.Exception lcAny PUnit :=
-      let _x.4 : String := _eval._closed_0.2;
-      let _x.5 : String := _eval._closed_1.2;
-      let _x.6 : Lean.Name := _eval._closed_2.2;
+      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 := _eval._closed_3.2;
-      let _x.9 : Array Lean.Name := _eval._closed_4.2;
+      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 → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._closed_5.2;
+            lcAny →
+              Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._lam_0.2 _x.9 _x.10;
       let _x.12 : EST.Out Lean.Exception lcAny PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 a.3;
       return _x.12
 -/

tests/lean/run/floatLetIn.lean

@@ -15,7 +15,7 @@ opaque State.restore (abc : Nat) (size : Nat) (s : State) : State
 
 def StateFn := State → State
 
-set_option trace.Compiler.result true
+set_option trace.Compiler.saveMono true
 
 /-!
 The `floatLetIn` pass moves values (here `st.size`) into one branch if they are only used in that
@@ -23,7 +23,7 @@ branch.
 -/
 
 /--
-trace: [Compiler.result] size: 7
+trace: [Compiler.saveMono] size: 7
     def test1 st : State :=
       cases st : State
       | State.mk abc xyz bool =>
@@ -49,7 +49,7 @@ This doesn't occur if it would destroy linearity.
 -/
 
 /--
-trace: [Compiler.result] size: 10
+trace: [Compiler.saveMono] size: 10
     def test2 fn st : State :=
       cases st : State
       | State.mk abc xyz bool =>
@@ -79,11 +79,17 @@ Passing a value to a function as a borrowed parameter doesn't count as a linear
 can be happily passed through it.
 -/
 
+/--
+trace: [Compiler.saveMono] size: 0
+    def State.remake @&s : State :=
+      extern
+-/
+#guard_msgs in
 @[extern]
 opaque State.remake (s : @& State) : State
 
 /--
-trace: [Compiler.result] size: 10
+trace: [Compiler.saveMono] size: 10
     def test3 st : State :=
       let st := State.remake st;
       cases st : State
@@ -113,7 +119,7 @@ This also doesn't occur if there are indirect uses of a variable in both branche
 -/
 
 /--
-trace: [Compiler.result] size: 13
+trace: [Compiler.saveMono] size: 13
     def test4 st : State :=
       cases st : State
       | State.mk abc xyz bool =>

tests/lean/run/inlineApp.lean

@@ -7,7 +7,7 @@ def h (x : Nat) :=
   inline <| f (x + x)
 
 /--
-trace: [Compiler.result] size: 8
+trace: [Compiler.saveMono] size: 8
     def h x : Nat :=
       let _x.1 := Nat.add x x;
       let _x.2 := 1;
@@ -19,48 +19,22 @@ trace: [Compiler.result] size: 8
       let _x.8 := Nat.add _x.6 _x.7;
       return _x.8
 ---
-trace: [Compiler.result] size: 1
+trace: [Compiler.saveMono] size: 1
     def _private.lean.run.inlineApp.0._eval._lam_0 _x.1 _y.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 : EST.Out Lean.Exception
       lcAny PUnit :=
       let _x.9 := Lean.Compiler.compile _x.1 _y.6 _y.7 _y.8;
       return _x.9
-[Compiler.result] size: 1
-    def _private.lean.run.inlineApp.0._eval._closed_0 : String :=
-      let _x.1 := "h";
-      return _x.1
-[Compiler.result] size: 2
-    def _private.lean.run.inlineApp.0._eval._closed_1 : Lean.Name :=
-      let _x.1 := _eval._closed_0.2;
-      let _x.2 := Lean.Name.mkStr1 _x.1;
-      return _x.2
-[Compiler.result] size: 2
-    def _private.lean.run.inlineApp.0._eval._closed_2 : Array Lean.Name :=
-      let _x.1 := 1;
-      let _x.2 := Array.mkEmpty ◾ _x.1;
-      return _x.2
-[Compiler.result] size: 3
-    def _private.lean.run.inlineApp.0._eval._closed_3 : Array Lean.Name :=
-      let _x.1 := _eval._closed_1.2;
-      let _x.2 := _eval._closed_2.2;
-      let _x.3 := Array.push ◾ _x.2 _x.1;
-      return _x.3
-[Compiler.result] size: 2
-    def _private.lean.run.inlineApp.0._eval._closed_4 : Lean.Elab.Term.Context →
-      lcAny → Lean.Meta.Context → lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit :=
-      let _x.1 := _eval._closed_3.2;
-      let _f.2 := _eval._lam_0.2 _x.1;
-      return _f.2
-[Compiler.result] size: 7
+[Compiler.saveMono] size: 7
     def _private.lean.run.inlineApp.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
-      let _x.4 := _eval._closed_0.2;
-      let _x.5 := _eval._closed_1.2;
+      let _x.4 := "h";
+      let _x.5 := Lean.Name.mkStr1 _x.4;
       let _x.6 := 1;
-      let _x.7 := _eval._closed_2.2;
-      let _x.8 := _eval._closed_3.2;
-      let _f.9 := _eval._closed_4.2;
+      let _x.7 := Array.mkEmpty ◾ _x.6;
+      let _x.8 := Array.push ◾ _x.7 _x.5;
+      let _f.9 := _eval._lam_0.2 _x.8;
       let _x.10 := Lean.Elab.Command.liftTermElabM._redArg _f.9 a.1 a.2 a.3;
       return _x.10
 -/
 #guard_msgs in
-set_option trace.Compiler.result true in
+set_option trace.Compiler.saveMono true in
 #eval Lean.Compiler.compile #[``h]

tests/lean/run/opaqueCodeGen.lean

@@ -1,22 +1,22 @@
 import Lean
 
 /--
-trace: [Compiler.result] size: 1
+trace: [Compiler.saveMono] size: 1
     def f x : Nat :=
       let _x.1 := Nat.add x x;
       return _x.1
 -/
 #guard_msgs in
-set_option trace.Compiler.result true in
+set_option trace.Compiler.saveMono true in
 opaque f : Nat → Nat :=
   fun x => Nat.add x x
 
 /--
-trace: [Compiler.result] size: 0
+trace: [Compiler.saveMono] size: 0
     def g a._@._internal._hyg.1 a._@._internal._hyg.2 : Nat :=
       extern
 -/
 #guard_msgs in
-set_option trace.Compiler.result true in
+set_option trace.Compiler.saveMono true in
 @[extern "lean_nat_gcd"]
 opaque g : Nat → Nat → Nat

tests/lean/run/tagged_return_1.lean

@@ -30,7 +30,7 @@ error: Error while compiling function 'illegal1': @[tagged_return] is only valid
 @[tagged_return]
 opaque illegal1 (a : Nat) : Nat
 
-/-- error: @[tagged_return] on function 'illegal2' with scalar return type u8 -/
+/-- error: @[tagged_return] on function 'illegal2' with scalar return type UInt8 -/
 #guard_msgs in
 @[extern "mytest", tagged_return]
 opaque illegal2 (a : Nat) : UInt8

tests/lean/run/toDeclEtaBug.lean

@@ -7,13 +7,13 @@ import Lean
     x + 2
 
 /--
-trace: [Compiler.result] size: 2
+trace: [Compiler.saveMono] size: 2
     def g c : Nat :=
       let _x.1 := 2;
       let _x.2 := Nat.add c _x.1;
       return _x.2
 -/
 #guard_msgs in
-set_option trace.Compiler.result true in
+set_option trace.Compiler.saveMono true in
 def g (c : Nat) : Nat :=
   f true false c

tests/lean/unhygienicCode.lean

@@ -1,7 +1,7 @@
 import Lean.Hygiene
 open Lean
 
-set_option trace.Compiler.result true
+set_option trace.Compiler.extractClosed true
 --set_option trace.compiler.ir.result true
 
 -- The following function should not allocate any closures,

tests/lean/unhygienicCode.lean.expected.out

@@ -1,49 +1,49 @@
-[Compiler.result] size: 3
+[Compiler.extractClosed] size: 3
     def foo._closed_0 : SourceInfo :=
       let _x.1 := false;
       let _x.2 := Syntax.missing;
       let _x.3 := @SourceInfo.fromRef _x.2 _x.1;
       return _x.3
-[Compiler.result] size: 1
+[Compiler.extractClosed] size: 1
     def foo._closed_1 : String :=
       let _x.1 := "UnhygienicMain";
       return _x.1
-[Compiler.result] size: 2
+[Compiler.extractClosed] size: 2
     def foo._closed_2 : Name :=
       let _x.1 := foo._closed_1;
       let _x.2 := Name.mkStr1 _x.1;
       return _x.2
-[Compiler.result] size: 1
+[Compiler.extractClosed] size: 1
     def foo._closed_3 : String :=
       let _x.1 := "term_+_";
       return _x.1
-[Compiler.result] size: 2
+[Compiler.extractClosed] size: 2
     def foo._closed_4 : Name :=
       let _x.1 := foo._closed_3;
       let _x.2 := Name.mkStr1 _x.1;
       return _x.2
-[Compiler.result] size: 1
+[Compiler.extractClosed] size: 1
     def foo._closed_5 : String :=
       let _x.1 := "a";
       return _x.1
-[Compiler.result] size: 2
+[Compiler.extractClosed] size: 2
     def foo._closed_6 : Substring.Raw :=
       let _x.1 := foo._closed_5;
       let _x.2 := String.toRawSubstring' _x.1;
       return _x.2
-[Compiler.result] size: 2
+[Compiler.extractClosed] size: 2
     def foo._closed_7 : Name :=
       let _x.1 := foo._closed_5;
       let _x.2 := Name.mkStr1 _x.1;
       return _x.2
-[Compiler.result] size: 4
+[Compiler.extractClosed] size: 4
     def foo._closed_8 : Name :=
       let _x.1 := 1;
       let _x.2 := foo._closed_7;
       let _x.3 := foo._closed_2;
       let _x.4 := addMacroScope _x.3 _x.2 _x.1;
       return _x.4
-[Compiler.result] size: 5
+[Compiler.extractClosed] size: 5
     def foo._closed_9 : Syntax :=
       let _x.1 := [] ◾;
       let _x.2 := foo._closed_8;
@@ -51,17 +51,17 @@
       let _x.4 := foo._closed_0;
       let _x.5 := Syntax.ident _x.4 _x.3 _x.2 _x.1;
       return _x.5
-[Compiler.result] size: 1
+[Compiler.extractClosed] size: 1
     def foo._closed_10 : String :=
       let _x.1 := "+";
       return _x.1
-[Compiler.result] size: 3
+[Compiler.extractClosed] size: 3
     def foo._closed_11 : Syntax :=
       let _x.1 := foo._closed_10;
       let _x.2 := foo._closed_0;
       let _x.3 := Syntax.atom _x.2 _x.1;
       return _x.3
-[Compiler.result] size: 20
+[Compiler.extractClosed] size: 20
     def foo n : Syntax :=
       let _x.1 := Syntax.missing;
       let _x.2 := 1;