/
Main.lean
106 lines (95 loc) · 4.11 KB
/
Main.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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
import Lean.Compiler.LCNF.PullLetDecls
import Lean.Compiler.LCNF.PhaseExt
import Lean.Compiler.LCNF.CSE
namespace Lean.Compiler.LCNF
/--
We do not generate code for `declName` if
- Its type is a proposition.
- Its type is a type former.
- It is tagged as `[macro_inline]`.
- It is a type class instance.
Remark: we still generate code for declarations tagged as `[inline]`
and `[specialize]` since they can be partially applied.
-/
def shouldGenerateCode (declName : Name) : CoreM Bool := do
if (← isCompIrrelevant |>.run') then return false
let some info ← getDeclInfo? declName | return false
unless info.hasValue do return false
let env ← getEnv
if isExtern env declName then return false
if hasMacroInlineAttribute env declName then return false
if (← Meta.isMatcher declName) then return false
if isCasesOnRecursor env declName then return false
-- TODO: check if type class instance
return true
where
isCompIrrelevant : MetaM Bool := do
let info ← getConstInfo declName
Meta.isProp info.type <||> Meta.isTypeFormerType info.type
/--
A checkpoint in code generation to print all declarations in between
compiler passes in order to ease debugging.
The trace can be viewed with `set_option trace.Compiler.step true`.
-/
def checkpoint (stepName : Name) (decls : Array Decl) : CompilerM Unit := do
for decl in decls do
trace[Compiler.stat] "{decl.name} : {decl.size}"
withOptions (fun opts => opts.setBool `pp.motives.pi false) do
let clsName := `Compiler ++ stepName
if (← Lean.isTracingEnabledFor clsName) then
Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl' decl}"
if compiler.check.get (← getOptions) then
decl.check
if compiler.check.get (← getOptions) then
checkDeadLocalDecls decls
namespace PassManager
def run (declNames : Array Name) : CompilerM (Array Decl) := withAtLeastMaxRecDepth 8192 do
/-
Note: we need to increase the recursion depth because we currently do to save phase1
declarations in .olean files. Then, we have to recursively compile all dependencies,
and it often creates a very deep recursion.
Moreover, some declarations get very big during simplification.
-/
let declNames ← declNames.filterM (shouldGenerateCode ·)
if declNames.isEmpty then return #[]
let mut decls ← declNames.mapM toDecl
decls := markRecDecls decls
let manager ← getPassManager
for pass in manager.passes do
decls ← withTraceNode `Compiler (fun _ => return m!"new compiler phase: {pass.phase}, pass: {pass.name}") do
withPhase pass.phase <| pass.run decls
withPhase pass.phaseOut <| checkpoint pass.name decls
if (← Lean.isTracingEnabledFor `Compiler.result) then
for decl in decls do
-- We display the declaration saved in the environment because the names have been normalized
let some decl' ← getDeclAt? decl.name .mono | unreachable!
Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl'}"
return decls
end PassManager
def compile (declNames : Array Name) : CoreM (Array Decl) :=
CompilerM.run <| PassManager.run declNames
def showDecl (phase : Phase) (declName : Name) : CoreM Format := do
let some decl ← getDeclAt? declName phase | return "<not-available>"
ppDecl' decl
@[export lean_lcnf_compile_decls]
def main (declNames : List Name) : CoreM Unit := do
profileitM Exception "compilation new" (← getOptions) do
withTraceNode `Compiler (fun _ => return m!"compiling new: {declNames}") do
CompilerM.run <| discard <| PassManager.run declNames.toArray
builtin_initialize
registerTraceClass `Compiler.init (inherited := true)
registerTraceClass `Compiler.test (inherited := true)
registerTraceClass `Compiler.result (inherited := true)
registerTraceClass `Compiler.jp
end Lean.Compiler.LCNF