chore: update stage0

stage0/src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -7,9 +8,7 @@ import Lean.Compiler.IR.Format
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.CompilerM
 
-namespace Lean
-namespace IR
-namespace UnreachableBranches
+namespace Lean.IR.UnreachableBranches
 
 /-- Value used in the abstract interpreter -/
 inductive Value
@@ -25,11 +24,11 @@ instance : Inhabited Value := ⟨top⟩
 protected partial def beq : Value → Value → Bool
 | bot, bot => true
 | top, top => true
-| ctor i₁ vs₁, ctor i₂ vs₂ => i₁ == i₂ && Array.isEqv vs₁ vs₂ beq
+| ctor i₁ vs₁, ctor i₂ vs₂ => i₁ == i₂ && Array.isEqv vs₁ vs₂ Value.beq
 | choice vs₁, choice vs₂ =>
-  vs₁.all (fun v₁ => vs₂.any $ fun v₂ => beq v₁ v₂)
+  vs₁.all (fun v₁ => vs₂.any fun v₂ => Value.beq v₁ v₂)
   &&
-  vs₂.all (fun v₂ => vs₁.any $ fun v₁ => beq v₁ v₂)
+  vs₂.all (fun v₂ => vs₁.any fun v₁ => Value.beq v₁ v₂)
 | _, _ => false
 
 instance : HasBeq Value := ⟨Value.beq⟩
@@ -38,7 +37,7 @@ partial def addChoice (merge : Value → Value → Value) : List Value → Value
 | [], v => [v]
 | v₁@(ctor i₁ vs₁) :: cs, v₂@(ctor i₂ vs₂) =>
   if i₁ == i₂ then merge v₁ v₂ :: cs
-  else v₁ :: addChoice cs v₂
+  else v₁ :: addChoice merge cs v₂
 | _, _ => panic! "invalid addChoice"
 
 partial def merge : Value → Value → Value
@@ -47,7 +46,7 @@ partial def merge : Value → Value → Value
 | top, _ => top
 | _, top => top
 | v₁@(ctor i₁ vs₁), v₂@(ctor i₂ vs₂) =>
