chore: remove the LCNF testing framework (#12207)

This PR removes the LCNF testing framework. Unfortunately it never got
used much and porting it to
the extended LCNF structure now would be a bit of effort that would
ultimately be in vain.

src/Lean/Compiler/LCNF.lean

@@ -30,7 +30,6 @@ public import Lean.Compiler.LCNF.ReduceJpArity
 public import Lean.Compiler.LCNF.Simp
 public import Lean.Compiler.LCNF.Specialize
 public import Lean.Compiler.LCNF.SpecInfo
-public import Lean.Compiler.LCNF.Testing
 public import Lean.Compiler.LCNF.ToDecl
 public import Lean.Compiler.LCNF.ToExpr
 public import Lean.Compiler.LCNF.ToLCNF

src/Lean/Compiler/LCNF/Testing.lean

@@ -1,256 +0,0 @@
-/-
-Copyright (c) 2022 Henrik Böving. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-module
-
-prelude
-public import Lean.Compiler.LCNF.PrettyPrinter
-
-public section
-
-namespace Lean.Compiler.LCNF
-
-partial def Code.containsConst (constName : Name) (code : Code) : Bool :=
-  match code with
-  | .let decl k => goLetValue decl.value || containsConst constName k
-  | .fun decl k => containsConst constName decl.value || containsConst constName k
-  | .jp decl k => containsConst constName decl.value || containsConst constName k
-  | .cases cs => cs.alts.any fun alt => containsConst constName alt.getCode
-  | .return .. | .unreach .. | .jmp .. => false
-where
-  goExpr (e : Expr) : Bool :=
-    match e with
-    | .const name .. => name == constName
-    | .app fn arg .. => goExpr fn || goExpr arg
-    | .lam _ _ body .. => goExpr body
-    | .proj _ _ struct .. => goExpr struct
-    | .letE .. => unreachable! -- not possible in LCNF
-    | _ => false
-  goLetValue (l : LetValue) : Bool :=
-    match l with
-    | .lit .. | .erased | .proj .. | .fvar .. => false
-    | .const name .. => name == constName
-
-namespace Testing
-
-structure TestInstallerContext where
-  passUnderTestName : Name
-  testName : Name
-
-structure TestContext where
-  passUnderTest : Pass
-  testName : Name
-
-structure SimpleAssertionContext where
-  decls : Array Decl
-
-structure InOutAssertionContext where
-  input : Array Decl
-  output : Array Decl
-
-abbrev TestInstallerM := ReaderM TestInstallerContext
-abbrev TestInstaller := TestInstallerM PassInstaller
-
-abbrev TestM := ReaderT TestContext CompilerM
-abbrev SimpleAssertionM := ReaderT SimpleAssertionContext TestM
-abbrev InOutAssertionM := ReaderT InOutAssertionContext TestM
-abbrev SimpleTest := SimpleAssertionM Unit
-abbrev InOutTest := InOutAssertionM Unit
-
-def TestInstaller.install (x : TestInstaller) (passUnderTestName testName : Name) : PassInstaller :=
-  x { passUnderTestName, testName }
-
-def TestM.run (x : TestM α) (passUnderTest : Pass) (testName : Name) : CompilerM α :=
-  x { passUnderTest, testName }
-
-def SimpleAssertionM.run (x : SimpleAssertionM α) (decls : Array Decl) (passUnderTest : Pass) (testName : Name) : CompilerM α :=
-  x { decls } { passUnderTest, testName }
-
-def InOutAssertionM.run (x : InOutAssertionM α) (input output : Array Decl) (passUnderTest : Pass) (testName : Name) : CompilerM α :=
-  x { input, output } { passUnderTest, testName }
-
-def getTestName : TestM Name := do
-  return (←read).testName
-
-def getPassUnderTest : TestM Pass := do
-  return (←read).passUnderTest
-
-def getDecls : SimpleAssertionM (Array Decl) := do
-  return (←read).decls
-
-def getInputDecls : InOutAssertionM (Array Decl) := do
-  return (←read).input
-
-def getOutputDecls : InOutAssertionM (Array Decl) := do
-  return (←read).output
-
-/--
-If `property` is `false` throw an exception with `msg`.
--/
-def assert (property : Bool) (msg : String) : TestM Unit := do
-  unless property do
-    throwError msg
-
-private def assertAfterTest (test : SimpleTest) : TestInstallerM (Pass → Pass) := do
-  let testName := (←read).testName
-  return fun passUnderTest => {
-    phase := passUnderTest.phase
-    name := testName
-    run := fun decls => do
-      trace[Compiler.test] "Starting post condition test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence}"
-      test.run decls passUnderTest testName
-      trace[Compiler.test] "Post condition test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence} successful"
-      return decls
-  }
-
-/--
-Install an assertion pass right after a specific occurrence of a pass,
-default is first.
--/
-def assertAfter (phase : Phase) (test : SimpleTest) (occurrence : Nat := 0): TestInstaller := do
-  let passUnderTestName := (←read).passUnderTestName
-  let assertion ← assertAfterTest test
-  return .installAfter phase passUnderTestName assertion occurrence
-
-/--
-Install an assertion pass right after each occurrence of a pass.
--/
-def assertAfterEachOccurrence (phase : Phase) (test : SimpleTest) : TestInstaller := do
-  let passUnderTestName := (←read).passUnderTestName
-  let assertion ← assertAfterTest test
-  return .installAfterEach phase passUnderTestName assertion
-
-/--
-Install an assertion pass right after a specific occurrence of a pass,
-default is first. The assertion operates on a per declaration basis.
--/
-def assertForEachDeclAfter (phase : Phase) (assertion : Pass → Decl → Bool) (msg : String) (occurrence : Nat := 0) : TestInstaller :=
-  let assertion := do
-    let pass ← getPassUnderTest
-    (←getDecls).forM (fun decl => assert (assertion pass decl) msg)
-  assertAfter phase assertion occurrence
-
-/--
-Install an assertion pass right after the each occurrence of a pass. The
-assertion operates on a per declaration basis.
--/
-def assertForEachDeclAfterEachOccurrence (phase : Phase) (assertion : Pass → Decl → Bool) (msg : String) : TestInstaller :=
-  assertAfterEachOccurrence phase <| do
-    let pass ← getPassUnderTest
-    (←getDecls).forM (fun decl => assert (assertion pass decl) msg)
-
-private def assertAroundTest (test : InOutTest) : TestInstallerM (Pass → Pass) := do
-  let testName := (←read).testName
-  return fun passUnderTest => {
-    phase := passUnderTest.phase
-    name := passUnderTest.name
-    run := fun decls => do
-      trace[Compiler.test] "Starting wrapper test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence}"
-      let newDecls ← passUnderTest.run decls
-      test.run decls newDecls passUnderTest testName
-      trace[Compiler.test] "Wrapper test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence} successful"
-      return newDecls
-  }
-
-/--
-Replace a specific occurrence, default is first, of a pass with a wrapper one that allows
-the user to provide an assertion which takes into account both the
-declarations that were sent to and produced by the pass under test.
--/
-def assertAround (phase : Phase) (test : InOutTest) (occurrence : Nat := 0) : TestInstaller := do
-  let passUnderTestName := (←read).passUnderTestName
-  let assertion ← assertAroundTest test
-  return .replacePass phase passUnderTestName assertion occurrence
-
-/--
-Replace all occurrences of a pass with a wrapper one that allows
-the user to provide an assertion which takes into account both the
-declarations that were sent to and produced by the pass under test.
--/
-def assertAroundEachOccurrence (phase : Phase) (test : InOutTest) : TestInstaller := do
-  let passUnderTestName := (←read).passUnderTestName
-  let assertion ← assertAroundTest test
-  return .replaceEachOccurrence phase passUnderTestName assertion
-
-private def throwFixPointError (err : String) (firstResult secondResult : Array Decl) : CompilerM Unit := do
-  let mut err := err
-  err := err ++ "Result after usual run:"
-  let folder := fun err decl => do return err ++ s!"\n{←ppDecl decl}"
-  err ← firstResult.foldlM (init := err) folder
-  err := err ++ "Result after further run:"
-  err ← secondResult.foldlM (init := err) folder
-  throwError err
-
-/--
-Insert a pass after `passUnderTestName`, that ensures, that if
-`passUnderTestName` is executed twice in a row, no change in the resulting
-expression will occur, i.e. the pass is at a fix point.
--/
-def assertIsAtFixPoint (phase : Phase) : TestInstaller :=
-  let test := do
-    let passUnderTest ← getPassUnderTest
-    let decls ← getDecls
-    let secondResult ← passUnderTest.run decls
-    if decls.size < secondResult.size then
-      let err := s!"Pass {passUnderTest.name} did not reach a fixpoint, it added declarations on further runs:\n"
-      throwFixPointError err decls secondResult
-    else if decls.size > secondResult.size then
-      let err := s!"Pass {passUnderTest.name} did not reach a fixpoint, it removed declarations on further runs:\n"
-      throwFixPointError err decls secondResult
-    else if decls != secondResult then
-      let err := s!"Pass {passUnderTest.name} did not reach a fixpoint, it either changed declarations or their order:\n"
-      throwFixPointError err decls secondResult
-  assertAfterEachOccurrence phase test
-
-/--
-Compare the overall sizes of the input and output of `passUnderTest` with `assertion`.
-If `assertion inputSize outputSize` is `false` throw an exception with `msg`.
--/
-def assertSize (phase : Phase) (assertion : Nat → Nat → Bool) (msg : String) : TestInstaller :=
-  let sumDeclSizes := fun decls => decls.map Decl.size |>.foldl (init := 0) (· + ·)
-  let assertion := (fun inputS outputS => Testing.assert (assertion inputS outputS) s!"{msg}: input size {inputS} output size {outputS}")
-  assertAroundEachOccurrence phase (do assertion (sumDeclSizes (←getInputDecls)) (sumDeclSizes (←getOutputDecls)))
-
-/--
-Assert that the overall size of the `Decl`s in the compilation pipeline does not change
-after `passUnderTestName`.
--/
-def assertPreservesSize (phase : Phase) (msg : String) : TestInstaller :=
-  assertSize phase (· == ·) msg
-
-/--
-Assert that the overall size of the `Decl`s in the compilation pipeline gets reduced by `passUnderTestName`.
--/
-def assertReducesSize (phase : Phase) (msg : String) : TestInstaller :=
-  assertSize phase (· > ·) msg
-
-/--
-Assert that the overall size of the `Decl`s in the compilation pipeline gets reduced or stays unchanged
-by `passUnderTestName`.
--/
-def assertReducesOrPreservesSize (phase : Phase) (msg : String) : TestInstaller :=
-  assertSize phase (· ≥ ·) msg
-
-/--
-Assert that the pass under test produces `Decl`s that do not contain
-`Expr.const constName` in their `Code.let` values anymore.
--/
-def assertDoesNotContainConstAfter (phase : Phase) (constName : Name) (msg : String) : TestInstaller :=
-  assertForEachDeclAfterEachOccurrence phase
-    fun _ decl =>
-      match decl.value with
-      | .code c => !c.containsConst constName
-      | .extern .. => true
-    msg
-
-def assertNoFun (phase : Phase) : TestInstaller :=
-  assertAfter phase do
-    for decl in (← getDecls) do
-      decl.value.forCodeM fun
-        | .fun .. => throwError "declaration `{decl.name}` contains a local function declaration"
-        | _ => return ()
-
-end Testing
-end Lean.Compiler.LCNF

tests/lean/run/inlineApp.lean

@@ -6,11 +6,61 @@ def f (x : Nat) :=
 def h (x : Nat) :=
   inline <| f (x + x)
 
-#eval Lean.Compiler.compile #[``h]
-
-open Lean Compiler LCNF in
-@[cpass] def simpInline : PassInstaller :=
-  Testing.assertDoesNotContainConstAfter .mono ``inline "simp did not inline `inline`" |>.install `simp `simpInlinesInline
-
-set_option trace.Compiler.result true
+/--
+trace: [Compiler.result] size: 8
+    def h x : Nat :=
+      let _x.1 := Nat.add x x;
+      let _x.2 := 1;
+      let _x.3 := Nat.sub _x.1 _x.2;
+      let _x.4 := 2;
+      let _x.5 := Nat.mul _x.1 _x.4;
+      let _x.6 := Nat.add _x.3 _x.5;
+      let _x.7 := Nat.mul _x.1 _x.1;
+      let _x.8 := Nat.add _x.6 _x.7;
+      return _x.8
+---
+trace: [Compiler.result] size: 1
+    def _private.lean.run.inlineApp.0._eval._lam_0 _x.1 _y.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 : EST.Out Lean.Exception
+      lcAny PUnit :=
+      let _x.9 := Lean.Compiler.compile _x.1 _y.6 _y.7 _y.8;
+      return _x.9
+[Compiler.result] size: 1
+    def _private.lean.run.inlineApp.0._eval._closed_0 : String :=
+      let _x.1 := "h";
+      return _x.1
+[Compiler.result] size: 2
+    def _private.lean.run.inlineApp.0._eval._closed_1 : Lean.Name :=
+      let _x.1 := _eval._closed_0.2;
+      let _x.2 := Lean.Name.mkStr1 _x.1;
+      return _x.2
+[Compiler.result] size: 2
+    def _private.lean.run.inlineApp.0._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 _private.lean.run.inlineApp.0._eval._closed_3 : Array Lean.Name :=
+      let _x.1 := _eval._closed_1.2;
+      let _x.2 := _eval._closed_2.2;
+      let _x.3 := Array.push ◾ _x.2 _x.1;
+      return _x.3
+[Compiler.result] size: 2
+    def _private.lean.run.inlineApp.0._eval._closed_4 : Lean.Elab.Term.Context →
+      lcAny → Lean.Meta.Context → lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit :=
+      let _x.1 := _eval._closed_3.2;
+      let _f.2 := _eval._lam_0.2 _x.1;
+      return _f.2
+[Compiler.result] size: 7
+    def _private.lean.run.inlineApp.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
+      let _x.4 := _eval._closed_0.2;
+      let _x.5 := _eval._closed_1.2;
+      let _x.6 := 1;
+      let _x.7 := _eval._closed_2.2;
+      let _x.8 := _eval._closed_3.2;
+      let _f.9 := _eval._closed_4.2;
+      let _x.10 := Lean.Elab.Command.liftTermElabM._redArg _f.9 a.1 a.2 a.3;
+      return _x.10
+-/
+#guard_msgs in
+set_option trace.Compiler.result true in
 #eval Lean.Compiler.compile #[``h]

tests/lean/run/toDeclEtaBug.lean

@@ -1,15 +1,19 @@
 import Lean
 
-open Lean Compiler LCNF Testing
-
 @[inline] def f (c b : Bool) (x : Nat) : Nat :=
   if c && b then
     x + 1
   else
     x + 2
 
--- TODO: uncomment after the new compiler is executed by default
--- @[cpass] def cseSizeTest : PassInstaller := Testing.assertNoFun |>.install `specialize `noFun
-
+/--
+trace: [Compiler.result] size: 2
+    def g c : Nat :=
+      let _x.1 := 2;
+      let _x.2 := Nat.add c _x.1;
+      return _x.2
+-/
+#guard_msgs in
+set_option trace.Compiler.result true in
 def g (c : Nat) : Nat :=
   f true false c