chore: typo
This commit is contained in:
Leonardo de Moura
parent
50fe9ceeaa
commit
db6ee72aed
8 changed files with 71 additions and 71 deletions
|
|
@ -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) }
|
||||
|
|
|
|||
|
|
@ -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
|
||||
]
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue