-
Notifications
You must be signed in to change notification settings - Fork 25
/
Tracing.lean
160 lines (128 loc) · 5.05 KB
/
Tracing.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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
/-
Copyright (c) 2021 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/
import Aesop.Util.Basic
import Lean.Elab.Term
import Lean.Meta.Tactic.Simp
open Lean Lean.Meta
namespace Aesop
structure TraceOption where
traceClass : Name
option : Lean.Option Bool
deriving Inhabited
def registerTraceOption (traceName : Name) (descr : String) :
IO TraceOption := do
let option ← Option.register (`trace.aesop ++ traceName) {
defValue := false
group := "trace"
descr
}
return { traceClass := `aesop ++ traceName, option }
namespace TraceOption
def isEnabled [Monad m] [MonadOptions m] (opt : TraceOption) : m Bool :=
return opt.option.get (← getOptions)
def withEnabled [Monad m] [MonadWithOptions m] (opt : TraceOption) (k : m α) :
m α := do
withOptions (λ opts => opt.option.set opts true) k
initialize steps : TraceOption ←
registerTraceOption .anonymous
"(aesop) Print actions taken by Aesop during the proof search."
initialize ruleSet : TraceOption ←
registerTraceOption `ruleSet
"(aesop) Print the rule set before starting the search."
initialize proof : TraceOption ←
registerTraceOption `proof
"(aesop) If the search is successful, print the produced proof term."
initialize tree : TraceOption ←
registerTraceOption `tree
"(aesop) Once the search has concluded (successfully or unsuccessfully), print the final search tree."
initialize extraction : TraceOption ←
registerTraceOption `extraction
"(aesop) Print a trace of the proof extraction procedure."
initialize profile : TraceOption ←
registerTraceOption `profile
"(aesop) If the search is successful, print a summary of where Aesop spent its time. Enable the `profiler` and `trace.aesop` options for finer-grained information."
end TraceOption
section
open Lean.Elab Lean.Elab.Term
private def isFullyQualifiedGlobalName (n : Name) : MacroM Bool :=
return (← Macro.resolveGlobalName n).any (·.fst == n)
def resolveTraceOption (stx : Ident) : MacroM Name :=
withRef stx do
let n := stx.getId
let fqn := ``TraceOption ++ n
if ← isFullyQualifiedGlobalName fqn then
return fqn
else
return n
macro "aesop_trace![" opt:ident "] " msg:(interpolatedStr(term) <|> term) :
doElem => do
let opt ← mkIdent <$> resolveTraceOption opt
let msg := msg.raw
let msg ← if msg.getKind == interpolatedStrKind then
`(m! $(⟨msg⟩):interpolatedStr)
else
`(toMessageData ($(⟨msg⟩)))
`(doElem| Lean.addTrace (Aesop.TraceOption.traceClass $opt) $msg)
macro "aesop_trace[" opt:ident "] "
msg:(interpolatedStr(term) <|> Parser.Term.do <|> term) : doElem => do
let msg := msg.raw
let opt ← mkIdent <$> resolveTraceOption opt
match msg with
| `(do $action) =>
`(doElem| do
if ← Aesop.TraceOption.isEnabled $opt then
$action)
| _ =>
`(doElem| do
if ← Aesop.TraceOption.isEnabled $opt then
aesop_trace![$opt] $(⟨msg⟩))
end
def ruleSuccessEmoji := checkEmoji
def ruleFailureEmoji := crossEmoji
def ruleProvedEmoji := "🏁"
def ruleErrorEmoji := bombEmoji
def rulePostponedEmoji := "⏳️"
def ruleSkippedEmoji := "⏩️"
def nodeUnknownEmoji := "❓️"
def nodeProvedEmoji := ruleProvedEmoji
def nodeUnprovableEmoji := ruleFailureEmoji
def newNodeEmoji := "🆕"
def exceptRuleResultToEmoji (toEmoji : α → String) : Except ε α → String
| .error _ => ruleFailureEmoji
| .ok r => toEmoji r
section
variable [Monad m] [MonadTrace m] [MonadLiftT BaseIO m] [MonadLiftT IO m]
[MonadRef m] [AddMessageContext m] [MonadOptions m] [MonadExcept ε m]
@[inline, always_inline]
def withAesopTraceNode (opt : TraceOption)
(msg : Except ε α → m MessageData) (k : m α) (collapsed := true) : m α :=
withTraceNode opt.traceClass msg k collapsed
@[inline, always_inline]
def withConstAesopTraceNode (opt : TraceOption) (msg : m MessageData) (k : m α)
(collapsed := true) : m α :=
withAesopTraceNode opt (λ _ => msg) k collapsed
end
def traceSimpTheoremTreeContents (t : SimpTheoremTree) (opt : TraceOption) :
CoreM Unit := do
if ! (← opt.isEnabled) then
return
for e in t.values.map (toString ·.origin.key) |>.qsortOrd do
aesop_trace![opt] e
def traceSimpTheorems (s : SimpTheorems) (opt : TraceOption) : CoreM Unit := do
if ! (← opt.isEnabled) then
return
withConstAesopTraceNode opt (return "Erased entries") do
aesop_trace![opt] "(Note: even if these entries appear in the sections below, they will not be used by simp.)"
for e in PersistentHashSet.toArray s.erased |>.map (toString ·.key) |>.qsortOrd do
aesop_trace![opt] e
withConstAesopTraceNode opt (return "Pre lemmas") do
traceSimpTheoremTreeContents s.pre opt
withConstAesopTraceNode opt (return "Post lemmas") do
traceSimpTheoremTreeContents s.post opt
withConstAesopTraceNode opt (return "Constants to unfold") do
for e in PersistentHashSet.toArray s.toUnfold |>.map toString |>.qsortOrd do
aesop_trace![opt] e
end Aesop