chore: update stage0

stage0/src/Lean/Compiler/LCNF.lean

@@ -35,4 +35,5 @@ import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.Util
 import Lean.Compiler.LCNF.ConfigOptions
 import Lean.Compiler.LCNF.ForEachExpr
-import Lean.Compiler.LCNF.MonoTypes
+import Lean.Compiler.LCNF.MonoTypes
+import Lean.Compiler.LCNF.ToMono

stage0/src/Lean/Compiler/LCNF/Check.lean

@@ -31,6 +31,12 @@ def checkFVar (fvarId : FVarId) : CheckM Unit :=
   unless (← read).vars.contains fvarId do
     throwError "invalid out of scope free variable {← getBinderName fvarId}"
 
+/-- Return true `f` is a constructor and `i` is less than its number of parameters. -/
+def isCtorParam (f : Expr) (i : Nat) : CoreM Bool := do
+  let .const declName _ := f | return false
+  let .ctorInfo info ← getConstInfo declName | return false
+  return i < info.numParams
+
 def checkAppArgs (f : Expr) (args : Array Expr) : CheckM Unit := do
   let mut fType ← inferType f
   let mut j := 0
@@ -54,9 +60,12 @@ def checkAppArgs (f : Expr) (args : Array Expr) : CheckM Unit := do
     unless (← InferType.compatibleTypes argType expectedType) do
       throwError "type mismatch at LCNF application{indentExpr (mkAppN f args)}\nargument {arg} has type{indentExpr argType}\nbut is expected to have type{indentExpr expectedType}"
     unless (← pure (maybeTypeFormerType expectedType) <||> isErasedCompatible expectedType) do
-      unless arg.isFVar do
-        throwError "invalid LCNF application{indentExpr (mkAppN f args)}\nargument{indentExpr arg}\nhas type{indentExpr expectedType}\nmust be a free variable"
-      checkFVar arg.fvarId!
+      if arg.isFVar then
+        checkFVar arg.fvarId!
+      else
+        -- Constructor parameters that are not type formers are erased at phase .mono
+        unless arg.isErased && (← getPhase) ≥ .mono && (← isCtorParam f i) do
+          throwError "invalid LCNF application{indentExpr (mkAppN f args)}\nargument{indentExpr arg}\nhas type{indentExpr expectedType}\nmust be a free variable"
     fType := b
 
 def checkApp (f : Expr) (args : Array Expr) : CheckM Unit := do

stage0/src/Lean/Compiler/LCNF/Main.lean

@@ -73,7 +73,7 @@ def run (declNames : Array Name) : CompilerM (Array Decl) := withAtLeastMaxRecDe
   for pass in manager.passes do
     trace[Compiler] s!"Running pass: {pass.name}"
     decls ← withPhase pass.phase <| pass.run decls