-  if i₁ == i₂ then ctor i₁ $ vs₁.size.fold (fun i r => r.push (merge (vs₁.get! i) (vs₂.get! i))) #[]
+  if i₁ == i₂ then ctor i₁ $ vs₁.size.fold (init := #[]) fun i r => r.push (merge vs₁[i] vs₂[i])
   else choice [v₁, v₂]
 | choice vs₁, choice vs₂ => choice $ vs₁.foldl (addChoice merge) vs₂
 | choice vs, v => choice $ addChoice merge vs v
@@ -56,8 +55,8 @@ partial def merge : Value → Value → Value
 protected partial def format : Value → Format
 | top => "top"
 | bot => "bot"
-| choice vs => fmt "@" ++ @List.format _ ⟨format⟩ vs
-| ctor i vs => fmt "#" ++ if vs.isEmpty then fmt i.name else Format.paren (fmt i.name ++ @formatArray _ ⟨format⟩ vs)
+| choice vs => fmt "@" ++ @List.format _ ⟨Value.format⟩ vs
+| ctor i vs => fmt "#" ++ if vs.isEmpty then fmt i.name else Format.paren (fmt i.name ++ @formatArray _ ⟨Value.format⟩ vs)
 
 instance : HasFormat Value := ⟨Value.format⟩
 instance : HasToString Value := ⟨Format.pretty ∘ Value.format⟩
@@ -67,19 +66,19 @@ instance : HasToString Value := ⟨Format.pretty ∘ Value.format⟩
    interpreter. -/
 partial def truncate (env : Environment) : Value → NameSet → Value
 | ctor i vs, found =>
-  let I := i.name.getPrefix;
+  let I := i.name.getPrefix
   if found.contains I then
     top
   else
     let cont (found' : NameSet) : Value :=
-      ctor i (vs.map $ fun v => truncate v found');
+      ctor i (vs.map fun v => truncate env v found')
     match env.find? I with
     | some (ConstantInfo.inductInfo d) =>
       if d.isRec then cont (found.insert I)
       else cont found
     | _ => cont found
 | choice vs, found =>
-  let newVs := vs.map $ fun v => truncate v found;
+  let newVs := vs.map fun v => truncate env v found
   if newVs.elem top then top
   else choice newVs
 | v, _ => v
@@ -96,7 +95,7 @@ def mkFunctionSummariesExtension : IO (SimplePersistentEnvExtension (FunId × Va
 registerSimplePersistentEnvExtension {
   name       := `unreachBranchesFunSummary,
   addImportedFn := fun as =>
-    let cache : FunctionSummaries := mkStateFromImportedEntries (fun s (p : FunId × Value) => s.insert p.1 p.2) {} as;
+    let cache : FunctionSummaries := mkStateFromImportedEntries (fun s (p : FunId × Value) => s.insert p.1 p.2) {} as
     cache.switch,
   addEntryFn := fun s ⟨e, n⟩ => s.insert e n
 }
@@ -127,9 +126,9 @@ abbrev M := ReaderT InterpContext (StateM InterpState)
 open Value
 
 def findVarValue (x : VarId) : M Value := do
-ctx ← read;
-s ← get;
-let assignment := s.assignments.get! ctx.currFnIdx;
+let ctx ← read
+let s ← get
+let assignment := s.assignments[ctx.currFnIdx]
 pure $ assignment.findD x bot
 
 def findArgValue (arg : Arg) : M Value :=
@@ -138,13 +137,13 @@ match arg with
 | _         => pure top
 
 def updateVarAssignment (x : VarId) (v : Value) : M Unit := do
-v' ← findVarValue x;
-ctx ← read;
-modify $ fun s => { s with assignments := s.assignments.modify ctx.currFnIdx $ fun a => a.insert x (merge v v') }
+let v' ← findVarValue x
+let ctx ← read
+modify fun s => { s with assignments := s.assignments.modify ctx.currFnIdx fun a => a.insert x (merge v v') }
 
 def resetVarAssignment (x : VarId) : M Unit := do
-ctx ← read;
-modify $ fun s => { s with assignments := s.assignments.modify ctx.currFnIdx $ fun a => a.insert x Value.bot }
+let ctx ← read
+modify fun s => { s with assignments := s.assignments.modify ctx.currFnIdx fun a => a.insert x Value.bot }
 
 def resetParamAssignment (y : Param) : M Unit :=
 resetVarAssignment y.x
@@ -155,16 +154,16 @@ partial def projValue : Value → Nat → Value
 | v, _         => v
 
 def interpExpr : Expr → M Value
-| Expr.ctor i ys => ctor i <$> ys.mapM (fun y => findArgValue y)
-| Expr.proj i x  => do v ← findVarValue x; pure $ projValue v i
+| Expr.ctor i ys => do return ctor i (← ys.mapM fun y => findArgValue y)
+| Expr.proj i x  => do return projValue (← findVarValue x) i
 | Expr.fap fid ys => do
-  ctx ← read;
+  let ctx ← read
   match getFunctionSummary? ctx.env fid with
   | some v => pure v
   | none   => do
-    s ← get;
+    let s ← get
     match ctx.decls.findIdx? (fun decl => decl.name == fid) with
-    | some idx => pure $ s.funVals.get! idx
+    | some idx => pure s.funVals[idx]
     | none     => pure top
 | _ => pure top
 
@@ -175,32 +174,31 @@ partial def containsCtor : Value → CtorInfo → Bool
 | _,         _ => false
 
 def updateCurrFnSummary (v : Value) : M Unit := do
-ctx ← read;
-let currFnIdx := ctx.currFnIdx;
-modify $ fun s => { s with funVals := s.funVals.modify currFnIdx (fun v' => widening ctx.env v v') }
+let ctx ← read
+let currFnIdx := ctx.currFnIdx
+modify fun s => { s with funVals := s.funVals.modify currFnIdx (fun v' => widening ctx.env v v') }
 
 /-- Return true if the assignment of at least one parameter has been updated. -/
 def updateJPParamsAssignment (ys : Array Param) (xs : Array Arg) : M Bool := do
-ctx ← read;
-let currFnIdx := ctx.currFnIdx;
-ys.size.foldM
-  (fun i r => do
-    let y := ys.get! i;
-    let x := xs.get! i;
-    yVal ← findVarValue y.x;
-    xVal ← findArgValue x;
-    let newVal := merge yVal xVal;
-    if newVal == yVal then pure r
-    else do
-      modify $ fun s => { s with assignments := s.assignments.modify currFnIdx $ fun a => a.insert y.x newVal };
-      pure true)
-  false
+let ctx ← read
+let currFnIdx := ctx.currFnIdx
+ys.size.foldM (init := false) fun i r => do
+  let y := ys[i]
+  let x := xs[i]
+  let yVal ← findVarValue y.x
+  let xVal ← findArgValue x
+  let newVal := merge yVal xVal
+  if newVal == yVal then
+    pure r
+  else
+    modify fun s => { s with assignments := s.assignments.modify currFnIdx fun a => a.insert y.x newVal }
+    pure true
 
 private partial def resetNestedJPParams : FnBody → M Unit
 | FnBody.jdecl _ ys b k => do
-  ctx ← read;
-  let currFnIdx := ctx.currFnIdx;
-  ys.forM resetParamAssignment;
+  let ctx ← read
+  let currFnIdx := ctx.currFnIdx
+  ys.forM resetParamAssignment
   /- Remark we don't need to reset the parameters of joint-points
     nested in `b` since they will be reset if this JP is used. -/
   resetNestedJPParams k
@@ -208,75 +206,75 @@ private partial def resetNestedJPParams : FnBody → M Unit
   alts.forM fun alt => match alt with
     | Alt.ctor _ b  => resetNestedJPParams b
     | Alt.default b => resetNestedJPParams b
-| e => unless (e.isTerminal) $ resetNestedJPParams e.body
+| e => do unless e.isTerminal do resetNestedJPParams e.body
 
 partial def interpFnBody : FnBody → M Unit
 | FnBody.vdecl x _ e b => do
-  v ← interpExpr e;
-  updateVarAssignment x v;
+  let v ← interpExpr e
+  updateVarAssignment x v
   interpFnBody b
 | FnBody.jdecl j ys v b =>
-  withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) $
+  withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) do
     interpFnBody b
 | FnBody.case _ x _ alts => do
-  v ← findVarValue x;
-  alts.forM $ fun alt =>
+  let v ← findVarValue x
+  alts.forM fun alt => do
     match alt with
-    | Alt.ctor i b  => when (containsCtor v i) $ interpFnBody b
+    | Alt.ctor i b  => if containsCtor v i then interpFnBody b
     | Alt.default b => interpFnBody b
 | FnBody.ret x => do
-  v ← findArgValue x;
+  let v ← findArgValue x
   -- dbgTrace ("ret " ++ toString v) $ fun _ =>
   updateCurrFnSummary v
 | FnBody.jmp j xs => do
-  ctx ← read;
-  let ys := (ctx.lctx.getJPParams j).get!;
-  let b  := (ctx.lctx.getJPBody j).get!;
-  updated ← updateJPParamsAssignment ys xs;
-  when updated do
+  let ctx ← read
+  let ys := (ctx.lctx.getJPParams j).get!
+  let b  := (ctx.lctx.getJPBody j).get!
+  let updated ← updateJPParamsAssignment ys xs
+  if updated then
     -- We must reset the value of nested join-point parameters since they depend on `ys` values
-    resetNestedJPParams b;
+    resetNestedJPParams b
     interpFnBody b
-| e => unless (e.isTerminal) $ interpFnBody e.body
+| e => do
+  unless e.isTerminal do
+    interpFnBody e.body
 
 def inferStep : M Bool := do
-ctx ← read;
-modify $ fun s => { s with assignments := ctx.decls.map $ fun _ => {} };
-ctx.decls.size.foldM (fun idx modified => do
-  match ctx.decls.get! idx with
+let ctx ← read
+modify fun s => { s with assignments := ctx.decls.map fun _ => {} }
+ctx.decls.size.foldM (init := false) fun idx modified => do
+  match ctx.decls[idx] with
   | Decl.fdecl fid ys _ b => do
-    s ← get;
-    -- dbgTrace (">> " ++ toString fid) $ fun _ =>
-    let currVals := s.funVals.get! idx;
-    withReader (fun ctx => { ctx with currFnIdx := idx }) $ do
-      ys.forM $ fun y => updateVarAssignment y.x top;
-      interpFnBody b;
-    s ← get;
-    let newVals := s.funVals.get! idx;
-    pure (modified || currVals != newVals)
-  | Decl.extern _ _ _ _ => pure modified)
-  false
+    let s ← get
+    let currVals := s.funVals[idx]
+    withReader (fun ctx => { ctx with currFnIdx := idx }) do
+      ys.forM fun y => updateVarAssignment y.x top
+      interpFnBody b
+      let s ← get
+      let newVals := s.funVals[idx]
+      pure (modified || currVals != newVals)
+  | Decl.extern _ _ _ _ => pure modified
 
 partial def inferMain : Unit → M Unit
 | _ => do
-  modified ← inferStep;
+  let modified ← inferStep
   if modified then inferMain () else pure ()
 
 partial def elimDeadAux (assignment : Assignment) : FnBody → FnBody
-| FnBody.vdecl x t e b  => FnBody.vdecl x t e (elimDeadAux b)
-| FnBody.jdecl j ys v b => FnBody.jdecl j ys (elimDeadAux v) (elimDeadAux b)
+| FnBody.vdecl x t e b  => FnBody.vdecl x t e (elimDeadAux assignment b)
+| FnBody.jdecl j ys v b => FnBody.jdecl j ys (elimDeadAux assignment v) (elimDeadAux assignment b)
 | FnBody.case tid x xType alts =>
-  let v := assignment.findD x bot;
-  let alts := alts.map $ fun alt =>
+  let v := assignment.findD x bot
+  let alts := alts.map fun alt =>
     match alt with
-    | Alt.ctor i b  => Alt.ctor i $ if containsCtor v i then elimDeadAux b else FnBody.unreachable
-    | Alt.default b => Alt.default (elimDeadAux b);
+    | Alt.ctor i b  => Alt.ctor i $ if containsCtor v i then elimDeadAux assignment b else FnBody.unreachable
+    | Alt.default b => Alt.default (elimDeadAux assignment b)
   FnBody.case tid x xType alts
 | e =>
   if e.isTerminal then e
   else
-    let (instr, b) := e.split;
-    let b := elimDeadAux b;
+    let (instr, b) := e.split
+    let b := elimDeadAux assignment b
     instr.setBody b
 
 partial def elimDead (assignment : Assignment) : Decl → Decl
@@ -288,22 +286,19 @@ end UnreachableBranches
 open UnreachableBranches
 
 def elimDeadBranches (decls : Array Decl) : CompilerM (Array Decl) := do
-s ← get;
-let env := s.env;
-let assignments : Array Assignment := decls.map $ fun _ => {};
-let funVals := Std.mkPArray decls.size Value.bot;
-let ctx : InterpContext := { decls := decls, env := env };
-let s : InterpState := { assignments := assignments, funVals := funVals };
-let (_, s) := (inferMain () ctx).run s;
-let funVals := s.funVals;
-let assignments := s.assignments;
-modify $ fun s =>
-  let env := decls.size.fold (fun i env =>
-    -- dbgTrace (">> " ++ toString (decls.get! i).name ++ " " ++ toString (funVals.get! i)) $ fun _ =>
-    addFunctionSummary env (decls.get! i).name (funVals.get! i))
-    s.env;
-  { s with env := env };
-pure $ decls.mapIdx $ fun i decl => elimDead (assignments.get! i) decl
+let s ← get
+let env := s.env
+let assignments : Array Assignment := decls.map fun _ => {}
+let funVals := Std.mkPArray decls.size Value.bot
+let ctx : InterpContext := { decls := decls, env := env }
+let s : InterpState := { assignments := assignments, funVals := funVals }
+let (_, s) := (inferMain () ctx).run s
+let funVals := s.funVals
+let assignments := s.assignments
+modify fun s =>
+  let env := decls.size.fold (init := s.env) fun i env =>
+    addFunctionSummary env decls[i].name funVals[i]
+  { s with env := env }
+pure $ decls.mapIdx fun i decl => elimDead assignments[i] decl
 
-end IR
-end Lean
+end Lean.IR

stage0/src/Lean/Compiler/IR/FreeVars.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -5,8 +6,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Compiler.IR.Basic
 
-namespace Lean
-namespace IR
+namespace Lean.IR
 
 namespace MaxIndex
 /- Compute the maximum index `M` used in a declaration.
@@ -210,19 +210,19 @@ def visitExpr (w : Index) : Expr → Bool
 | Expr.isTaggedPtr x  => visitVar w x
 
 partial def visitFnBody (w : Index) : FnBody → Bool
-| FnBody.vdecl x _ v b    => visitExpr w v || visitFnBody b
-| FnBody.jdecl j ys v b   => visitFnBody v || visitFnBody b
-| FnBody.set x _ y b      => visitVar w x || visitArg w y || visitFnBody b
-| FnBody.uset x _ y b     => visitVar w x || visitVar w y || visitFnBody b
-| FnBody.sset x _ _ y _ b => visitVar w x || visitVar w y || visitFnBody b
-| FnBody.setTag x _ b     => visitVar w x || visitFnBody b
-| FnBody.inc x _ _ _ b    => visitVar w x || visitFnBody b
-| FnBody.dec x _ _ _ b    => visitVar w x || visitFnBody b
-| FnBody.del x b          => visitVar w x || visitFnBody b
-| FnBody.mdata _ b        => visitFnBody b
+| FnBody.vdecl x _ v b    => visitExpr w v || visitFnBody w b
+| FnBody.jdecl j ys v b   => visitFnBody w v || visitFnBody w b
+| FnBody.set x _ y b      => visitVar w x || visitArg w y || visitFnBody w b
+| FnBody.uset x _ y b     => visitVar w x || visitVar w y || visitFnBody w b
+| FnBody.sset x _ _ y _ b => visitVar w x || visitVar w y || visitFnBody w b
+| FnBody.setTag x _ b     => visitVar w x || visitFnBody w b
+| FnBody.inc x _ _ _ b    => visitVar w x || visitFnBody w b
+| FnBody.dec x _ _ _ b    => visitVar w x || visitFnBody w b
+| FnBody.del x b          => visitVar w x || visitFnBody w b
+| FnBody.mdata _ b        => visitFnBody w b
 | FnBody.jmp j ys         => visitJP w j || visitArgs w ys
 | FnBody.ret x            => visitArg w x
-| FnBody.case _ x _ alts  => visitVar w x || alts.any (fun alt => visitFnBody alt.body)
+| FnBody.case _ x _ alts  => visitVar w x || alts.any (fun alt => visitFnBody w alt.body)
 | FnBody.unreachable      => false
 
 end HasIndex
@@ -231,5 +231,4 @@ def Arg.hasFreeVar (arg : Arg) (x : VarId) : Bool := HasIndex.visitArg x.idx arg
 def Expr.hasFreeVar (e : Expr) (x : VarId) : Bool := HasIndex.visitExpr x.idx e
 def FnBody.hasFreeVar (b : FnBody) (x : VarId) : Bool := HasIndex.visitFnBody x.idx b
 
-end IR
-end Lean
+end Lean.IR

stage0/src/Lean/Compiler/IR/LiveVars.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,8 +7,7 @@ Authors: Leonardo de Moura
 import Lean.Compiler.IR.Basic
 import Lean.Compiler.IR.FreeVars
 
-namespace Lean
-namespace IR
+namespace Lean.IR
 
 /- Remark: in the paper "Counting Immutable Beans" the concepts of
    free and live variables coincide because the paper does *not* consider
@@ -44,29 +44,28 @@ abbrev M := StateM LocalContext
 @[inline] def visitExpr (w : Index) (e : Expr) : M Bool := pure (HasIndex.visitExpr w e)
 
 partial def visitFnBody (w : Index) : FnBody → M Bool
-| FnBody.vdecl x _ v b    => visitExpr w v <||> visitFnBody b
-| FnBody.jdecl j ys v b   => visitFnBody v <||> visitFnBody b
-| FnBody.set x _ y b      => visitVar w x <||> visitArg w y <||> visitFnBody b
-| FnBody.uset x _ y b     => visitVar w x <||> visitVar w y <||> visitFnBody b
-| FnBody.sset x _ _ y _ b => visitVar w x <||> visitVar w y <||> visitFnBody b
-| FnBody.setTag x _ b     => visitVar w x <||> visitFnBody b
-| FnBody.inc x _ _ _ b    => visitVar w x <||> visitFnBody b
-| FnBody.dec x _ _ _ b    => visitVar w x <||> visitFnBody b
-| FnBody.del x b          => visitVar w x <||> visitFnBody b
-| FnBody.mdata _ b        => visitFnBody b
-| FnBody.jmp j ys         => visitArgs w ys <||> do {
-    ctx ← get;
+| FnBody.vdecl x _ v b    => visitExpr w v <||> visitFnBody w b
+| FnBody.jdecl j ys v b   => visitFnBody w v <||> visitFnBody w b
+| FnBody.set x _ y b      => visitVar w x <||> visitArg w y <||> visitFnBody w b
+| FnBody.uset x _ y b     => visitVar w x <||> visitVar w y <||> visitFnBody w b
+| FnBody.sset x _ _ y _ b => visitVar w x <||> visitVar w y <||> visitFnBody w b
+| FnBody.setTag x _ b     => visitVar w x <||> visitFnBody w b
+| FnBody.inc x _ _ _ b    => visitVar w x <||> visitFnBody w b
+| FnBody.dec x _ _ _ b    => visitVar w x <||> visitFnBody w b
+| FnBody.del x b          => visitVar w x <||> visitFnBody w b
+| FnBody.mdata _ b        => visitFnBody w b
+| FnBody.jmp j ys         => visitArgs w ys <||> do
+    let ctx ← get
     match ctx.getJPBody j with
     | some b =>
       -- `j` is not a local join point since we assume we cannot shadow join point declarations.
       -- Instead of marking the join points that we have already been visited, we permanently remove `j` from the context.
-      set (ctx.eraseJoinPointDecl j) *> visitFnBody b
+      set (ctx.eraseJoinPointDecl j) *> visitFnBody w b
     | none   =>
       -- `j` must be a local join point. So do nothing since we have already visite its body.
       pure false
-  }
 | FnBody.ret x            => visitArg w x
-| FnBody.case _ x _ alts  => visitVar w x <||> alts.anyM (fun alt => visitFnBody alt.body)
+| FnBody.case _ x _ alts  => visitVar w x <||> alts.anyM (fun alt => visitFnBody w alt.body)
 | FnBody.unreachable      => pure false
 
 end IsLive
@@ -161,5 +160,4 @@ LiveVars.collectFnBody b m v
 
 export LiveVars (updateJPLiveVarMap)
 
-end IR
-end Lean
+end Lean.IR

stage0/stdlib/Lean/Compiler/IR/ElimDeadVars.c

@@ -27,6 +27,7 @@ lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_FnBody_freeIndices(lean_object*);
 lean_object* l_Lean_IR_FnBody_elimDead_match__2(lean_object*);
+lean_object* l_Std_RBNode_findCore___main___at___private_Lean_Compiler_IR_FreeVars_0__Lean_IR_FreeIndices_collectIndex___spec__1(lean_object*, lean_object*);
 uint8_t l_Array_isEmpty___rarg(lean_object*);
 lean_object* l_Lean_IR_reshapeWithoutDeadAux_match__1(lean_object*);
 lean_object* l_Lean_IR_reshapeWithoutDeadAux(lean_object*, lean_object*, lean_object*);
@@ -43,7 +44,6 @@ lean_object* l_Lean_IR_FnBody_elimDead_match__1(lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_IR_FnBody_elimDead___spec__2(lean_object*, lean_object*);
 lean_object* l_Array_back___at_Lean_IR_reshapeWithoutDeadAux___spec__1___boxed(lean_object*);
 lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
-lean_object* l_Std_RBNode_findCore___main___at___private_Lean_Compiler_IR_FreeVars_14__collectIndex___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_IR_FnBody_collectFreeIndices(lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Lean_IR_FnBody_elimDead_match__3(lean_object*);
@@ -152,7 +152,7 @@ case 0:
 lean_object* x_7; lean_object* x_8; 
 x_7 = lean_ctor_get(x_5, 0);
 lean_inc(x_7);
-x_8 = l_Std_RBNode_findCore___main___at___private_Lean_Compiler_IR_FreeVars_14__collectIndex___spec__1(x_3, x_7);
+x_8 = l_Std_RBNode_findCore___main___at___private_Lean_Compiler_IR_FreeVars_0__Lean_IR_FreeIndices_collectIndex___spec__1(x_3, x_7);
 lean_dec(x_7);
 if (lean_obj_tag(x_8) == 0)
 {
@@ -178,7 +178,7 @@ case 1:
 lean_object* x_13; lean_object* x_14; 
 x_13 = lean_ctor_get(x_5, 0);
 lean_inc(x_13);
-x_14 = l_Std_RBNode_findCore___main___at___private_Lean_Compiler_IR_FreeVars_14__collectIndex___spec__1(x_3, x_13);
+x_14 = l_Std_RBNode_findCore___main___at___private_Lean_Compiler_IR_FreeVars_0__Lean_IR_FreeIndices_collectIndex___spec__1(x_3, x_13);
 lean_dec(x_13);
 if (lean_obj_tag(x_14) == 0)
 {

stage0/stdlib/Lean/Compiler/IR/RC.c

@@ -43,6 +43,7 @@ lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_updateRefUsin
 lean_object* l_Array_iterateMAux___main___at_Lean_IR_ExplicitRC_updateVarInfoWithParams___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_ExplicitRC_visitFnBody_match__8(lean_object*);
 lean_object* l_Lean_IR_ExplicitRC_getDecl_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_LiveVars_collectFnBody(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecAfterFullApp___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_getNumConsumptions___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBefore___spec__2___lambda__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_IR_ExplicitRC_visitFnBody_match__2___rarg(lean_object*, lean_object*);
@@ -84,6 +85,7 @@ lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBefore(
 lean_object* l_Lean_IR_ExplicitRC_getVarInfo___closed__1;
 lean_object* l_Std_RBNode_fold___main___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecForAlt___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_ExplicitRC_getJPLiveVars_match__1(lean_object*);
+lean_object* l_Std_RBNode_find___main___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_collectJP___spec__1(lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_isBorrowParamAux___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_setBlack___rarg(lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
@@ -105,16 +107,13 @@ uint8_t l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_isBorrowParamAux(l
 lean_object* l_Lean_IR_ExplicitRC_getJPParams(lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_isScalarBoxedInTaggedPtr_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_ExplicitRC_visitFnBody_match__11(lean_object*);
-lean_object* l_Lean_IR_LiveVars_collectFnBody___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_ExplicitRC_visitFnBody_match__4___rarg(lean_object*, lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_fold___main___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecForAlt___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addDecForDeadParams___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Std_RBNode_find___main___at___private_Lean_Compiler_IR_LiveVars_7__collectJP___spec__1(lean_object*, lean_object*);
 lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
 uint8_t l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_getNumConsumptions___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBefore___spec__2___lambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_IR_ExplicitRC_Context_jpLiveVarMap___default;
-lean_object* l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_isBorrowParamAux___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___spec__4___rarg___boxed(lean_object*);
 lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_isBorrowParamAux___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___spec__4(lean_object*);
 lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeAux___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -168,6 +167,7 @@ uint8_t l_Std_RBNode_isRed___rarg(lean_object*);
 lean_object* l_Lean_IR_ExplicitRC_visitFnBody___closed__1;
 lean_object* l_Lean_IR_ExplicitRC_addInc___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_isPersistent_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_IR_ExplicitRC_visitFnBody_match__10(lean_object*);
 lean_object* l_Lean_IR_ExplicitRC_getDecl(lean_object*, lean_object*);
 uint8_t l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_consumeExpr(lean_object*, lean_object*);
@@ -564,7 +564,7 @@ _start:
 {
 lean_object* x_3; lean_object* x_4; 
 x_3 = lean_ctor_get(x_1, 3);
-x_4 = l_Std_RBNode_find___main___at___private_Lean_Compiler_IR_LiveVars_7__collectJP___spec__1(x_3, x_2);
+x_4 = l_Std_RBNode_find___main___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_collectJP___spec__1(x_3, x_2);
 if (lean_obj_tag(x_4) == 0)
 {
 lean_object* x_5; 
@@ -6057,7 +6057,7 @@ lean_ctor_set(x_9, 3, x_5);
 x_10 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeAux___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___spec__1(x_1, x_8, x_9, x_6);
 lean_dec(x_6);
 lean_dec(x_8);
-x_11 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(x_2, x_7);
+x_11 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
 lean_dec(x_2);
 x_12 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_12, 0, x_10);
@@ -6078,7 +6078,7 @@ lean_ctor_set(x_14, 3, x_5);
 x_15 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeAux___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___spec__1(x_1, x_13, x_14, x_6);
 lean_dec(x_6);
 lean_dec(x_13);
-x_16 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(x_2, x_7);
+x_16 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
 lean_dec(x_2);
 x_17 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_17, 0, x_15);
@@ -6106,7 +6106,7 @@ lean_ctor_set(x_22, 0, x_2);
 lean_ctor_set(x_22, 1, x_3);
 lean_ctor_set(x_22, 2, x_4);
 lean_ctor_set(x_22, 3, x_19);
-x_23 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(x_2, x_7);
+x_23 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
 lean_dec(x_2);
 x_24 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_24, 0, x_22);
@@ -6134,7 +6134,7 @@ lean_ctor_set(x_30, 0, x_2);
 lean_ctor_set(x_30, 1, x_3);
 lean_ctor_set(x_30, 2, x_4);
 lean_ctor_set(x_30, 3, x_29);
-x_31 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(x_2, x_7);
+x_31 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
 lean_dec(x_2);
 x_32 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_32, 0, x_30);
@@ -6155,7 +6155,7 @@ lean_ctor_set(x_35, 0, x_2);
 lean_ctor_set(x_35, 1, x_3);
 lean_ctor_set(x_35, 2, x_4);
 lean_ctor_set(x_35, 3, x_34);
-x_36 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(x_2, x_7);
+x_36 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
 lean_dec(x_2);
 x_37 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_37, 0, x_35);
@@ -6175,7 +6175,7 @@ lean_ctor_set(x_40, 0, x_2);
 lean_ctor_set(x_40, 1, x_3);
 lean_ctor_set(x_40, 2, x_4);
 lean_ctor_set(x_40, 3, x_39);
-x_41 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(x_2, x_7);
+x_41 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
 lean_dec(x_2);
 x_42 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_42, 0, x_40);
@@ -6203,7 +6203,7 @@ lean_ctor_set(x_48, 3, x_47);
 x_49 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeAux___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBefore___spec__1(x_46, x_1, x_44, x_48, x_6);
 lean_dec(x_6);
 lean_dec(x_44);
-x_50 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(x_2, x_7);
+x_50 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
 lean_dec(x_2);
 x_51 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_51, 0, x_49);
@@ -6224,7 +6224,7 @@ lean_ctor_set(x_53, 3, x_5);
 x_54 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeAux___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___spec__1(x_1, x_52, x_53, x_6);
 lean_dec(x_6);
 lean_dec(x_52);
-x_55 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(x_2, x_7);
+x_55 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
 lean_dec(x_2);
 x_56 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_56, 0, x_54);
@@ -6250,7 +6250,7 @@ lean_ctor_set(x_61, 3, x_5);
 x_62 = l___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeAux___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_addIncBeforeConsumeAll___spec__1(x_1, x_60, x_61, x_6);
 lean_dec(x_6);
 lean_dec(x_60);
-x_63 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(x_2, x_7);
+x_63 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
 lean_dec(x_2);
 x_64 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_64, 0, x_62);
@@ -6270,7 +6270,7 @@ lean_ctor_set(x_67, 0, x_2);
 lean_ctor_set(x_67, 1, x_3);
 lean_ctor_set(x_67, 2, x_4);
 lean_ctor_set(x_67, 3, x_66);
-x_68 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(x_2, x_7);
+x_68 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
 lean_dec(x_2);
 x_69 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_69, 0, x_67);
@@ -6287,7 +6287,7 @@ lean_ctor_set(x_70, 0, x_2);
 lean_ctor_set(x_70, 1, x_3);
 lean_ctor_set(x_70, 2, x_4);
 lean_ctor_set(x_70, 3, x_5);
-x_71 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_8__bindVar___spec__1(x_2, x_7);
+x_71 = l_Std_RBNode_erase___at___private_Lean_Compiler_IR_LiveVars_0__Lean_IR_LiveVars_bindVar___spec__1(x_2, x_7);
 lean_dec(x_2);
 x_72 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_72, 0, x_70);
@@ -7513,7 +7513,7 @@ x_142 = lean_ctor_get(x_2, 3);
 lean_inc(x_142);
 x_143 = lean_box(0);
 lean_inc(x_1);
-x_144 = l_Lean_IR_LiveVars_collectFnBody___main(x_1, x_142, x_143);
+x_144 = l_Lean_IR_LiveVars_collectFnBody(x_1, x_142, x_143);
 x_145 = !lean_is_exclusive(x_1);
 if (x_145 == 0)
 {
@@ -7658,7 +7658,7 @@ lean_inc(x_185);
 lean_dec(x_2);
 x_186 = lean_box(0);
 lean_inc(x_184);
-x_187 = l_Lean_IR_LiveVars_collectFnBody___main(x_184, x_185, x_186);
+x_187 = l_Lean_IR_LiveVars_collectFnBody(x_184, x_185, x_186);
 x_188 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_188, 0, x_184);
 lean_ctor_set(x_188, 1, x_187);

stage0/stdlib/Lean/Compiler/IR/ResetReuse.c

@@ -24,7 +24,6 @@ uint8_t lean_name_eq(lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_ResetReuse_0__Lean_IR_ResetReuse_Dfinalize___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_ResetReuse_0__Lean_IR_ResetReuse_Dfinalize(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_ResetReuse_R_match__1(lean_object*);
-uint8_t l_Lean_IR_HasIndex_visitFnBody___main(lean_object*, lean_object*);
 uint8_t l_Lean_IR_CtorInfo_isScalar(lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l___private_Lean_Compiler_IR_ResetReuse_0__Lean_IR_ResetReuse_Dfinalize_match__1___rarg(lean_object*, lean_object*, lean_object*);
@@ -70,6 +69,7 @@ lean_object* l___private_Lean_Compiler_IR_ResetReuse_0__Lean_IR_ResetReuse_mayRe
 lean_object* l___private_Lean_Compiler_IR_ResetReuse_0__Lean_IR_ResetReuse_argsContainsVar___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_IR_FnBody_hasLiveVar(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_ResetReuse_R_match__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l_Lean_IR_HasIndex_visitFnBody(lean_object*, lean_object*);
 lean_object* l_Lean_Name_getPrefix(lean_object*);
 lean_object* l_Lean_IR_ResetReuse_R(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_ResetReuse_0__Lean_IR_ResetReuse_argsContainsVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
@@ -1785,7 +1785,7 @@ lean_object* x_108; lean_object* x_109; uint8_t x_110;
 x_108 = lean_ctor_get(x_101, 0);
 x_109 = lean_ctor_get(x_101, 1);
 lean_dec(x_109);
-x_110 = l_Lean_IR_HasIndex_visitFnBody___main(x_1, x_98);
+x_110 = l_Lean_IR_HasIndex_visitFnBody(x_1, x_98);
 if (x_110 == 0)
 {
 lean_object* x_111; 
@@ -1845,7 +1845,7 @@ lean_object* x_125; uint8_t x_126;
 x_125 = lean_ctor_get(x_101, 0);
 lean_inc(x_125);
 lean_dec(x_101);
-x_126 = l_Lean_IR_HasIndex_visitFnBody___main(x_1, x_98);
+x_126 = l_Lean_IR_HasIndex_visitFnBody(x_1, x_98);
 if (x_126 == 0)
 {
 lean_object* x_127; lean_object* x_128; 
@@ -1912,7 +1912,7 @@ if (lean_is_exclusive(x_101)) {
  lean_dec_ref(x_101);
  x_140 = lean_box(0);
 }
-x_141 = l_Lean_IR_HasIndex_visitFnBody___main(x_1, x_98);
+x_141 = l_Lean_IR_HasIndex_visitFnBody(x_1, x_98);
 if (x_141 == 0)
 {
 lean_object* x_142; lean_object* x_143; lean_object* x_144;