refactor(library/init/lean/compiler/ir): remove redundant field from FnBody.jdecl

The result type of a join point is always equal to the function return
type. Moreover, the extra bookkeeping introduces extra work, and doesn't
really help.

library/init/lean/compiler/ir/basic.lean

@@ -178,8 +178,8 @@ inductive AltCore (FnBody : Type) : Type
 inductive FnBody
 /- `let x : ty := e; b` -/
 | vdecl (x : VarId) (ty : IRType) (e : Expr) (b : FnBody)
-/- Join point Declaration `let j (xs) : ty := e; b` -/
-| jdecl (j : JoinPointId) (xs : Array Param) (ty : IRType) (v : FnBody) (b : FnBody)
+/- Join point Declaration `block_j (xs) := e; b` -/
+| jdecl (j : JoinPointId) (xs : Array Param) (v : FnBody) (b : FnBody)
 /- Store `y` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1.
    This operation is not part of λPure is only used during optimization. -/
 | set (x : VarId) (i : Nat) (y : VarId) (b : FnBody)
@@ -205,7 +205,7 @@ instance : Inhabited FnBody := ⟨FnBody.unreachable⟩
 abbrev FnBody.nil := FnBody.unreachable
 
 @[export lean.ir.mk_vdecl_core] def mkVDecl (x : VarId) (ty : IRType) (e : Expr) (b : FnBody) : FnBody := FnBody.vdecl x ty e b
-@[export lean.ir.mk_jdecl_core] def mkJDecl (j : JoinPointId) (xs : Array Param) (ty : IRType) (v : FnBody) (b : FnBody) : FnBody := FnBody.jdecl j xs ty v b
+@[export lean.ir.mk_jdecl_core] def mkJDecl (j : JoinPointId) (xs : Array Param) (v : FnBody) (b : FnBody) : FnBody := FnBody.jdecl j xs v b
 @[export lean.ir.mk_uset_core] def mkUSet (x : VarId) (i : Nat) (y : VarId) (b : FnBody) : FnBody := FnBody.uset x i y b
 @[export lean.ir.mk_sset_core] def mkSSet (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody) : FnBody := FnBody.sset x i offset y ty b
 @[export lean.ir.mk_case_core] def mkCase (tid : Name) (x : VarId) (cs : Array (AltCore FnBody)) : FnBody := FnBody.case tid x cs
@@ -229,7 +229,7 @@ def FnBody.isTerminal : FnBody → Bool
 
 def FnBody.body : FnBody → FnBody
 | (FnBody.vdecl _ _ _ b)    := b
-| (FnBody.jdecl _ _ _ _ b)  := b
+| (FnBody.jdecl _ _ _ b)  := b
 | (FnBody.set _ _ _ b)      := b
 | (FnBody.uset _ _ _ b)     := b
 | (FnBody.sset _ _ _ _ _ b) := b
@@ -241,7 +241,7 @@ def FnBody.body : FnBody → FnBody
 
 def FnBody.setBody : FnBody → FnBody → FnBody
 | (FnBody.vdecl x t v _)    b := FnBody.vdecl x t v b
-| (FnBody.jdecl j xs t v _) b := FnBody.jdecl j xs t v b
+| (FnBody.jdecl j xs v _)   b := FnBody.jdecl j xs v b
 | (FnBody.set x i y _)      b := FnBody.set x i y b
 | (FnBody.uset x i y _)     b := FnBody.uset x i y b
 | (FnBody.sset x i o y t _) b := FnBody.sset x i o y t b
@@ -309,13 +309,13 @@ reshapeAux bs bs.size term
 
 @[inline] def modifyJPs (bs : Array FnBody) (f : FnBody → FnBody) : Array FnBody :=
 bs.hmap $ λ b, match b with
-  | FnBody.jdecl j xs t v k := FnBody.jdecl j xs t (f v) k
-  | other                   := other
+  | FnBody.jdecl j xs v k := FnBody.jdecl j xs (f v) k
+  | other                 := other
 
 @[inline] def mmodifyJPs {m : Type → Type} [Monad m] (bs : Array FnBody) (f : FnBody → m FnBody) : m (Array FnBody) :=
 bs.hmmap $ λ b, match b with
-  | FnBody.jdecl j xs t v k := do v ← f v, pure $ FnBody.jdecl j xs t v k
-  | other                   := pure other
+  | FnBody.jdecl j xs v k := do v ← f v, pure $ FnBody.jdecl j xs v k
+  | other                 := pure other
 
 @[export lean.ir.mk_alt_core] def mkAlt (n : Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (b : FnBody) : Alt := Alt.ctor ⟨n, cidx, size, usize, ssize⟩ b
 
@@ -344,7 +344,7 @@ def Expr.isPure : Expr → Bool
 /-- `FnBody.isPure b` return `true` Iff `b` is in the `λPure` fragment. -/
 partial def FnBody.isPure : FnBody → Bool
 | (FnBody.vdecl _ _ e b)    := e.isPure && b.isPure
-| (FnBody.jdecl _ _ _ e b)  := e.isPure && b.isPure
+| (FnBody.jdecl _ _ e b)  := e.isPure && b.isPure
 | (FnBody.uset _ _ _ b)     := b.isPure
 | (FnBody.sset _ _ _ _ _ b) := b.isPure
 | (FnBody.mdata _ b)        := b.isPure
@@ -368,8 +368,8 @@ structure Context :=
 
 def Context.addDecl (ctx : Context) (b : FnBody) : Context :=
 match b with
-| FnBody.vdecl x _ _ _   := { locals := ctx.locals.insert x.idx b, .. ctx }
-| FnBody.jdecl j _ _ _ _ := { locals := ctx.locals.insert j.idx b, .. ctx }
+| FnBody.vdecl x _ _ _ := { locals := ctx.locals.insert x.idx b, .. ctx }
+| FnBody.jdecl j _ _ _ := { locals := ctx.locals.insert j.idx b, .. ctx }
 | other := ctx
 
 def Context.addParam (ctx : Context) (p : Param) : Context :=
@@ -377,12 +377,12 @@ def Context.addParam (ctx : Context) (p : Param) : Context :=
 
 def Context.isJP (ctx : Context) (idx : Index) : Bool :=
 match ctx.locals.find idx with
-| some (FnBody.jdecl _ _ _ _ _) := true
+| some (FnBody.jdecl _ _ _ _) := true
 | other := false
 
 def Context.getJoinPointBody (ctx : Context) (j : JoinPointId) : Option FnBody :=
 match ctx.locals.find j.idx with
-| some (FnBody.jdecl _ _ _ v _) := some v
+| some (FnBody.jdecl _ _ v _) := some v
 | other := none
 
 def Context.isParam (ctx : Context) (idx : Index) : Bool :=
@@ -457,9 +457,9 @@ else Array.foldl₂ ps₁ ps₂ (λ ρ p₁ p₂, do ρ ← ρ, addParamRename
 
 partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool
 | ρ (FnBody.vdecl x₁ t₁ v₁ b₁)      (FnBody.vdecl x₂ t₂ v₂ b₂)        := t₁ == t₂ && v₁ =[ρ]= v₂ && FnBody.alphaEqv (addVarRename ρ x₁.idx x₂.idx) b₁ b₂
-| ρ (FnBody.jdecl j₁ ys₁ t₁ v₁ b₁)  (FnBody.jdecl j₂ ys₂ t₂ v₂ b₂)    :=
+| ρ (FnBody.jdecl j₁ ys₁ v₁ b₁)  (FnBody.jdecl j₂ ys₂ v₂ b₂)    :=
   match addParamsRename ρ ys₁ ys₂ with
-  | some ρ' := t₁ == t₂ && FnBody.alphaEqv ρ' v₁ v₂ && FnBody.alphaEqv (addVarRename ρ j₁.idx j₂.idx) b₁ b₂
+  | some ρ' := FnBody.alphaEqv ρ' v₁ v₂ && FnBody.alphaEqv (addVarRename ρ j₁.idx j₂.idx) b₁ b₂
   | none    := false
 | ρ (FnBody.set x₁ i₁ y₁ b₁)        (FnBody.set x₂ i₂ y₂ b₂)          := x₁ =[ρ]= x₂ && i₁ == i₂ && y₁ =[ρ]= y₂ && FnBody.alphaEqv ρ b₁ b₂
 | ρ (FnBody.uset x₁ i₁ y₁ b₁)       (FnBody.uset x₂ i₂ y₂ b₂)         := x₁ =[ρ]= x₂ && i₁ == i₂ && y₁ =[ρ]= y₂ && FnBody.alphaEqv ρ b₁ b₂

library/init/lean/compiler/ir/checker.lean

@@ -48,7 +48,7 @@ partial def checkFnBody : FnBody → M Unit
   ctx ← read,
   when (ctx.contains x.idx) $ throw ("invalid variable declaration, shadowing is not allowed"),
   adaptReader (λ ctx : Context, ctx.addDecl d) (checkFnBody b)
-| d@(FnBody.jdecl j ys _ v b) := do
+| d@(FnBody.jdecl j ys v b) := do
   withParams ys (checkFnBody v),
   ctx ← read,
   when (ctx.contains j.idx) $ throw ("invalid join point declaration, shadowing is not allowed"),

library/init/lean/compiler/ir/elimdead.lean

@@ -24,9 +24,9 @@ partial def reshapeWithoutDeadAux : Array FnBody → FnBody → IndexSet → FnB
       if used.contains vidx then keep ()
       else reshapeWithoutDeadAux bs b used in
     match curr with
-    | FnBody.vdecl x _ _  _  := keepIfUsed x.idx
-    | FnBody.jdecl j _ _ _ _ := keepIfUsed j.idx
-    | _                      := keep ()
+    | FnBody.vdecl x _ _ _  := keepIfUsed x.idx
+    | FnBody.jdecl j _ _ _  := keepIfUsed j.idx
+    | _                     := keep ()
 
 def reshapeWithoutDead (bs : Array FnBody) (term : FnBody) : FnBody :=
 reshapeWithoutDeadAux bs term term.freeIndices

library/init/lean/compiler/ir/format.lean

@@ -75,7 +75,7 @@ def formatAlt (fmt : FnBody → Format) (indent : Nat) : Alt → Format
 
 partial def formatFnBody (indent : Nat := 2) : FnBody → Format
 | (FnBody.vdecl x ty e b)    := "let " ++ format x ++ " : " ++ format ty ++ " := " ++ format e ++ ";" ++ Format.line ++ formatFnBody b
-| (FnBody.jdecl j xs ty v b) := format j ++ formatArray xs ++ " : " ++ format ty ++ " :=" ++ Format.nest indent (Format.line ++ formatFnBody v) ++ ";" ++ Format.line ++ formatFnBody b
+| (FnBody.jdecl j xs v b)    := format j ++ formatArray xs ++ " :=" ++ Format.nest indent (Format.line ++ formatFnBody v) ++ ";" ++ Format.line ++ formatFnBody b
 | (FnBody.set x i y b)       := "set " ++ format x ++ "[" ++ format i ++ "] := " ++ format y ++ ";" ++ Format.line ++ formatFnBody b
 | (FnBody.uset x i y b)      := "uset " ++ format x ++ "[" ++ format i ++ "] := " ++ format y ++ ";" ++ Format.line ++ formatFnBody b
 | (FnBody.sset x i o y ty b) := "sset " ++ format x ++ "[" ++ format i ++ ", " ++ format o ++ "] : " ++ format ty ++ " := " ++ format y ++ ";" ++ Format.line ++ formatFnBody b

library/init/lean/compiler/ir/freevars.lean

@@ -59,7 +59,7 @@ collectArray alts $ λ alt, f alt.body
 
 partial def collectFnBody : FnBody → Collector
 | (FnBody.vdecl x _ v b)    := collectExpr v; collectFnBody b
-| (FnBody.jdecl j ys _ v b) := collectFnBody v; collectParams ys; collectFnBody b
+| (FnBody.jdecl j ys v b)   := collectFnBody v; collectParams ys; collectFnBody b
 | (FnBody.set x _ y b)      := collectVar x; collectVar y; collectFnBody b
 | (FnBody.uset x _ y b)     := collectVar x; collectVar y; collectFnBody b
 | (FnBody.sset x _ _ y _ b) := collectVar x; collectVar y; collectFnBody b
@@ -153,7 +153,7 @@ collectArray alts $ λ alt, f alt.body
 
 partial def collectFnBody : FnBody → Collector
 | (FnBody.vdecl x _ v b)    := collectExpr v; withVar x (collectFnBody b)
-| (FnBody.jdecl j ys _ v b) := withParams ys (collectFnBody v); withJP j (collectFnBody b)
+| (FnBody.jdecl j ys v b)   := withParams ys (collectFnBody v); withJP j (collectFnBody b)
 | (FnBody.set x _ y b)      := collectVar x; collectVar y; collectFnBody b
 | (FnBody.uset x _ y b)     := collectVar x; collectVar y; collectFnBody b
 | (FnBody.sset x _ _ y _ b) := collectVar x; collectVar y; collectFnBody b
@@ -210,7 +210,7 @@ def visitExpr (w : Index) : Expr → Bool
 
 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.jdecl j ys v b)   := visitFnBody v || visitFnBody b
 | (FnBody.set x _ y b)      := visitVar w x || visitVar 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

library/init/lean/compiler/ir/livevars.lean

@@ -50,7 +50,7 @@ local attribute [instance] monadInhabited
 
 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.jdecl j ys v b)   := visitFnBody v <||> visitFnBody b
 | (FnBody.set x _ y b)      := visitVar w x <||> visitVar 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

library/init/lean/compiler/ir/normids.lean

@@ -74,9 +74,9 @@ local attribute [instance] monadInhabited
 
 partial def normFnBody : FnBody → N FnBody
 | (FnBody.vdecl x t v b)     := do v ← normExpr v, withVar x $ λ x, FnBody.vdecl x t v <$> normFnBody b
-| (FnBody.jdecl j ys t v b)  := do
+| (FnBody.jdecl j ys v b)    := do
   (ys, v) ← withParams ys $ λ ys, do { v ← normFnBody v, pure (ys, v) },
-  withJP j $ λ j, FnBody.jdecl j ys t v <$> normFnBody b
+  withJP j $ λ j, FnBody.jdecl j ys v <$> normFnBody b
 | (FnBody.set x i y b)       := do x ← normVar x, y ← normVar y, FnBody.set x i y <$> normFnBody b
 | (FnBody.uset x i y b)      := do x ← normVar x, y ← normVar y, FnBody.uset x i y <$> normFnBody b
 | (FnBody.sset x i o y t b)  := do x ← normVar x, y ← normVar y, FnBody.sset x i o y t <$> normFnBody b

library/init/lean/compiler/ir/resetreuse.lean

@@ -42,10 +42,10 @@ private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
     FnBody.vdecl x t (Expr.reuse w c updtCidx ys) b
   else
     FnBody.vdecl x t v (S b)
-| (FnBody.jdecl j ys t v b) :=
+| (FnBody.jdecl j ys v b) :=
   let v' := S v in
-  if v == v' then FnBody.jdecl j ys t v (S b)
-  else FnBody.jdecl j ys t v' b
+  if v == v' then FnBody.jdecl j ys v (S b)
+  else FnBody.jdecl j ys v' b
 | (FnBody.case tid x alts)  := FnBody.case tid x $ alts.hmap $ λ alt, alt.modifyBody S
 | b :=
   if b.isTerminal then b
@@ -79,13 +79,13 @@ private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody → M (FnBody × B
     alts ← alts.hmmap $ λ alt, alt.mmodifyBody (λ b, Dmain b >>= Dfinalize x c),
     pure (FnBody.case tid y alts, true)
   else pure (e, false)
-| e@(FnBody.jdecl j ys t v b) := do
+| e@(FnBody.jdecl j ys v b) := do
   (b, _) ← adaptReader (λ ctx : Context, ctx.addDecl e) (Dmain b),
   (v, found) ← Dmain v,
   /- If `found == true`, then `Dmain b` must also have returned `(b, true)` since
      we assume the IR does not have dead join points. So, if `x` is live in `j`,
      then it must also live in `b` since `j` is reachable from `b` with a `jmp`. -/
-  pure (FnBody.jdecl j ys t v b, found)
+  pure (FnBody.jdecl j ys v b, found)
 | e := do
   ctx ← read,
   if e.isTerminal then
@@ -108,8 +108,8 @@ private partial def hasCtorUsing (x : VarId) : FnBody → Bool
            | Arg.var y := x == y
            | _         := false)
   || hasCtorUsing b
-| (FnBody.jdecl _ _ _ v b) := hasCtorUsing v || hasCtorUsing b
-| b                        := !b.isTerminal && hasCtorUsing b.body
+| (FnBody.jdecl _ _ v b) := hasCtorUsing v || hasCtorUsing b
+| b                      := !b.isTerminal && hasCtorUsing b.body
 
 private def D (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody :=
 /- If the scrutinee `x` (the one that is providing memory) is being
@@ -127,10 +127,10 @@ private partial def R : FnBody → M FnBody
       | _            := pure alt
     },
     pure $ FnBody.case tid x alts
-| e@(FnBody.jdecl j ys t v b) := do
+| e@(FnBody.jdecl j ys v b) := do
   v ← R v,
   b ← adaptReader (λ ctx : Context, ctx.addDecl e) (R b),
-  pure $ FnBody.jdecl j ys t v b
+  pure $ FnBody.jdecl j ys v b
 | e := do
   if e.isTerminal then pure e
   else do

src/library/compiler/ir.cpp

@@ -27,7 +27,7 @@ object * mk_app_expr_core(object * x, object * ys);
 object * mk_num_expr_core(object * v);
 object * mk_str_expr_core(object * v);
 object * mk_vdecl_core(object * x, uint8 ty, object * e, object * b);
-object * mk_jdecl_core(object * j, object * xs, uint8 ty, object * v, object * b);
+object * mk_jdecl_core(object * j, object * xs, object * v, object * b);
 object * mk_uset_core(object * x, object * i, object * y, object * b);
 object * mk_sset_core(object * x, object * i, object * o, object * y, uint8 ty, object * b);
 object * mk_case_core(object * tid, object * x, object * cs);
@@ -79,9 +79,9 @@ fn_body mk_vdecl(var_id const & x, type ty, expr const & e, fn_body const & b) {
     inc(x.raw()); inc(e.raw()), inc(b.raw());
     return fn_body(mk_vdecl_core(x.raw(), static_cast<uint8>(ty), e.raw(), b.raw()));
 }
-fn_body mk_jdecl(jp_id const & j, buffer<param> const & xs, type ty, expr const & v, fn_body const & b) {
+fn_body mk_jdecl(jp_id const & j, buffer<param> const & xs, expr const & v, fn_body const & b) {
     inc(j.raw()); inc(v.raw()); inc(b.raw());
-    return fn_body(mk_jdecl_core(j.raw(), to_array(xs), static_cast<uint8>(ty), v.raw(), b.raw()));
+    return fn_body(mk_jdecl_core(j.raw(), to_array(xs), v.raw(), b.raw()));
 }
 fn_body mk_uset(var_id const & x, unsigned i, var_id const & y, fn_body const & b) {
     inc(x.raw()); inc(y.raw()); inc(b.raw());
@@ -293,8 +293,7 @@ class to_ir_fn {
         expr val = *decl.get_value();
         buffer<ir::param> xs;
         ir::fn_body v = visit_lambda(val, xs);
-        ir::type t    = to_ir_result_type(decl.get_type(), xs.size());
-        return ir::mk_jdecl(to_jp_id(decl), xs, t, v, b);
+        return ir::mk_jdecl(to_jp_id(decl), xs, v, b);
     }
 
     ir::fn_body visit_ctor(local_decl const & decl, ir::fn_body const & b) {

src/stage0/CMakeLists.txt

@@ -1 +1 @@
-add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/stringliteral.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
+add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/stringliteral.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)

src/stage0/init/control/default.cpp

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.control.default
-// Imports: init.control.applicative init.control.functor init.control.alternative init.control.monad init.control.lift init.control.state init.control.id init.control.except init.control.reader init.control.option init.control.combinators
+// Imports: init.control.applicative init.control.functor init.control.alternative init.control.monad init.control.lift init.control.state init.control.id init.control.except init.control.reader init.control.option init.control.combinators init.control.conditional
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -25,6 +25,7 @@ obj* initialize_init_control_except(obj*);
 obj* initialize_init_control_reader(obj*);
 obj* initialize_init_control_option(obj*);
 obj* initialize_init_control_combinators(obj*);
+obj* initialize_init_control_conditional(obj*);
 static bool _G_initialized = false;
 obj* initialize_init_control_default(obj* w) {
  if (_G_initialized) return w;
@@ -52,5 +53,7 @@ w = initialize_init_control_option(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_control_combinators(w);
 if (io_result_is_error(w)) return w;
+w = initialize_init_control_conditional(w);
+if (io_result_is_error(w)) return w;
 return w;
 }

src/stage0/init/core.cpp

@@ -52,7 +52,6 @@ obj* l_Thunk_bind___boxed(obj*, obj*, obj*, obj*);
 obj* l_decidableOfDecidableOfEq___boxed(obj*, obj*);
 obj* l_ite___boxed(obj*);
 obj* l_Quot_liftOn___rarg(obj*, obj*, obj*);
-uint8 l_Decidable_toBool___rarg(uint8);
 uint8 l_Bool_DecidableEq(uint8, uint8);
 obj* l_Function_onFun___boxed(obj*, obj*, obj*);
 obj* l_inline(obj*);
@@ -156,6 +155,7 @@ obj* l_Prod_DecidableEq___boxed(obj*, obj*);
 obj* l_Subtype_sizeof___main(obj*);
 obj* l_Quot_recOnSubsingleton(obj*, obj*, obj*, obj*);
 obj* l_Prod_HasSizeof___boxed(obj*, obj*);
+obj* l_Decidable_decide___boxed(obj*);
 obj* l_Quotient_liftOn___boxed(obj*, obj*, obj*);
 obj* l_PSum_sizeof(obj*, obj*);
 obj* l_Task_map___boxed(obj*, obj*, obj*, obj*);
@@ -284,6 +284,7 @@ obj* l_Prod_map___main___rarg(obj*, obj*, obj*);
 uint8 l_ite_Decidable___rarg(uint8, uint8, uint8);
 obj* l___private_init_core_21__funSetoid(obj*, obj*);
 obj* l_Quot_hrecOn___boxed(obj*, obj*, obj*);
+uint8 l_Decidable_decide___rarg(uint8);
 obj* l_Xor_Decidable(obj*, obj*);
 obj* l_Nat_add___boxed(obj*, obj*);
 obj* l_PSum_sizeof___rarg(obj*, obj*, obj*);
@@ -340,7 +341,6 @@ uint8 l_Xor_Decidable___rarg(uint8, uint8);
 obj* l_typedExpr___boxed(obj*);
 obj* l_Decidable_byCases___boxed(obj*, obj*);
 obj* l_cond___rarg(uint8, obj*, obj*);
-obj* l_Decidable_toBool(obj*);
 obj* l_Bool_sizeof(uint8);
 obj* l_Pi_Inhabited___boxed(obj*, obj*);
 obj* l_Prod_map(obj*, obj*, obj*, obj*);
@@ -379,6 +379,7 @@ obj* l_Function_const___rarg(obj*, obj*);
 obj* l_Eq_ndrec(obj*, obj*, obj*);
 obj* l_Subtype_HasSizeof___boxed(obj*);
 uint8 l_xor___main(uint8, uint8);
+obj* l_Decidable_decide(obj*);
 obj* l_idRhs___rarg___boxed(obj*);
 obj* l_Quotient_recOnSubsingleton_u_2082___at_Quotient_DecidableEq___spec__1(obj*, obj*);
 obj* l_Subtype_sizeof___rarg___boxed(obj*, obj*, obj*);
@@ -407,6 +408,7 @@ uint8 l_Quotient_DecidableEq___rarg___lambda__1(obj*, obj*, obj*);
 obj* l_inferInstanceAs(obj*);
 obj* l_absurd___boxed(obj*, obj*, obj*, obj*);
 obj* l_PSigma_HasSizeof___boxed(obj*, obj*);
+obj* l_Decidable_decide___rarg___boxed(obj*);
 obj* l_Function_comp(obj*, obj*, obj*);
 uint8 l_prodHasDecidableLt___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Function_combine(obj*, obj*, obj*, obj*, obj*);
@@ -439,7 +441,6 @@ obj* l_inferInstance(obj*);
 obj* l_absurd(obj*, obj*, obj*, obj*);
 obj* l_xor___main___boxed(obj*, obj*);
 uint8 l_decidableOfDecidableOfIff___rarg(uint8, obj*);
-obj* l_Decidable_toBool___boxed(obj*);
 obj* l_PSigma_sizeof___rarg(obj*, obj*, obj*);
 obj* l_Decidable_byCases(obj*, obj*);
 obj* l_Ne_Decidable___boxed(obj*);
@@ -452,7 +453,6 @@ obj* l_Prod_sizeof___boxed(obj*, obj*);
 obj* l_PSigma_sizeof___main___rarg(obj*, obj*, obj*);
 obj* l_Option_sizeof(obj*);
 obj* l_Quotient_recOnSubsingleton___boxed(obj*, obj*, obj*, obj*);
-obj* l_Decidable_toBool___rarg___boxed(obj*);
 obj* l_Sigma_sizeof___main___boxed(obj*, obj*);
 obj* l_Sum_inhabitedLeft(obj*, obj*);
 obj* l_Function_swap___rarg(obj*, obj*, obj*);
@@ -2692,7 +2692,7 @@ lean::dec(x_2);
 return x_3;
 }
 }
-uint8 l_Decidable_toBool___rarg(uint8 x_0) {
+uint8 l_Decidable_decide___rarg(uint8 x_0) {
 _start:
 {
 if (x_0 == 0)
@@ -2709,29 +2709,29 @@ return x_2;
 }
 }
 }
-obj* l_Decidable_toBool(obj* x_0) {
+obj* l_Decidable_decide(obj* x_0) {
 _start:
 {
 obj* x_1; 
-x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Decidable_toBool___rarg___boxed), 1, 0);
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Decidable_decide___rarg___boxed), 1, 0);
 return x_1;
 }
 }
