0 | module Core.Options.Log
2 | import public Data.List
4 | import public Data.Maybe
5 | import Libraries.Data.StringMap
6 | import Libraries.Data.StringTrie
9 | import Libraries.Text.PrettyPrint.Prettyprinter
10 | import Libraries.Text.PrettyPrint.Prettyprinter.Util
38 | knownTopics : List (String, Maybe String)
40 | ("auto", Just "Auto proof search"),
41 | ("auto.determining", Just "Checking that interface's determining argument are concrete"),
42 | ("builtin.Natural", Just "Log each encountered %builtin Natural declaration."),
43 | ("builtin.NaturalToInteger", Just "Log each encountered %builtin NaturalToInteger declaration."),
44 | ("builtin.IntegerToNatural", Just "Log each encountered %builtin IntegerToNatural declaration."),
45 | ("compile.execute", Nothing),
46 | ("compile.export", Just "Log each name exported using %export"),
47 | ("compile.casetree", Nothing),
48 | ("compile.casetree.clauses", Nothing),
49 | ("compile.casetree.getpmdef", Nothing),
50 | ("compile.casetree.intermediate", Nothing),
51 | ("compile.casetree.measure", Just "Log the node counts of each runtime case tree."),
52 | ("compile.casetree.missing", Just "Log when we add an error case for uncovered branches."),
53 | ("compile.casetree.partition", Nothing),
54 | ("compile.casetree.pick", Nothing),
55 | ("compiler.const-fold", Just "Log definitions before and after constant folding."),
56 | ("compiler.cse", Just "Log information about common sub-expression elimination."),
57 | ("compiler.identity", Just "Log definitions that are equivalent to identity at runtime."),
58 | ("compiler.inline.eval", Just "Log function definitions before and after inlining."),
59 | ("compiler.inline.heuristic", Just "Log names the inlining heuristic(s) have decided to inline."),
60 | ("compiler.inline.io_bind", Just "Log the attempts to inline `io_bind`."),
61 | ("compiler.interpreter", Just "Log the call-stack of the VMCode interpreter."),
62 | ("compiler.javascript.doc", Just "Generating doc comments for the JS backend."),
63 | ("compiler.newtype.world", Just "Inlining matches on newtypes."),
64 | ("compiler.refc", Nothing),
65 | ("compiler.refc.cc", Nothing),
66 | ("compiler.scheme.chez", Nothing),
67 | ("coverage", Nothing),
68 | ("coverage.empty", Nothing),
69 | ("coverage.missing", Nothing),
70 | ("coverage.recover", Nothing),
71 | ("declare.data", Nothing),
72 | ("declare.data.constructor", Nothing),
73 | ("declare.data.parameters", Nothing),
74 | ("declare.def", Nothing),
75 | ("declare.def.alias", Nothing),
76 | ("declare.def.clause", Nothing),
77 | ("declare.def.clause.impossible", Nothing),
78 | ("declare.def.clause.with", Nothing),
79 | ("declare.def.impossible", Nothing),
80 | ("declare.def.lhs", Nothing),
81 | ("declare.def.lhs.implicits", Nothing),
82 | ("declare.param", Nothing),
83 | ("declare.record", Nothing),
84 | ("declare.record.field", Nothing),
85 | ("declare.record.parameters", Just "Showing the implicitlty bound parameters"),
86 | ("declare.record.projection", Nothing),
87 | ("declare.record.projection.prefix", Nothing),
88 | ("declare.record.projection.claim", Just "Showing the clause of an elaborated projection function"),
89 | ("declare.record.projection.clause", Just "Showing the clause of an elaborated projection function"),
90 | ("declare.type", Nothing),
91 | ("desugar.idiom", Nothing),
92 | ("desugar.failing", Just "Log result of desugaring a `failing' block"),
93 | ("desugar.fixity", Just "Log result of desugaring a fixity declaration"),
94 | ("desugar.lhs", Just "Log result of desugaring a left hand side"),
95 | ("doc.data", Nothing),
96 | ("doc.implementation", Nothing),
97 | ("doc.record", Nothing),
98 | ("doc.module", Nothing),
99 | ("doc.module.definitions", Nothing),
101 | ("elab.ambiguous", Nothing),
102 | ("elab.app.var", Nothing),
103 | ("elab.app.dot", Just "Dealing with forced expressions when elaborating applications"),
104 | ("elab.app.lhs", Nothing),
105 | ("elab.as", Nothing),
106 | ("elab.bindnames", Nothing),
107 | ("elab.binder", Nothing),
108 | ("elab.case", Nothing),
109 | ("elab.def.local", Nothing),
110 | ("elab.delay", Nothing),
111 | ("elab.failing", Just "Elaborating a 'failing' block."),
112 | ("elab.hole", Nothing),
113 | ("elab.implicits", Nothing),
114 | ("elab.implementation", Nothing),
115 | ("elab.interface", Nothing),
116 | ("elab.interface.default", Nothing),
117 | ("elab.local", Nothing),
118 | ("elab.prune", Nothing),
119 | ("elab.record", Nothing),
120 | ("elab.retry", Nothing),
121 | ("elab.rewrite", Nothing),
122 | ("elab.unify", Nothing),
123 | ("elab.update", Nothing),
124 | ("elab.with", Nothing),
125 | ("eval.casetree", Nothing),
126 | ("eval.casetree.stuck", Nothing),
127 | ("eval.def.underapplied", Just "Evaluating definitions (unavailable by default, edit Core.Normalise.Eval & recompile)"),
128 | ("eval.def.stuck", Just "Evaluating definitions (unavailable by default, edit Core.Normalise.Eval & recompile)"),
129 | ("eval.eta", Nothing),
130 | ("eval.ref", Just "Evaluating refs (unavailable by default, edit Core.Normalise.Eval & recompile)"),
131 | ("eval.stuck", Nothing),
132 | ("eval.stuck.outofscope", Nothing),
133 | ("ide-mode.completion", Just "Autocompletion requests"),
134 | ("ide-mode.hole", Just "Displaying hole contexts"),
135 | ("ide-mode.highlight", Nothing),
136 | ("ide-mode.highlight.alias", Nothing),
137 | ("ide-mode.send", Just "The IDE mode's SExp traffic"),
138 | ("ide-mode.recv", Just "Messages received by the IDE mode"),
139 | ("import", Nothing),
140 | ("import.file", Nothing),
141 | ("interaction.casesplit", Nothing),
142 | ("interaction.generate", Nothing),
143 | ("interaction.search", Nothing),
144 | ("metadata.names", Nothing),
145 | ("module", Nothing),
146 | ("module.hash", Nothing),
147 | ("package.depends", Just "Log which packages are being added"),
148 | ("quantity", Nothing),
149 | ("quantity.hole", Nothing),
150 | ("quantity.hole.update", Nothing),
151 | ("reflection.reify", Just "Log what's happening when converting an `NF` to some real value"),
152 | ("repl.eval", Nothing),
153 | ("resugar.var", Just "Resugaring variables"),
154 | ("resugar.sectionL", Just "Resugaring left sections"),
155 | ("specialise", Just "Generating a partially-evaluated specialised version of a function"),
156 | ("specialise.declare", Just "Declaring our intention to specialise a function"),
157 | ("specialise.fail", Just "Generating the specialised function failed"),
158 | ("specialise.flags", Just "Listing the definition flags propagated to the specialised function"),
159 | ("totality", Nothing),
160 | ("totality.positivity", Nothing),
161 | ("totality.requirement", Nothing),
162 | ("totality.termination", Nothing),
163 | ("totality.termination.calc", Nothing),
164 | ("totality.termination.guarded", Nothing),
165 | ("totality.termination.sizechange", Nothing),
166 | ("totality.termination.sizechange.checkCall", Nothing),
167 | ("totality.termination.sizechange.checkCall.inPath", Nothing),
168 | ("totality.termination.sizechange.checkCall.inPathNot.restart", Nothing),
169 | ("totality.termination.sizechange.checkCall.inPathNot.return", Nothing),
170 | ("totality.termination.sizechange.inPath", Nothing),
171 | ("totality.termination.sizechange.isTerminating", Nothing),
172 | ("totality.termination.sizechange.needsChecking", Nothing),
173 | ("transform.lhs", Nothing),
174 | ("transform.rhs", Nothing),
175 | ("ttc.read", Nothing),
176 | ("ttc.write", Nothing),
177 | ("typesearch.equiv", Nothing),
178 | ("unelab.case", Just "Unelaborating a case block"),
179 | ("unelab.case.clause", Just "Unelaborating a case block's clauses"),
180 | ("unelab.var", Nothing),
181 | ("unify", Nothing),
182 | ("unify.application", Nothing),
183 | ("unify.binder", Nothing),
184 | ("unify.constant", Nothing),
185 | ("unify.constraint", Nothing),
186 | ("unify.delay", Nothing),
187 | ("unify.equal", Nothing),
188 | ("unify.head", Nothing),
189 | ("unify.hole", Nothing),
190 | ("unify.instantiate", Nothing),
191 | ("unify.invertible", Nothing),
192 | ("unify.meta", Nothing),
193 | ("unify.noeta", Nothing),
194 | ("unify.postpone", Nothing),
195 | ("unify.retry", Nothing),
196 | ("unify.search", Nothing),
197 | ("unify.unsolved", Nothing)
201 | helpTopics : String
202 | helpTopics = show $
vcat $
map helpTopic knownTopics
206 | helpTopic : (String, Maybe String) -> Doc Void
207 | helpTopic (str, mblurb)
208 | = let title = "+" <++> pretty str
209 | blurb = maybe [] ((::[]) . indent 2 . reflow) mblurb
210 | in vcat (title :: blurb)
213 | data KnownTopic : String -> Type where
214 | IsKnownTopic : IsJust (lookup s Log.knownTopics) => KnownTopic s
217 | record LogTopic where
218 | constructor MkLogTopic
220 | {auto 0 known : KnownTopic topic}
223 | fromString : (s : String) -> (0 _ : KnownTopic s) => LogTopic
224 | fromString = MkLogTopic
229 | data LogLevel : Type where
230 | MkLogLevel : List String -> Nat -> LogLevel
235 | mkLogLevel' : Maybe (List1 String) -> Nat -> LogLevel
236 | mkLogLevel' ps n = MkLogLevel (maybe [] forget ps) n
249 | mkUnverifiedLogLevel : (s : String) -> Nat -> LogLevel
250 | mkUnverifiedLogLevel "" = mkLogLevel' Nothing
251 | mkUnverifiedLogLevel ps = mkLogLevel' (Just (split (== '.') ps))
256 | mkLogLevel : LogTopic -> Nat -> LogLevel
257 | mkLogLevel s = mkUnverifiedLogLevel s.topic
262 | unsafeMkLogLevel : List String -> Nat -> LogLevel
263 | unsafeMkLogLevel = MkLogLevel
267 | topics : LogLevel -> List String
268 | topics (MkLogLevel ps _) = ps
272 | verbosity : LogLevel -> Nat
273 | verbosity (MkLogLevel _ n) = n
278 | withVerbosity : Nat -> LogLevel -> LogLevel
279 | withVerbosity n (MkLogLevel ps _) = MkLogLevel ps n
284 | Show LogLevel where
286 | show (MkLogLevel ps n) = case ps of
288 | _ => fastConcat (intersperse "." ps) ++ ":" ++ show n
291 | parseLogLevel : String -> Maybe LogLevel
292 | parseLogLevel str = do
293 | (c, n) <- let nns = split (== ':') str
297 | [] => pure (MkLogLevel [], n)
298 | [ns] => pure (mkUnverifiedLogLevel n, ns)
300 | lvl <- parsePositive n
301 | pure $
c (fromInteger lvl)
310 | LogLevels = StringTrie Nat
314 | defaultLogLevel : LogLevels
315 | defaultLogLevel = singleton [] 0
318 | insertLogLevel : LogLevel -> LogLevels -> LogLevels
319 | insertLogLevel (MkLogLevel ps n) = insert ps n
327 | keepLog : LogLevel -> LogLevels -> Bool
328 | keepLog (MkLogLevel _ Z) _ = True
329 | keepLog (MkLogLevel path n) levels = go path levels where
331 | go : List String -> StringTrie Nat -> Bool
332 | go path (MkStringTrie current) = here || there where
335 | here = case fromThis current of
340 | there = case path of
342 | (p :: rest) => fromMaybe False $
do
343 | assoc <- fromThat current
344 | next <- lookup p assoc
345 | pure $
go rest next