-    withPhase pass.phase <| checkpoint pass.name decls
+    withPhase pass.phaseOut <| checkpoint pass.name decls
   if (← Lean.isTracingEnabledFor `Compiler.result) then
     for decl in decls do
       -- We display the declaration saved in the environment because the names have been normalized

stage0/src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -42,7 +42,7 @@ Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t.
 def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo) := do
   if isRuntimeBultinType declName then return none
   let .inductInfo info ← getConstInfo declName | return none
-  if info.isUnsafe then return none
+  if info.isUnsafe || info.isRec then return none
   let [ctorName] := info.ctors | return none
   let mask ← getRelevantCtorFields ctorName
   let mut result := none

stage0/src/Lean/Compiler/LCNF/PassManager.lean

@@ -10,6 +10,23 @@ import Lean.Compiler.LCNF.CompilerM
 
 namespace Lean.Compiler.LCNF
 
+def Phase.toNat : Phase → Nat
+  | .base => 0
+  | .mono => 1
+  | .impure => 2
+
+instance : LT Phase where
+  lt l r := l.toNat < r.toNat
+
+instance : LE Phase where
+  le l r := l.toNat ≤ r.toNat
+
+instance {p1 p2 : Phase} : Decidable (p1 < p2) := Nat.decLt p1.toNat p2.toNat
+instance {p1 p2 : Phase} : Decidable (p1 ≤ p2) := Nat.decLe p1.toNat p2.toNat
+
+@[simp] theorem Phase.le_refl (p : Phase) : p ≤ p := by
+  cases p <;> decide
+
 /--
 A single compiler `Pass`, consisting of the actual pass function operating
 on the `Decl`s as well as meta information.
@@ -26,6 +43,11 @@ structure Pass where
   -/
   phase : Phase
   /--
+  Resulting phase.
+  -/
+  phaseOut : Phase := phase
+  phaseInv : phaseOut ≥ phase := by simp
+  /--
   The name of the `Pass`
   -/
   name : Name
@@ -33,7 +55,9 @@ structure Pass where
   The actual pass function, operating on the `Decl`s.
   -/
   run : Array Decl → CompilerM (Array Decl)
-  deriving Inhabited
+
+instance : Inhabited Pass where
+  default := { phase := .base, name := default, run := fun decls => return decls }
 
 /--
 Can be used to install, remove, replace etc. passes by tagging a declaration
@@ -56,30 +80,12 @@ structure PassManager where
   passes : Array Pass
   deriving Inhabited
 
-namespace Phase
-
-def toNat : Phase → Nat
-  | .base => 0
-  | .mono => 1
-  | .impure => 2
-
-instance : LT Phase where
-  lt l r := l.toNat < r.toNat
-
-instance : LE Phase where
-  le l r := l.toNat ≤ r.toNat
-
-instance {p1 p2 : Phase} : Decidable (p1 < p2) := Nat.decLt p1.toNat p2.toNat
-instance {p1 p2 : Phase} : Decidable (p1 ≤ p2) := Nat.decLe p1.toNat p2.toNat
-
 instance : ToString Phase where
   toString
     | .base => "base"
     | .mono => "mono"
     | .impure => "impure"
 
-end Phase
-
 namespace Pass
 
 def mkPerDeclaration (name : Name) (run : Decl → CompilerM Decl) (phase : Phase) (occurrence : Nat := 0) : Pass where

stage0/src/Lean/Compiler/LCNF/Passes.lean

@@ -12,6 +12,7 @@ import Lean.Compiler.LCNF.ReduceJpArity
 import Lean.Compiler.LCNF.JoinPoints
 import Lean.Compiler.LCNF.Specialize
 import Lean.Compiler.LCNF.PhaseExt
+import Lean.Compiler.LCNF.ToMono
 
 namespace Lean.Compiler.LCNF
 
@@ -35,6 +36,9 @@ def normalizeFVarIds (decl : Decl) : CoreM Decl := do
 def saveBase : Pass :=
   .mkPerDeclaration `saveBase (fun decl => do (← normalizeFVarIds decl).saveBase; return decl) .base
 
+def saveMono : Pass :=
+  .mkPerDeclaration `saveMono (fun decl => do (← normalizeFVarIds decl).saveMono; return decl) .mono
+
 def builtinPassManager : PassManager := {
   passes := #[
     init,
@@ -49,7 +53,10 @@ def builtinPassManager : PassManager := {
     specialize,
     simp (occurrence := 2),
     cse,
-    saveBase -- End of base phase
+    saveBase, -- End of base phase
+    toMono,
+    -- TODO: lambda lifting, reduce function arity
+    saveMono  -- End of mono phase
   ]
 }
 

stage0/src/Lean/Compiler/LCNF/ToMono.lean

@@ -8,60 +8,155 @@ import Lean.Compiler.LCNF.InferType
 
 namespace Lean.Compiler.LCNF
 
-def Param.toMono (param : Param) : CompilerM Param := do
+structure ToMonoM.State where
+  typeParams : FVarIdSet := {}
+
+abbrev ToMonoM := StateRefT ToMonoM.State CompilerM
+
+def Param.toMono (param : Param) : ToMonoM Param := do
+  if isTypeFormerType param.type then
+    modify fun { typeParams, .. } => { typeParams := typeParams.insert param.fvarId }
   param.update (← toMonoType param.type)
 
-def _root_.Lean.Expr.toMono (e : Expr) : CompilerM Expr := do
+def isTrivialConstructorApp? (e : Expr) : ToMonoM (Option Expr) := do
+  let some ctorInfo := e.isConstructorApp? (← getEnv) | return none
+  let some info ← hasTrivialStructure? ctorInfo.induct | return none
+  assert! ctorInfo.numParams + info.fieldIdx < e.getAppNumArgs
+  return e.getArg! (ctorInfo.numParams + info.fieldIdx)
+
+def fvarToMono (e : Expr) : ToMonoM Expr := do
+  if (← get).typeParams.contains e.fvarId! then
+    return erasedExpr
+  else
+    return e
+
+def argToMono (arg : Expr) : ToMonoM Expr := do
+  if arg.isFVar then
+    fvarToMono arg
+  else
+    return erasedExpr
+
+def ctorAppToMono (ctorInfo : ConstructorVal) (args : Array Expr) : ToMonoM Expr := do
+  let argsNew ← args[:ctorInfo.numParams].toArray.mapM fun param => do
+    -- We only preserve constructor parameters that are types
+    if isTypeFormerType (← inferType param) then
+      toMonoType param
+    else
+      return erasedExpr
+  let argsNew := argsNew ++ (← args[ctorInfo.numParams:].toArray.mapM argToMono)
+  return mkAppN (mkConst ctorInfo.name) argsNew
+
+partial def _root_.Lean.Expr.toMono (e : Expr) : ToMonoM Expr := do
   match e with
-  | .fvar .. => if isTypeFormerType (← inferType e) then return erasedExpr else return e
-  | .lit .. | .const .. => return e
+  | .fvar .. => fvarToMono e
+  | .lit .. => return e
+  | .const declName _ => return mkConst declName
   | .sort .. => return erasedExpr
   | .mvar .. | .bvar .. | .letE .. => unreachable!
   | .mdata _ b => return e.updateMData! (← b.toMono)
-  | .proj _ _ b => return e.updateProj! (← b.toMono)
+  | .proj structName fieldIdx b =>
+    if let some info ← hasTrivialStructure? structName then
+      if info.fieldIdx == fieldIdx then
+        b.toMono
+      else
+        return erasedExpr
+    else
+      return e.updateProj! (← b.toMono)
   | .forallE .. | .lam .. => return erasedExpr
-  | .app f a =>
-    let a ← if a.isFVar then a.toMono else pure erasedExpr
-    return e.updateApp! (← f.toMono) a
+  | .app .. =>
+    if e.isAppOf ``Decidable.isTrue then
+      return mkConst ``Bool.true
+    else if e.isAppOf ``Decidable.isFalse then
+      return mkConst ``Bool.false
+    else if let some arg ← isTrivialConstructorApp? e then
+      arg.toMono
+    else if let some ctorInfo := e.isConstructorApp? (← getEnv) then
+      ctorAppToMono ctorInfo e.getAppArgs
+    else
+      let f := e.getAppFn
+      let args := e.getAppArgs
+      let args ← args.mapM argToMono
+      return mkAppN (← f.toMono) args
 
-def LetDecl.toMono (decl : LetDecl) : CompilerM LetDecl := do
+def LetDecl.toMono (decl : LetDecl) : ToMonoM LetDecl := do
   let type ← toMonoType decl.type
   let value ← decl.value.toMono
   decl.update type value
 
 mutual
 
-partial def FunDeclCore.toMono (decl : FunDecl) : CompilerM FunDecl := do
-  -- TODO: constructor Decidable to Bool, Trivial Structure
-  -- TODO: eliminate projection for trivial structure
+partial def FunDeclCore.toMono (decl : FunDecl) : ToMonoM FunDecl := do
   let type ← toMonoType decl.type
   let params ← decl.params.mapM (·.toMono)
   let value ← decl.value.toMono
   decl.update type params value
 
-partial def AltCore.toMono (alt : Alt) : CompilerM Alt := do
-  -- TODO: Decidable to Bool, Trivial Structure
-  match alt with
-  | .default k => return alt.updateCode (← k.toMono)
-  | .alt _ ps k => return alt.updateAlt! (← ps.mapM (·.toMono)) (← k.toMono)
+/-- Convert `cases` `Decidable` => `Bool` -/
+partial def decToMono (c : Cases) (_ : c.typeName == ``Decidable) : ToMonoM Code := do
+  let resultType ← toMonoType c.resultType
+  let alts ← c.alts.mapM fun alt => do
+    match alt with
+    | .default k => return alt.updateCode (← k.toMono)
+    | .alt ctorName ps k =>
+      eraseParams ps
+      let ctorName := if ctorName == ``Decidable.isTrue then ``Bool.true else ``Bool.false
+      return .alt ctorName #[] (← k.toMono)
+  return .cases { c with resultType, alts, typeName := ``Bool }
 
-partial def Code.toMono (code : Code) : CompilerM Code := do
+/-- Eliminate `cases` for trivial structure. See `hasTrivialStructure?` -/
+partial def trivialStructToMono (info : TrivialStructureInfo) (c : Cases) : ToMonoM Code := do
+  assert! c.alts.size == 1
+  let .alt ctorName ps k := c.alts[0]! | unreachable!
+  assert! ctorName == info.ctorName
+  assert! info.fieldIdx < ps.size
+  let p := ps[info.fieldIdx]!
+  eraseParams ps
+  /- We reuse `p`s `fvarId` to avoid substitution -/
+  let decl := { fvarId := p.fvarId, binderName := p.binderName, type := (← toMonoType p.type), value := .fvar c.discr }
+  modifyLCtx fun lctx => lctx.addLetDecl decl
+  let k ← k.toMono
+  return .let decl k
+
+partial def Code.toMono (code : Code) : ToMonoM Code := do
   match code with
   | .let decl k => return code.updateLet! (← decl.toMono) (← k.toMono)
   | .fun decl k | .jp decl k => return code.updateFun! (← decl.toMono) (← k.toMono)
   | .unreach type => return .unreach (← toMonoType type)
   | .return .. | .jmp .. => return code
   | .cases c =>
-    let type ← toMonoType c.resultType
-    let alts ← c.alts.mapM (·.toMono)
-    return code.updateCases! type c.discr alts
+    if h : c.typeName == ``Decidable then
+      decToMono c h
+    else if let some info ← hasTrivialStructure? c.typeName then
+      trivialStructToMono info c
+    else
+      -- TODO: `casesOn` `[implementedBy]` support
+      let type ← toMonoType c.resultType
+      let alts ← c.alts.mapM fun alt =>
+        match alt with
+        | .default k => return alt.updateCode (← k.toMono)
+        | .alt _ ps k => return alt.updateAlt! (← ps.mapM (·.toMono)) (← k.toMono)
+      return code.updateCases! type c.discr alts
 
 end
 
 def Decl.toMono (decl : Decl) : CompilerM Decl := do
-  let type ← toMonoType decl.type
-  let params ← decl.params.mapM (·.toMono)
-  let value ← decl.value.toMono
-  return { decl with type, params, value, levelParams := [] }
+  go |>.run' {}
+where
+  go : ToMonoM Decl := do
+    let type ← toMonoType decl.type
+    let params ← decl.params.mapM (·.toMono)
+    let value ← decl.value.toMono
+    let decl := { decl with type, params, value, levelParams := [] }
+    decl.saveMono
+    return decl
+
+def toMono : Pass where
+  name     := `toMono
+  run      := fun decls => decls.mapM (·.toMono)
+  phase    := .base
+  phaseOut := .mono
+
+builtin_initialize
+  registerTraceClass `Compiler.toMono (inherited := true)
 
 end Lean.Compiler.LCNF

stage0/stdlib/Lean/Compiler/LCNF.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Compiler.LCNF
-// Imports: Init Lean.Compiler.LCNF.AlphaEqv Lean.Compiler.LCNF.Basic Lean.Compiler.LCNF.Bind Lean.Compiler.LCNF.Check Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.CSE Lean.Compiler.LCNF.DependsOn Lean.Compiler.LCNF.ElimDead Lean.Compiler.LCNF.FixedArgs Lean.Compiler.LCNF.InferType Lean.Compiler.LCNF.JoinPoints Lean.Compiler.LCNF.LCtx Lean.Compiler.LCNF.Level Lean.Compiler.LCNF.Main Lean.Compiler.LCNF.Passes Lean.Compiler.LCNF.PassManager Lean.Compiler.LCNF.PhaseExt Lean.Compiler.LCNF.PrettyPrinter Lean.Compiler.LCNF.PullFunDecls Lean.Compiler.LCNF.PullLetDecls Lean.Compiler.LCNF.ReduceJpArity Lean.Compiler.LCNF.Simp Lean.Compiler.LCNF.Specialize Lean.Compiler.LCNF.SpecInfo Lean.Compiler.LCNF.Testing Lean.Compiler.LCNF.ToDecl Lean.Compiler.LCNF.ToExpr Lean.Compiler.LCNF.ToLCNF Lean.Compiler.LCNF.Types Lean.Compiler.LCNF.Util Lean.Compiler.LCNF.ConfigOptions Lean.Compiler.LCNF.ForEachExpr Lean.Compiler.LCNF.MonoTypes
+// Imports: Init Lean.Compiler.LCNF.AlphaEqv Lean.Compiler.LCNF.Basic Lean.Compiler.LCNF.Bind Lean.Compiler.LCNF.Check Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.CSE Lean.Compiler.LCNF.DependsOn Lean.Compiler.LCNF.ElimDead Lean.Compiler.LCNF.FixedArgs Lean.Compiler.LCNF.InferType Lean.Compiler.LCNF.JoinPoints Lean.Compiler.LCNF.LCtx Lean.Compiler.LCNF.Level Lean.Compiler.LCNF.Main Lean.Compiler.LCNF.Passes Lean.Compiler.LCNF.PassManager Lean.Compiler.LCNF.PhaseExt Lean.Compiler.LCNF.PrettyPrinter Lean.Compiler.LCNF.PullFunDecls Lean.Compiler.LCNF.PullLetDecls Lean.Compiler.LCNF.ReduceJpArity Lean.Compiler.LCNF.Simp Lean.Compiler.LCNF.Specialize Lean.Compiler.LCNF.SpecInfo Lean.Compiler.LCNF.Testing Lean.Compiler.LCNF.ToDecl Lean.Compiler.LCNF.ToExpr Lean.Compiler.LCNF.ToLCNF Lean.Compiler.LCNF.Types Lean.Compiler.LCNF.Util Lean.Compiler.LCNF.ConfigOptions Lean.Compiler.LCNF.ForEachExpr Lean.Compiler.LCNF.MonoTypes Lean.Compiler.LCNF.ToMono
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -47,6 +47,7 @@ lean_object* initialize_Lean_Compiler_LCNF_Util(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Compiler_LCNF_ConfigOptions(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Compiler_LCNF_ForEachExpr(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Compiler_LCNF_MonoTypes(uint8_t builtin, lean_object*);
+lean_object* initialize_Lean_Compiler_LCNF_ToMono(uint8_t builtin, lean_object*);
 static bool _G_initialized = false;
 LEAN_EXPORT lean_object* initialize_Lean_Compiler_LCNF(uint8_t builtin, lean_object* w) {
 lean_object * res;
@@ -154,6 +155,9 @@ lean_dec_ref(res);
 res = initialize_Lean_Compiler_LCNF_MonoTypes(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Lean_Compiler_LCNF_ToMono(builtin, lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Lean/Compiler/LCNF/Main.c

@@ -2184,211 +2184,220 @@ lean_inc(x_10);
 x_11 = !lean_is_exclusive(x_4);
 if (x_11 == 0)
 {
-lean_object* x_12; 
+lean_object* x_12; lean_object* x_13; 
+x_12 = lean_ctor_get(x_4, 0);
+lean_inc(x_12);
 lean_ctor_set_uint8(x_4, sizeof(void*)*1, x_9);
 lean_inc(x_7);
 lean_inc(x_6);
 lean_inc(x_5);
-lean_inc(x_4);
-x_12 = lean_apply_6(x_10, x_2, x_4, x_5, x_6, x_7, x_8);
-if (lean_obj_tag(x_12) == 0)
+x_13 = lean_apply_6(x_10, x_2, x_4, x_5, x_6, x_7, x_8);
+if (lean_obj_tag(x_13) == 0)
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
-x_13 = lean_ctor_get(x_12, 0);
-lean_inc(x_13);
-x_14 = lean_ctor_get(x_12, 1);
+lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+x_14 = lean_ctor_get(x_13, 0);
 lean_inc(x_14);
-lean_dec(x_12);
-x_15 = lean_ctor_get(x_1, 1);
+x_15 = lean_ctor_get(x_13, 1);
 lean_inc(x_15);
-lean_dec(x_1);
-lean_inc(x_13);
-x_16 = l_Lean_Compiler_LCNF_checkpoint(x_15, x_13, x_4, x_5, x_6, x_7, x_14);
-if (lean_obj_tag(x_16) == 0)
-{
-uint8_t x_17; 
-x_17 = !lean_is_exclusive(x_16);
-if (x_17 == 0)
-{
-lean_object* x_18; lean_object* x_19; 
-x_18 = lean_ctor_get(x_16, 0);
-lean_dec(x_18);
-x_19 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_19, 0, x_13);
-lean_ctor_set(x_16, 0, x_19);
-return x_16;
-}
-else
-{
-lean_object* x_20; lean_object* x_21; lean_object* x_22; 
-x_20 = lean_ctor_get(x_16, 1);
-lean_inc(x_20);
-lean_dec(x_16);
-x_21 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_21, 0, x_13);
-x_22 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_22, 0, x_21);
-lean_ctor_set(x_22, 1, x_20);
-return x_22;
-}
-}
-else
-{
-uint8_t x_23; 
 lean_dec(x_13);
-x_23 = !lean_is_exclusive(x_16);
-if (x_23 == 0)
+x_16 = lean_ctor_get_uint8(x_1, sizeof(void*)*3 + 1);
+x_17 = lean_ctor_get(x_1, 1);
+lean_inc(x_17);
+lean_dec(x_1);
+x_18 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_18, 0, x_12);
+lean_ctor_set_uint8(x_18, sizeof(void*)*1, x_16);
+lean_inc(x_14);
+x_19 = l_Lean_Compiler_LCNF_checkpoint(x_17, x_14, x_18, x_5, x_6, x_7, x_15);
+if (lean_obj_tag(x_19) == 0)
 {
-return x_16;
+uint8_t x_20; 
+x_20 = !lean_is_exclusive(x_19);
+if (x_20 == 0)
+{
+lean_object* x_21; lean_object* x_22; 
+x_21 = lean_ctor_get(x_19, 0);
+lean_dec(x_21);
+x_22 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_22, 0, x_14);
+lean_ctor_set(x_19, 0, x_22);
+return x_19;
 }
 else
 {
-lean_object* x_24; lean_object* x_25; lean_object* x_26; 
-x_24 = lean_ctor_get(x_16, 0);
-x_25 = lean_ctor_get(x_16, 1);
-lean_inc(x_25);
-lean_inc(x_24);
-lean_dec(x_16);
-x_26 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_26, 0, x_24);
-lean_ctor_set(x_26, 1, x_25);
-return x_26;
+lean_object* x_23; lean_object* x_24; lean_object* x_25; 
+x_23 = lean_ctor_get(x_19, 1);
+lean_inc(x_23);
+lean_dec(x_19);
+x_24 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_24, 0, x_14);
+x_25 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_25, 0, x_24);
+lean_ctor_set(x_25, 1, x_23);
+return x_25;
+}
+}
+else
+{
+uint8_t x_26; 
+lean_dec(x_14);
+x_26 = !lean_is_exclusive(x_19);
+if (x_26 == 0)
+{
+return x_19;
+}
+else
+{
+lean_object* x_27; lean_object* x_28; lean_object* x_29; 
+x_27 = lean_ctor_get(x_19, 0);
+x_28 = lean_ctor_get(x_19, 1);
+lean_inc(x_28);
+lean_inc(x_27);
+lean_dec(x_19);
+x_29 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_29, 0, x_27);
+lean_ctor_set(x_29, 1, x_28);
+return x_29;
 }
 }
 }
 else
 {
-uint8_t x_27; 
-lean_dec(x_4);
+uint8_t x_30; 
+lean_dec(x_12);
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_1);
-x_27 = !lean_is_exclusive(x_12);
-if (x_27 == 0)
+x_30 = !lean_is_exclusive(x_13);
+if (x_30 == 0)
 {
-return x_12;
-}
-else
-{
-lean_object* x_28; lean_object* x_29; lean_object* x_30; 
-x_28 = lean_ctor_get(x_12, 0);
-x_29 = lean_ctor_get(x_12, 1);
-lean_inc(x_29);
-lean_inc(x_28);
-lean_dec(x_12);
-x_30 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_30, 0, x_28);
-lean_ctor_set(x_30, 1, x_29);
-return x_30;
-}
-}
+return x_13;
 }
 else
 {
 lean_object* x_31; lean_object* x_32; lean_object* x_33; 
-x_31 = lean_ctor_get(x_4, 0);
+x_31 = lean_ctor_get(x_13, 0);
+x_32 = lean_ctor_get(x_13, 1);
+lean_inc(x_32);
 lean_inc(x_31);
+lean_dec(x_13);
+x_33 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_33, 0, x_31);
+lean_ctor_set(x_33, 1, x_32);
+return x_33;
+}
+}
+}
+else
+{
+lean_object* x_34; lean_object* x_35; lean_object* x_36; 
+x_34 = lean_ctor_get(x_4, 0);
+lean_inc(x_34);
 lean_dec(x_4);
-x_32 = lean_alloc_ctor(0, 1, 1);
-lean_ctor_set(x_32, 0, x_31);
-lean_ctor_set_uint8(x_32, sizeof(void*)*1, x_9);
+lean_inc(x_34);
+x_35 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_35, 0, x_34);
+lean_ctor_set_uint8(x_35, sizeof(void*)*1, x_9);
 lean_inc(x_7);
 lean_inc(x_6);
 lean_inc(x_5);
-lean_inc(x_32);
-x_33 = lean_apply_6(x_10, x_2, x_32, x_5, x_6, x_7, x_8);
-if (lean_obj_tag(x_33) == 0)
+x_36 = lean_apply_6(x_10, x_2, x_35, x_5, x_6, x_7, x_8);
+if (lean_obj_tag(x_36) == 0)
 {
-lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; 
-x_34 = lean_ctor_get(x_33, 0);
-lean_inc(x_34);
-x_35 = lean_ctor_get(x_33, 1);
-lean_inc(x_35);
-lean_dec(x_33);
-x_36 = lean_ctor_get(x_1, 1);
-lean_inc(x_36);
-lean_dec(x_1);
-lean_inc(x_34);
-x_37 = l_Lean_Compiler_LCNF_checkpoint(x_36, x_34, x_32, x_5, x_6, x_7, x_35);
-if (lean_obj_tag(x_37) == 0)
-{
-lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; 
-x_38 = lean_ctor_get(x_37, 1);
+lean_object* x_37; lean_object* x_38; uint8_t x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; 
+x_37 = lean_ctor_get(x_36, 0);
+lean_inc(x_37);
+x_38 = lean_ctor_get(x_36, 1);
 lean_inc(x_38);
-if (lean_is_exclusive(x_37)) {
- lean_ctor_release(x_37, 0);
- lean_ctor_release(x_37, 1);
- x_39 = x_37;
-} else {
- lean_dec_ref(x_37);
- x_39 = lean_box(0);
-}
-x_40 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_40, 0, x_34);
-if (lean_is_scalar(x_39)) {
- x_41 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_41 = x_39;
-}
-lean_ctor_set(x_41, 0, x_40);
-lean_ctor_set(x_41, 1, x_38);
-return x_41;
-}
-else
+lean_dec(x_36);
+x_39 = lean_ctor_get_uint8(x_1, sizeof(void*)*3 + 1);
+x_40 = lean_ctor_get(x_1, 1);
+lean_inc(x_40);
+lean_dec(x_1);
+x_41 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_41, 0, x_34);
+lean_ctor_set_uint8(x_41, sizeof(void*)*1, x_39);
+lean_inc(x_37);
+x_42 = l_Lean_Compiler_LCNF_checkpoint(x_40, x_37, x_41, x_5, x_6, x_7, x_38);
+if (lean_obj_tag(x_42) == 0)
 {
-lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; 
-lean_dec(x_34);
-x_42 = lean_ctor_get(x_37, 0);
-lean_inc(x_42);
-x_43 = lean_ctor_get(x_37, 1);
+lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; 
+x_43 = lean_ctor_get(x_42, 1);
 lean_inc(x_43);
-if (lean_is_exclusive(x_37)) {
- lean_ctor_release(x_37, 0);
- lean_ctor_release(x_37, 1);
- x_44 = x_37;
+if (lean_is_exclusive(x_42)) {
+ lean_ctor_release(x_42, 0);
+ lean_ctor_release(x_42, 1);
+ x_44 = x_42;
 } else {
- lean_dec_ref(x_37);
+ lean_dec_ref(x_42);
  x_44 = lean_box(0);
 }
+x_45 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_45, 0, x_37);
 if (lean_is_scalar(x_44)) {
- x_45 = lean_alloc_ctor(1, 2, 0);
+ x_46 = lean_alloc_ctor(0, 2, 0);
 } else {
- x_45 = x_44;
+ x_46 = x_44;
 }
-lean_ctor_set(x_45, 0, x_42);
-lean_ctor_set(x_45, 1, x_43);
-return x_45;
+lean_ctor_set(x_46, 0, x_45);
+lean_ctor_set(x_46, 1, x_43);
+return x_46;
+}
+else
+{
+lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; 
+lean_dec(x_37);
+x_47 = lean_ctor_get(x_42, 0);
+lean_inc(x_47);
+x_48 = lean_ctor_get(x_42, 1);
+lean_inc(x_48);
+if (lean_is_exclusive(x_42)) {
+ lean_ctor_release(x_42, 0);
+ lean_ctor_release(x_42, 1);
+ x_49 = x_42;
+} else {
+ lean_dec_ref(x_42);
+ x_49 = lean_box(0);
+}
+if (lean_is_scalar(x_49)) {
+ x_50 = lean_alloc_ctor(1, 2, 0);
+} else {
+ x_50 = x_49;
+}
+lean_ctor_set(x_50, 0, x_47);
+lean_ctor_set(x_50, 1, x_48);
+return x_50;
 }
 }
 else
 {
-lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; 
-lean_dec(x_32);
+lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; 
+lean_dec(x_34);
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_1);
-x_46 = lean_ctor_get(x_33, 0);
-lean_inc(x_46);
-x_47 = lean_ctor_get(x_33, 1);
-lean_inc(x_47);
-if (lean_is_exclusive(x_33)) {
- lean_ctor_release(x_33, 0);
- lean_ctor_release(x_33, 1);
- x_48 = x_33;
+x_51 = lean_ctor_get(x_36, 0);
+lean_inc(x_51);
+x_52 = lean_ctor_get(x_36, 1);
+lean_inc(x_52);
+if (lean_is_exclusive(x_36)) {
+ lean_ctor_release(x_36, 0);
+ lean_ctor_release(x_36, 1);
+ x_53 = x_36;
 } else {
- lean_dec_ref(x_33);
- x_48 = lean_box(0);
+ lean_dec_ref(x_36);
+ x_53 = lean_box(0);
 }
-if (lean_is_scalar(x_48)) {
- x_49 = lean_alloc_ctor(1, 2, 0);
+if (lean_is_scalar(x_53)) {
+ x_54 = lean_alloc_ctor(1, 2, 0);
 } else {
- x_49 = x_48;
+ x_54 = x_53;
 }
-lean_ctor_set(x_49, 0, x_46);
-lean_ctor_set(x_49, 1, x_47);
-return x_49;
+lean_ctor_set(x_54, 0, x_51);
+lean_ctor_set(x_54, 1, x_52);
+return x_54;
 }
 }
 }

stage0/stdlib/Lean/Compiler/LCNF/MonoTypes.c

@@ -58,7 +58,6 @@ static lean_object* l_Lean_Compiler_LCNF_getRelevantCtorFields___closed__6;
 static lean_object* l_Lean_Compiler_LCNF_getRelevantCtorFields___closed__8;
 extern lean_object* l_Lean_levelZero;
 lean_object* lean_nat_add(lean_object*, lean_object*);
-static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1586____closed__1;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_hasTrivialStructure_x3f___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Compiler_LCNF_MonoTypes_0__Lean_Compiler_LCNF_reprTrivialStructureInfo____x40_Lean_Compiler_LCNF_MonoTypes___hyg_242____closed__16;
 extern lean_object* l_Lean_Compiler_LCNF_erasedExpr;
@@ -158,7 +157,8 @@ uint8_t l_Lean_Compiler_LCNF_isTypeFormerType(lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_getRelevantCtorFields___closed__5;
 static lean_object* l_Lean_Compiler_LCNF_getRelevantCtorFields___closed__14;
 static lean_object* l_Std_Range_forIn_loop___at_Lean_Compiler_LCNF_hasTrivialStructure_x3f___spec__2___closed__2;
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1586_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1592_(lean_object*);
+static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1592____closed__1;
 static lean_object* l_Lean_Compiler_LCNF_getRelevantCtorFields___closed__20;
 static lean_object* l_Lean_Compiler_LCNF_getRelevantCtorFields___closed__10;
 lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
@@ -1833,96 +1833,130 @@ lean_dec(x_7);
 x_9 = lean_ctor_get_uint8(x_8, sizeof(void*)*5 + 1);
 if (x_9 == 0)
 {
-lean_object* x_10; lean_object* x_11; lean_object* x_12; 
-x_10 = lean_ctor_get(x_6, 1);
-lean_inc(x_10);
+uint8_t x_10; 
+x_10 = lean_ctor_get_uint8(x_8, sizeof(void*)*5);
+if (x_10 == 0)
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_11 = lean_ctor_get(x_6, 1);
+lean_inc(x_11);
 lean_dec(x_6);
-x_11 = lean_box(0);
-x_12 = l_Lean_Compiler_LCNF_hasTrivialStructure_x3f___lambda__2(x_8, x_11, x_3, x_4, x_10);
-return x_12;
+x_12 = lean_box(0);
+x_13 = l_Lean_Compiler_LCNF_hasTrivialStructure_x3f___lambda__2(x_8, x_12, x_3, x_4, x_11);
+return x_13;
 }
 else
 {
-uint8_t x_13; 
+uint8_t x_14; 
 lean_dec(x_8);
 lean_dec(x_4);
 lean_dec(x_3);
-x_13 = !lean_is_exclusive(x_6);
-if (x_13 == 0)
+x_14 = !lean_is_exclusive(x_6);
+if (x_14 == 0)
 {
-lean_object* x_14; lean_object* x_15; 
-x_14 = lean_ctor_get(x_6, 0);
-lean_dec(x_14);
-x_15 = lean_box(0);
-lean_ctor_set(x_6, 0, x_15);
+lean_object* x_15; lean_object* x_16; 
+x_15 = lean_ctor_get(x_6, 0);
+lean_dec(x_15);
+x_16 = lean_box(0);
+lean_ctor_set(x_6, 0, x_16);
 return x_6;
 }
 else
 {
-lean_object* x_16; lean_object* x_17; lean_object* x_18; 
-x_16 = lean_ctor_get(x_6, 1);
-lean_inc(x_16);
+lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+x_17 = lean_ctor_get(x_6, 1);
+lean_inc(x_17);
 lean_dec(x_6);
-x_17 = lean_box(0);
-x_18 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_18, 0, x_17);
-lean_ctor_set(x_18, 1, x_16);
-return x_18;
+x_18 = lean_box(0);
+x_19 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_19, 0, x_18);
+lean_ctor_set(x_19, 1, x_17);
+return x_19;
 }
 }
 }
 else
 {
-uint8_t x_19; 
+uint8_t x_20; 
+lean_dec(x_8);
+lean_dec(x_4);
+lean_dec(x_3);
+x_20 = !lean_is_exclusive(x_6);
+if (x_20 == 0)
+{
+lean_object* x_21; lean_object* x_22; 
+x_21 = lean_ctor_get(x_6, 0);
+lean_dec(x_21);
+x_22 = lean_box(0);
+lean_ctor_set(x_6, 0, x_22);
+return x_6;
+}
+else
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; 
+x_23 = lean_ctor_get(x_6, 1);
+lean_inc(x_23);
+lean_dec(x_6);
+x_24 = lean_box(0);
+x_25 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_25, 0, x_24);
+lean_ctor_set(x_25, 1, x_23);
+return x_25;
+}
+}
+}
+else
+{
+uint8_t x_26; 
 lean_dec(x_7);
 lean_dec(x_4);
 lean_dec(x_3);
-x_19 = !lean_is_exclusive(x_6);
-if (x_19 == 0)
+x_26 = !lean_is_exclusive(x_6);
+if (x_26 == 0)
 {
-lean_object* x_20; lean_object* x_21; 
-x_20 = lean_ctor_get(x_6, 0);
-lean_dec(x_20);
-x_21 = lean_box(0);
-lean_ctor_set(x_6, 0, x_21);
+lean_object* x_27; lean_object* x_28; 
+x_27 = lean_ctor_get(x_6, 0);
+lean_dec(x_27);
+x_28 = lean_box(0);
+lean_ctor_set(x_6, 0, x_28);
 return x_6;
 }
 else
 {
-lean_object* x_22; lean_object* x_23; lean_object* x_24; 
-x_22 = lean_ctor_get(x_6, 1);
-lean_inc(x_22);
+lean_object* x_29; lean_object* x_30; lean_object* x_31; 
+x_29 = lean_ctor_get(x_6, 1);
+lean_inc(x_29);
 lean_dec(x_6);
-x_23 = lean_box(0);
-x_24 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_24, 0, x_23);
-lean_ctor_set(x_24, 1, x_22);
-return x_24;
+x_30 = lean_box(0);
+x_31 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_31, 0, x_30);
+lean_ctor_set(x_31, 1, x_29);
+return x_31;
 }
 }
 }
 else
 {
-uint8_t x_25; 
+uint8_t x_32; 
 lean_dec(x_4);
 lean_dec(x_3);
-x_25 = !lean_is_exclusive(x_6);
-if (x_25 == 0)
+x_32 = !lean_is_exclusive(x_6);
+if (x_32 == 0)
 {
 return x_6;
 }
 else
 {
-lean_object* x_26; lean_object* x_27; lean_object* x_28; 
-x_26 = lean_ctor_get(x_6, 0);
-x_27 = lean_ctor_get(x_6, 1);
-lean_inc(x_27);
-lean_inc(x_26);
+lean_object* x_33; lean_object* x_34; lean_object* x_35; 
+x_33 = lean_ctor_get(x_6, 0);
+x_34 = lean_ctor_get(x_6, 1);
+lean_inc(x_34);
+lean_inc(x_33);
 lean_dec(x_6);
-x_28 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_28, 0, x_26);
-lean_ctor_set(x_28, 1, x_27);
-return x_28;
+x_35 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_35, 0, x_33);
+lean_ctor_set(x_35, 1, x_34);
+return x_35;
 }
 }
 }
@@ -2991,7 +3025,7 @@ x_1 = l_Lean_Compiler_LCNF_getRelevantCtorFields___closed__16;
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1586____closed__1() {
+static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1592____closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
@@ -3001,11 +3035,11 @@ lean_closure_set(x_2, 0, x_1);
 return x_2;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1586_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1592_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1586____closed__1;
+x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1592____closed__1;
 x_3 = l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(x_2, x_1);
 return x_3;
 }
@@ -3582,9 +3616,9 @@ l_Lean_Compiler_LCNF_MonoTypeExtState_mono___default = _init_l_Lean_Compiler_LCN
 lean_mark_persistent(l_Lean_Compiler_LCNF_MonoTypeExtState_mono___default);
 l_Lean_Compiler_LCNF_instInhabitedMonoTypeExtState = _init_l_Lean_Compiler_LCNF_instInhabitedMonoTypeExtState();
 lean_mark_persistent(l_Lean_Compiler_LCNF_instInhabitedMonoTypeExtState);
-l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1586____closed__1 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1586____closed__1();
-lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1586____closed__1);
-if (builtin) {res = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1586_(lean_io_mk_world());
+l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1592____closed__1 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1592____closed__1();
+lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1592____closed__1);
+if (builtin) {res = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_MonoTypes___hyg_1592_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 l_Lean_Compiler_LCNF_monoTypeExt = lean_io_result_get_value(res);
 lean_mark_persistent(l_Lean_Compiler_LCNF_monoTypeExt);

stage0/stdlib/Lean/Compiler/LCNF/Specialize.c

@@ -50,7 +50,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_shouldSpecialize(lean_o
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_Collector_collectCode(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_isTracingEnabledFor___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4913_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4917_(lean_object*);
 lean_object* l_Lean_EnvExtensionInterfaceUnsafe_imp___elambda__2___rarg(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__10;
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
@@ -185,12 +185,12 @@ static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_expandCodeDecls_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_visitCode(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Specialize_Collector_collectFVar___closed__4;
-static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4913____closed__1;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_of_nat(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_expandCodeDecls(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__5___closed__2;
 lean_object* l_Lean_Compiler_LCNF_findFunDecl_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4917____closed__1;
 LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_Collector_collectExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Compiler_LCNF_getDecl_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go___spec__3(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -14135,11 +14135,12 @@ x_1 = lean_unsigned_to_nat(0u);
 x_2 = 0;
 x_3 = l_Lean_Compiler_LCNF_specialize___closed__1;
 x_4 = l_Lean_Compiler_LCNF_specialize___closed__2;
-x_5 = lean_alloc_ctor(0, 3, 1);
+x_5 = lean_alloc_ctor(0, 3, 2);
 lean_ctor_set(x_5, 0, x_1);
 lean_ctor_set(x_5, 1, x_3);
 lean_ctor_set(x_5, 2, x_4);
 lean_ctor_set_uint8(x_5, sizeof(void*)*3, x_2);
+lean_ctor_set_uint8(x_5, sizeof(void*)*3 + 1, x_2);
 return x_5;
 }
 }
@@ -14173,7 +14174,7 @@ lean_dec(x_1);
 return x_7;
 }
 }
-static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4913____closed__1() {
+static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4917____closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@@ -14183,11 +14184,11 @@ x_3 = l_Lean_Name_mkStr2(x_1, x_2);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4913_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4917_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; uint8_t x_3; lean_object* x_4; 
-x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4913____closed__1;
+x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4917____closed__1;
 x_3 = 1;
 x_4 = l_Lean_registerTraceClass(x_2, x_3, x_1);
 if (lean_obj_tag(x_4) == 0)
@@ -14448,9 +14449,9 @@ l_Lean_Compiler_LCNF_specialize___closed__3 = _init_l_Lean_Compiler_LCNF_special
 lean_mark_persistent(l_Lean_Compiler_LCNF_specialize___closed__3);
 l_Lean_Compiler_LCNF_specialize = _init_l_Lean_Compiler_LCNF_specialize();
 lean_mark_persistent(l_Lean_Compiler_LCNF_specialize);
-l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4913____closed__1 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4913____closed__1();
-lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4913____closed__1);
-res = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4913_(lean_io_mk_world());
+l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4917____closed__1 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4917____closed__1();
+lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4917____closed__1);
+res = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4917_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));

stage0/stdlib/Lean/Compiler/LCNF/Testing.c

@@ -1511,6 +1511,7 @@ x_11 = lean_unsigned_to_nat(0u);
 lean_ctor_set(x_3, 2, x_6);
 lean_ctor_set(x_3, 1, x_4);
 lean_ctor_set(x_3, 0, x_11);
+lean_ctor_set_uint8(x_3, sizeof(void*)*3 + 1, x_5);
 return x_3;
 }
 else
@@ -1518,11 +1519,12 @@ else
 lean_object* x_12; lean_object* x_13; 
 lean_dec(x_3);
 x_12 = lean_unsigned_to_nat(0u);
-x_13 = lean_alloc_ctor(0, 3, 1);
+x_13 = lean_alloc_ctor(0, 3, 2);
 lean_ctor_set(x_13, 0, x_12);
 lean_ctor_set(x_13, 1, x_4);
 lean_ctor_set(x_13, 2, x_6);
 lean_ctor_set_uint8(x_13, sizeof(void*)*3, x_5);
+lean_ctor_set_uint8(x_13, sizeof(void*)*3 + 1, x_5);
 return x_13;
 }
 }
@@ -2365,6 +2367,7 @@ lean_dec(x_11);
 x_12 = lean_unsigned_to_nat(0u);
 lean_ctor_set(x_3, 2, x_7);
 lean_ctor_set(x_3, 0, x_12);
+lean_ctor_set_uint8(x_3, sizeof(void*)*3 + 1, x_5);
 return x_3;
 }
 else
@@ -2372,11 +2375,12 @@ else
 lean_object* x_13; lean_object* x_14; 
 lean_dec(x_3);
 x_13 = lean_unsigned_to_nat(0u);
-x_14 = lean_alloc_ctor(0, 3, 1);
+x_14 = lean_alloc_ctor(0, 3, 2);
 lean_ctor_set(x_14, 0, x_13);
 lean_ctor_set(x_14, 1, x_6);
 lean_ctor_set(x_14, 2, x_7);
 lean_ctor_set_uint8(x_14, sizeof(void*)*3, x_5);
+lean_ctor_set_uint8(x_14, sizeof(void*)*3 + 1, x_5);
 return x_14;
 }
 }