-obj* l_Decidable_toBool___rarg___boxed(obj* x_0) {
+obj* l_Decidable_decide___rarg___boxed(obj* x_0) {
 _start:
 {
 uint8 x_1; uint8 x_2; obj* x_3; 
 x_1 = lean::unbox(x_0);
-x_2 = l_Decidable_toBool___rarg(x_1);
+x_2 = l_Decidable_decide___rarg(x_1);
 x_3 = lean::box(x_2);
 return x_3;
 }
 }
-obj* l_Decidable_toBool___boxed(obj* x_0) {
+obj* l_Decidable_decide___boxed(obj* x_0) {
 _start:
 {
 obj* x_1; 
-x_1 = l_Decidable_toBool(x_0);
+x_1 = l_Decidable_decide(x_0);
 lean::dec(x_0);
 return x_1;
 }

src/stage0/init/data/array/basic.cpp

@@ -15,6 +15,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
 obj* l_List_toArrayAux___rarg(obj*, obj*);
+obj* l_Array_anyMAux___main___at_Array_any___spec__1(obj*);
 obj* l_Array_extractAux___main___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_append(obj*);
 obj* l_Array_foldlFrom___rarg(obj*, obj*, obj*, obj*);
@@ -24,6 +25,7 @@ obj* l_Array_hmmapAux___main___at_Array_hmapIdx___spec__1(obj*);
 obj* l_Array_miterateAux___main___at_Array_iterateFrom___spec__1___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_shrink___main___rarg___boxed(obj*, obj*);
 obj* l_Array_hmap(obj*);
+obj* l_Array_mforAux___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_miterate_u_2082Aux___main___at_Array_foldl_u_2082___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_hmmap___rarg(obj*, obj*, obj*, obj*);
 obj* l_Array_toList___rarg___boxed(obj*);
@@ -32,6 +34,7 @@ obj* l_Array_empty___closed__1;
 namespace lean {
 obj* nat_sub(obj*, obj*);
 }
+obj* l_Array_anyMAux___main___at_Array_all___spec__1___rarg___boxed(obj*, obj*, obj*);
 obj* l_Array_getOpt(obj*);
 obj* l_Array_miterateAux___main___at_Array_foldlFrom___spec__1(obj*, obj*);
 obj* l_Array_any(obj*);
@@ -40,9 +43,9 @@ obj* l_Array_swap___boxed(obj*, obj*, obj*, obj*);
 obj* l___private_init_data_array_basic_1__revIterateAux___main___at_Array_toList___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_revFoldl(obj*, obj*);
 obj* l_Array_back___boxed(obj*);
+obj* l_Array_mfor___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_extract___rarg___boxed(obj*, obj*, obj*);
 obj* l_Array_miterate___boxed(obj*, obj*, obj*);
-uint8 l_Array_anyAux___rarg(obj*, obj*, obj*);
 obj* l_Array_isEmpty___boxed(obj*);
 obj* l_Array_iterate___rarg___boxed(obj*, obj*, obj*);
 obj* l_Array_mfoldl___rarg(obj*, obj*, obj*, obj*);
@@ -51,6 +54,7 @@ obj* l_Array_miterateAux___main___at_Array_iterate___spec__1(obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_foldlFrom___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_reverse(obj*);
 obj* l_Array_filter(obj*);
+obj* l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_hmmapAux___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_mfoldl_u_2082___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_all___rarg___boxed(obj*, obj*);
@@ -66,7 +70,7 @@ obj* l_Array_any___boxed(obj*);
 obj* l_Array_extractAux(obj*);
 obj* l_Array_HasRepr(obj*);
 obj* l_Array_singleton___boxed(obj*);
-obj* l_Array_anyAux___main___at_Array_all___spec__1(obj*);
+obj* l_Array_allM___boxed(obj*, obj*);
 obj* l_Array_hmmapAux___main___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_iterate_u_2082___rarg___boxed(obj*, obj*, obj*, obj*);
 obj* l_Array_back___rarg___boxed(obj*, obj*);
@@ -83,12 +87,13 @@ obj* l_Array_iterate___boxed(obj*, obj*);
 obj* l_Array_size___boxed(obj*, obj*);
 obj* l_Array_uset___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_iterateFrom___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_anyMAux___main___rarg(obj*, obj*, obj*, obj*);
 obj* l_Array_isEqvAux___main___boxed(obj*);
 obj* l_List_toArrayAux___main___rarg(obj*, obj*);
 obj* l_Array_isEqv___rarg___boxed(obj*, obj*, obj*);
 obj* l_Array_fswapAt___rarg___boxed(obj*, obj*, obj*);
 obj* l_Array_mfoldlFrom___rarg(obj*, obj*, obj*, obj*, obj*);
-uint8 l_Array_anyAux___main___at_Array_all___spec__1___rarg(obj*, obj*, obj*);
+obj* l_Array_anyMAux(obj*, obj*);
 obj* l_Array_extractAux___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_miterate_u_2082___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_mfoldlFrom___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
@@ -108,6 +113,7 @@ obj* l_Array_miterateAux___main___at_Array_mfoldl___spec__1(obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_iterate___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_pop___boxed(obj*, obj*);
 obj* l_Array_foldlFrom___rarg___boxed(obj*, obj*, obj*, obj*);
+obj* l_Array_anyMAux___main___at_Array_all___spec__1(obj*);
 uint8 l_Array_isEqvAux___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_hmmapAux___main___at_Array_hmap___spec__1___boxed(obj*);
 obj* l_Array_Inhabited___boxed(obj*);
@@ -133,21 +139,24 @@ obj* l_Array_toList___rarg(obj*);
 obj* l_Array_uget___boxed(obj*, obj*, obj*, obj*);
 obj* l___private_init_data_array_basic_1__revIterateAux___main___at_Array_revFoldl___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 uint8 l_Array_HasBeq___rarg(obj*, obj*, obj*);
+obj* l_Array_allM(obj*, obj*);
 obj* l_Array_hmapIdx(obj*);
 obj* l_Array_get___boxed(obj*, obj*, obj*, obj*);
 obj* l_Array_miterate_u_2082Aux___boxed(obj*, obj*, obj*);
 obj* l_Array_iterate(obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_mmap___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_mfindAux___boxed(obj*, obj*, obj*);
+obj* l_Array_mfor(obj*);
 obj* l_Array_reverseAux___main___boxed(obj*);
 obj* l_Array_mfindAux___main___at_Array_find___spec__1(obj*, obj*);
 obj* l_Array_extract___rarg(obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_mfoldl___spec__1___boxed(obj*, obj*, obj*);
 obj* l_Array_hmmapAux___main(obj*, obj*);
 obj* l_Array_miterate_u_2082Aux___main___at_Array_iterate_u_2082___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
+uint8 l_Array_allM___rarg___lambda__1(uint8);
 obj* l_Array_mfindAux___main___rarg(obj*, obj*, obj*, obj*);
-obj* l_Array_anyAux(obj*);
 obj* l_Array_isEqv(obj*);
+obj* l_Array_anyMAux___main___at_Array_any___spec__1___boxed(obj*);
 obj* l_Array_mfind___boxed(obj*, obj*, obj*);
 obj* l_Array_iterateFrom___boxed(obj*, obj*);
 obj* l_Array_mfindAux___main(obj*, obj*, obj*);
@@ -159,6 +168,7 @@ obj* l___private_init_data_array_basic_1__revIterateAux___main___rarg(obj*, obj*
 obj* l_List_toString___rarg(obj*, obj*);
 obj* l_Array_miterate_u_2082Aux(obj*, obj*, obj*);
 obj* l_Array_revIterate___boxed(obj*, obj*);
+obj* l_Array_anyMAux___main___at_Array_all___spec__1___boxed(obj*);
 obj* l_Array_revFoldl___rarg___boxed(obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_foldlFrom___spec__1___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_swapAt___rarg___boxed(obj*, obj*, obj*);
@@ -170,18 +180,22 @@ obj* l_Array_miterateAux___main(obj*, obj*, obj*);
 obj* l_Array_mfindAux___main___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_miterate_u_2082Aux___main(obj*, obj*, obj*);
 obj* l_Array_HasBeq___rarg___boxed(obj*, obj*, obj*);
+obj* l_Array_allM___rarg___lambda__1___boxed(obj*);
 obj* l_Array_foldl(obj*, obj*);
 obj* l_Array_miterate_u_2082Aux___main___at_Array_mfoldl_u_2082___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_mfindAux___main___at_Array_find___spec__1___rarg(obj*, obj*, obj*);
 obj* l_Array_hmap___rarg(obj*, obj*, obj*);
 obj* l_Array_append___boxed(obj*);
 obj* l_Array_hmmapAux___main___at_Array_hmmap___spec__1(obj*, obj*);
+obj* l_Array_anyMAux___main___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_filterAux___main___rarg(obj*, obj*, obj*, obj*);
 obj* l_Array_foldl___boxed(obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_mmap___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_mforAux___main___boxed(obj*);
 obj* l_Array_singleton___rarg(obj*);
 obj* l_Array_HasEmptyc___boxed(obj*);
 obj* l_Array_miterateAux___main___at_Array_foldl___spec__1___boxed(obj*, obj*);
+uint8 l_Array_anyMAux___main___at_Array_all___spec__1___rarg(obj*, obj*, obj*);
 obj* l_Array_filter___rarg(obj*, obj*);
 namespace lean {
 obj* nat_add(obj*, obj*);
@@ -198,45 +212,50 @@ uint8 l_Array_isEmpty___rarg(obj*);
 obj* l_Array_miterateAux___main___at_Array_iterateFrom___spec__1___boxed(obj*, obj*);
 uint8 l_Array_any___rarg(obj*, obj*);
 obj* l_Array_iterateFrom(obj*, obj*);
+obj* l_Array_anyMAux___main(obj*, obj*);
+obj* l_Array_mforAux___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_map___rarg___boxed(obj*, obj*);
 obj* l_Array_push___boxed(obj*, obj*, obj*);
 obj* l_Array_fget___boxed(obj*, obj*, obj*);
-uint8 l_Array_anyAux___main___rarg(obj*, obj*, obj*);
 obj* l_Array_foldl_u_2082(obj*, obj*);
 obj* l_Array_reverseAux___rarg(obj*, obj*);
 obj* l_Array_miterate_u_2082Aux___main___boxed(obj*, obj*, obj*);
-obj* l_Array_anyAux___boxed(obj*);
+obj* l_Array_anyMAux___main___at_Array_allM___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
 uint8 l_Array_isEqv___rarg(obj*, obj*, obj*);
 obj* l_Array_map(obj*, obj*);
 obj* l_Array_map___boxed(obj*, obj*);
 obj* l_Array_hmap___boxed(obj*);
 obj* l_Array_foldl_u_2082___boxed(obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_foldl___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_anyMAux___main___at_Array_any___spec__1___rarg___boxed(obj*, obj*, obj*);
 obj* l_Array_mmap___rarg(obj*, obj*, obj*, obj*);
 obj* l___private_init_data_array_basic_1__revIterateAux___boxed(obj*, obj*);
 obj* l_Array_miterate_u_2082___boxed(obj*, obj*, obj*);
 obj* l_Array_mfoldl_u_2082(obj*, obj*, obj*);
 obj* l_Array_filterAux___rarg(obj*, obj*, obj*, obj*);
 obj* l_Array_miterate_u_2082Aux___main___at_Array_foldl_u_2082___spec__1___boxed(obj*, obj*);
+obj* l_Array_mforAux(obj*);
 obj* l_Array_iterateFrom___rarg___boxed(obj*, obj*, obj*, obj*);
 obj* l_Array_back(obj*);
 obj* l_Array_miterateAux___main___at_Array_mmap___spec__1___rarg___lambda__1(obj*, obj*, obj*);
 obj* l___private_init_data_array_basic_1__revIterateAux___main___at_Array_toList___spec__1___boxed(obj*);
 obj* l_Array_isEqvAux___main(obj*);
+obj* l_Array_anyMAux___main___at_Array_allM___spec__1___boxed(obj*, obj*);
 obj* l_Array_shrink___main(obj*);
 obj* l___private_init_data_array_basic_1__revIterateAux___main___at_Array_toList___spec__1___rarg(obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_anyMAux___boxed(obj*, obj*);
 obj* l_Array_miterateAux___main___boxed(obj*, obj*, obj*);
 obj* l_List_toArray(obj*);
 obj* l_List_redLength___boxed(obj*);
 obj* l_Array_getOpt___rarg(obj*, obj*);
 obj* l_Array_reverseAux___main(obj*);
 obj* l_Array_hmmapAux___main___at_Array_hmap___spec__1(obj*);
+obj* l_Array_mfor___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_List_toArrayAux___boxed(obj*);
 obj* l_Array_hmmapAux___main___at_Array_hmapIdx___spec__1___boxed(obj*);
 obj* l_Array_append___rarg(obj*, obj*);
 obj* l_Array_miterate_u_2082Aux___main___at_Array_iterate_u_2082___spec__1___boxed(obj*, obj*);
 obj* l_Array_mmap___rarg___boxed(obj*, obj*, obj*, obj*);
-obj* l_Array_anyAux___main___at_Array_all___spec__1___boxed(obj*);
 obj* l_Array_Inhabited(obj*);
 obj* l_Array_miterate_u_2082Aux___main___at_Array_iterate_u_2082___spec__1(obj*, obj*);
 obj* l_Array_modify___rarg___boxed(obj*, obj*, obj*, obj*);
@@ -244,8 +263,10 @@ obj* l_Array_revIterate___rarg(obj*, obj*, obj*);
 obj* l_Array_HasRepr___rarg___closed__1;
 obj* l_Array_HasToString(obj*);
 obj* l_Array_singleton(obj*);
+obj* l_Array_allM___rarg___closed__1;
 obj* l_Array_shrink___rarg___boxed(obj*, obj*);
 obj* l_List_toArray___boxed(obj*);
+obj* l_Array_mforAux___main___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_hmapIdx___boxed(obj*);
 obj* l_Array_HasAppend___closed__1;
 obj* l_Array_isEmpty___rarg___boxed(obj*);
@@ -262,16 +283,16 @@ obj* l_Array_empty___boxed(obj*);
 obj* l_Array_filterAux___main(obj*);
 obj* l_Array_reverseAux___main___rarg(obj*, obj*);
 obj* l_Array_HasToString___boxed(obj*);
+obj* l_Array_anyMAux___main___rarg___lambda__1(obj*, obj*, obj*, obj*, uint8);
 obj* l_List_redLength___main___boxed(obj*);
-obj* l_Array_anyAux___main(obj*);
 obj* l_Array_miterateAux(obj*, obj*, obj*);
-obj* l_Array_anyAux___main___boxed(obj*);
 obj* l_Array_extractAux___main(obj*);
 obj* l_Array_miterate_u_2082Aux___main___at_Array_iterate_u_2082___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_hmmapAux___main___at_Array_hmmap___spec__1___boxed(obj*, obj*);
 obj* l_Array_modify___boxed(obj*);
 obj* l_Array_mfindAux___main___at_Array_find___spec__1___rarg___boxed(obj*, obj*, obj*);
 obj* l_Array_modify___rarg(obj*, obj*, obj*, obj*);
+obj* l_Array_mforAux___main___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_map___spec__1(obj*, obj*);
 obj* l_Array_isEmpty(obj*);
 obj* l_Array_mfoldl_u_2082___boxed(obj*, obj*, obj*);
@@ -281,20 +302,22 @@ obj* l_Array_hmmapAux(obj*, obj*);
 obj* l_Array_reverse___boxed(obj*);
 obj* l_Array_foldl_u_2082___rarg(obj*, obj*, obj*, obj*);
 obj* l_Array_mfoldlFrom___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
-obj* l_Array_anyAux___main___rarg___boxed(obj*, obj*, obj*);
+obj* l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*, uint8);
 obj* l_Array_HasAppend___boxed(obj*);
 obj* l_Array_mfoldl(obj*, obj*, obj*);
-obj* l_Array_anyAux___rarg___boxed(obj*, obj*, obj*);
 obj* l_Array_mfind___rarg(obj*, obj*, obj*);
 obj* l_Array_miterate(obj*, obj*, obj*);
 obj* l_Array_revFoldl___boxed(obj*, obj*);
 uint8 l_Array_isEqvAux___main___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_foldlFrom(obj*, obj*);
+uint8 l_Array_anyMAux___main___at_Array_any___spec__1___rarg(obj*, obj*, obj*);
+obj* l_Array_anyMAux___main___boxed(obj*, obj*);
 obj* l_Array_isEqvAux___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_HasRepr___boxed(obj*);
 obj* l___private_init_data_array_basic_1__revIterateAux___main___at_Array_toList___spec__1(obj*);
 obj* l___private_init_data_array_basic_1__revIterateAux(obj*, obj*);
 obj* l_Array_extract___boxed(obj*);
+obj* l_Array_anyM(obj*, obj*);
 obj* l_Array_hmmapAux___main___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_HasRepr___rarg(obj*);
 obj* l_Array_find___rarg(obj*, obj*);
@@ -311,6 +334,7 @@ obj* l_Array_hmapIdx___rarg(obj*, obj*, obj*);
 obj* l_Array_getOpt___boxed(obj*);
 obj* l___private_init_data_array_basic_1__revIterateAux___main___boxed(obj*, obj*);
 obj* l_Array_shrink(obj*);
+obj* l_Array_anyM___rarg(obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_append___spec__1___rarg___boxed(obj*, obj*, obj*, obj*);
 namespace lean {
 obj* nat_div(obj*, obj*);
@@ -321,6 +345,7 @@ obj* l_Array_hmmap___boxed(obj*, obj*);
 obj* l_Array_HasToString___rarg(obj*);
 obj* l_Array_miterateAux___main___at_Array_mfoldl___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_reverse___rarg(obj*);
+obj* l_Array_mfor___boxed(obj*);
 obj* l_Array_mmap___boxed(obj*, obj*);
 obj* l_Array_shrink___main___boxed(obj*);
 obj* l_Array_find(obj*, obj*);
@@ -330,11 +355,15 @@ obj* l_Array_miterateAux___main___at_Array_mmap___spec__1(obj*, obj*);
 obj* l_Array_miterate_u_2082Aux___main___at_Array_mfoldl_u_2082___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_miterate_u_2082Aux___main___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___rarg(obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_anyMAux___main___at_Array_allM___spec__1(obj*, obj*);
 obj* l_Array_revIterate(obj*, obj*);
+obj* l_Array_mforAux___boxed(obj*);
 obj* l_Array_miterateAux___main___at_Array_mfoldl___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_getOpt___rarg___boxed(obj*, obj*);
+obj* l_Array_allM___rarg(obj*, obj*, obj*);
 obj* l_Array_foldl_u_2082___rarg___boxed(obj*, obj*, obj*, obj*);
 obj* l_Array_miterate_u_2082Aux___main___at_Array_foldl_u_2082___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_anyM___boxed(obj*, obj*);
 obj* l_Array_mmap(obj*, obj*);
 obj* l_Array_find___rarg___boxed(obj*, obj*);
 obj* l_Array_toList(obj*);
@@ -356,7 +385,6 @@ obj* l_Array_foldlFrom___boxed(obj*, obj*);
 obj* l_Array_modify(obj*);
 obj* l_Array_mfindAux(obj*, obj*, obj*);
 obj* l_Array_miterateAux___boxed(obj*, obj*, obj*);
-obj* l_Array_anyAux___main___at_Array_all___spec__1___rarg___boxed(obj*, obj*, obj*);
 obj* l_Array_mkEmpty___boxed(obj*, obj*);
 obj* l_Array_iterateFrom___rarg(obj*, obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_map___spec__1___boxed(obj*, obj*);
@@ -371,6 +399,8 @@ obj* l_Array_miterate_u_2082Aux___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_back___rarg(obj*, obj*);
 obj* l_List_redLength___rarg(obj*);
 obj* l_Array_find___boxed(obj*, obj*);
+obj* l_Array_anyMAux___rarg(obj*, obj*, obj*, obj*);
+obj* l_Array_mforAux___main(obj*);
 obj* l_Array_size___boxed(obj* x_0, obj* x_1) {
 _start:
 {
@@ -2308,17 +2338,348 @@ lean::dec(x_1);
 return x_2;
 }
 }
-uint8 l_Array_anyAux___main___rarg(obj* x_0, obj* x_1, obj* x_2) {
+obj* l_Array_anyMAux___main___rarg___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, uint8 x_4) {
+_start:
+{
+if (x_4 == 0)
+{
+obj* x_5; obj* x_6; obj* x_7; 
+x_5 = lean::mk_nat_obj(1ul);
+x_6 = lean::nat_add(x_0, x_5);
+x_7 = l_Array_anyMAux___main___rarg(x_1, x_2, x_3, x_6);
+return x_7;
+}
+else
+{
+obj* x_10; obj* x_13; obj* x_16; obj* x_17; 
+lean::dec(x_3);
+lean::dec(x_2);
+x_10 = lean::cnstr_get(x_1, 0);
+lean::inc(x_10);
+lean::dec(x_1);
+x_13 = lean::cnstr_get(x_10, 1);
+lean::inc(x_13);
+lean::dec(x_10);
+x_16 = lean::box(x_4);
+x_17 = lean::apply_2(x_13, lean::box(0), x_16);
+return x_17;
+}
+}
+}
+obj* l_Array_anyMAux___main___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; uint8 x_5; 
+x_4 = lean::array_get_size(x_1);
+x_5 = lean::nat_dec_lt(x_3, x_4);
+lean::dec(x_4);
+if (x_5 == 0)
+{
+obj* x_10; obj* x_13; uint8 x_16; obj* x_17; obj* x_18; 
+lean::dec(x_1);
+lean::dec(x_3);
+lean::dec(x_2);
+x_10 = lean::cnstr_get(x_0, 0);
+lean::inc(x_10);
+lean::dec(x_0);
+x_13 = lean::cnstr_get(x_10, 1);
+lean::inc(x_13);
+lean::dec(x_10);
+x_16 = 0;
+x_17 = lean::box(x_16);
+x_18 = lean::apply_2(x_13, lean::box(0), x_17);
+return x_18;
+}
+else
+{
+obj* x_19; obj* x_21; obj* x_23; obj* x_24; obj* x_25; 
+x_19 = lean::cnstr_get(x_0, 1);
+lean::inc(x_19);
+x_21 = lean::array_fget(x_1, x_3);
+lean::inc(x_2);
+x_23 = lean::apply_1(x_2, x_21);
+x_24 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_anyMAux___main___rarg___lambda__1___boxed), 5, 4);
+lean::closure_set(x_24, 0, x_3);
+lean::closure_set(x_24, 1, x_0);
+lean::closure_set(x_24, 2, x_1);
+lean::closure_set(x_24, 3, x_2);
+x_25 = lean::apply_4(x_19, lean::box(0), lean::box(0), x_23, x_24);
+return x_25;
+}
+}
+}
+obj* l_Array_anyMAux___main(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_anyMAux___main___rarg), 4, 0);
+return x_2;
+}
+}
+obj* l_Array_anyMAux___main___rarg___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+uint8 x_5; obj* x_6; 
+x_5 = lean::unbox(x_4);
+x_6 = l_Array_anyMAux___main___rarg___lambda__1(x_0, x_1, x_2, x_3, x_5);
+lean::dec(x_0);
+return x_6;
+}
+}
+obj* l_Array_anyMAux___main___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Array_anyMAux___main(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_Array_anyMAux___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Array_anyMAux___main___rarg(x_0, x_1, x_2, x_3);
+return x_4;
+}
+}
+obj* l_Array_anyMAux(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_anyMAux___rarg), 4, 0);
+return x_2;
+}
+}
+obj* l_Array_anyMAux___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Array_anyMAux(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_Array_anyM___rarg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; obj* x_4; 
+x_3 = lean::mk_nat_obj(0ul);
+x_4 = l_Array_anyMAux___main___rarg(x_0, x_1, x_2, x_3);
+return x_4;
+}
+}
+obj* l_Array_anyM(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_anyM___rarg), 3, 0);
+return x_2;
+}
+}
+obj* l_Array_anyM___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Array_anyM(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, uint8 x_6) {
+_start:
+{
+if (x_6 == 0)
+{
+obj* x_7; obj* x_8; obj* x_9; 
+x_7 = lean::mk_nat_obj(1ul);
+x_8 = lean::nat_add(x_0, x_7);
+x_9 = l_Array_anyMAux___main___at_Array_allM___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_8);
+return x_9;
+}
+else
+{
+obj* x_14; obj* x_17; obj* x_20; obj* x_21; 
+lean::dec(x_5);
+lean::dec(x_4);
+lean::dec(x_3);
+lean::dec(x_2);
+x_14 = lean::cnstr_get(x_1, 0);
+lean::inc(x_14);
+lean::dec(x_1);
+x_17 = lean::cnstr_get(x_14, 1);
+lean::inc(x_17);
+lean::dec(x_14);
+x_20 = lean::box(x_6);
+x_21 = lean::apply_2(x_17, lean::box(0), x_20);
+return x_21;
+}
+}
+}
+obj* l_Array_anyMAux___main___at_Array_allM___spec__1___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
+_start:
+{
+obj* x_6; uint8 x_7; 
+x_6 = lean::array_get_size(x_4);
+x_7 = lean::nat_dec_lt(x_5, x_6);
+lean::dec(x_6);
+if (x_7 == 0)
+{
+obj* x_14; obj* x_17; uint8 x_20; obj* x_21; obj* x_22; 
+lean::dec(x_5);
+lean::dec(x_4);
+lean::dec(x_1);
+lean::dec(x_3);
+lean::dec(x_2);
+x_14 = lean::cnstr_get(x_0, 0);
+lean::inc(x_14);
+lean::dec(x_0);
+x_17 = lean::cnstr_get(x_14, 1);
+lean::inc(x_17);
+lean::dec(x_14);
+x_20 = 0;
+x_21 = lean::box(x_20);
+x_22 = lean::apply_2(x_17, lean::box(0), x_21);
+return x_22;
+}
+else
+{
+obj* x_23; obj* x_25; obj* x_27; obj* x_30; obj* x_31; obj* x_32; 
+x_23 = lean::cnstr_get(x_0, 1);
+lean::inc(x_23);
+x_25 = lean::array_fget(x_4, x_5);
+lean::inc(x_1);
+x_27 = lean::apply_1(x_1, x_25);
+lean::inc(x_3);
+lean::inc(x_2);
+x_30 = lean::apply_4(x_2, lean::box(0), lean::box(0), x_3, x_27);
+x_31 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___lambda__1___boxed), 7, 6);
+lean::closure_set(x_31, 0, x_5);
+lean::closure_set(x_31, 1, x_0);
+lean::closure_set(x_31, 2, x_1);
+lean::closure_set(x_31, 3, x_2);
+lean::closure_set(x_31, 4, x_3);
+lean::closure_set(x_31, 5, x_4);
+x_32 = lean::apply_4(x_23, lean::box(0), lean::box(0), x_30, x_31);
+return x_32;
+}
+}
+}
+obj* l_Array_anyMAux___main___at_Array_allM___spec__1(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_anyMAux___main___at_Array_allM___spec__1___rarg), 6, 0);
+return x_2;
+}
+}
+uint8 l_Array_allM___rarg___lambda__1(uint8 x_0) {
+_start:
+{
+if (x_0 == 0)
+{
+uint8 x_1; 
+x_1 = 1;
+return x_1;
+}
+else
+{
+uint8 x_2; 
+x_2 = 0;
+return x_2;
+}
+}
+}
+obj* _init_l_Array_allM___rarg___closed__1() {
+_start:
+{
+obj* x_0; 
+x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_allM___rarg___lambda__1___boxed), 1, 0);
+return x_0;
+}
+}
+obj* l_Array_allM___rarg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; obj* x_5; obj* x_8; obj* x_11; obj* x_12; obj* x_14; obj* x_15; 
+x_3 = lean::cnstr_get(x_0, 0);
+lean::inc(x_3);
+x_5 = lean::cnstr_get(x_3, 0);
+lean::inc(x_5);
+lean::dec(x_3);
+x_8 = lean::cnstr_get(x_5, 0);
+lean::inc(x_8);
+lean::dec(x_5);
+x_11 = l_Array_allM___rarg___closed__1;
+x_12 = lean::mk_nat_obj(0ul);
+lean::inc(x_8);
+x_14 = l_Array_anyMAux___main___at_Array_allM___spec__1___rarg(x_0, x_2, x_8, x_11, x_1, x_12);
+x_15 = lean::apply_4(x_8, lean::box(0), lean::box(0), x_11, x_14);
+return x_15;
+}
+}
+obj* l_Array_allM(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_allM___rarg), 3, 0);
+return x_2;
+}
+}
+obj* l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___lambda__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
+_start:
+{
+uint8 x_7; obj* x_8; 
+x_7 = lean::unbox(x_6);
+x_8 = l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___lambda__1(x_0, x_1, x_2, x_3, x_4, x_5, x_7);
+lean::dec(x_0);
+return x_8;
+}
+}
+obj* l_Array_anyMAux___main___at_Array_allM___spec__1___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Array_anyMAux___main___at_Array_allM___spec__1(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l_Array_allM___rarg___lambda__1___boxed(obj* x_0) {
+_start:
+{
+uint8 x_1; uint8 x_2; obj* x_3; 
+x_1 = lean::unbox(x_0);
+x_2 = l_Array_allM___rarg___lambda__1(x_1);
+x_3 = lean::box(x_2);
+return x_3;
+}
+}
+obj* l_Array_allM___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l_Array_allM(x_0, x_1);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_2;
+}
+}
+uint8 l_Array_anyMAux___main___at_Array_any___spec__1___rarg(obj* x_0, obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; uint8 x_4; 
-x_3 = lean::array_get_size(x_0);
+x_3 = lean::array_get_size(x_1);
 x_4 = lean::nat_dec_lt(x_2, x_3);
 lean::dec(x_3);
 if (x_4 == 0)
 {
 uint8 x_8; 
-lean::dec(x_1);
+lean::dec(x_0);
 lean::dec(x_2);
 x_8 = 0;
 return x_8;
@@ -2326,9 +2687,9 @@ return x_8;
 else
 {
 obj* x_9; obj* x_11; uint8 x_12; 
-x_9 = lean::array_fget(x_0, x_2);
-lean::inc(x_1);
-x_11 = lean::apply_1(x_1, x_9);
+x_9 = lean::array_fget(x_1, x_2);
+lean::inc(x_0);
+x_11 = lean::apply_1(x_0, x_9);
 x_12 = lean::unbox(x_11);
 if (x_12 == 0)
 {
@@ -2341,74 +2702,18 @@ goto _start;
 }
 else
 {
-uint8 x_19; 
-lean::dec(x_1);
+lean::dec(x_0);
 lean::dec(x_2);
-x_19 = 1;
-return x_19;
+return x_12;
 }
 }
 }
 }
