From c1949e05e0b79f6c51faea92b6898132aa688a55 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 1 Sep 2022 00:16:52 +0200 Subject: [PATCH] feat: migrate to new pass manager --- src/Lean/Compiler/LCNF/Main.lean | 1 + src/Lean/Compiler/LCNF/Passes.lean | 20 ++++++++++++++++++++ 2 files changed, 21 insertions(+) create mode 100644 src/Lean/Compiler/LCNF/Passes.lean 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