partial def Lean.Compiler.LCNF.Code.containsConst (constName : Name) (code : Code) : Bool

structure Lean.Compiler.LCNF.Testing.TestInstallerContext : Type

• passUnderTestName : Name
• testName : Name

structure Lean.Compiler.LCNF.Testing.TestContext : Type

• passUnderTest : Pass
• testName : Name

structure Lean.Compiler.LCNF.Testing.SimpleAssertionContext : Type

• decls : Array Decl

structure Lean.Compiler.LCNF.Testing.InOutAssertionContext : Type

• input : Array Decl
• output : Array Decl

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Testing.TestInstallerM (α : Type) : Type

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Testing.TestInstaller : Type

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Testing.TestM (α : Type) : Type

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Testing.SimpleAssertionM (α : Type) : Type

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Testing.InOutAssertionM (α : Type) : Type

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Testing.SimpleTest : Type

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Testing.InOutTest : Type

def Lean.Compiler.LCNF.Testing.TestInstaller.install (x : TestInstaller) (passUnderTestName testName : Name) : PassInstaller

def Lean.Compiler.LCNF.Testing.TestM.run {α : Type} (x : TestM α) (passUnderTest : Pass) (testName : Name) : CompilerM α

def Lean.Compiler.LCNF.Testing.SimpleAssertionM.run {α : Type} (x : SimpleAssertionM α) (decls : Array Decl) (passUnderTest : Pass) (testName : Name) : CompilerM α

def Lean.Compiler.LCNF.Testing.InOutAssertionM.run {α : Type} (x : InOutAssertionM α) (input output : Array Decl) (passUnderTest : Pass) (testName : Name) : CompilerM α

def Lean.Compiler.LCNF.Testing.getTestName : TestM Name

def Lean.Compiler.LCNF.Testing.getPassUnderTest : TestM Pass

def Lean.Compiler.LCNF.Testing.getDecls : SimpleAssertionM (Array Decl)

def Lean.Compiler.LCNF.Testing.getInputDecls : InOutAssertionM (Array Decl)

def Lean.Compiler.LCNF.Testing.getOutputDecls : InOutAssertionM (Array Decl)

def Lean.Compiler.LCNF.Testing.assert (property : Bool) (msg : String) : TestM Unit

If property is false throw an exception with msg.

def Lean.Compiler.LCNF.Testing.assertAfter (phase : Phase) (test : SimpleTest) (occurrence : Nat := 0) : TestInstaller

Install an assertion pass right after a specific occurrence of a pass, default is first.

def Lean.Compiler.LCNF.Testing.assertAfterEachOccurrence (phase : Phase) (test : SimpleTest) : TestInstaller

Install an assertion pass right after each occurrence of a pass.

def Lean.Compiler.LCNF.Testing.assertForEachDeclAfter (phase : Phase) (assertion : Pass → Decl → Bool) (msg : String) (occurrence : Nat := 0) : TestInstaller

Install an assertion pass right after a specific occurrence of a pass, default is first. The assertion operates on a per declaration basis.

def Lean.Compiler.LCNF.Testing.assertForEachDeclAfterEachOccurrence (phase : Phase) (assertion : Pass → Decl → Bool) (msg : String) : TestInstaller

Install an assertion pass right after the each occurrence of a pass. The assertion operates on a per declaration basis.

def Lean.Compiler.LCNF.Testing.assertAround (phase : Phase) (test : InOutTest) (occurrence : Nat := 0) : TestInstaller

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 Lean.Compiler.LCNF.Testing.assertAroundEachOccurrence (phase : Phase) (test : InOutTest) : TestInstaller

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 Lean.Compiler.LCNF.Testing.assertIsAtFixPoint (phase : Phase) : TestInstaller

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 Lean.Compiler.LCNF.Testing.assertSize (phase : Phase) (assertion : Nat → Nat → Bool) (msg : String) : TestInstaller

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 Lean.Compiler.LCNF.Testing.assertPreservesSize (phase : Phase) (msg : String) : TestInstaller

Assert that the overall size of the Decls in the compilation pipeline does not change after passUnderTestName.

def Lean.Compiler.LCNF.Testing.assertReducesSize (phase : Phase) (msg : String) : TestInstaller

Assert that the overall size of the Decls in the compilation pipeline gets reduced by passUnderTestName.

def Lean.Compiler.LCNF.Testing.assertReducesOrPreservesSize (phase : Phase) (msg : String) : TestInstaller

Assert that the overall size of the Decls in the compilation pipeline gets reduced or stays unchanged by passUnderTestName.

def Lean.Compiler.LCNF.Testing.assertDoesNotContainConstAfter (phase : Phase) (constName : Name) (msg : String) : TestInstaller

Assert that the pass under test produces Decls that do not contain Expr.const constName in their Code.let values anymore.

def Lean.Compiler.LCNF.Testing.assertNoFun (phase : Phase) : TestInstaller