-obj* l_Array_anyAux___main(obj* x_0) {
+obj* l_Array_anyMAux___main___at_Array_any___spec__1(obj* x_0) {
 _start:
 {
 obj* x_1; 
-x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_anyAux___main___rarg___boxed), 3, 0);
-return x_1;
-}
-}
-obj* l_Array_anyAux___main___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {
-_start:
-{
-uint8 x_3; obj* x_4; 
-x_3 = l_Array_anyAux___main___rarg(x_0, x_1, x_2);
-x_4 = lean::box(x_3);
-lean::dec(x_0);
-return x_4;
-}
-}
-obj* l_Array_anyAux___main___boxed(obj* x_0) {
-_start:
-{
-obj* x_1; 
-x_1 = l_Array_anyAux___main(x_0);
-lean::dec(x_0);
-return x_1;
-}
-}
-uint8 l_Array_anyAux___rarg(obj* x_0, obj* x_1, obj* x_2) {
-_start:
-{
-uint8 x_3; 
-x_3 = l_Array_anyAux___main___rarg(x_0, x_1, x_2);
-return x_3;
-}
-}
-obj* l_Array_anyAux(obj* x_0) {
-_start:
-{
-obj* x_1; 
-x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_anyAux___rarg___boxed), 3, 0);
-return x_1;
-}
-}
-obj* l_Array_anyAux___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {
-_start:
-{
-uint8 x_3; obj* x_4; 
-x_3 = l_Array_anyAux___rarg(x_0, x_1, x_2);
-x_4 = lean::box(x_3);
-lean::dec(x_0);
-return x_4;
-}
-}
-obj* l_Array_anyAux___boxed(obj* x_0) {
-_start:
-{
-obj* x_1; 
-x_1 = l_Array_anyAux(x_0);
-lean::dec(x_0);
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_anyMAux___main___at_Array_any___spec__1___rarg___boxed), 3, 0);
 return x_1;
 }
 }
@@ -2417,7 +2722,7 @@ _start:
 {
 obj* x_2; uint8 x_3; 
 x_2 = lean::mk_nat_obj(0ul);
-x_3 = l_Array_anyAux___main___rarg(x_0, x_1, x_2);
+x_3 = l_Array_anyMAux___main___at_Array_any___spec__1___rarg(x_1, x_0, x_2);
 return x_3;
 }
 }
@@ -2429,6 +2734,25 @@ x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_any___rarg___boxed), 2
 return x_1;
 }
 }
+obj* l_Array_anyMAux___main___at_Array_any___spec__1___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+uint8 x_3; obj* x_4; 
+x_3 = l_Array_anyMAux___main___at_Array_any___spec__1___rarg(x_0, x_1, x_2);
+x_4 = lean::box(x_3);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* l_Array_anyMAux___main___at_Array_any___spec__1___boxed(obj* x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = l_Array_anyMAux___main___at_Array_any___spec__1(x_0);
+lean::dec(x_0);
+return x_1;
+}
+}
 obj* l_Array_any___rarg___boxed(obj* x_0, obj* x_1) {
 _start:
 {
@@ -2448,7 +2772,7 @@ lean::dec(x_0);
 return x_1;
 }
 }
-uint8 l_Array_anyAux___main___at_Array_all___spec__1___rarg(obj* x_0, obj* x_1, obj* x_2) {
+uint8 l_Array_anyMAux___main___at_Array_all___spec__1___rarg(obj* x_0, obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; uint8 x_4; 
@@ -2490,11 +2814,11 @@ goto _start;
 }
 }
 }
-obj* l_Array_anyAux___main___at_Array_all___spec__1(obj* x_0) {
+obj* l_Array_anyMAux___main___at_Array_all___spec__1(obj* x_0) {
 _start:
 {
 obj* x_1; 
-x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_anyAux___main___at_Array_all___spec__1___rarg___boxed), 3, 0);
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_anyMAux___main___at_Array_all___spec__1___rarg___boxed), 3, 0);
 return x_1;
 }
 }
@@ -2503,7 +2827,7 @@ _start:
 {
 obj* x_2; uint8 x_3; 
 x_2 = lean::mk_nat_obj(0ul);
-x_3 = l_Array_anyAux___main___at_Array_all___spec__1___rarg(x_1, x_0, x_2);
+x_3 = l_Array_anyMAux___main___at_Array_all___spec__1___rarg(x_1, x_0, x_2);
 if (x_3 == 0)
 {
 uint8 x_4; 
@@ -2526,21 +2850,21 @@ x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_all___rarg___boxed), 2
 return x_1;
 }
 }
-obj* l_Array_anyAux___main___at_Array_all___spec__1___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {
+obj* l_Array_anyMAux___main___at_Array_all___spec__1___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {
 _start:
 {
 uint8 x_3; obj* x_4; 
-x_3 = l_Array_anyAux___main___at_Array_all___spec__1___rarg(x_0, x_1, x_2);
+x_3 = l_Array_anyMAux___main___at_Array_all___spec__1___rarg(x_0, x_1, x_2);
 x_4 = lean::box(x_3);
 lean::dec(x_1);
 return x_4;
 }
 }
-obj* l_Array_anyAux___main___at_Array_all___spec__1___boxed(obj* x_0) {
+obj* l_Array_anyMAux___main___at_Array_all___spec__1___boxed(obj* x_0) {
 _start:
 {
 obj* x_1; 
-x_1 = l_Array_anyAux___main___at_Array_all___spec__1(x_0);
+x_1 = l_Array_anyMAux___main___at_Array_all___spec__1(x_0);
 lean::dec(x_0);
 return x_1;
 }
@@ -3592,6 +3916,150 @@ lean::dec(x_1);
 return x_2;
 }
 }
+obj* l_Array_mforAux___main___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
+_start:
+{
+obj* x_6; uint8 x_7; 
+x_6 = lean::array_get_size(x_4);
+x_7 = lean::nat_dec_lt(x_5, x_6);
+lean::dec(x_6);
+if (x_7 == 0)
+{
+obj* x_10; obj* x_13; obj* x_16; obj* x_17; 
+lean::dec(x_3);
+x_10 = lean::cnstr_get(x_0, 0);
+lean::inc(x_10);
+lean::dec(x_0);
+x_13 = lean::cnstr_get(x_10, 1);
+lean::inc(x_13);
+lean::dec(x_10);
+x_16 = lean::box(0);
+x_17 = lean::apply_2(x_13, lean::box(0), x_16);
+return x_17;
+}
+else
+{
+obj* x_18; obj* x_19; obj* x_21; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_30; 
+x_18 = lean::array_fget(x_4, x_5);
+x_19 = lean::cnstr_get(x_0, 0);
+lean::inc(x_19);
+x_21 = lean::cnstr_get(x_19, 4);
+lean::inc(x_21);
+lean::dec(x_19);
+lean::inc(x_3);
+x_25 = lean::apply_1(x_3, x_18);
+x_26 = lean::mk_nat_obj(1ul);
+x_27 = lean::nat_add(x_5, x_26);
+x_28 = l_Array_mforAux___main___rarg(x_0, lean::box(0), lean::box(0), x_3, x_4, x_27);
+lean::dec(x_27);
+x_30 = lean::apply_4(x_21, lean::box(0), lean::box(0), x_25, x_28);
+return x_30;
+}
+}
+}
+obj* l_Array_mforAux___main(obj* x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_mforAux___main___rarg___boxed), 6, 0);
+return x_1;
+}
+}
+obj* l_Array_mforAux___main___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
+_start:
+{
+obj* x_6; 
+x_6 = l_Array_mforAux___main___rarg(x_0, x_1, x_2, x_3, x_4, x_5);
+lean::dec(x_1);
+lean::dec(x_2);
+lean::dec(x_4);
+lean::dec(x_5);
+return x_6;
+}
+}
+obj* l_Array_mforAux___main___boxed(obj* x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = l_Array_mforAux___main(x_0);
+lean::dec(x_0);
+return x_1;
+}
+}
+obj* l_Array_mforAux___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
+_start:
+{
+obj* x_6; 
+x_6 = l_Array_mforAux___main___rarg(x_0, lean::box(0), lean::box(0), x_3, x_4, x_5);
+return x_6;
+}
+}
+obj* l_Array_mforAux(obj* x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_mforAux___rarg___boxed), 6, 0);
+return x_1;
+}
+}
+obj* l_Array_mforAux___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
+_start:
+{
+obj* x_6; 
+x_6 = l_Array_mforAux___rarg(x_0, x_1, x_2, x_3, x_4, x_5);
+lean::dec(x_1);
+lean::dec(x_2);
+lean::dec(x_4);
+lean::dec(x_5);
+return x_6;
+}
+}
+obj* l_Array_mforAux___boxed(obj* x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = l_Array_mforAux(x_0);
+lean::dec(x_0);
+return x_1;
+}
+}
+obj* l_Array_mfor___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; obj* x_6; 
+x_5 = lean::mk_nat_obj(0ul);
+x_6 = l_Array_mforAux___main___rarg(x_0, lean::box(0), lean::box(0), x_3, x_4, x_5);
+return x_6;
+}
+}
+obj* l_Array_mfor(obj* x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Array_mfor___rarg___boxed), 5, 0);
+return x_1;
+}
+}
+obj* l_Array_mfor___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+_start:
+{
+obj* x_5; 
+x_5 = l_Array_mfor___rarg(x_0, x_1, x_2, x_3, x_4);
+lean::dec(x_1);
+lean::dec(x_2);
+lean::dec(x_4);
+return x_5;
+}
+}
+obj* l_Array_mfor___boxed(obj* x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = l_Array_mfor(x_0);
+lean::dec(x_0);
+return x_1;
+}
+}
 obj* l_Array_extractAux___main___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
@@ -4476,6 +4944,8 @@ w = initialize_init_control_id(w);
 if (io_result_is_error(w)) return w;
  l_Array_empty___closed__1 = _init_l_Array_empty___closed__1();
 lean::mark_persistent(l_Array_empty___closed__1);
+ l_Array_allM___rarg___closed__1 = _init_l_Array_allM___rarg___closed__1();
+lean::mark_persistent(l_Array_allM___rarg___closed__1);
  l_Array_HasRepr___rarg___closed__1 = _init_l_Array_HasRepr___rarg___closed__1();
 lean::mark_persistent(l_Array_HasRepr___rarg___closed__1);
  l_Array_HasAppend___closed__1 = _init_l_Array_HasAppend___closed__1();

src/stage0/init/data/string/basic.cpp

@@ -1407,18 +1407,7 @@ x_1 = lean::string_utf8_byte_size(x_0);
 x_2 = lean::mk_nat_obj(0ul);
 x_3 = lean::nat_dec_eq(x_1, x_2);
 lean::dec(x_1);
-if (x_3 == 0)
-{
-uint8 x_5; 
-x_5 = 0;
-return x_5;
-}
-else
-{
-uint8 x_6; 
-x_6 = 1;
-return x_6;
-}
+return x_3;
 }
 }
 obj* l_String_isEmpty___boxed(obj* x_0) {

src/stage0/init/io.cpp

@@ -29,6 +29,7 @@ obj* l_IO_Fs_handle_isEof___rarg(obj*, obj*);
 obj* l_getModify___rarg___lambda__1___boxed(obj*, obj*, obj*);
 obj* l_IO_Fs_handle_close___rarg(obj*, obj*);
 obj* l_IO_Ref_swap(obj*, obj*);
+obj* l_IO_RefPointed___boxed(obj*);
 obj* l_EIO_Inhabited___rarg(obj*);
 obj* l_HasRepr_HasEval___rarg(obj*, obj*, obj*);
 obj* l_IO_Prim_Ref_swap___boxed(obj*, obj*, obj*, obj*);
@@ -152,7 +153,7 @@ obj* l_IO_Fs_handle_isEof___at_IO_Fs_handle_readToEnd___spec__1(obj*, obj*);
 obj* l_IO_Fs_handle_close(obj*, obj*);
 obj* l_IO_Fs_handle_mk___rarg(obj*, obj*, uint8, uint8);
 obj* l_IO_Prim_liftIO___rarg(obj*, obj*);
-obj* l_IO_RefPointed;
+obj* l_IO_RefPointed(obj*);
 obj* l_IO_println___rarg___closed__1;
 obj* l_IO_Prim_mkRef___boxed(obj*, obj*, obj*);
 obj* l_IO_lazyPure___rarg(obj*, obj*);
@@ -1201,12 +1202,21 @@ lean::dec(x_0);
 return x_1;
 }
 }
-obj* _init_l_IO_RefPointed() {
+obj* l_IO_RefPointed(obj* x_0) {
 _start:
 {
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
+obj* x_1; 
+x_1 = lean::box(0);
+return x_1;
+}
+}
+obj* l_IO_RefPointed___boxed(obj* x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = l_IO_RefPointed(x_0);
+lean::dec(x_0);
+return x_1;
 }
 }
 obj* l_IO_Inhabited(obj* x_0) {
@@ -1775,7 +1785,5 @@ lean::mark_persistent(l_IO_error_HasToString);
 lean::mark_persistent(l_IO_error_Inhabited);
  l_IO_println___rarg___closed__1 = _init_l_IO_println___rarg___closed__1();
 lean::mark_persistent(l_IO_println___rarg___closed__1);
- l_IO_RefPointed = _init_l_IO_RefPointed();
-lean::mark_persistent(l_IO_RefPointed);
 return w;
 }

src/stage0/init/lean/compiler/ir/default.cpp

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.compiler.ir.default
-// Imports: init.lean.compiler.ir.basic init.lean.compiler.ir.format init.lean.compiler.ir.pushproj init.lean.compiler.ir.elimdead init.lean.compiler.ir.simpcase init.lean.compiler.ir.resetreuse init.lean.compiler.ir.normids
+// Imports: init.lean.compiler.ir.basic init.lean.compiler.ir.format init.lean.compiler.ir.pushproj init.lean.compiler.ir.elimdead init.lean.compiler.ir.simpcase init.lean.compiler.ir.resetreuse init.lean.compiler.ir.normids init.lean.compiler.ir.checker
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -27,9 +27,9 @@ obj* decl_to_string_core(obj*);
 }}
 extern "C" obj* lean_io_prim_put_str(obj*, obj*);
 obj* l_IO_println___at_Lean_IR_test___spec__1(obj*, obj*);
+obj* l_Lean_IR_MaxIndex_collectDecl___main(obj*, obj*);
 obj* l_Lean_IR_Decl_pushProj___main(obj*);
 obj* l_Nat_repr(obj*);
-obj* l_Lean_IR_MaxVar_collectDecl___main(obj*, obj*);
 namespace lean {
 obj* string_append(obj*, obj*);
 }
@@ -42,6 +42,7 @@ obj* l_Lean_IR_test___closed__6;
 obj* l_IO_print___at_Lean_IR_test___spec__2(obj*, obj*);
 obj* l_Lean_IR_Decl_simpCase___main(obj*);
 extern obj* l_IO_println___rarg___closed__1;
