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

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

def Lean.Compiler.LCNF.Code.containsConst.goLetValue (constName : Lake.Name) (l : Lean.Compiler.LCNF.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 : Lake.Name
• testName : Lake.Name

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

• passUnderTest : Lean.Compiler.LCNF.Pass
• testName : Lake.Name

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

• decls : Array Lean.Compiler.LCNF.Decl

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

• input : Array Lean.Compiler.LCNF.Decl
• output : Array Lean.Compiler.LCNF.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 : Lean.Compiler.LCNF.Testing.TestInstaller) (passUnderTestName : Lake.Name) (testName : Lake.Name) : Lean.Compiler.LCNF.PassInstaller

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.Testing.getOutputDecls : Lean.Compiler.LCNF.Testing.InOutAssertionM (Array Lean.Compiler.LCNF.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) : Lean.Compiler.LCNF.Testing.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 ∘ Lean.format) msg)

def Lean.Compiler.LCNF.Testing.assertAfter (test : Lean.Compiler.LCNF.Testing.SimpleTest) (occurrence : optParam Nat 0) : Lean.Compiler.LCNF.Testing.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 : Lean.Compiler.LCNF.Testing.SimpleTest) : Lean.Compiler.LCNF.Testing.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 : Lean.Compiler.LCNF.Pass → Lean.Compiler.LCNF.Decl → Bool) (msg : String) (occurrence : optParam Nat 0) : Lean.Compiler.LCNF.Testing.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 : Lean.Compiler.LCNF.Pass → Lean.Compiler.LCNF.Decl → Bool) (msg : String) : Lean.Compiler.LCNF.Testing.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 : Lean.Compiler.LCNF.Testing.InOutTest) (occurrence : optParam Nat 0) : Lean.Compiler.LCNF.Testing.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 : Lean.Compiler.LCNF.Testing.InOutTest) : Lean.Compiler.LCNF.Testing.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 : Lean.Compiler.LCNF.Testing.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) : Lean.Compiler.LCNF.Testing.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) : Lean.Compiler.LCNF.Testing.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) : Lean.Compiler.LCNF.Testing.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) : Lean.Compiler.LCNF.Testing.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 : Lake.Name) (msg : String) : Lean.Compiler.LCNF.Testing.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 : Lean.Compiler.LCNF.Testing.TestInstaller

Equations

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