chore: update stage0

This makes it easier to distinguish tests that are actually
failing while we work on the new codegen.

src/Lean/Compiler/LCNF/ExtractClosed.lean

@@ -111,7 +111,7 @@ partial def visitCode (code : Code) : M Code := do
         eraseCode closedCode
         pure closedTermName
       else
-        let name := (← read).baseName ++ (`_closedTerm).appendIndexAfter (← get).decls.size
+        let name := (← read).baseName ++ (`_closed).appendIndexAfter (← get).decls.size
         cacheClosedTermName env closedExpr name |> setEnv
         let decl := { name, levelParams := [], type := decl.type, params := #[],
                       value := .code closedCode, inlineAttr? := some .noinline }

src/Lean/CoreM.lean

@@ -667,9 +667,9 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla
     | _ => pure ()
 
 register_builtin_option compiler.enableNew : Bool := {
-  defValue := false
+  defValue := true
   group    := "compiler"
-  descr    := "(compiler) enable the new code generator, this should have no significant effect on your code but it does help to test the new code generator; unset to only use the old code generator instead"
+  descr    := "(compiler) enable the new code generator, unset to use the old code generator instead"
 }
 
 /--

tests/lean/4089.lean.expected.out

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

tests/lean/4240.lean.expected.out

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

tests/lean/496.lean.expected.out

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

tests/lean/baseIO.lean.expected.out

@@ -0,0 +1,16 @@
+[Compiler.saveBase] size: 11
+    def test a.1 : EStateM.Result Empty PUnit UInt32 :=
+      let _x.2 := 42;
+      let _x.3 := @ST.Prim.mkRef _ _ _x.2 a.1;
+      cases _x.3 : EStateM.Result Empty PUnit UInt32
+      | EStateM.Result.ok a.4 a.5 =>
+        let _x.6 := 10;
+        let _x.7 := @ST.Prim.Ref.set _ _ a.4 _x.6 a.5;
+        cases _x.7 : EStateM.Result Empty PUnit UInt32
+        | EStateM.Result.ok a.8 a.9 =>
+          let _x.10 := @ST.Prim.Ref.get _ _ a.4 a.9;
+          return _x.10
+        | EStateM.Result.error a.11 a.12 =>
+          ⊥
+      | EStateM.Result.error a.13 a.14 =>
+        ⊥

tests/lean/computedFieldsCode.lean.expected.out

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

tests/lean/csimpAttr.lean.expected.out

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

tests/lean/csimpAttrAppend.lean.expected.out

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

tests/lean/doubleReset.lean.expected.out

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

tests/lean/lambdaLiftCache.lean.expected.out

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

tests/lean/listLength.lean.expected.out

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

tests/lean/new-compiler/CompilerElimDeadBranches.lean

@@ -1,37 +0,0 @@
-def someVal (_x : Nat) : Option Nat := some 0
-
-/-
-This test demonstrates two things:
-1. We eliminate all branches except the some, some one
-2. We communicate correctly to the constant folder that the `n` and `m`
-   are always 0 and can thus collapse the computation.
--/
-set_option trace.Compiler.elimDeadBranches true in
-set_option trace.Compiler.result true in
-def addSomeVal (x : Nat) :=
-  match someVal x, someVal x with
-  | some n, some m => some (n + m)
-  | _, _ => none
-
-
-def throwMyError (m n : Nat) : Except String Unit :=
-  throw s!"Ahhhh {m + n}"
-
-/-
-This demonstrates that the optimization does do good things to monadic
-code. In this snippet Lean would usually perform a cases on the result
-of `throwMyError` in order to figure out whether it has to:
-- raise an error and exit right now
-- jump to the `return x + y` continuation
-Since the abstract interpreter knows that `throwMyError` always returns
-an `Except.error` it will drop the branch where we jump to the continuation.
-This will in turn allow the simplifier to drop the join point that represents
-the continuation, saving us more code size.
--/
-set_option trace.Compiler.elimDeadBranches true in
-set_option trace.Compiler.result true in
-def monadic (x y : Nat) : Except String Nat := do
-  if let some m := addSomeVal x then
-    if let some n := addSomeVal y then
-      throwMyError m n
-  return x + y

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

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

tests/lean/new-compiler/CompilerProvokeFloatLet.lean

@@ -1,12 +0,0 @@
-set_option trace.Compiler.floatLetIn true in
-def provokeFloatLet (x y : Nat) (cond : Bool) : Nat :=
-  let a := x ^ y
-  let b := x + y
-  let c := x - y
-  let dual := x * y
-  if cond then
-    match dual with
-    | 0 => a
-    | _ + 1 => c
-  else
-    b + dual

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

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

tests/lean/new-compiler/README.md

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

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