+obj* l_Lean_IR_Decl_check(obj*, obj*);
 obj* l_Lean_IR_test___closed__3;
 obj* l_IO_print___at_Lean_IR_test___spec__2(obj* x_0, obj* x_1) {
 _start:
@@ -110,7 +111,7 @@ obj* _init_l_Lean_IR_test___closed__1() {
 _start:
 {
 obj* x_0; 
-x_0 = lean::mk_string("Max variable ");
+x_0 = lean::mk_string("Max index ");
 return x_0;
 }
 }
@@ -161,10 +162,10 @@ _start:
 {
 obj* x_3; 
 lean::inc(x_0);
-x_3 = l_IO_println___at_Lean_IR_test___spec__1(x_0, x_1);
+x_3 = l_Lean_IR_Decl_check(x_0, x_1);
 if (lean::obj_tag(x_3) == 0)
 {
-obj* x_4; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_16; 
+obj* x_4; obj* x_6; obj* x_7; obj* x_8; obj* x_10; 
 x_4 = lean::cnstr_get(x_3, 1);
 if (lean::is_exclusive(x_3)) {
  lean::cnstr_release(x_3, 0);
@@ -182,61 +183,61 @@ if (lean::is_scalar(x_6)) {
 }
 lean::cnstr_set(x_8, 0, x_7);
 lean::cnstr_set(x_8, 1, x_4);
-x_9 = lean::mk_nat_obj(0ul);
 lean::inc(x_0);
-x_11 = l_Lean_IR_MaxVar_collectDecl___main(x_0, x_9);
-x_12 = l_Nat_repr(x_11);
-x_13 = l_Lean_IR_test___closed__1;
-x_14 = lean::string_append(x_13, x_12);
-lean::dec(x_12);
-x_16 = l_IO_println___at_HasRepr_HasEval___spec__1(x_14, x_8);
-lean::dec(x_14);
-if (lean::obj_tag(x_16) == 0)
+x_10 = l_IO_println___at_Lean_IR_test___spec__1(x_0, x_8);
+if (lean::obj_tag(x_10) == 0)
 {
-obj* x_18; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; 
-x_18 = lean::cnstr_get(x_16, 1);
-if (lean::is_exclusive(x_16)) {
- lean::cnstr_release(x_16, 0);
- x_20 = x_16;
+obj* x_11; obj* x_13; obj* x_14; obj* x_15; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_22; 
+x_11 = lean::cnstr_get(x_10, 1);
+if (lean::is_exclusive(x_10)) {
+ lean::cnstr_release(x_10, 0);
+ x_13 = x_10;
 } else {
- lean::inc(x_18);
- lean::dec(x_16);
- x_20 = lean::box(0);
+ lean::inc(x_11);
+ lean::dec(x_10);
+ x_13 = lean::box(0);
 }
-if (lean::is_scalar(x_20)) {
- x_21 = lean::alloc_cnstr(0, 2, 0);
+if (lean::is_scalar(x_13)) {
+ x_14 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_21 = x_20;
+ x_14 = x_13;
 }
-lean::cnstr_set(x_21, 0, x_7);
-lean::cnstr_set(x_21, 1, x_18);
-x_22 = l_Lean_IR_Decl_pushProj___main(x_0);
-x_23 = l_Lean_IR_test___closed__2;
-x_24 = l_IO_println___at_HasRepr_HasEval___spec__1(x_23, x_21);
-if (lean::obj_tag(x_24) == 0)
+lean::cnstr_set(x_14, 0, x_7);
+lean::cnstr_set(x_14, 1, x_11);
+x_15 = lean::mk_nat_obj(0ul);
+lean::inc(x_0);
+x_17 = l_Lean_IR_MaxIndex_collectDecl___main(x_0, x_15);
+x_18 = l_Nat_repr(x_17);
+x_19 = l_Lean_IR_test___closed__1;
+x_20 = lean::string_append(x_19, x_18);
+lean::dec(x_18);
+x_22 = l_IO_println___at_HasRepr_HasEval___spec__1(x_20, x_14);
+lean::dec(x_20);
+if (lean::obj_tag(x_22) == 0)
 {
-obj* x_25; obj* x_27; obj* x_28; obj* x_30; 
-x_25 = lean::cnstr_get(x_24, 1);
-if (lean::is_exclusive(x_24)) {
- lean::cnstr_release(x_24, 0);
- x_27 = x_24;
+obj* x_24; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; 
+x_24 = lean::cnstr_get(x_22, 1);
+if (lean::is_exclusive(x_22)) {
+ lean::cnstr_release(x_22, 0);
+ x_26 = x_22;
 } else {
- lean::inc(x_25);
- lean::dec(x_24);
- x_27 = lean::box(0);
+ lean::inc(x_24);
+ lean::dec(x_22);
+ x_26 = lean::box(0);
 }
-if (lean::is_scalar(x_27)) {
- x_28 = lean::alloc_cnstr(0, 2, 0);
+if (lean::is_scalar(x_26)) {
+ x_27 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_28 = x_27;
+ x_27 = x_26;
 }
-lean::cnstr_set(x_28, 0, x_7);
-lean::cnstr_set(x_28, 1, x_25);
-lean::inc(x_22);
-x_30 = l_IO_println___at_Lean_IR_test___spec__1(x_22, x_28);
+lean::cnstr_set(x_27, 0, x_7);
+lean::cnstr_set(x_27, 1, x_24);
+x_28 = l_Lean_IR_Decl_pushProj___main(x_0);
+x_29 = l_Lean_IR_test___closed__2;
+x_30 = l_IO_println___at_HasRepr_HasEval___spec__1(x_29, x_27);
 if (lean::obj_tag(x_30) == 0)
 {
-obj* x_31; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; 
+obj* x_31; obj* x_33; obj* x_34; obj* x_36; 
 x_31 = lean::cnstr_get(x_30, 1);
 if (lean::is_exclusive(x_30)) {
  lean::cnstr_release(x_30, 0);
@@ -253,33 +254,33 @@ if (lean::is_scalar(x_33)) {
 }
 lean::cnstr_set(x_34, 0, x_7);
 lean::cnstr_set(x_34, 1, x_31);
-x_35 = l_Lean_IR_Decl_insertResetReuse___main(x_22);
-x_36 = l_Lean_IR_test___closed__3;
-x_37 = l_IO_println___at_HasRepr_HasEval___spec__1(x_36, x_34);
-if (lean::obj_tag(x_37) == 0)
+lean::inc(x_28);
+x_36 = l_IO_println___at_Lean_IR_test___spec__1(x_28, x_34);
+if (lean::obj_tag(x_36) == 0)
 {
-obj* x_38; obj* x_40; obj* x_41; obj* x_43; 
-x_38 = lean::cnstr_get(x_37, 1);
-if (lean::is_exclusive(x_37)) {
- lean::cnstr_release(x_37, 0);
- x_40 = x_37;
+obj* x_37; obj* x_39; obj* x_40; obj* x_41; obj* x_42; obj* x_43; 
+x_37 = lean::cnstr_get(x_36, 1);
+if (lean::is_exclusive(x_36)) {
+ lean::cnstr_release(x_36, 0);
+ x_39 = x_36;
 } else {
- lean::inc(x_38);
- lean::dec(x_37);
- x_40 = lean::box(0);
+ lean::inc(x_37);
+ lean::dec(x_36);
+ x_39 = lean::box(0);
 }
-if (lean::is_scalar(x_40)) {
- x_41 = lean::alloc_cnstr(0, 2, 0);
+if (lean::is_scalar(x_39)) {
+ x_40 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_41 = x_40;
+ x_40 = x_39;
 }
-lean::cnstr_set(x_41, 0, x_7);
-lean::cnstr_set(x_41, 1, x_38);
-lean::inc(x_35);
-x_43 = l_IO_println___at_Lean_IR_test___spec__1(x_35, x_41);
+lean::cnstr_set(x_40, 0, x_7);
+lean::cnstr_set(x_40, 1, x_37);
+x_41 = l_Lean_IR_Decl_insertResetReuse___main(x_28);
+x_42 = l_Lean_IR_test___closed__3;
+x_43 = l_IO_println___at_HasRepr_HasEval___spec__1(x_42, x_40);
 if (lean::obj_tag(x_43) == 0)
 {
-obj* x_44; obj* x_46; obj* x_47; obj* x_48; obj* x_49; obj* x_50; 
+obj* x_44; obj* x_46; obj* x_47; obj* x_49; 
 x_44 = lean::cnstr_get(x_43, 1);
 if (lean::is_exclusive(x_43)) {
  lean::cnstr_release(x_43, 0);
@@ -296,33 +297,33 @@ if (lean::is_scalar(x_46)) {
 }
 lean::cnstr_set(x_47, 0, x_7);
 lean::cnstr_set(x_47, 1, x_44);
-x_48 = l_Lean_IR_Decl_elimDead___main(x_35);
-x_49 = l_Lean_IR_test___closed__4;
-x_50 = l_IO_println___at_HasRepr_HasEval___spec__1(x_49, x_47);
-if (lean::obj_tag(x_50) == 0)
+lean::inc(x_41);
+x_49 = l_IO_println___at_Lean_IR_test___spec__1(x_41, x_47);
+if (lean::obj_tag(x_49) == 0)
 {
-obj* x_51; obj* x_53; obj* x_54; obj* x_56; 
-x_51 = lean::cnstr_get(x_50, 1);
-if (lean::is_exclusive(x_50)) {
- lean::cnstr_release(x_50, 0);
- x_53 = x_50;
+obj* x_50; obj* x_52; obj* x_53; obj* x_54; obj* x_55; obj* x_56; 
+x_50 = lean::cnstr_get(x_49, 1);
+if (lean::is_exclusive(x_49)) {
+ lean::cnstr_release(x_49, 0);
+ x_52 = x_49;
 } else {
- lean::inc(x_51);
- lean::dec(x_50);
- x_53 = lean::box(0);
+ lean::inc(x_50);
+ lean::dec(x_49);
+ x_52 = lean::box(0);
 }
-if (lean::is_scalar(x_53)) {
- x_54 = lean::alloc_cnstr(0, 2, 0);
+if (lean::is_scalar(x_52)) {
+ x_53 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_54 = x_53;
+ x_53 = x_52;
 }
-lean::cnstr_set(x_54, 0, x_7);
-lean::cnstr_set(x_54, 1, x_51);
-lean::inc(x_48);
-x_56 = l_IO_println___at_Lean_IR_test___spec__1(x_48, x_54);
+lean::cnstr_set(x_53, 0, x_7);
+lean::cnstr_set(x_53, 1, x_50);
+x_54 = l_Lean_IR_Decl_elimDead___main(x_41);
+x_55 = l_Lean_IR_test___closed__4;
+x_56 = l_IO_println___at_HasRepr_HasEval___spec__1(x_55, x_53);
 if (lean::obj_tag(x_56) == 0)
 {
-obj* x_57; obj* x_59; obj* x_60; obj* x_61; obj* x_62; obj* x_63; 
+obj* x_57; obj* x_59; obj* x_60; obj* x_62; 
 x_57 = lean::cnstr_get(x_56, 1);
 if (lean::is_exclusive(x_56)) {
  lean::cnstr_release(x_56, 0);
@@ -339,33 +340,33 @@ if (lean::is_scalar(x_59)) {
 }
 lean::cnstr_set(x_60, 0, x_7);
 lean::cnstr_set(x_60, 1, x_57);
-x_61 = l_Lean_IR_Decl_simpCase___main(x_48);
-x_62 = l_Lean_IR_test___closed__5;
-x_63 = l_IO_println___at_HasRepr_HasEval___spec__1(x_62, x_60);
-if (lean::obj_tag(x_63) == 0)
+lean::inc(x_54);
+x_62 = l_IO_println___at_Lean_IR_test___spec__1(x_54, x_60);
+if (lean::obj_tag(x_62) == 0)
 {
-obj* x_64; obj* x_66; obj* x_67; obj* x_69; 
-x_64 = lean::cnstr_get(x_63, 1);
-if (lean::is_exclusive(x_63)) {
- lean::cnstr_release(x_63, 0);
- x_66 = x_63;
+obj* x_63; obj* x_65; obj* x_66; obj* x_67; obj* x_68; obj* x_69; 
+x_63 = lean::cnstr_get(x_62, 1);
+if (lean::is_exclusive(x_62)) {
+ lean::cnstr_release(x_62, 0);
+ x_65 = x_62;
 } else {
- lean::inc(x_64);
- lean::dec(x_63);
- x_66 = lean::box(0);
+ lean::inc(x_63);
+ lean::dec(x_62);
+ x_65 = lean::box(0);
 }
-if (lean::is_scalar(x_66)) {
- x_67 = lean::alloc_cnstr(0, 2, 0);
+if (lean::is_scalar(x_65)) {
+ x_66 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_67 = x_66;
+ x_66 = x_65;
 }
-lean::cnstr_set(x_67, 0, x_7);
-lean::cnstr_set(x_67, 1, x_64);
-lean::inc(x_61);
-x_69 = l_IO_println___at_Lean_IR_test___spec__1(x_61, x_67);
+lean::cnstr_set(x_66, 0, x_7);
+lean::cnstr_set(x_66, 1, x_63);
+x_67 = l_Lean_IR_Decl_simpCase___main(x_54);
+x_68 = l_Lean_IR_test___closed__5;
+x_69 = l_IO_println___at_HasRepr_HasEval___spec__1(x_68, x_66);
 if (lean::obj_tag(x_69) == 0)
 {
-obj* x_70; obj* x_72; obj* x_73; obj* x_74; obj* x_75; obj* x_76; 
+obj* x_70; obj* x_72; obj* x_73; obj* x_75; 
 x_70 = lean::cnstr_get(x_69, 1);
 if (lean::is_exclusive(x_69)) {
  lean::cnstr_release(x_69, 0);
@@ -382,335 +383,425 @@ if (lean::is_scalar(x_72)) {
 }
 lean::cnstr_set(x_73, 0, x_7);
 lean::cnstr_set(x_73, 1, x_70);
-x_74 = l_Lean_IR_Decl_normalizeIds(x_61);
-x_75 = l_Lean_IR_test___closed__6;
-x_76 = l_IO_println___at_HasRepr_HasEval___spec__1(x_75, x_73);
-if (lean::obj_tag(x_76) == 0)
+lean::inc(x_67);
+x_75 = l_IO_println___at_Lean_IR_test___spec__1(x_67, x_73);
+if (lean::obj_tag(x_75) == 0)
 {
-obj* x_77; obj* x_79; obj* x_80; obj* x_81; 
-x_77 = lean::cnstr_get(x_76, 1);
-if (lean::is_exclusive(x_76)) {
- lean::cnstr_release(x_76, 0);
- x_79 = x_76;
+obj* x_76; obj* x_78; obj* x_79; obj* x_80; obj* x_81; obj* x_82; 
+x_76 = lean::cnstr_get(x_75, 1);
+if (lean::is_exclusive(x_75)) {
+ lean::cnstr_release(x_75, 0);
+ x_78 = x_75;
 } else {
- lean::inc(x_77);
- lean::dec(x_76);
- x_79 = lean::box(0);
+ lean::inc(x_76);
+ lean::dec(x_75);
+ x_78 = lean::box(0);
 }
-if (lean::is_scalar(x_79)) {
- x_80 = lean::alloc_cnstr(0, 2, 0);
+if (lean::is_scalar(x_78)) {
+ x_79 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_80 = x_79;
+ x_79 = x_78;
 }
-lean::cnstr_set(x_80, 0, x_7);
-lean::cnstr_set(x_80, 1, x_77);
-x_81 = l_IO_println___at_Lean_IR_test___spec__1(x_74, x_80);
-if (lean::obj_tag(x_81) == 0)
+lean::cnstr_set(x_79, 0, x_7);
+lean::cnstr_set(x_79, 1, x_76);
+x_80 = l_Lean_IR_Decl_normalizeIds(x_67);
+x_81 = l_Lean_IR_test___closed__6;
+x_82 = l_IO_println___at_HasRepr_HasEval___spec__1(x_81, x_79);
+if (lean::obj_tag(x_82) == 0)
 {
-obj* x_82; obj* x_84; obj* x_85; 
-x_82 = lean::cnstr_get(x_81, 1);
-if (lean::is_exclusive(x_81)) {
- lean::cnstr_release(x_81, 0);
- x_84 = x_81;
+obj* x_83; obj* x_85; obj* x_86; obj* x_88; 
+x_83 = lean::cnstr_get(x_82, 1);
+if (lean::is_exclusive(x_82)) {
+ lean::cnstr_release(x_82, 0);
+ x_85 = x_82;
 } else {
- lean::inc(x_82);
- lean::dec(x_81);
- x_84 = lean::box(0);
+ lean::inc(x_83);
+ lean::dec(x_82);
+ x_85 = lean::box(0);
 }
-if (lean::is_scalar(x_84)) {
- x_85 = lean::alloc_cnstr(0, 2, 0);
+if (lean::is_scalar(x_85)) {
+ x_86 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_85 = x_84;
+ x_86 = x_85;
 }
-lean::cnstr_set(x_85, 0, x_7);
-lean::cnstr_set(x_85, 1, x_82);
-return x_85;
+lean::cnstr_set(x_86, 0, x_7);
+lean::cnstr_set(x_86, 1, x_83);
+lean::inc(x_80);
+x_88 = l_IO_println___at_Lean_IR_test___spec__1(x_80, x_86);
+if (lean::obj_tag(x_88) == 0)
+{
+obj* x_89; obj* x_91; obj* x_92; obj* x_93; 
+x_89 = lean::cnstr_get(x_88, 1);
+if (lean::is_exclusive(x_88)) {
+ lean::cnstr_release(x_88, 0);
+ x_91 = x_88;
+} else {
+ lean::inc(x_89);
+ lean::dec(x_88);
+ x_91 = lean::box(0);
+}
+if (lean::is_scalar(x_91)) {
+ x_92 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_92 = x_91;
+}
+lean::cnstr_set(x_92, 0, x_7);
+lean::cnstr_set(x_92, 1, x_89);
+x_93 = l_Lean_IR_Decl_check(x_80, x_92);
+if (lean::obj_tag(x_93) == 0)
+{
+obj* x_94; obj* x_96; obj* x_97; 
+x_94 = lean::cnstr_get(x_93, 1);
+if (lean::is_exclusive(x_93)) {
+ lean::cnstr_release(x_93, 0);
+ x_96 = x_93;
+} else {
+ lean::inc(x_94);
+ lean::dec(x_93);
+ x_96 = lean::box(0);
+}
+if (lean::is_scalar(x_96)) {
+ x_97 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_97 = x_96;
+}
+lean::cnstr_set(x_97, 0, x_7);
+lean::cnstr_set(x_97, 1, x_94);
+return x_97;
 }
 else
 {
-obj* x_86; obj* x_88; obj* x_90; obj* x_91; 
-x_86 = lean::cnstr_get(x_81, 0);
-x_88 = lean::cnstr_get(x_81, 1);
-if (lean::is_exclusive(x_81)) {
- x_90 = x_81;
-} else {
- lean::inc(x_86);
- lean::inc(x_88);
- lean::dec(x_81);
- x_90 = lean::box(0);
-}
-if (lean::is_scalar(x_90)) {
- x_91 = lean::alloc_cnstr(1, 2, 0);
-} else {
- x_91 = x_90;
-}
-lean::cnstr_set(x_91, 0, x_86);
-lean::cnstr_set(x_91, 1, x_88);
-return x_91;
-}
-}
-else
-{
-obj* x_93; obj* x_95; obj* x_97; obj* x_98; 
-lean::dec(x_74);
-x_93 = lean::cnstr_get(x_76, 0);
-x_95 = lean::cnstr_get(x_76, 1);
-if (lean::is_exclusive(x_76)) {
- x_97 = x_76;
-} else {
- lean::inc(x_93);
- lean::inc(x_95);
- lean::dec(x_76);
- x_97 = lean::box(0);
-}
-if (lean::is_scalar(x_97)) {
- x_98 = lean::alloc_cnstr(1, 2, 0);
-} else {
- x_98 = x_97;
-}
-lean::cnstr_set(x_98, 0, x_93);
-lean::cnstr_set(x_98, 1, x_95);
-return x_98;
-}
-}
-else
-{
-obj* x_100; obj* x_102; obj* x_104; obj* x_105; 
-lean::dec(x_61);
-x_100 = lean::cnstr_get(x_69, 0);
-x_102 = lean::cnstr_get(x_69, 1);
-if (lean::is_exclusive(x_69)) {
- x_104 = x_69;
+obj* x_98; obj* x_100; obj* x_102; obj* x_103; 
+x_98 = lean::cnstr_get(x_93, 0);
+x_100 = lean::cnstr_get(x_93, 1);
+if (lean::is_exclusive(x_93)) {
+ x_102 = x_93;
 } else {
+ lean::inc(x_98);
  lean::inc(x_100);
- lean::inc(x_102);
- lean::dec(x_69);
- x_104 = lean::box(0);
+ lean::dec(x_93);
+ x_102 = lean::box(0);
 }
-if (lean::is_scalar(x_104)) {
- x_105 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_102)) {
+ x_103 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_105 = x_104;
+ x_103 = x_102;
 }
-lean::cnstr_set(x_105, 0, x_100);
-lean::cnstr_set(x_105, 1, x_102);
-return x_105;
+lean::cnstr_set(x_103, 0, x_98);
+lean::cnstr_set(x_103, 1, x_100);
+return x_103;
 }
 }
 else
 {
-obj* x_107; obj* x_109; obj* x_111; obj* x_112; 
-lean::dec(x_61);
-x_107 = lean::cnstr_get(x_63, 0);
-x_109 = lean::cnstr_get(x_63, 1);
-if (lean::is_exclusive(x_63)) {
- x_111 = x_63;
+obj* x_105; obj* x_107; obj* x_109; obj* x_110; 
+lean::dec(x_80);
+x_105 = lean::cnstr_get(x_88, 0);
+x_107 = lean::cnstr_get(x_88, 1);
+if (lean::is_exclusive(x_88)) {
+ x_109 = x_88;
 } else {
+ lean::inc(x_105);
  lean::inc(x_107);
- lean::inc(x_109);
- lean::dec(x_63);
- x_111 = lean::box(0);
+ lean::dec(x_88);
+ x_109 = lean::box(0);
 }
-if (lean::is_scalar(x_111)) {
- x_112 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_109)) {
+ x_110 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_112 = x_111;
+ x_110 = x_109;
 }
-lean::cnstr_set(x_112, 0, x_107);
-lean::cnstr_set(x_112, 1, x_109);
-return x_112;
+lean::cnstr_set(x_110, 0, x_105);
+lean::cnstr_set(x_110, 1, x_107);
+return x_110;
 }
 }
 else
 {
-obj* x_114; obj* x_116; obj* x_118; obj* x_119; 
-lean::dec(x_48);
-x_114 = lean::cnstr_get(x_56, 0);
-x_116 = lean::cnstr_get(x_56, 1);
-if (lean::is_exclusive(x_56)) {
- x_118 = x_56;
+obj* x_112; obj* x_114; obj* x_116; obj* x_117; 
+lean::dec(x_80);
+x_112 = lean::cnstr_get(x_82, 0);
+x_114 = lean::cnstr_get(x_82, 1);
+if (lean::is_exclusive(x_82)) {
+ x_116 = x_82;
 } else {
+ lean::inc(x_112);
  lean::inc(x_114);
- lean::inc(x_116);
- lean::dec(x_56);
- x_118 = lean::box(0);
+ lean::dec(x_82);
+ x_116 = lean::box(0);
 }
-if (lean::is_scalar(x_118)) {
- x_119 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_116)) {
+ x_117 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_119 = x_118;
+ x_117 = x_116;
 }
-lean::cnstr_set(x_119, 0, x_114);
-lean::cnstr_set(x_119, 1, x_116);
-return x_119;
+lean::cnstr_set(x_117, 0, x_112);
+lean::cnstr_set(x_117, 1, x_114);
+return x_117;
 }
 }
 else
 {
-obj* x_121; obj* x_123; obj* x_125; obj* x_126; 
-lean::dec(x_48);
-x_121 = lean::cnstr_get(x_50, 0);
-x_123 = lean::cnstr_get(x_50, 1);
-if (lean::is_exclusive(x_50)) {
- x_125 = x_50;
+obj* x_119; obj* x_121; obj* x_123; obj* x_124; 
+lean::dec(x_67);
+x_119 = lean::cnstr_get(x_75, 0);
+x_121 = lean::cnstr_get(x_75, 1);
+if (lean::is_exclusive(x_75)) {
+ x_123 = x_75;
 } else {
+ lean::inc(x_119);
  lean::inc(x_121);
- lean::inc(x_123);
- lean::dec(x_50);
- x_125 = lean::box(0);
+ lean::dec(x_75);
+ x_123 = lean::box(0);
 }
-if (lean::is_scalar(x_125)) {
- x_126 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_123)) {
+ x_124 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_126 = x_125;
+ x_124 = x_123;
 }
-lean::cnstr_set(x_126, 0, x_121);
-lean::cnstr_set(x_126, 1, x_123);
-return x_126;
+lean::cnstr_set(x_124, 0, x_119);
+lean::cnstr_set(x_124, 1, x_121);
+return x_124;
 }
 }
 else
 {
-obj* x_128; obj* x_130; obj* x_132; obj* x_133; 
-lean::dec(x_35);
-x_128 = lean::cnstr_get(x_43, 0);
-x_130 = lean::cnstr_get(x_43, 1);
-if (lean::is_exclusive(x_43)) {
- x_132 = x_43;
+obj* x_126; obj* x_128; obj* x_130; obj* x_131; 
+lean::dec(x_67);
+x_126 = lean::cnstr_get(x_69, 0);
+x_128 = lean::cnstr_get(x_69, 1);
+if (lean::is_exclusive(x_69)) {
+ x_130 = x_69;
 } else {
+ lean::inc(x_126);
  lean::inc(x_128);
- lean::inc(x_130);
- lean::dec(x_43);
- x_132 = lean::box(0);
+ lean::dec(x_69);
+ x_130 = lean::box(0);
 }
-if (lean::is_scalar(x_132)) {
- x_133 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_130)) {
+ x_131 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_133 = x_132;
+ x_131 = x_130;
 }
-lean::cnstr_set(x_133, 0, x_128);
-lean::cnstr_set(x_133, 1, x_130);
-return x_133;
+lean::cnstr_set(x_131, 0, x_126);
+lean::cnstr_set(x_131, 1, x_128);
+return x_131;
 }
 }
 else
 {
-obj* x_135; obj* x_137; obj* x_139; obj* x_140; 
-lean::dec(x_35);
-x_135 = lean::cnstr_get(x_37, 0);
-x_137 = lean::cnstr_get(x_37, 1);
-if (lean::is_exclusive(x_37)) {
- x_139 = x_37;
+obj* x_133; obj* x_135; obj* x_137; obj* x_138; 
+lean::dec(x_54);
+x_133 = lean::cnstr_get(x_62, 0);
+x_135 = lean::cnstr_get(x_62, 1);
+if (lean::is_exclusive(x_62)) {
+ x_137 = x_62;
 } else {
+ lean::inc(x_133);
  lean::inc(x_135);
- lean::inc(x_137);
- lean::dec(x_37);
- x_139 = lean::box(0);
+ lean::dec(x_62);
+ x_137 = lean::box(0);
 }
-if (lean::is_scalar(x_139)) {
- x_140 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_137)) {
+ x_138 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_140 = x_139;
+ x_138 = x_137;
 }
-lean::cnstr_set(x_140, 0, x_135);
-lean::cnstr_set(x_140, 1, x_137);
-return x_140;
+lean::cnstr_set(x_138, 0, x_133);
+lean::cnstr_set(x_138, 1, x_135);
+return x_138;
 }
 }
 else
 {
-obj* x_142; obj* x_144; obj* x_146; obj* x_147; 
-lean::dec(x_22);
-x_142 = lean::cnstr_get(x_30, 0);
-x_144 = lean::cnstr_get(x_30, 1);
-if (lean::is_exclusive(x_30)) {
- x_146 = x_30;
+obj* x_140; obj* x_142; obj* x_144; obj* x_145; 
+lean::dec(x_54);
+x_140 = lean::cnstr_get(x_56, 0);
+x_142 = lean::cnstr_get(x_56, 1);
+if (lean::is_exclusive(x_56)) {
+ x_144 = x_56;
 } else {
+ lean::inc(x_140);
  lean::inc(x_142);
- lean::inc(x_144);
- lean::dec(x_30);
- x_146 = lean::box(0);
+ lean::dec(x_56);
+ x_144 = lean::box(0);
 }
-if (lean::is_scalar(x_146)) {
- x_147 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_144)) {
+ x_145 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_147 = x_146;
+ x_145 = x_144;
 }
-lean::cnstr_set(x_147, 0, x_142);
-lean::cnstr_set(x_147, 1, x_144);
-return x_147;
+lean::cnstr_set(x_145, 0, x_140);
+lean::cnstr_set(x_145, 1, x_142);
+return x_145;
 }
 }
 else
 {
-obj* x_149; obj* x_151; obj* x_153; obj* x_154; 
-lean::dec(x_22);
-x_149 = lean::cnstr_get(x_24, 0);
-x_151 = lean::cnstr_get(x_24, 1);
-if (lean::is_exclusive(x_24)) {
- x_153 = x_24;
+obj* x_147; obj* x_149; obj* x_151; obj* x_152; 
+lean::dec(x_41);
+x_147 = lean::cnstr_get(x_49, 0);
+x_149 = lean::cnstr_get(x_49, 1);
+if (lean::is_exclusive(x_49)) {
+ x_151 = x_49;
 } else {
+ lean::inc(x_147);
  lean::inc(x_149);
- lean::inc(x_151);
- lean::dec(x_24);
- x_153 = lean::box(0);
+ lean::dec(x_49);
+ x_151 = lean::box(0);
 }
-if (lean::is_scalar(x_153)) {
- x_154 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_151)) {
+ x_152 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_154 = x_153;
+ x_152 = x_151;
 }
-lean::cnstr_set(x_154, 0, x_149);
-lean::cnstr_set(x_154, 1, x_151);
-return x_154;
+lean::cnstr_set(x_152, 0, x_147);
+lean::cnstr_set(x_152, 1, x_149);
+return x_152;
 }
 }
 else
 {
-obj* x_156; obj* x_158; obj* x_160; obj* x_161; 
-lean::dec(x_0);
-x_156 = lean::cnstr_get(x_16, 0);
-x_158 = lean::cnstr_get(x_16, 1);
-if (lean::is_exclusive(x_16)) {
- x_160 = x_16;
+obj* x_154; obj* x_156; obj* x_158; obj* x_159; 
+lean::dec(x_41);
+x_154 = lean::cnstr_get(x_43, 0);
+x_156 = lean::cnstr_get(x_43, 1);
+if (lean::is_exclusive(x_43)) {
+ x_158 = x_43;
 } else {
+ lean::inc(x_154);
  lean::inc(x_156);
- lean::inc(x_158);
- lean::dec(x_16);
- x_160 = lean::box(0);
+ lean::dec(x_43);
+ x_158 = lean::box(0);
 }
-if (lean::is_scalar(x_160)) {
- x_161 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_158)) {
+ x_159 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_161 = x_160;
+ x_159 = x_158;
 }
-lean::cnstr_set(x_161, 0, x_156);
-lean::cnstr_set(x_161, 1, x_158);
-return x_161;
+lean::cnstr_set(x_159, 0, x_154);
+lean::cnstr_set(x_159, 1, x_156);
+return x_159;
 }
 }
 else
 {
-obj* x_163; obj* x_165; obj* x_167; obj* x_168; 
-lean::dec(x_0);
-x_163 = lean::cnstr_get(x_3, 0);
-x_165 = lean::cnstr_get(x_3, 1);
-if (lean::is_exclusive(x_3)) {
- x_167 = x_3;
+obj* x_161; obj* x_163; obj* x_165; obj* x_166; 
+lean::dec(x_28);
+x_161 = lean::cnstr_get(x_36, 0);
+x_163 = lean::cnstr_get(x_36, 1);
+if (lean::is_exclusive(x_36)) {
+ x_165 = x_36;
 } else {
+ lean::inc(x_161);
  lean::inc(x_163);
- lean::inc(x_165);
- lean::dec(x_3);
- x_167 = lean::box(0);
+ lean::dec(x_36);
+ x_165 = lean::box(0);
 }
-if (lean::is_scalar(x_167)) {
- x_168 = lean::alloc_cnstr(1, 2, 0);
+if (lean::is_scalar(x_165)) {
+ x_166 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_168 = x_167;
+ x_166 = x_165;
 }
-lean::cnstr_set(x_168, 0, x_163);
-lean::cnstr_set(x_168, 1, x_165);
-return x_168;
+lean::cnstr_set(x_166, 0, x_161);
+lean::cnstr_set(x_166, 1, x_163);
+return x_166;
+}
+}
+else
+{
+obj* x_168; obj* x_170; obj* x_172; obj* x_173; 
+lean::dec(x_28);
+x_168 = lean::cnstr_get(x_30, 0);
+x_170 = lean::cnstr_get(x_30, 1);
+if (lean::is_exclusive(x_30)) {
+ x_172 = x_30;
+} else {
+ lean::inc(x_168);
+ lean::inc(x_170);
+ lean::dec(x_30);
+ x_172 = lean::box(0);
+}
+if (lean::is_scalar(x_172)) {
+ x_173 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_173 = x_172;
+}
+lean::cnstr_set(x_173, 0, x_168);
+lean::cnstr_set(x_173, 1, x_170);
+return x_173;
+}
+}
+else
+{
+obj* x_175; obj* x_177; obj* x_179; obj* x_180; 
+lean::dec(x_0);
+x_175 = lean::cnstr_get(x_22, 0);
+x_177 = lean::cnstr_get(x_22, 1);
+if (lean::is_exclusive(x_22)) {
+ x_179 = x_22;
+} else {
+ lean::inc(x_175);
+ lean::inc(x_177);
+ lean::dec(x_22);
+ x_179 = lean::box(0);
+}
+if (lean::is_scalar(x_179)) {
+ x_180 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_180 = x_179;
+}
+lean::cnstr_set(x_180, 0, x_175);
+lean::cnstr_set(x_180, 1, x_177);
+return x_180;
+}
+}
+else
+{
+obj* x_182; obj* x_184; obj* x_186; obj* x_187; 
+lean::dec(x_0);
+x_182 = lean::cnstr_get(x_10, 0);
+x_184 = lean::cnstr_get(x_10, 1);
+if (lean::is_exclusive(x_10)) {
+ x_186 = x_10;
+} else {
+ lean::inc(x_182);
+ lean::inc(x_184);
+ lean::dec(x_10);
+ x_186 = lean::box(0);
+}
+if (lean::is_scalar(x_186)) {
+ x_187 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_187 = x_186;
+}
+lean::cnstr_set(x_187, 0, x_182);
+lean::cnstr_set(x_187, 1, x_184);
+return x_187;
+}
+}
+else
+{
+obj* x_189; obj* x_191; obj* x_193; obj* x_194; 
+lean::dec(x_0);
+x_189 = lean::cnstr_get(x_3, 0);
+x_191 = lean::cnstr_get(x_3, 1);
+if (lean::is_exclusive(x_3)) {
+ x_193 = x_3;
+} else {
+ lean::inc(x_189);
+ lean::inc(x_191);
+ lean::dec(x_3);
+ x_193 = lean::box(0);
+}
+if (lean::is_scalar(x_193)) {
+ x_194 = lean::alloc_cnstr(1, 2, 0);
+} else {
+ x_194 = x_193;
+}
+lean::cnstr_set(x_194, 0, x_189);
+lean::cnstr_set(x_194, 1, x_191);
+return x_194;
 }
 }
 }
@@ -722,6 +813,7 @@ obj* initialize_init_lean_compiler_ir_elimdead(obj*);
 obj* initialize_init_lean_compiler_ir_simpcase(obj*);
 obj* initialize_init_lean_compiler_ir_resetreuse(obj*);
 obj* initialize_init_lean_compiler_ir_normids(obj*);
+obj* initialize_init_lean_compiler_ir_checker(obj*);
 static bool _G_initialized = false;
 obj* initialize_init_lean_compiler_ir_default(obj* w) {
  if (_G_initialized) return w;
@@ -740,6 +832,8 @@ if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_ir_resetreuse(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_ir_normids(w);
+if (io_result_is_error(w)) return w;
+w = initialize_init_lean_compiler_ir_checker(w);
 if (io_result_is_error(w)) return w;
  l_Lean_IR_test___closed__1 = _init_l_Lean_IR_test___closed__1();
 lean::mark_persistent(l_Lean_IR_test___closed__1);

src/stage0/init/lean/compiler/ir/elimdead.cpp

@@ -14,18 +14,18 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-label"
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
-obj* l_Lean_IR_FnBody_collectFreeVars(obj*, obj*);
 namespace lean {
 obj* nat_sub(obj*, obj*);
 }
 obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_elimDead___main___spec__2___closed__1;
 obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_elimDead___main___spec__1(obj*, obj*);
 obj* l_Lean_IR_reshapeWithoutDead(obj*, obj*);
+obj* l_Lean_IR_FnBody_freeIndices(obj*);
 obj* l_Array_back___at_Lean_IR_reshapeWithoutDeadAux___main___spec__1(obj*);
 obj* l_Lean_IR_reshapeWithoutDeadAux(obj*, obj*, obj*);
 obj* l_Array_back___at_Lean_IR_reshapeWithoutDeadAux___main___spec__1___boxed(obj*);
 obj* l_Lean_IR_FnBody_elimDead___main(obj*);
-obj* l_Lean_IR_FnBody_freeVars(obj*);
+obj* l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_14__collectIndex___spec__1(obj*, obj*);
 obj* l_Lean_IR_reshapeWithoutDeadAux___main(obj*, obj*, obj*);
 namespace lean {
 uint8 nat_dec_lt(obj*, obj*);
@@ -37,7 +37,7 @@ obj* nat_add(obj*, obj*);
 }
 uint8 l_Array_isEmpty___rarg(obj*);
 obj* l_Lean_IR_Decl_elimDead___main(obj*);
-obj* l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(obj*, obj*);
+obj* l_Lean_IR_FnBody_collectFreeIndices(obj*, obj*);
 obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_elimDead___main___spec__2(obj*, obj*);
 obj* l_Lean_IR_FnBody_setBody___main(obj*, obj*);
 obj* l_Lean_IR_FnBody_elimDead(obj*);
@@ -96,7 +96,7 @@ lbl_7:
 obj* x_17; obj* x_18; 
 lean::dec(x_6);
 lean::inc(x_4);
-x_17 = l_Lean_IR_FnBody_collectFreeVars(x_4, x_2);
+x_17 = l_Lean_IR_FnBody_collectFreeIndices(x_4, x_2);
 x_18 = l_Lean_IR_FnBody_setBody___main(x_4, x_1);
 x_0 = x_5;
 x_1 = x_18;
@@ -107,7 +107,7 @@ lbl_9:
 {
 obj* x_21; 
 lean::inc(x_2);
-x_21 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_2, x_8);
+x_21 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_14__collectIndex___spec__1(x_2, x_8);
 lean::dec(x_8);
 if (lean::obj_tag(x_21) == 0)
 {
@@ -155,7 +155,7 @@ _start:
 {
 obj* x_3; obj* x_4; 
 lean::inc(x_1);
-x_3 = l_Lean_IR_FnBody_freeVars(x_1);
+x_3 = l_Lean_IR_FnBody_freeIndices(x_1);
 x_4 = l_Lean_IR_reshapeWithoutDeadAux___main(x_0, x_1, x_3);
 return x_4;
 }
@@ -183,47 +183,44 @@ x_10 = lean::nat_add(x_0, x_9);
 switch (lean::obj_tag(x_6)) {
 case 1:
 {
-obj* x_11; obj* x_13; uint8 x_15; obj* x_16; obj* x_18; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; 
+obj* x_11; obj* x_13; obj* x_15; obj* x_17; obj* x_19; obj* x_20; obj* x_21; obj* x_22; 
 x_11 = lean::cnstr_get(x_6, 0);
 x_13 = lean::cnstr_get(x_6, 1);
-x_15 = lean::cnstr_get_scalar<uint8>(x_6, sizeof(void*)*4);
-x_16 = lean::cnstr_get(x_6, 2);
-x_18 = lean::cnstr_get(x_6, 3);
+x_15 = lean::cnstr_get(x_6, 2);
+x_17 = lean::cnstr_get(x_6, 3);
 if (lean::is_exclusive(x_6)) {
- x_20 = x_6;
+ x_19 = x_6;
 } else {
  lean::inc(x_11);
  lean::inc(x_13);
- lean::inc(x_16);
- lean::inc(x_18);
+ lean::inc(x_15);
+ lean::inc(x_17);
  lean::dec(x_6);
- x_20 = lean::box(0);
+ x_19 = lean::box(0);
 }
-x_21 = l_Lean_IR_FnBody_elimDead___main(x_16);
-if (lean::is_scalar(x_20)) {
- x_22 = lean::alloc_cnstr(1, 4, 1);
+x_20 = l_Lean_IR_FnBody_elimDead___main(x_15);
+if (lean::is_scalar(x_19)) {
+ x_21 = lean::alloc_cnstr(1, 4, 0);
 } else {
- x_22 = x_20;
+ x_21 = x_19;
 }
-lean::cnstr_set(x_22, 0, x_11);
-lean::cnstr_set(x_22, 1, x_13);
-lean::cnstr_set(x_22, 2, x_21);
-lean::cnstr_set(x_22, 3, x_18);
-lean::cnstr_set_scalar(x_22, sizeof(void*)*4, x_15);
-x_23 = x_22;
-x_24 = lean::array_fset(x_8, x_0, x_23);
+lean::cnstr_set(x_21, 0, x_11);
+lean::cnstr_set(x_21, 1, x_13);
+lean::cnstr_set(x_21, 2, x_20);
+lean::cnstr_set(x_21, 3, x_17);
+x_22 = lean::array_fset(x_8, x_0, x_21);
 lean::dec(x_0);
 x_0 = x_10;
-x_1 = x_24;
+x_1 = x_22;
 goto _start;
 }
 default:
 {
-obj* x_27; 
-x_27 = lean::array_fset(x_8, x_0, x_6);
+obj* x_25; 
+x_25 = lean::array_fset(x_8, x_0, x_6);
 lean::dec(x_0);
 x_0 = x_10;
-x_1 = x_27;
+x_1 = x_25;
 goto _start;
 }
 }

src/stage0/init/lean/compiler/ir/livevars.cpp

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.compiler.ir.livevars
-// Imports: init.default init.lean.compiler.ir.basic
+// Imports: init.lean.compiler.ir.basic init.lean.compiler.ir.freevars init.control.reader init.control.conditional
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -14,16 +14,639 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-label"
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
-obj* initialize_init_default(obj*);
+obj* l_Lean_IR_IsLive_visitArgs___boxed(obj*, obj*, obj*);
+uint8 l_Lean_IR_HasIndex_visitExpr___main(obj*, obj*);
+uint8 l_Array_anyMAux___main___at_Lean_IR_HasIndex_visitArgs___spec__1(obj*, obj*, obj*);
+obj* l_Lean_IR_IsLive_visitFnBody___main(obj*, obj*, obj*);
+obj* l_Lean_IR_IsLive_visitArg(obj*, obj*, obj*);
+obj* l_Lean_IR_IsLive_visitExpr___boxed(obj*, obj*, obj*);
+obj* l_Lean_IR_IsLive_visitVar___boxed(obj*, obj*, obj*);
+obj* l_Lean_IR_FnBody_hasLiveVar___boxed(obj*, obj*, obj*);
+namespace lean {
+uint8 nat_dec_lt(obj*, obj*);
+}
+namespace lean {
+obj* nat_add(obj*, obj*);
+}
+namespace lean {
+uint8 nat_dec_eq(obj*, obj*);
+}
+obj* l_Lean_IR_IsLive_visitFnBody___main___boxed(obj*, obj*, obj*);
+obj* l_Lean_IR_FnBody_hasLiveVar(obj*, obj*, obj*);
+obj* l_Lean_IR_IsLive_visitJP___boxed(obj*, obj*, obj*);
+obj* l_Lean_IR_Context_eraseJoinPointDecl(obj*, obj*);
+obj* l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1(obj*, obj*, obj*, obj*);
+obj* l_Lean_IR_IsLive_visitExpr(obj*, obj*, obj*);
+obj* l_Lean_IR_AltCore_body___main(obj*);
+obj* l_Lean_IR_IsLive_visitJP(obj*, obj*, obj*);
+obj* l_Lean_IR_IsLive_visitArgs(obj*, obj*, obj*);
+obj* l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1___boxed(obj*, obj*, obj*, obj*);
+obj* l_Lean_IR_IsLive_visitFnBody(obj*, obj*, obj*);
+obj* l_Lean_IR_IsLive_visitFnBody___boxed(obj*, obj*, obj*);
+obj* l_Lean_IR_IsLive_visitVar(obj*, obj*, obj*);
+uint8 l_Lean_IR_HasIndex_visitArg___main(obj*, obj*);
+obj* l_Lean_IR_Context_getJoinPointBody(obj*, obj*);
+obj* l_Lean_IR_IsLive_visitArg___boxed(obj*, obj*, obj*);
+obj* l_Lean_IR_IsLive_visitVar(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+uint8 x_3; obj* x_4; obj* x_5; 
+x_3 = lean::nat_dec_eq(x_0, x_1);
+x_4 = lean::box(x_3);
+x_5 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_5, 0, x_4);
+lean::cnstr_set(x_5, 1, x_2);
+return x_5;
+}
+}
+obj* l_Lean_IR_IsLive_visitVar___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_IR_IsLive_visitVar(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* l_Lean_IR_IsLive_visitJP(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+uint8 x_3; obj* x_4; obj* x_5; 
+x_3 = lean::nat_dec_eq(x_0, x_1);
+x_4 = lean::box(x_3);
+x_5 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_5, 0, x_4);
+lean::cnstr_set(x_5, 1, x_2);
+return x_5;
+}
+}
+obj* l_Lean_IR_IsLive_visitJP___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_IR_IsLive_visitJP(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* l_Lean_IR_IsLive_visitArg(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+uint8 x_3; obj* x_4; obj* x_5; 
+x_3 = l_Lean_IR_HasIndex_visitArg___main(x_0, x_1);
+x_4 = lean::box(x_3);
+x_5 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_5, 0, x_4);
+lean::cnstr_set(x_5, 1, x_2);
+return x_5;
+}
+}
+obj* l_Lean_IR_IsLive_visitArg___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_IR_IsLive_visitArg(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* l_Lean_IR_IsLive_visitArgs(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; uint8 x_4; obj* x_5; obj* x_6; 
+x_3 = lean::mk_nat_obj(0ul);
+x_4 = l_Array_anyMAux___main___at_Lean_IR_HasIndex_visitArgs___spec__1(x_0, x_1, x_3);
+x_5 = lean::box(x_4);
+x_6 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_6, 0, x_5);
+lean::cnstr_set(x_6, 1, x_2);
+return x_6;
+}
+}
+obj* l_Lean_IR_IsLive_visitArgs___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_IR_IsLive_visitArgs(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* l_Lean_IR_IsLive_visitExpr(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+uint8 x_3; obj* x_4; obj* x_5; 
+x_3 = l_Lean_IR_HasIndex_visitExpr___main(x_0, x_1);
+x_4 = lean::box(x_3);
+x_5 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_5, 0, x_4);
+lean::cnstr_set(x_5, 1, x_2);
+return x_5;
+}
+}
+obj* l_Lean_IR_IsLive_visitExpr___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_IR_IsLive_visitExpr(x_0, x_1, x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; uint8 x_5; 
+x_4 = lean::array_get_size(x_1);
+x_5 = lean::nat_dec_lt(x_2, x_4);
+lean::dec(x_4);
+if (x_5 == 0)
+{
+uint8 x_8; obj* x_9; obj* x_10; 
+lean::dec(x_2);
+x_8 = 0;
+x_9 = lean::box(x_8);
+x_10 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_10, 0, x_9);
+lean::cnstr_set(x_10, 1, x_3);
+return x_10;
+}
+else
+{
+obj* x_11; obj* x_12; obj* x_14; obj* x_15; uint8 x_17; 
+x_11 = lean::array_fget(x_1, x_2);
+x_12 = l_Lean_IR_AltCore_body___main(x_11);
+lean::dec(x_11);
+x_14 = l_Lean_IR_IsLive_visitFnBody___main(x_0, x_12, x_3);
+x_15 = lean::cnstr_get(x_14, 0);
+lean::inc(x_15);
+x_17 = lean::unbox(x_15);
+if (x_17 == 0)
+{
+obj* x_18; obj* x_21; obj* x_22; 
+x_18 = lean::cnstr_get(x_14, 1);
+lean::inc(x_18);
+lean::dec(x_14);
+x_21 = lean::mk_nat_obj(1ul);
+x_22 = lean::nat_add(x_2, x_21);
+lean::dec(x_2);
+x_2 = x_22;
+x_3 = x_18;
+goto _start;
+}
+else
+{
+obj* x_26; obj* x_28; obj* x_29; 
+lean::dec(x_2);
+x_26 = lean::cnstr_get(x_14, 1);
+if (lean::is_exclusive(x_14)) {
+ lean::cnstr_release(x_14, 0);
+ x_28 = x_14;
+} else {
+ lean::inc(x_26);
+ lean::dec(x_14);
+ x_28 = lean::box(0);
+}
+if (lean::is_scalar(x_28)) {
+ x_29 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_29 = x_28;
+}
+lean::cnstr_set(x_29, 0, x_15);
+lean::cnstr_set(x_29, 1, x_26);
+return x_29;
+}
+}
+}
+}
+obj* l_Lean_IR_IsLive_visitFnBody___main(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+switch (lean::obj_tag(x_1)) {
+case 0:
+{
+obj* x_3; obj* x_5; uint8 x_8; 
+x_3 = lean::cnstr_get(x_1, 1);
+lean::inc(x_3);
+x_5 = lean::cnstr_get(x_1, 2);
+lean::inc(x_5);
+lean::dec(x_1);
+x_8 = l_Lean_IR_HasIndex_visitExpr___main(x_0, x_3);
+lean::dec(x_3);
+if (x_8 == 0)
+{
+x_1 = x_5;
+goto _start;
+}
+else
+{
+obj* x_12; obj* x_13; 
+lean::dec(x_5);
+x_12 = lean::box(x_8);
+x_13 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_13, 0, x_12);
+lean::cnstr_set(x_13, 1, x_2);
+return x_13;
+}
+}
+case 1:
+{
+obj* x_14; obj* x_16; obj* x_19; obj* x_20; uint8 x_22; 
+x_14 = lean::cnstr_get(x_1, 2);
+lean::inc(x_14);
+x_16 = lean::cnstr_get(x_1, 3);
+lean::inc(x_16);
+lean::dec(x_1);
+x_19 = l_Lean_IR_IsLive_visitFnBody___main(x_0, x_14, x_2);
+x_20 = lean::cnstr_get(x_19, 0);
+lean::inc(x_20);
+x_22 = lean::unbox(x_20);
+if (x_22 == 0)
+{
+obj* x_23; 
+x_23 = lean::cnstr_get(x_19, 1);
+lean::inc(x_23);
+lean::dec(x_19);
+x_1 = x_16;
+x_2 = x_23;
+goto _start;
+}
+else
+{
+obj* x_28; obj* x_30; obj* x_31; 
+lean::dec(x_16);
+x_28 = lean::cnstr_get(x_19, 1);
+if (lean::is_exclusive(x_19)) {
+ lean::cnstr_release(x_19, 0);
+ x_30 = x_19;
+} else {
+ lean::inc(x_28);
+ lean::dec(x_19);
+ x_30 = lean::box(0);
+}
+if (lean::is_scalar(x_30)) {
+ x_31 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_31 = x_30;
+}
+lean::cnstr_set(x_31, 0, x_20);
+lean::cnstr_set(x_31, 1, x_28);
+return x_31;
+}
+}
+case 2:
+{
+obj* x_32; obj* x_34; obj* x_36; uint8 x_39; 
+x_32 = lean::cnstr_get(x_1, 0);
+lean::inc(x_32);
+x_34 = lean::cnstr_get(x_1, 2);
+lean::inc(x_34);
+x_36 = lean::cnstr_get(x_1, 3);
+lean::inc(x_36);
+lean::dec(x_1);
+x_39 = lean::nat_dec_eq(x_0, x_32);
+lean::dec(x_32);
+if (x_39 == 0)
+{
+uint8 x_41; 
+x_41 = lean::nat_dec_eq(x_0, x_34);
+lean::dec(x_34);
+if (x_41 == 0)
+{
+x_1 = x_36;
+goto _start;
+}
+else
+{
+obj* x_45; obj* x_46; 
+lean::dec(x_36);
+x_45 = lean::box(x_41);
+x_46 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_46, 0, x_45);
+lean::cnstr_set(x_46, 1, x_2);
+return x_46;
+}
+}
+else
+{
+obj* x_49; obj* x_50; 
+lean::dec(x_34);
+lean::dec(x_36);
+x_49 = lean::box(x_39);
+x_50 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_50, 0, x_49);
+lean::cnstr_set(x_50, 1, x_2);
+return x_50;
+}
+}
+case 3:
+{
+obj* x_51; obj* x_53; obj* x_55; uint8 x_58; 
+x_51 = lean::cnstr_get(x_1, 0);
+lean::inc(x_51);
+x_53 = lean::cnstr_get(x_1, 2);
+lean::inc(x_53);
+x_55 = lean::cnstr_get(x_1, 3);
+lean::inc(x_55);
+lean::dec(x_1);
+x_58 = lean::nat_dec_eq(x_0, x_51);
+lean::dec(x_51);
+if (x_58 == 0)
+{
+uint8 x_60; 
+x_60 = lean::nat_dec_eq(x_0, x_53);
+lean::dec(x_53);
+if (x_60 == 0)
+{
+x_1 = x_55;
+goto _start;
+}
+else
+{
+obj* x_64; obj* x_65; 
+lean::dec(x_55);
+x_64 = lean::box(x_60);
+x_65 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_65, 0, x_64);
+lean::cnstr_set(x_65, 1, x_2);
+return x_65;
+}
+}
+else
+{
+obj* x_68; obj* x_69; 
+lean::dec(x_53);
+lean::dec(x_55);
+x_68 = lean::box(x_58);
+x_69 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_69, 0, x_68);
+lean::cnstr_set(x_69, 1, x_2);
+return x_69;
+}
+}
+case 4:
+{
+obj* x_70; obj* x_72; obj* x_74; uint8 x_77; 
+x_70 = lean::cnstr_get(x_1, 0);
+lean::inc(x_70);
+x_72 = lean::cnstr_get(x_1, 3);
+lean::inc(x_72);
+x_74 = lean::cnstr_get(x_1, 4);
+lean::inc(x_74);
+lean::dec(x_1);
+x_77 = lean::nat_dec_eq(x_0, x_70);
+lean::dec(x_70);
+if (x_77 == 0)
+{
+uint8 x_79; 
+x_79 = lean::nat_dec_eq(x_0, x_72);
+lean::dec(x_72);
+if (x_79 == 0)
+{
+x_1 = x_74;
+goto _start;
+}
+else
+{
+obj* x_83; obj* x_84; 
+lean::dec(x_74);
+x_83 = lean::box(x_79);
+x_84 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_84, 0, x_83);
+lean::cnstr_set(x_84, 1, x_2);
+return x_84;
+}
+}
+else
+{
+obj* x_87; obj* x_88; 
+lean::dec(x_74);
+lean::dec(x_72);
+x_87 = lean::box(x_77);
+x_88 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_88, 0, x_87);
+lean::cnstr_set(x_88, 1, x_2);
+return x_88;
+}
+}
+case 8:
+{
+obj* x_89; 
+x_89 = lean::cnstr_get(x_1, 1);
+lean::inc(x_89);
+lean::dec(x_1);
+x_1 = x_89;
+goto _start;
+}
+case 9:
+{
+obj* x_93; obj* x_95; uint8 x_98; 
+x_93 = lean::cnstr_get(x_1, 1);
+lean::inc(x_93);
+x_95 = lean::cnstr_get(x_1, 2);
+lean::inc(x_95);
+lean::dec(x_1);
+x_98 = lean::nat_dec_eq(x_0, x_93);
+lean::dec(x_93);
+if (x_98 == 0)
+{
+obj* x_100; obj* x_101; 
+x_100 = lean::mk_nat_obj(0ul);
+x_101 = l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1(x_0, x_95, x_100, x_2);
+lean::dec(x_95);
+return x_101;
+}
+else
+{
+obj* x_104; obj* x_105; 
+lean::dec(x_95);
+x_104 = lean::box(x_98);
+x_105 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_105, 0, x_104);
+lean::cnstr_set(x_105, 1, x_2);
+return x_105;
+}
+}
+case 10:
+{
+obj* x_106; uint8 x_109; obj* x_111; obj* x_112; 
+x_106 = lean::cnstr_get(x_1, 0);
+lean::inc(x_106);
+lean::dec(x_1);
+x_109 = l_Lean_IR_HasIndex_visitArg___main(x_0, x_106);
+lean::dec(x_106);
+x_111 = lean::box(x_109);
+x_112 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_112, 0, x_111);
+lean::cnstr_set(x_112, 1, x_2);
+return x_112;
+}
+case 11:
+{
+obj* x_113; obj* x_115; obj* x_118; uint8 x_119; 
+x_113 = lean::cnstr_get(x_1, 0);
+lean::inc(x_113);
+x_115 = lean::cnstr_get(x_1, 1);
+lean::inc(x_115);
+lean::dec(x_1);
+x_118 = lean::mk_nat_obj(0ul);
+x_119 = l_Array_anyMAux___main___at_Lean_IR_HasIndex_visitArgs___spec__1(x_0, x_115, x_118);
+lean::dec(x_115);
+if (x_119 == 0)
+{
+obj* x_122; 
+lean::inc(x_2);
+x_122 = l_Lean_IR_Context_getJoinPointBody(x_2, x_113);
+if (lean::obj_tag(x_122) == 0)
+{
+obj* x_124; obj* x_125; 
+lean::dec(x_113);
+x_124 = lean::box(x_119);
+x_125 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_125, 0, x_124);
+lean::cnstr_set(x_125, 1, x_2);
+return x_125;
+}
+else
+{
+obj* x_126; obj* x_129; 
+x_126 = lean::cnstr_get(x_122, 0);
+lean::inc(x_126);
+lean::dec(x_122);
+x_129 = l_Lean_IR_Context_eraseJoinPointDecl(x_2, x_113);
+lean::dec(x_113);
+x_1 = x_126;
+x_2 = x_129;
+goto _start;
+}
+}
+else
+{
+obj* x_133; obj* x_134; 
+lean::dec(x_113);
+x_133 = lean::box(x_119);
+x_134 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_134, 0, x_133);
+lean::cnstr_set(x_134, 1, x_2);
+return x_134;
+}
+}
+case 12:
+{
+uint8 x_135; obj* x_136; obj* x_137; 
+x_135 = 0;
+x_136 = lean::box(x_135);
+x_137 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_137, 0, x_136);
+lean::cnstr_set(x_137, 1, x_2);
+return x_137;
+}
+default:
+{
+obj* x_138; obj* x_140; uint8 x_143; 
+x_138 = lean::cnstr_get(x_1, 0);
+lean::inc(x_138);
+x_140 = lean::cnstr_get(x_1, 2);
+lean::inc(x_140);
+lean::dec(x_1);
+x_143 = lean::nat_dec_eq(x_0, x_138);
+lean::dec(x_138);
+if (x_143 == 0)
+{
+x_1 = x_140;
+goto _start;
+}
+else
+{
+obj* x_147; obj* x_148; 
+lean::dec(x_140);
+x_147 = lean::box(x_143);
+x_148 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_148, 0, x_147);
+lean::cnstr_set(x_148, 1, x_2);
+return x_148;
+}
+}
+}
+}
+}
+obj* l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1(x_0, x_1, x_2, x_3);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_4;
+}
+}
+obj* l_Lean_IR_IsLive_visitFnBody___main___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_IR_IsLive_visitFnBody___main(x_0, x_1, x_2);
+lean::dec(x_0);
+return x_3;
+}
+}
+obj* l_Lean_IR_IsLive_visitFnBody(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_IR_IsLive_visitFnBody___main(x_0, x_1, x_2);
+return x_3;
+}
+}
+obj* l_Lean_IR_IsLive_visitFnBody___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_IR_IsLive_visitFnBody(x_0, x_1, x_2);
+lean::dec(x_0);
+return x_3;
+}
+}
+obj* l_Lean_IR_FnBody_hasLiveVar(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; obj* x_4; 
+x_3 = l_Lean_IR_IsLive_visitFnBody___main(x_2, x_0, x_1);
+x_4 = lean::cnstr_get(x_3, 0);
+lean::inc(x_4);
+lean::dec(x_3);
+return x_4;
+}
+}
+obj* l_Lean_IR_FnBody_hasLiveVar___boxed(obj* x_0, obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_IR_FnBody_hasLiveVar(x_0, x_1, x_2);
+lean::dec(x_2);
+return x_3;
+}
+}
 obj* initialize_init_lean_compiler_ir_basic(obj*);
+obj* initialize_init_lean_compiler_ir_freevars(obj*);
+obj* initialize_init_control_reader(obj*);
+obj* initialize_init_control_conditional(obj*);
 static bool _G_initialized = false;
 obj* initialize_init_lean_compiler_ir_livevars(obj* w) {
  if (_G_initialized) return w;
  _G_initialized = true;
 if (io_result_is_error(w)) return w;
-w = initialize_init_default(w);
-if (io_result_is_error(w)) return w;
 w = initialize_init_lean_compiler_ir_basic(w);
 if (io_result_is_error(w)) return w;
+w = initialize_init_lean_compiler_ir_freevars(w);
+if (io_result_is_error(w)) return w;
+w = initialize_init_control_reader(w);
+if (io_result_is_error(w)) return w;
+w = initialize_init_control_conditional(w);
+if (io_result_is_error(w)) return w;
 return w;
 }

src/stage0/init/lean/compiler/ir/normids.cpp

@@ -1055,527 +1055,524 @@ return x_25;
 }
 case 1:
 {
-obj* x_26; obj* x_28; uint8 x_30; obj* x_31; obj* x_33; obj* x_35; obj* x_36; obj* x_38; obj* x_39; obj* x_41; obj* x_45; obj* x_46; obj* x_47; obj* x_49; obj* x_52; obj* x_53; obj* x_55; obj* x_56; obj* x_57; obj* x_59; obj* x_61; obj* x_62; obj* x_63; obj* x_64; 
+obj* x_26; obj* x_28; obj* x_30; obj* x_32; obj* x_34; obj* x_35; obj* x_37; obj* x_38; obj* x_40; obj* x_44; obj* x_45; obj* x_46; obj* x_48; obj* x_51; obj* x_52; obj* x_54; obj* x_55; obj* x_56; obj* x_58; obj* x_60; obj* x_61; obj* x_62; 
 x_26 = lean::cnstr_get(x_0, 0);
 x_28 = lean::cnstr_get(x_0, 1);
-x_30 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*4);
-x_31 = lean::cnstr_get(x_0, 2);
-x_33 = lean::cnstr_get(x_0, 3);
+x_30 = lean::cnstr_get(x_0, 2);
+x_32 = lean::cnstr_get(x_0, 3);
 if (lean::is_exclusive(x_0)) {
- x_35 = x_0;
+ x_34 = x_0;
 } else {
  lean::inc(x_26);
  lean::inc(x_28);
- lean::inc(x_31);
- lean::inc(x_33);
+ lean::inc(x_30);
+ lean::inc(x_32);
  lean::dec(x_0);
- x_35 = lean::box(0);
+ x_34 = lean::box(0);
 }
