chore: reenable subset of new-compiler tests and delete others

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/lambdaLiftCache.lean.expected.out

@@ -2,7 +2,11 @@
     def foo._lam_0 x x.1 : Nat :=
       let _x.2 := Nat.add x.1 x;
       return _x.2
-[Compiler.saveMono] size: 2 def foo x xs : List Nat := let _f.1 := foo._lam_0 x; let _x.2 := map _f.1 xs; return _x.2
+[Compiler.saveMono] size: 2
+    def foo x xs : List Nat :=
+      let _f.1 := foo._lam_0 x;
+      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;

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.36",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("val.20", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
-      ("_x.35", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("_x.37",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor
-         `Option.some
-         #[Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]])]
-[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.205",
-       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]),
-      ("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("a.208", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("_x.207",
-       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.212",
-       Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
-      ("a.206", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("val.200", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
-      ("_x.88", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("x", 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,64 +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 `Bool.true 0
-[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.false 0
-[Compiler.floatLetIn] size: 13
-    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 =>
-        let zero := 0;
-        let isZero := Nat.decEq dual zero;
-        cases isZero : Nat
-        | Bool.true =>
-          let a := Nat.pow x y;
-          return a
-        | Bool.false =>
-          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 `Bool.true 0
-[Compiler.floatLetIn] Size of code that was pushed into arm: Lean.Compiler.LCNF.FloatLetIn.Decision.arm `Bool.false 0
-[Compiler.floatLetIn] size: 13
-    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 =>
-        let zero := 0;
-        let isZero := Nat.decEq dual zero;
-        cases isZero : Nat
-        | Bool.true =>
-          let a := Nat.pow x y;
-          return a
-        | Bool.false =>
-          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 =>
-        ⊥