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

partial def Lean.Compiler.LCNF.Code.containsConst.goExpr (constName : Name) (e : Expr) : Bool

def Lean.Compiler.LCNF.Code.containsConst.goLetValue (constName : Name) (l : LetValue) : Bool

Equations

• Lean.Compiler.LCNF.Code.containsConst.goLetValue constName (Lean.Compiler.LCNF.LetValue.value value) = false
• Lean.Compiler.LCNF.Code.containsConst.goLetValue constName Lean.Compiler.LCNF.LetValue.erased = false
• Lean.Compiler.LCNF.Code.containsConst.goLetValue constName (Lean.Compiler.LCNF.LetValue.proj typeName idx struct) = false
• Lean.Compiler.LCNF.Code.containsConst.goLetValue constName (Lean.Compiler.LCNF.LetValue.fvar fvarId args) = false
• Lean.Compiler.LCNF.Code.containsConst.goLetValue constName (Lean.Compiler.LCNF.LetValue.const name us args) = (name == constName)

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

Equations

• Lean.Compiler.LCNF.Testing.TestInstallerM = ReaderM Lean.Compiler.LCNF.Testing.TestInstallerContext

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.Testing.TestInstaller = Lean.Compiler.LCNF.Testing.TestInstallerM Lean.Compiler.LCNF.PassInstaller

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.Testing.TestM = ReaderT Lean.Compiler.LCNF.Testing.TestContext Lean.Compiler.LCNF.CompilerM

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.Testing.SimpleAssertionM = ReaderT Lean.Compiler.LCNF.Testing.SimpleAssertionContext Lean.Compiler.LCNF.Testing.TestM

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.Testing.InOutAssertionM = ReaderT Lean.Compiler.LCNF.Testing.InOutAssertionContext Lean.Compiler.LCNF.Testing.TestM

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.Testing.SimpleTest = Lean.Compiler.LCNF.Testing.SimpleAssertionM Unit

@[reducible, inline]

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

Equations

• Lean.Compiler.LCNF.Testing.InOutTest = Lean.Compiler.LCNF.Testing.InOutAssertionM Unit

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

Equations

• x.install passUnderTestName testName = x { passUnderTestName := passUnderTestName, testName := testName }

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

Equations

• x.run passUnderTest testName = x { passUnderTest := passUnderTest, testName := testName }

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

Equations

• x.run decls passUnderTest testName = x { decls := decls } { passUnderTest := passUnderTest, testName := testName }

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

Equations

• x.run input output passUnderTest testName = x { input := input, output := output } { passUnderTest := passUnderTest, testName := testName }

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

Equations

• Lean.Compiler.LCNF.Testing.getTestName = do let __do_lift ← read pure __do_lift.testName

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

Equations

• Lean.Compiler.LCNF.Testing.getPassUnderTest = do let __do_lift ← read pure __do_lift.passUnderTest

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

Equations

• Lean.Compiler.LCNF.Testing.getDecls = do let __do_lift ← read pure __do_lift.decls

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

Equations

• Lean.Compiler.LCNF.Testing.getInputDecls = do let __do_lift ← read pure __do_lift.input

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

Equations

• Lean.Compiler.LCNF.Testing.getOutputDecls = do let __do_lift ← read pure __do_lift.output

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

If property is false throw an exception with msg.

Equations

• Lean.Compiler.LCNF.Testing.assert property msg = if property = true then pure PUnit.unit else Lean.throwError ((Lean.MessageData.ofFormat ∘ Std.format) msg)

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Testing.assertForEachDeclAfter (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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Testing.assertForEachDeclAfterEachOccurrence (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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Testing.assertAround (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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Testing.assertAroundEachOccurrence (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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Testing.assertIsAtFixPoint : 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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Testing.assertSize (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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Testing.assertPreservesSize (msg : String) : TestInstaller

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

Equations

• Lean.Compiler.LCNF.Testing.assertPreservesSize msg = Lean.Compiler.LCNF.Testing.assertSize (fun (x1 x2 : Nat) => x1 == x2) msg

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

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

Equations

• Lean.Compiler.LCNF.Testing.assertReducesSize msg = Lean.Compiler.LCNF.Testing.assertSize (fun (x1 x2 : Nat) => decide (x1 > x2)) msg

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

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

Equations

• Lean.Compiler.LCNF.Testing.assertReducesOrPreservesSize msg = Lean.Compiler.LCNF.Testing.assertSize (fun (x1 x2 : Nat) => decide (x1 ≥ x2)) msg

def Lean.Compiler.LCNF.Testing.assertDoesNotContainConstAfter (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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.Testing.assertNoFun : TestInstaller

Equations

• One or more equations did not get rendered due to their size.