-x_36 = lean::mk_nat_obj(0ul);
+x_35 = lean::mk_nat_obj(0ul);
 lean::inc(x_1);
-x_38 = l_Array_miterateAux___main___at_Lean_IR_NormalizeIds_normFnBody___main___spec__1(x_28, x_28, x_36, x_1, x_2);
-x_39 = lean::cnstr_get(x_38, 0);
-lean::inc(x_39);
-x_41 = lean::cnstr_get(x_38, 1);
-lean::inc(x_41);
-lean::dec(x_38);
-lean::inc(x_39);
-x_45 = l_Array_hmmapAux___main___at_Lean_IR_NormalizeIds_normFnBody___main___spec__2(x_39, x_36, x_28);
-x_46 = l_Lean_IR_NormalizeIds_normFnBody___main(x_31, x_39, x_41);
-x_47 = lean::cnstr_get(x_46, 0);
-lean::inc(x_47);
-x_49 = lean::cnstr_get(x_46, 1);
-lean::inc(x_49);
-lean::dec(x_46);
-x_52 = lean::mk_nat_obj(1ul);
-x_53 = lean::nat_add(x_49, x_52);
-lean::inc(x_49);
-x_55 = l_RBNode_insert___at_Lean_IR_addVarRename___spec__1(x_1, x_26, x_49);
-x_56 = l_Lean_IR_NormalizeIds_normFnBody___main(x_33, x_55, x_53);
-x_57 = lean::cnstr_get(x_56, 0);
-x_59 = lean::cnstr_get(x_56, 1);
-if (lean::is_exclusive(x_56)) {
- x_61 = x_56;
+x_37 = l_Array_miterateAux___main___at_Lean_IR_NormalizeIds_normFnBody___main___spec__1(x_28, x_28, x_35, x_1, x_2);
+x_38 = lean::cnstr_get(x_37, 0);
+lean::inc(x_38);
+x_40 = lean::cnstr_get(x_37, 1);
+lean::inc(x_40);
+lean::dec(x_37);
+lean::inc(x_38);
+x_44 = l_Array_hmmapAux___main___at_Lean_IR_NormalizeIds_normFnBody___main___spec__2(x_38, x_35, x_28);
+x_45 = l_Lean_IR_NormalizeIds_normFnBody___main(x_30, x_38, x_40);
+x_46 = lean::cnstr_get(x_45, 0);
+lean::inc(x_46);
+x_48 = lean::cnstr_get(x_45, 1);
+lean::inc(x_48);
+lean::dec(x_45);
+x_51 = lean::mk_nat_obj(1ul);
+x_52 = lean::nat_add(x_48, x_51);
+lean::inc(x_48);
+x_54 = l_RBNode_insert___at_Lean_IR_addVarRename___spec__1(x_1, x_26, x_48);
+x_55 = l_Lean_IR_NormalizeIds_normFnBody___main(x_32, x_54, x_52);
+x_56 = lean::cnstr_get(x_55, 0);
+x_58 = lean::cnstr_get(x_55, 1);
+if (lean::is_exclusive(x_55)) {
+ x_60 = x_55;
 } else {
- lean::inc(x_57);
- lean::inc(x_59);
- lean::dec(x_56);
- x_61 = lean::box(0);
+ lean::inc(x_56);
+ lean::inc(x_58);
+ lean::dec(x_55);
+ x_60 = lean::box(0);
 }
-if (lean::is_scalar(x_35)) {
- x_62 = lean::alloc_cnstr(1, 4, 1);
+if (lean::is_scalar(x_34)) {
+ x_61 = lean::alloc_cnstr(1, 4, 0);
 } else {
- x_62 = x_35;
+ x_61 = x_34;
 }
-lean::cnstr_set(x_62, 0, x_49);
-lean::cnstr_set(x_62, 1, x_45);
-lean::cnstr_set(x_62, 2, x_47);
-lean::cnstr_set(x_62, 3, x_57);
-lean::cnstr_set_scalar(x_62, sizeof(void*)*4, x_30);
-x_63 = x_62;
-if (lean::is_scalar(x_61)) {
- x_64 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_61, 0, x_48);
+lean::cnstr_set(x_61, 1, x_44);
+lean::cnstr_set(x_61, 2, x_46);
+lean::cnstr_set(x_61, 3, x_56);
+if (lean::is_scalar(x_60)) {
+ x_62 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_64 = x_61;
+ x_62 = x_60;
 }
-lean::cnstr_set(x_64, 0, x_63);
-lean::cnstr_set(x_64, 1, x_59);
-return x_64;
+lean::cnstr_set(x_62, 0, x_61);
+lean::cnstr_set(x_62, 1, x_58);
+return x_62;
 }
 case 2:
 {
-obj* x_65; obj* x_67; obj* x_69; obj* x_71; obj* x_73; obj* x_75; obj* x_78; obj* x_80; obj* x_81; obj* x_83; obj* x_85; obj* x_86; obj* x_87; 
-x_65 = lean::cnstr_get(x_0, 0);
-x_67 = lean::cnstr_get(x_0, 1);
-x_69 = lean::cnstr_get(x_0, 2);
-x_71 = lean::cnstr_get(x_0, 3);
+obj* x_63; obj* x_65; obj* x_67; obj* x_69; obj* x_71; obj* x_73; obj* x_76; obj* x_78; obj* x_79; obj* x_81; obj* x_83; obj* x_84; obj* x_85; 
+x_63 = lean::cnstr_get(x_0, 0);
+x_65 = lean::cnstr_get(x_0, 1);
+x_67 = lean::cnstr_get(x_0, 2);
+x_69 = lean::cnstr_get(x_0, 3);
 if (lean::is_exclusive(x_0)) {
- x_73 = x_0;
+ x_71 = x_0;
 } else {
+ lean::inc(x_63);
  lean::inc(x_65);
  lean::inc(x_67);
  lean::inc(x_69);
- lean::inc(x_71);
  lean::dec(x_0);
- x_73 = lean::box(0);
+ x_71 = lean::box(0);
 }
 lean::inc(x_1);
-x_75 = l_Lean_IR_NormalizeIds_normIndex(x_65, x_1);
-lean::dec(x_65);
+x_73 = l_Lean_IR_NormalizeIds_normIndex(x_63, x_1);
+lean::dec(x_63);
 lean::inc(x_1);
-x_78 = l_Lean_IR_NormalizeIds_normIndex(x_69, x_1);
-lean::dec(x_69);
-x_80 = l_Lean_IR_NormalizeIds_normFnBody___main(x_71, x_1, x_2);
-x_81 = lean::cnstr_get(x_80, 0);
-x_83 = lean::cnstr_get(x_80, 1);
-if (lean::is_exclusive(x_80)) {
- x_85 = x_80;
+x_76 = l_Lean_IR_NormalizeIds_normIndex(x_67, x_1);
+lean::dec(x_67);
+x_78 = l_Lean_IR_NormalizeIds_normFnBody___main(x_69, x_1, x_2);
+x_79 = lean::cnstr_get(x_78, 0);
+x_81 = lean::cnstr_get(x_78, 1);
+if (lean::is_exclusive(x_78)) {
+ x_83 = x_78;
 } else {
+ lean::inc(x_79);
  lean::inc(x_81);
- lean::inc(x_83);
- lean::dec(x_80);
- x_85 = lean::box(0);
+ lean::dec(x_78);
+ x_83 = lean::box(0);
 }
-if (lean::is_scalar(x_73)) {
- x_86 = lean::alloc_cnstr(2, 4, 0);
+if (lean::is_scalar(x_71)) {
+ x_84 = lean::alloc_cnstr(2, 4, 0);
 } else {
- x_86 = x_73;
+ x_84 = x_71;
 }
-lean::cnstr_set(x_86, 0, x_75);
-lean::cnstr_set(x_86, 1, x_67);
-lean::cnstr_set(x_86, 2, x_78);
-lean::cnstr_set(x_86, 3, x_81);
-if (lean::is_scalar(x_85)) {
- x_87 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_84, 0, x_73);
+lean::cnstr_set(x_84, 1, x_65);
+lean::cnstr_set(x_84, 2, x_76);
+lean::cnstr_set(x_84, 3, x_79);
+if (lean::is_scalar(x_83)) {
+ x_85 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_87 = x_85;
+ x_85 = x_83;
 }
-lean::cnstr_set(x_87, 0, x_86);
-lean::cnstr_set(x_87, 1, x_83);
-return x_87;
+lean::cnstr_set(x_85, 0, x_84);
+lean::cnstr_set(x_85, 1, x_81);
+return x_85;
 }
 case 3:
 {
-obj* x_88; obj* x_90; obj* x_92; obj* x_94; obj* x_96; obj* x_98; obj* x_101; obj* x_103; obj* x_104; obj* x_106; obj* x_108; obj* x_109; obj* x_110; 
-x_88 = lean::cnstr_get(x_0, 0);
-x_90 = lean::cnstr_get(x_0, 1);
-x_92 = lean::cnstr_get(x_0, 2);
-x_94 = lean::cnstr_get(x_0, 3);
+obj* x_86; obj* x_88; obj* x_90; obj* x_92; obj* x_94; obj* x_96; obj* x_99; obj* x_101; obj* x_102; obj* x_104; obj* x_106; obj* x_107; obj* x_108; 
+x_86 = lean::cnstr_get(x_0, 0);
+x_88 = lean::cnstr_get(x_0, 1);
+x_90 = lean::cnstr_get(x_0, 2);
+x_92 = lean::cnstr_get(x_0, 3);
 if (lean::is_exclusive(x_0)) {
- x_96 = x_0;
+ x_94 = x_0;
 } else {
+ lean::inc(x_86);
  lean::inc(x_88);
  lean::inc(x_90);
  lean::inc(x_92);
- lean::inc(x_94);
  lean::dec(x_0);
- x_96 = lean::box(0);
+ x_94 = lean::box(0);
 }
 lean::inc(x_1);
-x_98 = l_Lean_IR_NormalizeIds_normIndex(x_88, x_1);
-lean::dec(x_88);
+x_96 = l_Lean_IR_NormalizeIds_normIndex(x_86, x_1);
+lean::dec(x_86);
 lean::inc(x_1);
-x_101 = l_Lean_IR_NormalizeIds_normIndex(x_92, x_1);
-lean::dec(x_92);
-x_103 = l_Lean_IR_NormalizeIds_normFnBody___main(x_94, x_1, x_2);
-x_104 = lean::cnstr_get(x_103, 0);
-x_106 = lean::cnstr_get(x_103, 1);
-if (lean::is_exclusive(x_103)) {
- x_108 = x_103;
+x_99 = l_Lean_IR_NormalizeIds_normIndex(x_90, x_1);
+lean::dec(x_90);
+x_101 = l_Lean_IR_NormalizeIds_normFnBody___main(x_92, x_1, x_2);
+x_102 = lean::cnstr_get(x_101, 0);
+x_104 = lean::cnstr_get(x_101, 1);
+if (lean::is_exclusive(x_101)) {
+ x_106 = x_101;
 } else {
+ lean::inc(x_102);
  lean::inc(x_104);
- lean::inc(x_106);
- lean::dec(x_103);
- x_108 = lean::box(0);
+ lean::dec(x_101);
+ x_106 = lean::box(0);
 }
-if (lean::is_scalar(x_96)) {
- x_109 = lean::alloc_cnstr(3, 4, 0);
+if (lean::is_scalar(x_94)) {
+ x_107 = lean::alloc_cnstr(3, 4, 0);
 } else {
- x_109 = x_96;
+ x_107 = x_94;
 }
-lean::cnstr_set(x_109, 0, x_98);
-lean::cnstr_set(x_109, 1, x_90);
-lean::cnstr_set(x_109, 2, x_101);
-lean::cnstr_set(x_109, 3, x_104);
-if (lean::is_scalar(x_108)) {
- x_110 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_107, 0, x_96);
+lean::cnstr_set(x_107, 1, x_88);
+lean::cnstr_set(x_107, 2, x_99);
+lean::cnstr_set(x_107, 3, x_102);
+if (lean::is_scalar(x_106)) {
+ x_108 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_110 = x_108;
+ x_108 = x_106;
 }
-lean::cnstr_set(x_110, 0, x_109);
-lean::cnstr_set(x_110, 1, x_106);
-return x_110;
+lean::cnstr_set(x_108, 0, x_107);
+lean::cnstr_set(x_108, 1, x_104);
+return x_108;
 }
 case 4:
 {
-obj* x_111; obj* x_113; obj* x_115; obj* x_117; uint8 x_119; obj* x_120; obj* x_122; obj* x_124; obj* x_127; obj* x_129; obj* x_130; obj* x_132; obj* x_134; obj* x_135; obj* x_136; obj* x_137; 
-x_111 = lean::cnstr_get(x_0, 0);
-x_113 = lean::cnstr_get(x_0, 1);
-x_115 = lean::cnstr_get(x_0, 2);
-x_117 = lean::cnstr_get(x_0, 3);
-x_119 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*5);
-x_120 = lean::cnstr_get(x_0, 4);
+obj* x_109; obj* x_111; obj* x_113; obj* x_115; uint8 x_117; obj* x_118; obj* x_120; obj* x_122; obj* x_125; obj* x_127; obj* x_128; obj* x_130; obj* x_132; obj* x_133; obj* x_134; obj* x_135; 
+x_109 = lean::cnstr_get(x_0, 0);
+x_111 = lean::cnstr_get(x_0, 1);
+x_113 = lean::cnstr_get(x_0, 2);
+x_115 = lean::cnstr_get(x_0, 3);
+x_117 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*5);
+x_118 = lean::cnstr_get(x_0, 4);
 if (lean::is_exclusive(x_0)) {
- x_122 = x_0;
+ x_120 = x_0;
 } else {
+ lean::inc(x_109);
  lean::inc(x_111);
  lean::inc(x_113);
  lean::inc(x_115);
- lean::inc(x_117);
- lean::inc(x_120);
+ lean::inc(x_118);
  lean::dec(x_0);
- x_122 = lean::box(0);
+ x_120 = lean::box(0);
 }
 lean::inc(x_1);
-x_124 = l_Lean_IR_NormalizeIds_normIndex(x_111, x_1);
-lean::dec(x_111);
+x_122 = l_Lean_IR_NormalizeIds_normIndex(x_109, x_1);
+lean::dec(x_109);
 lean::inc(x_1);
-x_127 = l_Lean_IR_NormalizeIds_normIndex(x_117, x_1);
-lean::dec(x_117);
-x_129 = l_Lean_IR_NormalizeIds_normFnBody___main(x_120, x_1, x_2);
-x_130 = lean::cnstr_get(x_129, 0);
-x_132 = lean::cnstr_get(x_129, 1);
-if (lean::is_exclusive(x_129)) {
- x_134 = x_129;
+x_125 = l_Lean_IR_NormalizeIds_normIndex(x_115, x_1);
+lean::dec(x_115);
+x_127 = l_Lean_IR_NormalizeIds_normFnBody___main(x_118, x_1, x_2);
+x_128 = lean::cnstr_get(x_127, 0);
+x_130 = lean::cnstr_get(x_127, 1);
+if (lean::is_exclusive(x_127)) {
+ x_132 = x_127;
 } else {
+ lean::inc(x_128);
  lean::inc(x_130);
- lean::inc(x_132);
- lean::dec(x_129);
- x_134 = lean::box(0);
+ lean::dec(x_127);
+ x_132 = lean::box(0);
 }
-if (lean::is_scalar(x_122)) {
- x_135 = lean::alloc_cnstr(4, 5, 1);
+if (lean::is_scalar(x_120)) {
+ x_133 = lean::alloc_cnstr(4, 5, 1);
 } else {
- x_135 = x_122;
+ x_133 = x_120;
 }
-lean::cnstr_set(x_135, 0, x_124);
-lean::cnstr_set(x_135, 1, x_113);
-lean::cnstr_set(x_135, 2, x_115);
-lean::cnstr_set(x_135, 3, x_127);
-lean::cnstr_set(x_135, 4, x_130);
-lean::cnstr_set_scalar(x_135, sizeof(void*)*5, x_119);
-x_136 = x_135;
-if (lean::is_scalar(x_134)) {
- x_137 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_133, 0, x_122);
+lean::cnstr_set(x_133, 1, x_111);
+lean::cnstr_set(x_133, 2, x_113);
+lean::cnstr_set(x_133, 3, x_125);
+lean::cnstr_set(x_133, 4, x_128);
+lean::cnstr_set_scalar(x_133, sizeof(void*)*5, x_117);
+x_134 = x_133;
+if (lean::is_scalar(x_132)) {
+ x_135 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_137 = x_134;
+ x_135 = x_132;
 }
-lean::cnstr_set(x_137, 0, x_136);
-lean::cnstr_set(x_137, 1, x_132);
-return x_137;
+lean::cnstr_set(x_135, 0, x_134);
+lean::cnstr_set(x_135, 1, x_130);
+return x_135;
 }
 case 5:
 {
-obj* x_138; obj* x_140; obj* x_142; obj* x_144; obj* x_146; obj* x_148; obj* x_149; obj* x_151; obj* x_153; obj* x_154; obj* x_155; 
-x_138 = lean::cnstr_get(x_0, 0);
-x_140 = lean::cnstr_get(x_0, 1);
-x_142 = lean::cnstr_get(x_0, 2);
+obj* x_136; obj* x_138; obj* x_140; obj* x_142; obj* x_144; obj* x_146; obj* x_147; obj* x_149; obj* x_151; obj* x_152; obj* x_153; 
+x_136 = lean::cnstr_get(x_0, 0);
+x_138 = lean::cnstr_get(x_0, 1);
+x_140 = lean::cnstr_get(x_0, 2);
 if (lean::is_exclusive(x_0)) {
- x_144 = x_0;
+ x_142 = x_0;
 } else {
+ lean::inc(x_136);
  lean::inc(x_138);
  lean::inc(x_140);
- lean::inc(x_142);
  lean::dec(x_0);
- x_144 = lean::box(0);
+ x_142 = lean::box(0);
 }
 lean::inc(x_1);
-x_146 = l_Lean_IR_NormalizeIds_normIndex(x_138, x_1);
-lean::dec(x_138);
-x_148 = l_Lean_IR_NormalizeIds_normFnBody___main(x_142, x_1, x_2);
-x_149 = lean::cnstr_get(x_148, 0);
-x_151 = lean::cnstr_get(x_148, 1);
-if (lean::is_exclusive(x_148)) {
- x_153 = x_148;
+x_144 = l_Lean_IR_NormalizeIds_normIndex(x_136, x_1);
+lean::dec(x_136);
+x_146 = l_Lean_IR_NormalizeIds_normFnBody___main(x_140, x_1, x_2);
+x_147 = lean::cnstr_get(x_146, 0);
+x_149 = lean::cnstr_get(x_146, 1);
+if (lean::is_exclusive(x_146)) {
+ x_151 = x_146;
 } else {
+ lean::inc(x_147);
  lean::inc(x_149);
- lean::inc(x_151);
- lean::dec(x_148);
- x_153 = lean::box(0);
+ lean::dec(x_146);
+ x_151 = lean::box(0);
 }
-if (lean::is_scalar(x_144)) {
- x_154 = lean::alloc_cnstr(5, 3, 0);
+if (lean::is_scalar(x_142)) {
+ x_152 = lean::alloc_cnstr(5, 3, 0);
 } else {
- x_154 = x_144;
+ x_152 = x_142;
 }
-lean::cnstr_set(x_154, 0, x_146);
-lean::cnstr_set(x_154, 1, x_140);
-lean::cnstr_set(x_154, 2, x_149);
-if (lean::is_scalar(x_153)) {
- x_155 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_152, 0, x_144);
+lean::cnstr_set(x_152, 1, x_138);
+lean::cnstr_set(x_152, 2, x_147);
+if (lean::is_scalar(x_151)) {
+ x_153 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_155 = x_153;
+ x_153 = x_151;
 }
-lean::cnstr_set(x_155, 0, x_154);
-lean::cnstr_set(x_155, 1, x_151);
-return x_155;
+lean::cnstr_set(x_153, 0, x_152);
+lean::cnstr_set(x_153, 1, x_149);
+return x_153;
 }
 case 6:
 {
-obj* x_156; obj* x_158; uint8 x_160; obj* x_161; obj* x_163; obj* x_165; obj* x_167; obj* x_168; obj* x_170; obj* x_172; obj* x_173; obj* x_174; obj* x_175; 
-x_156 = lean::cnstr_get(x_0, 0);
-x_158 = lean::cnstr_get(x_0, 1);
-x_160 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*3);
-x_161 = lean::cnstr_get(x_0, 2);
+obj* x_154; obj* x_156; uint8 x_158; obj* x_159; obj* x_161; obj* x_163; obj* x_165; obj* x_166; obj* x_168; obj* x_170; obj* x_171; obj* x_172; obj* x_173; 
+x_154 = lean::cnstr_get(x_0, 0);
+x_156 = lean::cnstr_get(x_0, 1);
+x_158 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*3);
+x_159 = lean::cnstr_get(x_0, 2);
 if (lean::is_exclusive(x_0)) {
- x_163 = x_0;
+ x_161 = x_0;
 } else {
+ lean::inc(x_154);
  lean::inc(x_156);
- lean::inc(x_158);
- lean::inc(x_161);
+ lean::inc(x_159);
  lean::dec(x_0);
- x_163 = lean::box(0);
+ x_161 = lean::box(0);
 }
 lean::inc(x_1);
-x_165 = l_Lean_IR_NormalizeIds_normIndex(x_156, x_1);
-lean::dec(x_156);
-x_167 = l_Lean_IR_NormalizeIds_normFnBody___main(x_161, x_1, x_2);
-x_168 = lean::cnstr_get(x_167, 0);
-x_170 = lean::cnstr_get(x_167, 1);
-if (lean::is_exclusive(x_167)) {
- x_172 = x_167;
+x_163 = l_Lean_IR_NormalizeIds_normIndex(x_154, x_1);
+lean::dec(x_154);
+x_165 = l_Lean_IR_NormalizeIds_normFnBody___main(x_159, x_1, x_2);
+x_166 = lean::cnstr_get(x_165, 0);
+x_168 = lean::cnstr_get(x_165, 1);
+if (lean::is_exclusive(x_165)) {
+ x_170 = x_165;
 } else {
+ lean::inc(x_166);
  lean::inc(x_168);
- lean::inc(x_170);
- lean::dec(x_167);
- x_172 = lean::box(0);
+ lean::dec(x_165);
+ x_170 = lean::box(0);
 }
-if (lean::is_scalar(x_163)) {
- x_173 = lean::alloc_cnstr(6, 3, 1);
+if (lean::is_scalar(x_161)) {
+ x_171 = lean::alloc_cnstr(6, 3, 1);
 } else {
- x_173 = x_163;
+ x_171 = x_161;
 }
-lean::cnstr_set(x_173, 0, x_165);
-lean::cnstr_set(x_173, 1, x_158);
-lean::cnstr_set(x_173, 2, x_168);
-lean::cnstr_set_scalar(x_173, sizeof(void*)*3, x_160);
-x_174 = x_173;
-if (lean::is_scalar(x_172)) {
- x_175 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_171, 0, x_163);
+lean::cnstr_set(x_171, 1, x_156);
+lean::cnstr_set(x_171, 2, x_166);
+lean::cnstr_set_scalar(x_171, sizeof(void*)*3, x_158);
+x_172 = x_171;
+if (lean::is_scalar(x_170)) {
+ x_173 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_175 = x_172;
+ x_173 = x_170;
 }
-lean::cnstr_set(x_175, 0, x_174);
-lean::cnstr_set(x_175, 1, x_170);
-return x_175;
+lean::cnstr_set(x_173, 0, x_172);
+lean::cnstr_set(x_173, 1, x_168);
+return x_173;
 }
 case 7:
 {
-obj* x_176; obj* x_178; uint8 x_180; obj* x_181; obj* x_183; obj* x_185; obj* x_187; obj* x_188; obj* x_190; obj* x_192; obj* x_193; obj* x_194; obj* x_195; 
-x_176 = lean::cnstr_get(x_0, 0);
-x_178 = lean::cnstr_get(x_0, 1);
-x_180 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*3);
-x_181 = lean::cnstr_get(x_0, 2);
+obj* x_174; obj* x_176; uint8 x_178; obj* x_179; obj* x_181; obj* x_183; obj* x_185; obj* x_186; obj* x_188; obj* x_190; obj* x_191; obj* x_192; obj* x_193; 
+x_174 = lean::cnstr_get(x_0, 0);
+x_176 = lean::cnstr_get(x_0, 1);
+x_178 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*3);
+x_179 = lean::cnstr_get(x_0, 2);
 if (lean::is_exclusive(x_0)) {
- x_183 = x_0;
+ x_181 = x_0;
 } else {
+ lean::inc(x_174);
  lean::inc(x_176);
- lean::inc(x_178);
- lean::inc(x_181);
+ lean::inc(x_179);
  lean::dec(x_0);
- x_183 = lean::box(0);
+ x_181 = lean::box(0);
 }
 lean::inc(x_1);
-x_185 = l_Lean_IR_NormalizeIds_normIndex(x_176, x_1);
-lean::dec(x_176);
-x_187 = l_Lean_IR_NormalizeIds_normFnBody___main(x_181, x_1, x_2);
-x_188 = lean::cnstr_get(x_187, 0);
-x_190 = lean::cnstr_get(x_187, 1);
-if (lean::is_exclusive(x_187)) {
- x_192 = x_187;
+x_183 = l_Lean_IR_NormalizeIds_normIndex(x_174, x_1);
+lean::dec(x_174);
+x_185 = l_Lean_IR_NormalizeIds_normFnBody___main(x_179, x_1, x_2);
+x_186 = lean::cnstr_get(x_185, 0);
+x_188 = lean::cnstr_get(x_185, 1);
+if (lean::is_exclusive(x_185)) {
+ x_190 = x_185;
 } else {
+ lean::inc(x_186);
  lean::inc(x_188);
- lean::inc(x_190);
- lean::dec(x_187);
- x_192 = lean::box(0);
+ lean::dec(x_185);
+ x_190 = lean::box(0);
 }
-if (lean::is_scalar(x_183)) {
- x_193 = lean::alloc_cnstr(7, 3, 1);
+if (lean::is_scalar(x_181)) {
+ x_191 = lean::alloc_cnstr(7, 3, 1);
 } else {
- x_193 = x_183;
+ x_191 = x_181;
 }
-lean::cnstr_set(x_193, 0, x_185);
-lean::cnstr_set(x_193, 1, x_178);
-lean::cnstr_set(x_193, 2, x_188);
-lean::cnstr_set_scalar(x_193, sizeof(void*)*3, x_180);
-x_194 = x_193;
-if (lean::is_scalar(x_192)) {
- x_195 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_191, 0, x_183);
+lean::cnstr_set(x_191, 1, x_176);
+lean::cnstr_set(x_191, 2, x_186);
+lean::cnstr_set_scalar(x_191, sizeof(void*)*3, x_178);
+x_192 = x_191;
+if (lean::is_scalar(x_190)) {
+ x_193 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_195 = x_192;
+ x_193 = x_190;
 }
-lean::cnstr_set(x_195, 0, x_194);
-lean::cnstr_set(x_195, 1, x_190);
-return x_195;
+lean::cnstr_set(x_193, 0, x_192);
+lean::cnstr_set(x_193, 1, x_188);
+return x_193;
 }
 case 8:
 {
-obj* x_196; obj* x_198; obj* x_200; obj* x_201; obj* x_202; obj* x_204; obj* x_206; obj* x_207; obj* x_208; 
-x_196 = lean::cnstr_get(x_0, 0);
-x_198 = lean::cnstr_get(x_0, 1);
+obj* x_194; obj* x_196; obj* x_198; obj* x_199; obj* x_200; obj* x_202; obj* x_204; obj* x_205; obj* x_206; 
+x_194 = lean::cnstr_get(x_0, 0);
+x_196 = lean::cnstr_get(x_0, 1);
 if (lean::is_exclusive(x_0)) {
- x_200 = x_0;
+ x_198 = x_0;
 } else {
+ lean::inc(x_194);
  lean::inc(x_196);
- lean::inc(x_198);
  lean::dec(x_0);
- x_200 = lean::box(0);
+ x_198 = lean::box(0);
 }
-x_201 = l_Lean_IR_NormalizeIds_normFnBody___main(x_198, x_1, x_2);
-x_202 = lean::cnstr_get(x_201, 0);
-x_204 = lean::cnstr_get(x_201, 1);
-if (lean::is_exclusive(x_201)) {
- x_206 = x_201;
+x_199 = l_Lean_IR_NormalizeIds_normFnBody___main(x_196, x_1, x_2);
+x_200 = lean::cnstr_get(x_199, 0);
+x_202 = lean::cnstr_get(x_199, 1);
+if (lean::is_exclusive(x_199)) {
+ x_204 = x_199;
 } else {
+ lean::inc(x_200);
  lean::inc(x_202);
- lean::inc(x_204);
- lean::dec(x_201);
- x_206 = lean::box(0);
+ lean::dec(x_199);
+ x_204 = lean::box(0);
 }
-if (lean::is_scalar(x_200)) {
- x_207 = lean::alloc_cnstr(8, 2, 0);
+if (lean::is_scalar(x_198)) {
+ x_205 = lean::alloc_cnstr(8, 2, 0);
 } else {
- x_207 = x_200;
+ x_205 = x_198;
 }
-lean::cnstr_set(x_207, 0, x_196);
-lean::cnstr_set(x_207, 1, x_202);
-if (lean::is_scalar(x_206)) {
- x_208 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_205, 0, x_194);
+lean::cnstr_set(x_205, 1, x_200);
+if (lean::is_scalar(x_204)) {
+ x_206 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_208 = x_206;
+ x_206 = x_204;
 }
-lean::cnstr_set(x_208, 0, x_207);
-lean::cnstr_set(x_208, 1, x_204);
-return x_208;
+lean::cnstr_set(x_206, 0, x_205);
+lean::cnstr_set(x_206, 1, x_202);
+return x_206;
 }
 case 9:
 {
-obj* x_209; obj* x_211; obj* x_213; obj* x_215; obj* x_217; obj* x_219; obj* x_220; obj* x_221; obj* x_223; obj* x_225; obj* x_226; obj* x_227; 
-x_209 = lean::cnstr_get(x_0, 0);
-x_211 = lean::cnstr_get(x_0, 1);
-x_213 = lean::cnstr_get(x_0, 2);
+obj* x_207; obj* x_209; obj* x_211; obj* x_213; obj* x_215; obj* x_217; obj* x_218; obj* x_219; obj* x_221; obj* x_223; obj* x_224; obj* x_225; 
+x_207 = lean::cnstr_get(x_0, 0);
+x_209 = lean::cnstr_get(x_0, 1);
+x_211 = lean::cnstr_get(x_0, 2);
 if (lean::is_exclusive(x_0)) {
- x_215 = x_0;
+ x_213 = x_0;
 } else {
+ lean::inc(x_207);
  lean::inc(x_209);
  lean::inc(x_211);
- lean::inc(x_213);
  lean::dec(x_0);
- x_215 = lean::box(0);
+ x_213 = lean::box(0);
 }
 lean::inc(x_1);
-x_217 = l_Lean_IR_NormalizeIds_normIndex(x_211, x_1);
-lean::dec(x_211);
-x_219 = lean::mk_nat_obj(0ul);
-x_220 = l_Array_hmmapAux___main___at_Lean_IR_NormalizeIds_normFnBody___main___spec__3(x_219, x_213, x_1, x_2);
-x_221 = lean::cnstr_get(x_220, 0);
-x_223 = lean::cnstr_get(x_220, 1);
-if (lean::is_exclusive(x_220)) {
- x_225 = x_220;
+x_215 = l_Lean_IR_NormalizeIds_normIndex(x_209, x_1);
+lean::dec(x_209);
+x_217 = lean::mk_nat_obj(0ul);
+x_218 = l_Array_hmmapAux___main___at_Lean_IR_NormalizeIds_normFnBody___main___spec__3(x_217, x_211, x_1, x_2);
+x_219 = lean::cnstr_get(x_218, 0);
+x_221 = lean::cnstr_get(x_218, 1);
+if (lean::is_exclusive(x_218)) {
+ x_223 = x_218;
 } else {
+ lean::inc(x_219);
  lean::inc(x_221);
- lean::inc(x_223);
- lean::dec(x_220);
- x_225 = lean::box(0);
+ lean::dec(x_218);
+ x_223 = lean::box(0);
 }
-if (lean::is_scalar(x_215)) {
- x_226 = lean::alloc_cnstr(9, 3, 0);
+if (lean::is_scalar(x_213)) {
+ x_224 = lean::alloc_cnstr(9, 3, 0);
 } else {
- x_226 = x_215;
+ x_224 = x_213;
 }
-lean::cnstr_set(x_226, 0, x_209);
-lean::cnstr_set(x_226, 1, x_217);
-lean::cnstr_set(x_226, 2, x_221);
-if (lean::is_scalar(x_225)) {
- x_227 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_224, 0, x_207);
+lean::cnstr_set(x_224, 1, x_215);
+lean::cnstr_set(x_224, 2, x_219);
+if (lean::is_scalar(x_223)) {
+ x_225 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_227 = x_225;
+ x_225 = x_223;
 }
-lean::cnstr_set(x_227, 0, x_226);
-lean::cnstr_set(x_227, 1, x_223);
-return x_227;
+lean::cnstr_set(x_225, 0, x_224);
+lean::cnstr_set(x_225, 1, x_221);
+return x_225;
 }
 case 10:
 {
-obj* x_228; obj* x_230; obj* x_231; obj* x_232; obj* x_233; 
-x_228 = lean::cnstr_get(x_0, 0);
+obj* x_226; obj* x_228; obj* x_229; obj* x_230; obj* x_231; 
+x_226 = lean::cnstr_get(x_0, 0);
 if (lean::is_exclusive(x_0)) {
- x_230 = x_0;
+ x_228 = x_0;
 } else {
- lean::inc(x_228);
+ lean::inc(x_226);
  lean::dec(x_0);
- x_230 = lean::box(0);
+ x_228 = lean::box(0);
 }
-x_231 = l_Lean_IR_NormalizeIds_normArg___main(x_228, x_1);
-if (lean::is_scalar(x_230)) {
- x_232 = lean::alloc_cnstr(10, 1, 0);
+x_229 = l_Lean_IR_NormalizeIds_normArg___main(x_226, x_1);
+if (lean::is_scalar(x_228)) {
+ x_230 = lean::alloc_cnstr(10, 1, 0);
 } else {
- x_232 = x_230;
+ x_230 = x_228;
 }
-lean::cnstr_set(x_232, 0, x_231);
-x_233 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_233, 0, x_232);
-lean::cnstr_set(x_233, 1, x_2);
-return x_233;
+lean::cnstr_set(x_230, 0, x_229);
+x_231 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_231, 0, x_230);
+lean::cnstr_set(x_231, 1, x_2);
+return x_231;
 }
 case 11:
 {
-obj* x_234; obj* x_236; obj* x_238; obj* x_240; obj* x_242; obj* x_243; obj* x_244; obj* x_245; 
-x_234 = lean::cnstr_get(x_0, 0);
-x_236 = lean::cnstr_get(x_0, 1);
+obj* x_232; obj* x_234; obj* x_236; obj* x_238; obj* x_240; obj* x_241; obj* x_242; obj* x_243; 
+x_232 = lean::cnstr_get(x_0, 0);
+x_234 = lean::cnstr_get(x_0, 1);
 if (lean::is_exclusive(x_0)) {
- x_238 = x_0;
+ x_236 = x_0;
 } else {
+ lean::inc(x_232);
  lean::inc(x_234);
- lean::inc(x_236);
  lean::dec(x_0);
- x_238 = lean::box(0);
+ x_236 = lean::box(0);
 }
 lean::inc(x_1);
-x_240 = l_Lean_IR_NormalizeIds_normIndex(x_234, x_1);
-lean::dec(x_234);
-x_242 = lean::mk_nat_obj(0ul);
-x_243 = l_Array_hmmapAux___main___at_Lean_IR_NormalizeIds_normArgs___spec__1(x_1, x_242, x_236);
-if (lean::is_scalar(x_238)) {
- x_244 = lean::alloc_cnstr(11, 2, 0);
+x_238 = l_Lean_IR_NormalizeIds_normIndex(x_232, x_1);
+lean::dec(x_232);
+x_240 = lean::mk_nat_obj(0ul);
+x_241 = l_Array_hmmapAux___main___at_Lean_IR_NormalizeIds_normArgs___spec__1(x_1, x_240, x_234);
+if (lean::is_scalar(x_236)) {
+ x_242 = lean::alloc_cnstr(11, 2, 0);
 } else {
- x_244 = x_238;
+ x_242 = x_236;
 }
-lean::cnstr_set(x_244, 0, x_240);
-lean::cnstr_set(x_244, 1, x_243);
-x_245 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_245, 0, x_244);
-lean::cnstr_set(x_245, 1, x_2);
-return x_245;
+lean::cnstr_set(x_242, 0, x_238);
+lean::cnstr_set(x_242, 1, x_241);
+x_243 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_243, 0, x_242);
+lean::cnstr_set(x_243, 1, x_2);
+return x_243;
 }
 default:
 {
-obj* x_247; 
+obj* x_245; 
 lean::dec(x_1);
-x_247 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_247, 0, x_0);
-lean::cnstr_set(x_247, 1, x_2);
-return x_247;
+x_245 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_245, 0, x_0);
+lean::cnstr_set(x_245, 1, x_2);
+return x_245;
 }
 }
 }

src/stage0/init/lean/compiler/ir/pushproj.cpp

@@ -14,20 +14,21 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-label"
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(obj*, obj*, obj*, obj*, obj*, obj*);
-obj* l_Lean_IR_FnBody_collectFreeVars(obj*, obj*);
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(obj*, obj*, obj*, obj*, obj*);
 extern obj* l_Array_empty___closed__1;
 namespace lean {
 obj* nat_sub(obj*, obj*);
 }
 extern obj* l_Lean_IR_vsetInh;
 obj* l_Lean_IR_Decl_pushProj(obj*);
-obj* l_Lean_IR_pushProjs___main___closed__1;
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4___boxed(obj*, obj*, obj*, obj*, obj*);
+uint8 l_Array_anyMAux___main___at_Lean_IR_pushProjs___main___spec__2(obj*, obj*, obj*);
+obj* l_Lean_IR_FnBody_freeIndices(obj*);
+obj* l_Array_anyMAux___main___at_Lean_IR_pushProjs___main___spec__2___boxed(obj*, obj*, obj*);
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_Decl_pushProj___main(obj*);
-obj* l_Lean_IR_FnBody_freeVars(obj*);
+obj* l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_14__collectIndex___spec__1(obj*, obj*);
+obj* l_RBNode_insert___at___private_init_lean_compiler_ir_freevars_14__collectIndex___spec__2(obj*, obj*, obj*);
 obj* l_Lean_IR_reshape(obj*, obj*);
-uint8 l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_pushProj(obj*);
 namespace lean {
 uint8 nat_dec_lt(obj*, obj*);
@@ -39,23 +40,20 @@ obj* nat_add(obj*, obj*);
 uint8 l_Array_isEmpty___rarg(obj*);
 obj* l_Lean_IR_pushProjs(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_pushProj___main(obj*);
+obj* l_Lean_IR_FnBody_collectFreeIndices(obj*, obj*);
 obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_pushProj___main___spec__3(obj*, obj*);
-obj* l_Nat_decLt___boxed(obj*, obj*);
 obj* l_Array_reverseAux___main___rarg(obj*, obj*);
 obj* l_Lean_IR_AltCore_body___main(obj*);
 obj* l_Lean_IR_pushProjs___main(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_back___at_Lean_IR_pushProjs___main___spec__1(obj*);
-obj* l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(obj*, obj*);
 obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_pushProj___main___spec__1(obj*, obj*);
-obj* l_RBNode_insert___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__2(obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_setBody___main(obj*, obj*);
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(obj*, obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Lean_IR_FnBody_pushProj___main___spec__2(obj*, obj*, obj*, obj*);
-obj* l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2___boxed(obj*, obj*, obj*, obj*);
 obj* l_Array_back___at_Lean_IR_pushProjs___main___spec__1___boxed(obj*);
 obj* l_Array_miterateAux___main___at_Lean_IR_FnBody_pushProj___main___spec__2___boxed(obj*, obj*, obj*, obj*);
 obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1;
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at_Array_append___spec__1___rarg(obj*, obj*, obj*, obj*);
 extern obj* l_Lean_IR_Inhabited;
 obj* l_Array_back___at_Lean_IR_pushProjs___main___spec__1(obj* x_0) {
@@ -72,40 +70,40 @@ lean::dec(x_3);
 return x_6;
 }
 }
-uint8 l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+uint8 l_Array_anyMAux___main___at_Lean_IR_pushProjs___main___spec__2(obj* x_0, obj* x_1, obj* x_2) {
 _start:
 {
-obj* x_4; uint8 x_5; 
-x_4 = lean::array_get_size(x_2);
-x_5 = lean::nat_dec_lt(x_3, x_4);
-lean::dec(x_4);
-if (x_5 == 0)
-{
-uint8 x_8; 
+obj* x_3; uint8 x_4; 
+x_3 = lean::array_get_size(x_1);
+x_4 = lean::nat_dec_lt(x_2, x_3);
 lean::dec(x_3);
-x_8 = 0;
-return x_8;
+if (x_4 == 0)
+{
+uint8 x_7; 
+lean::dec(x_2);
+x_7 = 0;
+return x_7;
 }
 else
 {
-obj* x_9; obj* x_10; 
-x_9 = lean::array_fget(x_2, x_3);
-x_10 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_9, x_1);
-if (lean::obj_tag(x_10) == 0)
+obj* x_8; obj* x_9; 
+x_8 = lean::array_fget(x_1, x_2);
+x_9 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_14__collectIndex___spec__1(x_8, x_0);
+if (lean::obj_tag(x_9) == 0)
 {
-uint8 x_12; 
-lean::dec(x_3);
-x_12 = 1;
-return x_12;
+uint8 x_11; 
+lean::dec(x_2);
+x_11 = 1;
+return x_11;
 }
 else
 {
-obj* x_14; obj* x_15; 
-lean::dec(x_10);
-x_14 = lean::mk_nat_obj(1ul);
-x_15 = lean::nat_add(x_3, x_14);
-lean::dec(x_3);
-x_3 = x_15;
+obj* x_13; obj* x_14; 
+lean::dec(x_9);
+x_13 = lean::mk_nat_obj(1ul);
+x_14 = lean::nat_add(x_2, x_13);
+lean::dec(x_2);
+x_2 = x_14;
 goto _start;
 }
 }
@@ -121,134 +119,7 @@ lean::cnstr_set(x_1, 0, x_0);
 return x_1;
 }
 }
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
-_start:
-{
-obj* x_6; uint8 x_7; 
-x_6 = lean::array_get_size(x_5);
-x_7 = lean::nat_dec_lt(x_4, x_6);
-lean::dec(x_6);
-if (x_7 == 0)
-{
-lean::dec(x_4);
-lean::dec(x_1);
-return x_5;
-}
-else
-{
-obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; 
-x_11 = lean::array_fget(x_5, x_4);
-x_12 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1;
-x_13 = lean::array_fset(x_5, x_4, x_12);
-x_14 = lean::mk_nat_obj(1ul);
-x_15 = lean::nat_add(x_4, x_14);
-if (lean::obj_tag(x_11) == 0)
-{
-obj* x_16; obj* x_18; obj* x_20; obj* x_21; obj* x_22; obj* x_23; 
-x_16 = lean::cnstr_get(x_11, 0);
-x_18 = lean::cnstr_get(x_11, 1);
-if (lean::is_exclusive(x_11)) {
- lean::cnstr_set(x_11, 0, lean::box(0));
- lean::cnstr_set(x_11, 1, lean::box(0));
- x_20 = x_11;
-} else {
- lean::inc(x_16);
- lean::inc(x_18);
- lean::dec(x_11);
- x_20 = lean::box(0);
-}
-x_21 = l_Lean_IR_vsetInh;
-x_22 = lean::array_get(x_21, x_0, x_4);
-x_23 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_22, x_3);
-if (lean::obj_tag(x_23) == 0)
-{
-obj* x_24; obj* x_25; 
-if (lean::is_scalar(x_20)) {
- x_24 = lean::alloc_cnstr(0, 2, 0);
-} else {
- x_24 = x_20;
-}
-lean::cnstr_set(x_24, 0, x_16);
-lean::cnstr_set(x_24, 1, x_18);
-x_25 = lean::array_fset(x_13, x_4, x_24);
-lean::dec(x_4);
-x_4 = x_15;
-x_5 = x_25;
-goto _start;
-}
-else
-{
-obj* x_30; obj* x_31; obj* x_32; 
-lean::dec(x_23);
-lean::inc(x_1);
-x_30 = l_Lean_IR_FnBody_setBody___main(x_1, x_18);
-if (lean::is_scalar(x_20)) {
- x_31 = lean::alloc_cnstr(0, 2, 0);
-} else {
- x_31 = x_20;
-}
-lean::cnstr_set(x_31, 0, x_16);
-lean::cnstr_set(x_31, 1, x_30);
-x_32 = lean::array_fset(x_13, x_4, x_31);
-lean::dec(x_4);
-x_4 = x_15;
-x_5 = x_32;
-goto _start;
-}
-}
-else
-{
-obj* x_35; obj* x_37; obj* x_38; obj* x_39; obj* x_40; 
-x_35 = lean::cnstr_get(x_11, 0);
-if (lean::is_exclusive(x_11)) {
- lean::cnstr_set(x_11, 0, lean::box(0));
- x_37 = x_11;
-} else {
- lean::inc(x_35);
- lean::dec(x_11);
- x_37 = lean::box(0);
-}
-x_38 = l_Lean_IR_vsetInh;
-x_39 = lean::array_get(x_38, x_0, x_4);
-x_40 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_39, x_3);
-if (lean::obj_tag(x_40) == 0)
-{
-obj* x_41; obj* x_42; 
-if (lean::is_scalar(x_37)) {
- x_41 = lean::alloc_cnstr(1, 1, 0);
-} else {
- x_41 = x_37;
-}
-lean::cnstr_set(x_41, 0, x_35);
-x_42 = lean::array_fset(x_13, x_4, x_41);
-lean::dec(x_4);
-x_4 = x_15;
-x_5 = x_42;
-goto _start;
-}
-else
-{
-obj* x_47; obj* x_48; obj* x_49; 
-lean::dec(x_40);
-lean::inc(x_1);
-x_47 = l_Lean_IR_FnBody_setBody___main(x_1, x_35);
-if (lean::is_scalar(x_37)) {
- x_48 = lean::alloc_cnstr(1, 1, 0);
-} else {
- x_48 = x_37;
-}
-lean::cnstr_set(x_48, 0, x_47);
-x_49 = lean::array_fset(x_13, x_4, x_48);
-lean::dec(x_4);
-x_4 = x_15;
-x_5 = x_49;
-goto _start;
-}
-}
-}
-}
-}
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
 obj* x_5; uint8 x_6; 
@@ -257,50 +128,169 @@ x_6 = lean::nat_dec_lt(x_3, x_5);
 lean::dec(x_5);
 if (x_6 == 0)
 {
+lean::dec(x_1);
 lean::dec(x_3);
-lean::dec(x_0);
 return x_4;
 }
 else
 {
-obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_16; 
+obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; 
 x_10 = lean::array_fget(x_4, x_3);
-x_11 = lean::box(0);
+x_11 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1;
 x_12 = lean::array_fset(x_4, x_3, x_11);
 x_13 = lean::mk_nat_obj(1ul);
 x_14 = lean::nat_add(x_3, x_13);
-lean::inc(x_10);
-x_16 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_10, x_2);
-if (lean::obj_tag(x_16) == 0)
+if (lean::obj_tag(x_10) == 0)
 {
-obj* x_17; 
-x_17 = lean::array_fset(x_12, x_3, x_10);
+obj* x_15; obj* x_17; obj* x_19; obj* x_20; obj* x_21; obj* x_22; 
+x_15 = lean::cnstr_get(x_10, 0);
+x_17 = lean::cnstr_get(x_10, 1);
+if (lean::is_exclusive(x_10)) {
+ lean::cnstr_set(x_10, 0, lean::box(0));
+ lean::cnstr_set(x_10, 1, lean::box(0));
+ x_19 = x_10;
+} else {
+ lean::inc(x_15);
+ lean::inc(x_17);
+ lean::dec(x_10);
+ x_19 = lean::box(0);
+}
+x_20 = l_Lean_IR_vsetInh;
+x_21 = lean::array_get(x_20, x_0, x_3);
+x_22 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_14__collectIndex___spec__1(x_21, x_2);
+if (lean::obj_tag(x_22) == 0)
+{
+obj* x_23; obj* x_24; 
+if (lean::is_scalar(x_19)) {
+ x_23 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_23 = x_19;
+}
+lean::cnstr_set(x_23, 0, x_15);
+lean::cnstr_set(x_23, 1, x_17);
+x_24 = lean::array_fset(x_12, x_3, x_23);
 lean::dec(x_3);
 x_3 = x_14;
-x_4 = x_17;
+x_4 = x_24;
 goto _start;
 }
 else
 {
-obj* x_22; obj* x_23; 
-lean::dec(x_16);
-lean::inc(x_0);
-x_22 = l_Lean_IR_FnBody_collectFreeVars(x_0, x_10);
-x_23 = lean::array_fset(x_12, x_3, x_22);
+obj* x_29; obj* x_30; obj* x_31; 
+lean::dec(x_22);
+lean::inc(x_1);
+x_29 = l_Lean_IR_FnBody_setBody___main(x_1, x_17);
+if (lean::is_scalar(x_19)) {
+ x_30 = lean::alloc_cnstr(0, 2, 0);
+} else {
+ x_30 = x_19;
+}
+lean::cnstr_set(x_30, 0, x_15);
+lean::cnstr_set(x_30, 1, x_29);
+x_31 = lean::array_fset(x_12, x_3, x_30);
 lean::dec(x_3);
 x_3 = x_14;
-x_4 = x_23;
+x_4 = x_31;
+goto _start;
+}
+}
+else
+{
+obj* x_34; obj* x_36; obj* x_37; obj* x_38; obj* x_39; 
+x_34 = lean::cnstr_get(x_10, 0);
+if (lean::is_exclusive(x_10)) {
+ lean::cnstr_set(x_10, 0, lean::box(0));
+ x_36 = x_10;
+} else {
+ lean::inc(x_34);
+ lean::dec(x_10);
+ x_36 = lean::box(0);
+}
+x_37 = l_Lean_IR_vsetInh;
+x_38 = lean::array_get(x_37, x_0, x_3);
+x_39 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_14__collectIndex___spec__1(x_38, x_2);
+if (lean::obj_tag(x_39) == 0)
+{
+obj* x_40; obj* x_41; 
+if (lean::is_scalar(x_36)) {
+ x_40 = lean::alloc_cnstr(1, 1, 0);
+} else {
+ x_40 = x_36;
+}
+lean::cnstr_set(x_40, 0, x_34);
+x_41 = lean::array_fset(x_12, x_3, x_40);
+lean::dec(x_3);
+x_3 = x_14;
+x_4 = x_41;
+goto _start;
+}
+else
+{
+obj* x_46; obj* x_47; obj* x_48; 
+lean::dec(x_39);
+lean::inc(x_1);
+x_46 = l_Lean_IR_FnBody_setBody___main(x_1, x_34);
+if (lean::is_scalar(x_36)) {
+ x_47 = lean::alloc_cnstr(1, 1, 0);
+} else {
+ x_47 = x_36;
+}
+lean::cnstr_set(x_47, 0, x_46);
+x_48 = lean::array_fset(x_12, x_3, x_47);
+lean::dec(x_3);
+x_3 = x_14;
+x_4 = x_48;
 goto _start;
 }
 }
 }
 }
-obj* _init_l_Lean_IR_pushProjs___main___closed__1() {
+}
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
-obj* x_0; 
-x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Nat_decLt___boxed), 2, 0);
-return x_0;
+obj* x_4; uint8 x_5; 
+x_4 = lean::array_get_size(x_3);
+x_5 = lean::nat_dec_lt(x_2, x_4);
+lean::dec(x_4);
+if (x_5 == 0)
+{
+lean::dec(x_0);
+lean::dec(x_2);
+return x_3;
+}
+else
+{
+obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_15; 
+x_9 = lean::array_fget(x_3, x_2);
+x_10 = lean::box(0);
+x_11 = lean::array_fset(x_3, x_2, x_10);
+x_12 = lean::mk_nat_obj(1ul);
+x_13 = lean::nat_add(x_2, x_12);
+lean::inc(x_9);
+x_15 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_14__collectIndex___spec__1(x_9, x_1);
+if (lean::obj_tag(x_15) == 0)
+{
+obj* x_16; 
+x_16 = lean::array_fset(x_11, x_2, x_9);
+lean::dec(x_2);
+x_2 = x_13;
+x_3 = x_16;
+goto _start;
+}
+else
+{
+obj* x_21; obj* x_22; 
+lean::dec(x_15);
+lean::inc(x_0);
+x_21 = l_Lean_IR_FnBody_collectFreeIndices(x_0, x_9);
+x_22 = lean::array_fset(x_11, x_2, x_21);
+lean::dec(x_2);
+x_2 = x_13;
+x_3 = x_22;
+goto _start;
+}
+}
 }
 }
 obj* l_Lean_IR_pushProjs___main(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
@@ -327,121 +317,120 @@ lean::dec(x_12);
 x_15 = lean::cnstr_get(x_6, 0);
 lean::inc(x_15);
 lean::inc(x_4);
-x_18 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__1(x_4, x_15);
+x_18 = l_RBNode_findCore___main___at___private_init_lean_compiler_ir_freevars_14__collectIndex___spec__1(x_4, x_15);
 if (lean::obj_tag(x_18) == 0)
 {
-obj* x_19; obj* x_20; uint8 x_21; 
-x_19 = l_Lean_IR_pushProjs___main___closed__1;
-x_20 = lean::mk_nat_obj(0ul);
-x_21 = l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2(x_19, x_15, x_2, x_20);
-if (x_21 == 0)
+obj* x_19; uint8 x_20; 
+x_19 = lean::mk_nat_obj(0ul);
+x_20 = l_Array_anyMAux___main___at_Lean_IR_pushProjs___main___spec__2(x_15, x_2, x_19);
+if (x_20 == 0)
 {
-obj* x_23; 
+obj* x_22; 
 lean::dec(x_15);
-x_23 = lean::box(0);
-x_10 = x_23;
+x_22 = lean::box(0);
+x_10 = x_22;
 goto lbl_11;
 }
 else
 {
-obj* x_25; obj* x_26; 
+obj* x_24; obj* x_25; 
 lean::inc(x_6);
-x_25 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(x_2, x_6, x_19, x_15, x_20, x_1);
-x_26 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(x_6, x_19, x_15, x_20, x_2);
+x_24 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(x_2, x_6, x_15, x_19, x_1);
+x_25 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(x_6, x_15, x_19, x_2);
 lean::dec(x_15);
 x_0 = x_7;
-x_1 = x_25;
-x_2 = x_26;
+x_1 = x_24;
+x_2 = x_25;
 goto _start;
 }
 }
 else
 {
-obj* x_31; 
+obj* x_30; 
 lean::dec(x_15);
 lean::dec(x_18);
-x_31 = lean::box(0);
-x_10 = x_31;
+x_30 = lean::box(0);
+x_10 = x_30;
 goto lbl_11;
 }
 }
 case 4:
 {
-obj* x_33; 
+obj* x_32; 
 lean::dec(x_12);
-x_33 = lean::box(0);
-x_10 = x_33;
+x_32 = lean::box(0);
+x_10 = x_32;
 goto lbl_11;
 }
 case 5:
 {
-obj* x_35; 
+obj* x_34; 
 lean::dec(x_12);
-x_35 = lean::box(0);
-x_10 = x_35;
+x_34 = lean::box(0);
+x_10 = x_34;
 goto lbl_11;
 }
 default:
 {
-obj* x_39; 
+obj* x_38; 
 lean::dec(x_12);
 lean::dec(x_4);
 lean::dec(x_2);
-x_39 = lean::box(0);
-x_8 = x_39;
+x_38 = lean::box(0);
+x_8 = x_38;
 goto lbl_9;
 }
 }
 }
 default:
 {
-obj* x_42; 
+obj* x_41; 
 lean::dec(x_4);
 lean::dec(x_2);
-x_42 = lean::box(0);
-x_8 = x_42;
+x_41 = lean::box(0);
+x_8 = x_41;
 goto lbl_9;
 }
 }
 lbl_9:
 {
-obj* x_44; obj* x_45; obj* x_46; obj* x_47; obj* x_49; 
+obj* x_43; obj* x_44; obj* x_45; obj* x_46; obj* x_48; 
 lean::dec(x_8);
-x_44 = lean::array_push(x_7, x_6);
-x_45 = lean::mk_nat_obj(0ul);
-x_46 = l_Array_reverseAux___main___rarg(x_3, x_45);
-x_47 = l_Array_miterateAux___main___at_Array_append___spec__1___rarg(x_46, x_46, x_45, x_44);
-lean::dec(x_46);
-x_49 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_49, 0, x_47);
-lean::cnstr_set(x_49, 1, x_1);
-return x_49;
+x_43 = lean::array_push(x_7, x_6);
+x_44 = lean::mk_nat_obj(0ul);
+x_45 = l_Array_reverseAux___main___rarg(x_3, x_44);
+x_46 = l_Array_miterateAux___main___at_Array_append___spec__1___rarg(x_45, x_45, x_44, x_43);
+lean::dec(x_45);
+x_48 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_48, 0, x_46);
+lean::cnstr_set(x_48, 1, x_1);
+return x_48;
 }
 lbl_11:
 {
-obj* x_52; obj* x_53; 
+obj* x_51; obj* x_52; 
 lean::dec(x_10);
 lean::inc(x_6);
-x_52 = lean::array_push(x_3, x_6);
-x_53 = l_Lean_IR_FnBody_collectFreeVars(x_6, x_4);
+x_51 = lean::array_push(x_3, x_6);
+x_52 = l_Lean_IR_FnBody_collectFreeIndices(x_6, x_4);
 x_0 = x_7;
-x_3 = x_52;
-x_4 = x_53;
+x_3 = x_51;
+x_4 = x_52;
 goto _start;
 }
 }
 else
 {
-obj* x_58; obj* x_59; obj* x_60; 
+obj* x_57; obj* x_58; obj* x_59; 
 lean::dec(x_4);
 lean::dec(x_0);
 lean::dec(x_2);
-x_58 = lean::mk_nat_obj(0ul);
-x_59 = l_Array_reverseAux___main___rarg(x_3, x_58);
-x_60 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_60, 0, x_59);
-lean::cnstr_set(x_60, 1, x_1);
-return x_60;
+x_57 = lean::mk_nat_obj(0ul);
+x_58 = l_Array_reverseAux___main___rarg(x_3, x_57);
+x_59 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_59, 0, x_58);
+lean::cnstr_set(x_59, 1, x_1);
+return x_59;
 }
 }
 }
