From e53ac503dabfbbe45cc0027df1e6ac91b0417340 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Sep 2022 07:14:09 -0700 Subject: [PATCH] refactor: move `PassInstaller` to `CoreM` --- src/Lean/Compiler/LCNF/PassManager.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean index 661dd565cb..7adbe1cca8 100644 --- a/src/Lean/Compiler/LCNF/PassManager.lean +++ b/src/Lean/Compiler/LCNF/PassManager.lean @@ -59,7 +59,7 @@ structure PassInstaller where current `Pass`es and return a new one, this can modify the list (and the `Pass`es contained within) in any way it wants. -/ - install : Array Pass → CompilerM (Array Pass) + install : Array Pass → CoreM (Array Pass) deriving Inhabited /-- @@ -106,14 +106,14 @@ end Pass namespace PassManager -def validate (manager : PassManager) : CompilerM Unit := do +def validate (manager : PassManager) : CoreM Unit := do let mut current := .base for pass in manager.passes do if ¬(current ≤ pass.phase) then throwError s!"{pass.name} has phase {pass.phase} but should at least have {current}" current := pass.phase -def findHighestOccurrence (targetName : Name) (passes : Array Pass) : CompilerM Nat := do +def findHighestOccurrence (targetName : Name) (passes : Array Pass) : CoreM Nat := do let mut highest := none for pass in passes do if pass.name == targetName then