@@ -1,18 +0,0 @@
-[Compiler.saveBase] size: 13
-    def test a.1 : EStateM.Result Empty PUnit UInt32 :=
-      let _x.2 := 42;
-      let _x.3 := UInt32.ofNat _x.2;
-      let _x.4 := @ST.Prim.mkRef _ _ _x.3 a.1;
-      cases _x.4 : EStateM.Result Empty PUnit UInt32
-      | EStateM.Result.ok a.5 a.6 =>
-        let _x.7 := 10;
-        let _x.8 := UInt32.ofNat _x.7;
-        let _x.9 := @ST.Prim.Ref.set _ _ a.5 _x.8 a.6;
-        cases _x.9 : EStateM.Result Empty PUnit UInt32
-        | EStateM.Result.ok a.10 a.11 =>
-          let _x.12 := @ST.Prim.Ref.get _ _ a.5 a.11;
-          return _x.12
-        | EStateM.Result.error a.13 a.14 =>
-          ⊥
-      | EStateM.Result.error a.15 a.16 =>
-        ⊥

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

@@ -1,20 +0,0 @@
-[Compiler.result] size: 5
-    def g._redArg (n : Nat) (a : ◾) (f : ◾ → ◾) : ◾ :=
-      cases n : ◾
-      | Nat.zero =>
-        return a
-      | Nat.succ (n.1 : Nat) =>
-        let _x.2 := g._redArg n.1 a f;
-        let _x.3 := f _x.2;
-        return _x.3
-[Compiler.result] size: 1
-    def g (α : ◾) (n : Nat) (a : ◾) (b : ◾) (f : ◾ → ◾) : ◾ :=
-      let _x.1 := g._redArg n a f;
-      return _x.1
-[Compiler.result] size: 4
-    def h (n : Nat) (a : Nat) : Nat :=
-      let _x.1 := double;
-      let _x.2 := g._redArg n a _x.1;
-      let _x.3 := g._redArg a n _x.1;
-      let _x.4 := Nat.add _x.2 _x.3;
-      return _x.4

tests/lean/reduceArity.lean.expected.out

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

tests/lean/run/2291.lean

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

tests/lean/run/emptyLcnf.lean

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

tests/lean/run/erased.lean

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

tests/lean/run/noncomp.lean

@@ -1,7 +1,14 @@
 noncomputable def foo : Nat := Classical.choose (show ∃ x, x = 1 from ⟨1, rfl⟩)
 
-structure Bar (n : Nat) :=
+structure Bar (n : Nat) where
   x : Nat
 
 def baz : Bar foo :=
   { x := 1 }
+
+structure Bar2 (n : Nat) where
+  x : Nat
+  y : Nat
+
+def bax2 : Bar2 foo :=
+  { x := 1, y := 2 }

tests/lean/run/usesOfNoncomputable.lean

@@ -0,0 +1,69 @@
+noncomputable def badPair : Nat × (Nat × Nat) := ⟨1, ⟨2, 3⟩⟩
+noncomputable def badFun (a : Nat) : Nat := a
+
+structure S (n : Nat)
+structure T where
+  n : Nat
+
+def test1 : S badPair.2.1 := {}
+
+/--
+error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'badPair', which is 'noncomputable'
+-/
+#guard_msgs in
+def test2 : T := { n := badPair.2.1 }
+
+def test3 (a : Nat) : S (badFun a) := {}
+def test4 (a : Nat) : S ((badFun a) + 1) := {}
+
+/--
+error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'badFun', which is 'noncomputable'
+-/
+#guard_msgs in
+def test5 (a : Nat) : T := { n := badFun a }
+
+/--
+error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'badFun', which is 'noncomputable'
+-/
+#guard_msgs in
+def test6 (a : Nat) : T := { n := 2 * (badFun a) }
+
+structure U (a : Nat × Nat)
+structure V where
+  a : Nat × Nat
+
+def test7 (a : Nat) : U (⟨badFun a, 0⟩) := {}
+def test8 (a : Nat) : U ((V.mk ⟨badFun a, 1⟩).a) := {}
+
+/--
+error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'badFun', which is 'noncomputable'
+-/
+#guard_msgs in
+def test9 (a : Nat) : V := ⟨a, badFun a⟩
+
+universe u
+
+def Erased (α : Sort u) : Sort max 1 u :=
+  { s : α → Prop // ∃ a, (a = ·) = s }
+
+def Erased.mk {α} (a : α) : Erased α :=
+  ⟨fun b => a = b, a, rfl⟩
+
+noncomputable def Erased.out {α} : Erased α → α
+  | ⟨_, h⟩ => Classical.choose h
+
+structure Foo where
+  spec : Erased Nat
+  data : Nat
+
+def test10 : Foo where
+  spec := Erased.mk (Erased.mk 0).out
+  data := 0
+
+/--
+error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Erased.out', which is 'noncomputable'
+-/
+#guard_msgs in
+def test11 : Foo where
+  spec := Erased.mk 0
+  data := (Erased.mk 0).out

tests/lean/sint_basic.lean.expected.out

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

tests/lean/unboxStruct.lean.expected.out

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

tests/lean/unhygienicCode.lean.expected.out

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

tests/lean/updateExprIssue.lean.expected.out

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