@@ -454,39 +443,36 @@ lean::dec(x_0);
 return x_1;
 }
 }
-obj* l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+obj* l_Array_anyMAux___main___at_Lean_IR_pushProjs___main___spec__2___boxed(obj* x_0, obj* x_1, obj* x_2) {
 _start:
 {
-uint8 x_4; obj* x_5; 
-x_4 = l_Array_anyAux___main___at_Lean_IR_pushProjs___main___spec__2(x_0, x_1, x_2, x_3);
-x_5 = lean::box(x_4);
+uint8 x_3; obj* x_4; 
+x_3 = l_Array_anyMAux___main___at_Lean_IR_pushProjs___main___spec__2(x_0, x_1, x_2);
+x_4 = lean::box(x_3);
 lean::dec(x_0);
 lean::dec(x_1);
-lean::dec(x_2);
-return x_5;
+return x_4;
 }
 }
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
-_start:
-{
-obj* x_6; 
-x_6 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(x_0, x_1, x_2, x_3, x_4, x_5);
-lean::dec(x_0);
-lean::dec(x_2);
-lean::dec(x_3);
-return x_6;
-}
-}
-obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
 obj* x_5; 
-x_5 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(x_0, x_1, x_2, x_3, x_4);
-lean::dec(x_1);
+x_5 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3(x_0, x_1, x_2, x_3, x_4);
+lean::dec(x_0);
 lean::dec(x_2);
 return x_5;
 }
 }
+obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+_start:
+{
+obj* x_4; 
+x_4 = l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4(x_0, x_1, x_2, x_3);
+lean::dec(x_1);
+return x_4;
+}
+}
 obj* l_Lean_IR_pushProjs(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
@@ -518,47 +504,44 @@ x_10 = lean::nat_add(x_0, x_9);
 switch (lean::obj_tag(x_6)) {
 case 1:
 {
-obj* x_11; obj* x_13; uint8 x_15; obj* x_16; obj* x_18; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; 
+obj* x_11; obj* x_13; obj* x_15; obj* x_17; obj* x_19; obj* x_20; obj* x_21; obj* x_22; 
 x_11 = lean::cnstr_get(x_6, 0);
 x_13 = lean::cnstr_get(x_6, 1);
-x_15 = lean::cnstr_get_scalar<uint8>(x_6, sizeof(void*)*4);
-x_16 = lean::cnstr_get(x_6, 2);
-x_18 = lean::cnstr_get(x_6, 3);
+x_15 = lean::cnstr_get(x_6, 2);
+x_17 = lean::cnstr_get(x_6, 3);
 if (lean::is_exclusive(x_6)) {
- x_20 = x_6;
+ x_19 = x_6;
 } else {
  lean::inc(x_11);
  lean::inc(x_13);
- lean::inc(x_16);
- lean::inc(x_18);
+ lean::inc(x_15);
+ lean::inc(x_17);
  lean::dec(x_6);
- x_20 = lean::box(0);
+ x_19 = lean::box(0);
 }
-x_21 = l_Lean_IR_FnBody_pushProj___main(x_16);
-if (lean::is_scalar(x_20)) {
- x_22 = lean::alloc_cnstr(1, 4, 1);
+x_20 = l_Lean_IR_FnBody_pushProj___main(x_15);
+if (lean::is_scalar(x_19)) {
+ x_21 = lean::alloc_cnstr(1, 4, 0);
 } else {
- x_22 = x_20;
+ x_21 = x_19;
 }
-lean::cnstr_set(x_22, 0, x_11);
-lean::cnstr_set(x_22, 1, x_13);
-lean::cnstr_set(x_22, 2, x_21);
-lean::cnstr_set(x_22, 3, x_18);
-lean::cnstr_set_scalar(x_22, sizeof(void*)*4, x_15);
-x_23 = x_22;
-x_24 = lean::array_fset(x_8, x_0, x_23);
+lean::cnstr_set(x_21, 0, x_11);
+lean::cnstr_set(x_21, 1, x_13);
+lean::cnstr_set(x_21, 2, x_20);
+lean::cnstr_set(x_21, 3, x_17);
+x_22 = lean::array_fset(x_8, x_0, x_21);
 lean::dec(x_0);
 x_0 = x_10;
-x_1 = x_24;
+x_1 = x_22;
 goto _start;
 }
 default:
 {
-obj* x_27; 
-x_27 = lean::array_fset(x_8, x_0, x_6);
+obj* x_25; 
+x_25 = lean::array_fset(x_8, x_0, x_6);
 lean::dec(x_0);
 x_0 = x_10;
-x_1 = x_27;
+x_1 = x_25;
 goto _start;
 }
 }
@@ -583,7 +566,7 @@ obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_13; obj* x_14;
 x_8 = lean::array_fget(x_1, x_2);
 x_9 = l_Lean_IR_AltCore_body___main(x_8);
 lean::dec(x_8);
-x_11 = l_Lean_IR_FnBody_freeVars(x_9);
+x_11 = l_Lean_IR_FnBody_freeIndices(x_9);
 x_12 = lean::array_push(x_3, x_11);
 x_13 = lean::mk_nat_obj(1ul);
 x_14 = lean::nat_add(x_2, x_13);
@@ -703,7 +686,7 @@ x_19 = l_Array_miterateAux___main___at_Lean_IR_FnBody_pushProj___main___spec__2(
 x_20 = lean::box(0);
 x_21 = lean::box(0);
 lean::inc(x_11);
-x_23 = l_RBNode_insert___at___private_init_lean_compiler_ir_freevars_2__collectIndex___spec__2(x_20, x_11, x_21);
+x_23 = l_RBNode_insert___at___private_init_lean_compiler_ir_freevars_14__collectIndex___spec__2(x_20, x_11, x_21);
 x_24 = l_Array_empty___closed__1;
 x_25 = l_Lean_IR_pushProjs___main(x_8, x_13, x_19, x_24, x_23);
 x_26 = lean::cnstr_get(x_25, 0);
@@ -809,7 +792,5 @@ w = initialize_init_lean_compiler_ir_freevars(w);
 if (io_result_is_error(w)) return w;
  l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1 = _init_l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1();
 lean::mark_persistent(l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__3___closed__1);
- l_Lean_IR_pushProjs___main___closed__1 = _init_l_Lean_IR_pushProjs___main___closed__1();
-lean::mark_persistent(l_Lean_IR_pushProjs___main___closed__1);
 return w;
 }

src/stage0/init/lean/compiler/ir/simpcase.cpp

@@ -14,6 +14,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-label"
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
+uint8 l_Array_anyMAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1(obj*, obj*);
 obj* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_simpcase_1__maxOccs___spec__1___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_simpcase_1__maxOccs___spec__1(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_FnBody_simpCase(obj*);
@@ -24,7 +25,6 @@ obj* l___private_init_lean_compiler_ir_simpcase_1__maxOccs(obj*);
 obj* l___private_init_lean_compiler_ir_simpcase_2__addDefault(obj*);
 obj* l_Lean_IR_reshape(obj*, obj*);
 obj* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_simpcase_1__maxOccs___spec__2(obj*, obj*, obj*, obj*);
-obj* l_Array_anyAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1___boxed(obj*, obj*);
 namespace lean {
 uint8 nat_dec_lt(obj*, obj*);
 }
@@ -42,7 +42,6 @@ obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2(obj*,
 obj* l_Array_shrink___main___rarg(obj*, obj*);
 obj* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_simpcase_1__maxOccs___spec__2___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_AltCore_body___main(obj*);
-uint8 l_Array_anyAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1(obj*, obj*);
 uint8 l_Lean_IR_FnBody_beq(obj*, obj*);
 obj* l___private_init_lean_compiler_ir_simpcase_3__mkSimpCase(obj*, obj*, obj*);
 obj* l_Array_filterAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__2(obj*, obj*, obj*, obj*);
@@ -52,6 +51,7 @@ uint8 nat_dec_le(obj*, obj*);
 obj* l___private_init_lean_compiler_ir_simpcase_1__maxOccs___boxed(obj*);
 obj* l_Lean_IR_Decl_simpCase___main(obj*);
 obj* l_Array_filterAux___main___at___private_init_lean_compiler_ir_simpcase_3__mkSimpCase___spec__1(obj*, obj*, obj*);
+obj* l_Array_anyMAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1___boxed(obj*, obj*);
 obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__1(obj*, obj*);
 obj* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_simpcase_1__maxOccs___spec__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
@@ -185,7 +185,7 @@ lean::dec(x_0);
 return x_1;
 }
 }
-uint8 l_Array_anyAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1(obj* x_0, obj* x_1) {
+uint8 l_Array_anyMAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1(obj* x_0, obj* x_1) {
 _start:
 {
 obj* x_2; uint8 x_3; 
@@ -216,10 +216,8 @@ goto _start;
 }
 else
 {
-uint8 x_15; 
 lean::dec(x_1);
-x_15 = 1;
-return x_15;
+return x_8;
 }
 }
 }
@@ -302,7 +300,7 @@ if (x_3 == 0)
 {
 obj* x_5; uint8 x_6; 
 x_5 = lean::mk_nat_obj(0ul);
-x_6 = l_Array_anyAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1(x_0, x_5);
+x_6 = l_Array_anyMAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1(x_0, x_5);
 if (x_6 == 0)
 {
 obj* x_7; obj* x_8; obj* x_10; uint8 x_13; 
@@ -342,11 +340,11 @@ return x_0;
 }
 }
 }
-obj* l_Array_anyAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1___boxed(obj* x_0, obj* x_1) {
+obj* l_Array_anyMAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1___boxed(obj* x_0, obj* x_1) {
 _start:
 {
 uint8 x_2; obj* x_3; 
-x_2 = l_Array_anyAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1(x_0, x_1);
+x_2 = l_Array_anyMAux___main___at___private_init_lean_compiler_ir_simpcase_2__addDefault___spec__1(x_0, x_1);
 x_3 = lean::box(x_2);
 lean::dec(x_0);
 return x_3;
@@ -499,47 +497,44 @@ x_10 = lean::nat_add(x_0, x_9);
 switch (lean::obj_tag(x_6)) {
 case 1:
 {
-obj* x_11; obj* x_13; uint8 x_15; obj* x_16; obj* x_18; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; 
+obj* x_11; obj* x_13; obj* x_15; obj* x_17; obj* x_19; obj* x_20; obj* x_21; obj* x_22; 
 x_11 = lean::cnstr_get(x_6, 0);
 x_13 = lean::cnstr_get(x_6, 1);
-x_15 = lean::cnstr_get_scalar<uint8>(x_6, sizeof(void*)*4);
-x_16 = lean::cnstr_get(x_6, 2);
-x_18 = lean::cnstr_get(x_6, 3);
+x_15 = lean::cnstr_get(x_6, 2);
+x_17 = lean::cnstr_get(x_6, 3);
 if (lean::is_exclusive(x_6)) {
- x_20 = x_6;
+ x_19 = x_6;
 } else {
  lean::inc(x_11);
  lean::inc(x_13);
- lean::inc(x_16);
- lean::inc(x_18);
+ lean::inc(x_15);
+ lean::inc(x_17);
  lean::dec(x_6);
- x_20 = lean::box(0);
+ x_19 = lean::box(0);
 }
-x_21 = l_Lean_IR_FnBody_simpCase___main(x_16);
-if (lean::is_scalar(x_20)) {
- x_22 = lean::alloc_cnstr(1, 4, 1);
+x_20 = l_Lean_IR_FnBody_simpCase___main(x_15);
+if (lean::is_scalar(x_19)) {
+ x_21 = lean::alloc_cnstr(1, 4, 0);
 } else {
- x_22 = x_20;
+ x_21 = x_19;
 }
-lean::cnstr_set(x_22, 0, x_11);
-lean::cnstr_set(x_22, 1, x_13);
-lean::cnstr_set(x_22, 2, x_21);
-lean::cnstr_set(x_22, 3, x_18);
-lean::cnstr_set_scalar(x_22, sizeof(void*)*4, x_15);
-x_23 = x_22;
-x_24 = lean::array_fset(x_8, x_0, x_23);
+lean::cnstr_set(x_21, 0, x_11);
+lean::cnstr_set(x_21, 1, x_13);
+lean::cnstr_set(x_21, 2, x_20);
+lean::cnstr_set(x_21, 3, x_17);
+x_22 = lean::array_fset(x_8, x_0, x_21);
 lean::dec(x_0);
 x_0 = x_10;
-x_1 = x_24;
+x_1 = x_22;
 goto _start;
 }
 default:
 {
-obj* x_27; 
-x_27 = lean::array_fset(x_8, x_0, x_6);
+obj* x_25; 
+x_25 = lean::array_fset(x_8, x_0, x_6);
 lean::dec(x_0);
 x_0 = x_10;
-x_1 = x_27;
+x_1 = x_25;
 goto _start;
 }
 }