diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean index 44cab01fd0..13d2bb95fe 100644 --- a/src/Lean/Compiler/LCNF/PassManager.lean +++ b/src/Lean/Compiler/LCNF/PassManager.lean @@ -30,11 +30,11 @@ on the `Decl`s as well as meta information. -/ structure Pass where /-- - Which occurence of the pass in the pipeline this is. + Which occurrence of the pass in the pipeline this is. Some passes, like simp, can occur multiple times in the pipeline. For most passes this value does not matter. -/ - occurence : Nat := 0 + occurrence : Nat := 0 /-- Which phase this `Pass` is supposed to run in -/ @@ -96,8 +96,8 @@ end Phase namespace Pass -def mkPerDeclaration (name : Name) (run : Decl → CompilerM Decl) (phase : Phase) (occurence : Nat := 0) : Pass where - occurence := occurence +def mkPerDeclaration (name : Name) (run : Decl → CompilerM Decl) (phase : Phase) (occurrence : Nat := 0) : Pass where + occurrence := occurrence phase := phase name := name run := fun xs => xs.mapM run @@ -113,12 +113,12 @@ def validate (manager : PassManager) : CompilerM Unit := do throwError s!"{pass.name} has phase {pass.phase} but should at least have {current}" current := pass.phase -def findHighestOccurence (targetName : Name) (passes : Array Pass) : CompilerM Nat := do +def findHighestOccurrence (targetName : Name) (passes : Array Pass) : CompilerM Nat := do let mut highest := none for pass in passes do if pass.name == targetName then - highest := some pass.occurence - let some val := highest | throwError s!"Could not find any occurence of {targetName}" + highest := some pass.occurrence + let some val := highest | throwError s!"Could not find any occurrence of {targetName}" return val end PassManager @@ -131,45 +131,45 @@ def installAtEnd (p : Pass) : PassInstaller where def append (passesNew : Array Pass) : PassInstaller where install passes := return passes ++ passesNew -def withEachOccurence (targetName : Name) (f : Nat → PassInstaller) : PassInstaller where +def withEachOccurrence (targetName : Name) (f : Nat → PassInstaller) : PassInstaller where install passes := do - let highestOccurence ← PassManager.findHighestOccurence targetName passes + let highestOccurrence ← PassManager.findHighestOccurrence targetName passes let mut passes := passes - for occurence in [0:highestOccurence+1] do - passes ← f occurence |>.install passes + for occurrence in [0:highestOccurrence+1] do + passes ← f occurrence |>.install passes return passes -def installAfter (targetName : Name) (p : Pass → Pass) (occurence : Nat := 0) : PassInstaller where +def installAfter (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller where install passes := - if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurence == occurence) then + if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then let passUnderTest := passes[idx]! return passes.insertAt (idx + 1) (p passUnderTest) else - throwError s!"Tried to insert pass after {targetName}, occurence {occurence} but {targetName} is not in the pass list" + throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list" def installAfterEach (targetName : Name) (p : Pass → Pass) : PassInstaller := - withEachOccurence targetName (installAfter targetName p ·) + withEachOccurrence targetName (installAfter targetName p ·) -def installBefore (targetName : Name) (p : Pass → Pass) (occurence : Nat := 0): PassInstaller where +def installBefore (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0): PassInstaller where install passes := - if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurence == occurence) then + if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then let passUnderTest := passes[idx]! return passes.insertAt idx (p passUnderTest) else - throwError s!"Tried to insert pass after {targetName}, occurence {occurence} but {targetName} is not in the pass list" + throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list" -def installBeforeEachOccurence (targetName : Name) (p : Pass → Pass) : PassInstaller := - withEachOccurence targetName (installBefore targetName p ·) +def installBeforeEachOccurrence (targetName : Name) (p : Pass → Pass) : PassInstaller := + withEachOccurrence targetName (installBefore targetName p ·) -def replacePass (targetName : Name) (p : Pass → Pass) (occurence : Nat := 0) : PassInstaller where +def replacePass (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller where install passes := do - let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurence == occurence) | throwError s!"Tried to replace {targetName}, occurence {occurence} but {targetName} is not in the pass list" + let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) | throwError s!"Tried to replace {targetName}, occurrence {occurrence} but {targetName} is not in the pass list" let target := passes[idx]! let replacement := p target return passes.set! idx replacement -def replaceEachOccurence (targetName : Name) (p : Pass → Pass) : PassInstaller := - withEachOccurence targetName (replacePass targetName p ·) +def replaceEachOccurrence (targetName : Name) (p : Pass → Pass) : PassInstaller := + withEachOccurrence targetName (replacePass targetName p ·) def run (manager : PassManager) (installer : PassInstaller) : CompilerM PassManager := do return { manager with passes := (←installer.install manager.passes) } diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index 467acfef1a..c9dcd295a6 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -22,7 +22,7 @@ namespace Lean.Compiler.LCNF pullFunDecls, findJoinPoints, reduceJpArity, - simp { etaPoly := true, inlinePartial := true, implementedBy := true } (occurence := 1), + simp { etaPoly := true, inlinePartial := true, implementedBy := true } (occurrence := 1), specialize ] diff --git a/src/Lean/Compiler/LCNF/Simp.lean b/src/Lean/Compiler/LCNF/Simp.lean index 26c8c51d88..0a9b01814c 100644 --- a/src/Lean/Compiler/LCNF/Simp.lean +++ b/src/Lean/Compiler/LCNF/Simp.lean @@ -1059,8 +1059,8 @@ where else return decl -def simp (config : Config := {}) (occurence : Nat := 0) : Pass := - .mkPerDeclaration `simp (Decl.simp · config) .base (occurence := occurence) +def simp (config : Config := {}) (occurrence : Nat := 0) : Pass := + .mkPerDeclaration `simp (Decl.simp · config) .base (occurrence := occurrence) builtin_initialize registerTraceClass `Compiler.simp (inherited := true) diff --git a/src/Lean/Compiler/LCNF/Testing.lean b/src/Lean/Compiler/LCNF/Testing.lean index fdbaa252ae..576f0a4135 100644 --- a/src/Lean/Compiler/LCNF/Testing.lean +++ b/src/Lean/Compiler/LCNF/Testing.lean @@ -92,45 +92,45 @@ private def assertAfterTest (test : SimpleTest) : TestInstallerM (Pass → Pass) phase := passUnderTest.phase name := testName run := fun decls => do - trace[Compiler.test] s!"Starting post condition test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence}" + trace[Compiler.test] s!"Starting post condition test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence}" test.run decls passUnderTest testName - trace[Compiler.test] s!"Post condition test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence} successful" + trace[Compiler.test] s!"Post condition test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence} successful" return decls } /-- -Install an assertion pass right after a specific occurence of a pass, +Install an assertion pass right after a specific occurrence of a pass, default is first. -/ -def assertAfter (test : SimpleTest) (occurence : Nat := 0): TestInstaller := do +def assertAfter (test : SimpleTest) (occurrence : Nat := 0): TestInstaller := do let passUnderTestName := (←read).passUnderTestName let assertion ← assertAfterTest test - return .installAfter passUnderTestName assertion occurence + return .installAfter passUnderTestName assertion occurrence /-- -Install an assertion pass right after each occurence of a pass. +Install an assertion pass right after each occurrence of a pass. -/ -def assertAfterEachOccurence (test : SimpleTest) : TestInstaller := do +def assertAfterEachOccurrence (test : SimpleTest) : TestInstaller := do let passUnderTestName := (←read).passUnderTestName let assertion ← assertAfterTest test return .installAfterEach passUnderTestName assertion /-- -Install an assertion pass right after a specific occurence of a pass, +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 (assertion : Pass → Decl → Bool) (msg : String) (occurence : Nat := 0) : TestInstaller := +def assertForEachDeclAfter (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 assertion occurence + assertAfter assertion occurrence /-- -Install an assertion pass right after the each occurence of a pass. The +Install an assertion pass right after the each occurrence of a pass. The assertion operates on a per declaration basis. -/ -def assertForEachDeclAfterEachOccurence (assertion : Pass → Decl → Bool) (msg : String) : TestInstaller := - assertAfterEachOccurence <| do +def assertForEachDeclAfterEachOccurrence (assertion : Pass → Decl → Bool) (msg : String) : TestInstaller := + assertAfterEachOccurrence <| do let pass ← getPassUnderTest (←getDecls).forM (fun decl => assert (assertion pass decl) msg) @@ -140,32 +140,32 @@ private def assertAroundTest (test : InOutTest) : TestInstallerM (Pass → Pass) phase := passUnderTest.phase name := passUnderTest.name run := fun decls => do - trace[Compiler.test] s!"Starting wrapper test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence}" + trace[Compiler.test] s!"Starting wrapper test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence}" let newDecls ← passUnderTest.run decls test.run decls newDecls passUnderTest testName - trace[Compiler.test] s!"Wrapper test {testName} for {passUnderTest.name} occurence {passUnderTest.occurence} successful" + trace[Compiler.test] s!"Wrapper test {testName} for {passUnderTest.name} occurrence {passUnderTest.occurrence} successful" return newDecls } /-- -Replace a specific occurence, default is first, of a pass with a wrapper one that allows +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 (test : InOutTest) (occurence : Nat := 0) : TestInstaller := do +def assertAround (test : InOutTest) (occurrence : Nat := 0) : TestInstaller := do let passUnderTestName := (←read).passUnderTestName let assertion ← assertAroundTest test - return .replacePass passUnderTestName assertion occurence + return .replacePass passUnderTestName assertion occurrence /-- -Replace all occurences of a pass with a wrapper one that allows +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 assertAroundEachOccurence (test : InOutTest) : TestInstaller := do +def assertAroundEachOccurrence (test : InOutTest) : TestInstaller := do let passUnderTestName := (←read).passUnderTestName let assertion ← assertAroundTest test - return .replaceEachOccurence passUnderTestName assertion + return .replaceEachOccurrence passUnderTestName assertion private def throwFixPointError (err : String) (firstResult secondResult : Array Decl) : CompilerM Unit := do let mut err := err @@ -195,7 +195,7 @@ def assertIsAtFixPoint : TestInstaller := 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 - assertAfterEachOccurence test + assertAfterEachOccurrence test /-- Compare the overall sizes of the input and output of `passUnderTest` with `assertion`. @@ -204,7 +204,7 @@ If `assertion inputSize outputSize` is `false` throw an exception with `msg`. def assertSize (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}") - assertAroundEachOccurence (do assertion (sumDeclSizes (←getInputDecls)) (sumDeclSizes (←getOutputDecls))) + assertAroundEachOccurrence (do assertion (sumDeclSizes (←getInputDecls)) (sumDeclSizes (←getOutputDecls))) /-- Assert that the overall size of the `Decl`s in the compilation pipeline does not change @@ -231,7 +231,7 @@ Assert that the pass under test produces `Decl`s that do not contain `Expr.const constName` in their `Code.let` values anymore. -/ def assertDoesNotContainConstAfter (constName : Name) (msg : String) : TestInstaller := - assertForEachDeclAfterEachOccurence (fun _ decl => !decl.value.containsConst constName) msg + assertForEachDeclAfterEachOccurrence (fun _ decl => !decl.value.containsConst constName) msg def assertNoFun : TestInstaller := assertAfter do diff --git a/tests/lean/CompilerCSE.lean.expected.out b/tests/lean/CompilerCSE.lean.expected.out index 003e41d422..dd70cae0e5 100644 --- a/tests/lean/CompilerCSE.lean.expected.out +++ b/tests/lean/CompilerCSE.lean.expected.out @@ -1,5 +1,5 @@ -[Compiler.test] Starting wrapper test cseSizeLeq for cse occurence 0 -[Compiler.test] Wrapper test cseSizeLeq for cse occurence 0 successful -[Compiler.test] Starting post condition test cseFix for cse occurence 0 -[Compiler.test] Post condition test cseFix for cse occurence 0 successful +[Compiler.test] Starting wrapper test cseSizeLeq for cse occurrence 0 +[Compiler.test] Wrapper test cseSizeLeq for cse occurrence 0 successful +[Compiler.test] Starting post condition test cseFix for cse occurrence 0 +[Compiler.test] Post condition test cseFix for cse occurrence 0 successful diff --git a/tests/lean/CompilerFindJoinPoints.lean.expected.out b/tests/lean/CompilerFindJoinPoints.lean.expected.out index 4df1bda51c..f1a9944e7b 100644 --- a/tests/lean/CompilerFindJoinPoints.lean.expected.out +++ b/tests/lean/CompilerFindJoinPoints.lean.expected.out @@ -1,5 +1,5 @@ -[Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPoints occurence 0 -[Compiler.test] Wrapper test findJoinPointsSizeLeq for findJoinPoints occurence 0 successful -[Compiler.test] Starting post condition test findJoinPointsFix for findJoinPoints occurence 0 -[Compiler.test] Post condition test findJoinPointsFix for findJoinPoints occurence 0 successful +[Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPoints occurrence 0 +[Compiler.test] Wrapper test findJoinPointsSizeLeq for findJoinPoints occurrence 0 successful +[Compiler.test] Starting post condition test findJoinPointsFix for findJoinPoints occurrence 0 +[Compiler.test] Post condition test findJoinPointsFix for findJoinPoints occurrence 0 successful diff --git a/tests/lean/CompilerPullInstances.lean.expected.out b/tests/lean/CompilerPullInstances.lean.expected.out index 0ce3ec761e..f32dd801f4 100644 --- a/tests/lean/CompilerPullInstances.lean.expected.out +++ b/tests/lean/CompilerPullInstances.lean.expected.out @@ -1,5 +1,5 @@ -[Compiler.test] Starting wrapper test pullInstancesSizeEq for pullInstances occurence 0 -[Compiler.test] Wrapper test pullInstancesSizeEq for pullInstances occurence 0 successful -[Compiler.test] Starting post condition test pullInstancesFix for pullInstances occurence 0 -[Compiler.test] Post condition test pullInstancesFix for pullInstances occurence 0 successful +[Compiler.test] Starting wrapper test pullInstancesSizeEq for pullInstances occurrence 0 +[Compiler.test] Wrapper test pullInstancesSizeEq for pullInstances occurrence 0 successful +[Compiler.test] Starting post condition test pullInstancesFix for pullInstances occurrence 0 +[Compiler.test] Post condition test pullInstancesFix for pullInstances occurrence 0 successful diff --git a/tests/lean/CompilerSimp.lean.expected.out b/tests/lean/CompilerSimp.lean.expected.out index bb09e89762..ad92799f8e 100644 --- a/tests/lean/CompilerSimp.lean.expected.out +++ b/tests/lean/CompilerSimp.lean.expected.out @@ -1,9 +1,9 @@ -[Compiler.test] Starting post condition test simpInlinesBinds for simp occurence 0 -[Compiler.test] Post condition test simpInlinesBinds for simp occurence 0 successful -[Compiler.test] Starting post condition test simpFix for simp occurence 0 -[Compiler.test] Post condition test simpFix for simp occurence 0 successful -[Compiler.test] Starting post condition test simpInlinesBinds for simp occurence 1 -[Compiler.test] Post condition test simpInlinesBinds for simp occurence 1 successful -[Compiler.test] Starting post condition test simpFix for simp occurence 1 -[Compiler.test] Post condition test simpFix for simp occurence 1 successful +[Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 0 +[Compiler.test] Post condition test simpInlinesBinds for simp occurrence 0 successful +[Compiler.test] Starting post condition test simpFix for simp occurrence 0 +[Compiler.test] Post condition test simpFix for simp occurrence 0 successful +[Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 1 +[Compiler.test] Post condition test simpInlinesBinds for simp occurrence 1 successful +[Compiler.test] Starting post condition test simpFix for simp occurrence 1 +[Compiler.test] Post condition test simpFix for simp occurrence 1 successful