diff --git a/src/Lean/Compiler/LCNF/CSE.lean b/src/Lean/Compiler/LCNF/CSE.lean index a9bb844498..19ff3d5582 100644 --- a/src/Lean/Compiler/LCNF/CSE.lean +++ b/src/Lean/Compiler/LCNF/CSE.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.Compiler.LCNF.CompilerM import Lean.Compiler.LCNF.ToExpr +import Lean.Compiler.LCNF.PassManager namespace Lean.Compiler.LCNF @@ -98,4 +99,10 @@ def Decl.cse (decl : Decl) : CompilerM Decl := do let value ← decl.value.cse return { decl with value } +def cse : Pass := + .mkPerDeclaration `cse Decl.cse + +builtin_initialize + registerTraceClass `Compiler.cse (inherited := true) + end Lean.Compiler.LCNF diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean index 69c219c6b2..f44e43028e 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -66,6 +66,9 @@ def run (declNames : Array Name) : CompilerM (Array Decl) := do decls ← pass.run decls checkpoint pass.name decls saveStage1Decls decls + if (← Lean.isTracingEnabledFor `Compiler.result) then + for decl in decls do + Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl decl}" return decls end PassManager @@ -77,10 +80,8 @@ def compileStage1Impl (declNames : Array Name) : CoreM (Array Decl) := builtin_initialize registerTraceClass `Compiler.init (inherited := true) - registerTraceClass `Compiler.simp (inherited := true) - registerTraceClass `Compiler.pullInstances (inherited := true) - registerTraceClass `Compiler.cse (inherited := true) registerTraceClass `Compiler.test (inherited := true) + registerTraceClass `Compiler.result (inherited := true) registerTraceClass `Compiler.jp end Lean.Compiler.LCNF diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean index 409a78036d..e537863017 100644 --- a/src/Lean/Compiler/LCNF/PassManager.lean +++ b/src/Lean/Compiler/LCNF/PassManager.lean @@ -37,6 +37,9 @@ namespace PassInstaller def installAtEnd (p : Pass) : PassInstaller where install passes := return passes.push p +def append (passesNew : Array Pass) : PassInstaller where + install passes := return passes ++ passesNew + def installAfter (targetName : Name) (p : Pass) : PassInstaller where install passes := if let some idx := passes.findIdx? (·.name == targetName) then diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index 5b16202221..97b2786b6e 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -13,23 +13,7 @@ import Lean.Compiler.LCNF.ReduceJpArity namespace Lean.Compiler.LCNF @[cpass] -def pullInstancesInstaller : PassInstaller := - .installAfter `init (.mkPerDeclaration `pullInstances Decl.pullInstances) - -@[cpass] -def cseInstaller : PassInstaller := - .installAfter `pullInstances (.mkPerDeclaration `cse Decl.cse) - -@[cpass] -def simpInstaller : PassInstaller := - .installAfter `cse (.mkPerDeclaration `simp Decl.simp) - -@[cpass] -def toJoinPointInstaller : PassInstaller := - .installAfter `simp (.mkPerDeclaration `pullFunDecls Decl.pullFunDecls) - -@[cpass] -def reduceJpArityInstaller : PassInstaller := - .installAfter `pullFunDecls (.mkPerDeclaration `reduceJpArity Decl.reduceJpArity) +def builtin : PassInstaller := + .append #[pullInstances, cse, simp, pullFunDecls, reduceJpArity, simp] end Lean.Compiler.LCNF diff --git a/src/Lean/Compiler/LCNF/PullFunDecls.lean b/src/Lean/Compiler/LCNF/PullFunDecls.lean index 294a546e82..f5b86e4101 100644 --- a/src/Lean/Compiler/LCNF/PullFunDecls.lean +++ b/src/Lean/Compiler/LCNF/PullFunDecls.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.Compiler.LCNF.CompilerM import Lean.Compiler.LCNF.DependsOn +import Lean.Compiler.LCNF.PassManager namespace Lean.Compiler.LCNF namespace PullFunDecls @@ -179,6 +180,9 @@ def Decl.pullFunDecls (decl : Decl) : CompilerM Decl := do let value ← attach ps value |>.run' [] return { decl with value } +def pullFunDecls : Pass := + .mkPerDeclaration `pullFunDecls Decl.pullFunDecls + builtin_initialize registerTraceClass `Compiler.pullFunDecls (inherited := true) diff --git a/src/Lean/Compiler/LCNF/PullLetDecls.lean b/src/Lean/Compiler/LCNF/PullLetDecls.lean index 7a10f2c893..6447ba0459 100644 --- a/src/Lean/Compiler/LCNF/PullLetDecls.lean +++ b/src/Lean/Compiler/LCNF/PullLetDecls.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura import Lean.Compiler.LCNF.CompilerM import Lean.Compiler.LCNF.DependsOn import Lean.Compiler.LCNF.Types +import Lean.Compiler.LCNF.PassManager namespace Lean.Compiler.LCNF namespace PullLetDecls @@ -107,4 +108,10 @@ def Decl.pullInstances (decl : Decl) : CompilerM Decl := else return false +def pullInstances : Pass := + .mkPerDeclaration `pullInstances Decl.pullInstances + +builtin_initialize + registerTraceClass `Compiler.pullInstances (inherited := true) + end Lean.Compiler.LCNF diff --git a/src/Lean/Compiler/LCNF/ReduceJpArity.lean b/src/Lean/Compiler/LCNF/ReduceJpArity.lean index 2868f5ecab..1c359b1fb7 100644 --- a/src/Lean/Compiler/LCNF/ReduceJpArity.lean +++ b/src/Lean/Compiler/LCNF/ReduceJpArity.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.Compiler.LCNF.CompilerM import Lean.Compiler.LCNF.InferType +import Lean.Compiler.LCNF.PassManager namespace Lean.Compiler.LCNF /-! @@ -69,6 +70,9 @@ def Decl.reduceJpArity (decl : Decl) : CompilerM Decl := do let value ← reduce decl.value |>.run {} return { decl with value } +def reduceJpArity : Pass := + .mkPerDeclaration `reduceJpArity Decl.reduceJpArity + builtin_initialize registerTraceClass `Compiler.reduceJpArity (inherited := true) diff --git a/src/Lean/Compiler/LCNF/Simp.lean b/src/Lean/Compiler/LCNF/Simp.lean index 743e322638..f10753fd77 100644 --- a/src/Lean/Compiler/LCNF/Simp.lean +++ b/src/Lean/Compiler/LCNF/Simp.lean @@ -10,6 +10,7 @@ import Lean.Compiler.LCNF.ElimDead import Lean.Compiler.LCNF.Bind import Lean.Compiler.LCNF.PrettyPrinter import Lean.Compiler.LCNF.Stage1 +import Lean.Compiler.LCNF.PassManager namespace Lean.Compiler.LCNF namespace Simp @@ -769,12 +770,13 @@ partial def Decl.simp (decl : Decl) : CompilerM Decl := do else return decl +def simp : Pass := + .mkPerDeclaration `simp Decl.simp + builtin_initialize - registerTraceClass `Compiler.simp.inline - registerTraceClass `Compiler.simp.inline.info + registerTraceClass `Compiler.simp (inherited := true) registerTraceClass `Compiler.simp.stat registerTraceClass `Compiler.simp.step registerTraceClass `Compiler.simp.step.new - registerTraceClass `Compiler.simp.projInst end Lean.Compiler.LCNF \ No newline at end of file