diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean index 5361bed098..d441afb04a 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.Compiler.Options import Lean.Compiler.LCNF.PassManager +import Lean.Compiler.LCNF.Passes import Lean.Compiler.LCNF.PrettyPrinter import Lean.Compiler.LCNF.ToDecl import Lean.Compiler.LCNF.Check diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean new file mode 100644 index 0000000000..bb5a4cb0f5 --- /dev/null +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2022 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Lean.Compiler.LCNF.PassManager +import Lean.Compiler.LCNF.PullLetDecls +import Lean.Compiler.LCNF.CSE + +namespace Lean.Compiler.LCNF + +@[cpass] +def pullInstancesInstaller : PassInstaller := + .installAfter `init (.mkPerDeclaration `pullInstances Decl.pullInstances) + +@[cpass] +def cseInstaller : PassInstaller := + .installAfter `pullInstances (.mkPerDeclaration `cse Decl.cse) + +end Lean.Compiler.LCNF