Skip to content

Commit 364eaff

Browse files
stefan-hoeckgallais
stefan-hoeck
and
gallais
authored
[ towards #1124 ] Statically enforced logging (#1402)
Co-authored-by: Guillaume ALLAIS <[email protected]>
1 parent 004cc45 commit 364eaff

File tree

12 files changed

+195
-37
lines changed

12 files changed

+195
-37
lines changed

‎src/Core/Context/Log.idr

Lines changed: 18 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,9 @@ import System.Clock
1313
export
1414
logTerm : {vars : _} ->
1515
{auto c : Ref Ctxt Defs} ->
16-
String -> Nat -> Lazy String -> Term vars -> Core ()
16+
(s : String) ->
17+
{auto 0 _ : KnownTopic s} ->
18+
Nat -> Lazy String -> Term vars -> Core ()
1719
logTerm str n msg tm
1820
= do opts <- getSession
1921
let lvl = mkLogLevel (logEnabled opts) str n
@@ -35,22 +37,32 @@ log' lvl msg
3537
||| high log level numbers for more granular logging.
3638
export
3739
log : {auto c : Ref Ctxt Defs} ->
38-
String -> Nat -> Lazy String -> Core ()
40+
(s : String) ->
41+
{auto 0 _ : KnownTopic s} ->
42+
Nat -> Lazy String -> Core ()
3943
log str n msg
4044
= do let lvl = mkLogLevel (logEnabled !getSession) str n
4145
log' lvl msg
4246

4347
export
44-
logC : {auto c : Ref Ctxt Defs} ->
45-
String -> Nat -> Core String -> Core ()
46-
logC str n cmsg
48+
unverifiedLogC : {auto c : Ref Ctxt Defs} ->
49+
(s : String) ->
50+
Nat -> Core String -> Core ()
51+
unverifiedLogC str n cmsg
4752
= do opts <- getSession
48-
let lvl = mkLogLevel (logEnabled opts) str n
53+
let lvl = mkUnverifiedLogLevel (logEnabled opts) str n
4954
if keepLog lvl (logEnabled opts) (logLevel opts)
5055
then do msg <- cmsg
5156
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
5257
else pure ()
5358

59+
export
60+
logC : {auto c : Ref Ctxt Defs} ->
61+
(s : String) ->
62+
{auto 0 _ : KnownTopic s} ->
63+
Nat -> Core String -> Core ()
64+
logC str = unverifiedLogC str
65+
5466
export
5567
logTimeOver : Integer -> Core String -> Core a -> Core a
5668
logTimeOver nsecs str act

‎src/Core/Core.idr

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -769,4 +769,3 @@ readFile fname =
769769
coreLift (File.readFile fname) >>= \case
770770
Right content => pure content
771771
Left err => throw $ FileErr fname err
772-

‎src/Core/Normalise.idr

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1173,7 +1173,9 @@ getArity defs env tm = getValArity defs env !(nf defs env tm)
11731173
export
11741174
logNF : {vars : _} ->
11751175
{auto c : Ref Ctxt Defs} ->
1176-
String -> Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()
1176+
(s : String) ->
1177+
{auto 0 _ : KnownTopic s} ->
1178+
Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()
11771179
logNF str n msg env tmnf
11781180
= do opts <- getSession
11791181
let lvl = mkLogLevel (logEnabled opts) str n
@@ -1202,15 +1204,19 @@ logTermNF' lvl msg env tm
12021204
export
12031205
logTermNF : {vars : _} ->
12041206
{auto c : Ref Ctxt Defs} ->
1205-
String -> Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
1207+
(s : String) ->
1208+
{auto 0 _ : KnownTopic s} ->
1209+
Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
12061210
logTermNF str n msg env tm
12071211
= do let lvl = mkLogLevel (logEnabled !getSession) str n
12081212
logTermNF' lvl msg env tm
12091213

12101214
export
12111215
logGlue : {vars : _} ->
12121216
{auto c : Ref Ctxt Defs} ->
1213-
String -> Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
1217+
(s : String) ->
1218+
{auto 0 _ : KnownTopic s} ->
1219+
Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
12141220
logGlue str n msg env gtm
12151221
= do opts <- getSession
12161222
let lvl = mkLogLevel (logEnabled opts) str n
@@ -1224,7 +1230,9 @@ logGlue str n msg env gtm
12241230
export
12251231
logGlueNF : {vars : _} ->
12261232
{auto c : Ref Ctxt Defs} ->
1227-
String -> Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
1233+
(s : String) ->
1234+
{auto 0 _ : KnownTopic s} ->
1235+
Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
12281236
logGlueNF str n msg env gtm
12291237
= do opts <- getSession
12301238
let lvl = mkLogLevel (logEnabled opts) str n
@@ -1239,7 +1247,9 @@ logGlueNF str n msg env gtm
12391247
export
12401248
logEnv : {vars : _} ->
12411249
{auto c : Ref Ctxt Defs} ->
1242-
String -> Nat -> String -> Env Term vars -> Core ()
1250+
(s : String) ->
1251+
{auto 0 _ : KnownTopic s} ->
1252+
Nat -> String -> Env Term vars -> Core ()
12431253
logEnv str n msg env
12441254
= do opts <- getSession
12451255
when (logEnabled opts &&

‎src/Core/Options/Log.idr

Lines changed: 140 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
module Core.Options.Log
22

3-
import Data.List
3+
import public Data.List
44
import Data.List1
5-
import Data.Maybe
5+
import public Data.Maybe
66
import Libraries.Data.StringMap
77
import Libraries.Data.StringTrie
88
import Data.Strings
@@ -34,6 +34,126 @@ import Libraries.Text.PrettyPrint.Prettyprinter
3434
----------------------------------------------------------------------------------
3535
-- INDIVIDUAL LOG LEVEL
3636

37+
public export
38+
knownTopics : List (String,String)
39+
knownTopics = [
40+
("auto", "some documentation of this option"),
41+
("builtin.Natural", "some documentation of this option"),
42+
("builtin.Natural.addTransform", "some documentation of this option"),
43+
("builtin.NaturalToInteger", "some documentation of this option"),
44+
("builtin.NaturalToInteger.addTransforms", "some documentation of this option"),
45+
("compile.casetree", "some documentation of this option"),
46+
("compiler.inline.eval", "some documentation of this option"),
47+
("compiler.refc", "some documentation of this option"),
48+
("compiler.refc.cc", "some documentation of this option"),
49+
("compiler.scheme.chez", "some documentation of this option"),
50+
("coverage", "some documentation of this option"),
51+
("coverage.empty", "some documentation of this option"),
52+
("coverage.missing", "some documentation of this option"),
53+
("coverage.recover", "some documentation of this option"),
54+
("declare.data", "some documentation of this option"),
55+
("declare.data.constructor", "some documentation of this option"),
56+
("declare.data.parameters", "some documentation of this option"),
57+
("declare.def", "some documentation of this option"),
58+
("declare.def.clause", "some documentation of this option"),
59+
("declare.def.clause.impossible", "some documentation of this option"),
60+
("declare.def.clause.with", "some documentation of this option"),
61+
("declare.def.impossible", "some documentation of this option"),
62+
("declare.def.lhs", "some documentation of this option"),
63+
("declare.def.lhs.implicits", "some documentation of this option"),
64+
("declare.param", "some documentation of this option"),
65+
("declare.record", "some documentation of this option"),
66+
("declare.record.field", "some documentation of this option"),
67+
("declare.record.projection", "some documentation of this option"),
68+
("declare.record.projection.prefix", "some documentation of this option"),
69+
("declare.type", "some documentation of this option"),
70+
("desugar.idiom", "some documentation of this option"),
71+
("doc.record", "some documentation of this option"),
72+
("elab", "some documentation of this option"),
73+
("elab.ambiguous", "some documentation of this option"),
74+
("elab.app.lhs", "some documentation of this option"),
75+
("elab.as", "some documentation of this option"),
76+
("elab.bindnames", "some documentation of this option"),
77+
("elab.binder", "some documentation of this option"),
78+
("elab.case", "some documentation of this option"),
79+
("elab.def.local", "some documentation of this option"),
80+
("elab.delay", "some documentation of this option"),
81+
("elab.hole", "some documentation of this option"),
82+
("elab.implicits", "some documentation of this option"),
83+
("elab.implementation", "some documentation of this option"),
84+
("elab.interface", "some documentation of this option"),
85+
("elab.interface.default", "some documentation of this option"),
86+
("elab.local", "some documentation of this option"),
87+
("elab.prun", "some documentation of this option"),
88+
("elab.prune", "some documentation of this option"),
89+
("elab.record", "some documentation of this option"),
90+
("elab.retry", "some documentation of this option"),
91+
("elab.rewrite", "some documentation of this option"),
92+
("elab.unify", "some documentation of this option"),
93+
("elab.update", "some documentation of this option"),
94+
("elab.with", "some documentation of this option"),
95+
("eval.casetree", "some documentation of this option"),
96+
("eval.casetree.stuck", "some documentation of this option"),
97+
("eval.eta", "some documentation of this option"),
98+
("eval.stuck", "some documentation of this option"),
99+
("idemode.hole", "some documentation of this option"),
100+
("ide-mode.highlight", "some documentation of this option"),
101+
("ide-mode.highlight.alias", "some documentation of this option"),
102+
("ide-mode.send", "some documentation of this option"),
103+
("import", "some documentation of this option"),
104+
("import.file", "some documentation of this option"),
105+
("interaction.casesplit", "some documentation of this option"),
106+
("interaction.generate", "some documentation of this option"),
107+
("interaction.search", "some documentation of this option"),
108+
("metadata.names", "some documentation of this option"),
109+
("module.hash", "some documentation of this option"),
110+
("quantity", "some documentation of this option"),
111+
("quantity.hole", "some documentation of this option"),
112+
("quantity.hole.update", "some documentation of this option"),
113+
("repl.eval", "some documentation of this option"),
114+
("specialise", "some documentation of this option"),
115+
("totality", "some documentation of this option"),
116+
("totality.positivity", "some documentation of this option"),
117+
("totality.termination", "some documentation of this option"),
118+
("totality.termination.calc", "some documentation of this option"),
119+
("totality.termination.guarded", "some documentation of this option"),
120+
("totality.termination.sizechange", "some documentation of this option"),
121+
("totality.termination.sizechange.checkCall", "some documentation of this option"),
122+
("totality.termination.sizechange.checkCall.inPath", "some documentation of this option"),
123+
("totality.termination.sizechange.checkCall.inPathNot.restart", "some documentation of this option"),
124+
("totality.termination.sizechange.checkCall.inPathNot.return", "some documentation of this option"),
125+
("totality.termination.sizechange.inPath", "some documentation of this option"),
126+
("totality.termination.sizechange.isTerminating", "some documentation of this option"),
127+
("totality.termination.sizechange.needsChecking", "some documentation of this option"),
128+
("transform.lhs", "some documentation of this option"),
129+
("transform.rhs", "some documentation of this option"),
130+
("ttc.read", "some documentation of this option"),
131+
("ttc.write", "some documentation of this option"),
132+
("typesearch.equiv", "some documentation of this option"),
133+
("unelab.case", "some documentation of this option"),
134+
("unify", "some documentation of this option"),
135+
("unify.application", "some documentation of this option"),
136+
("unify.binder", "some documentation of this option"),
137+
("unify.constant", "some documentation of this option"),
138+
("unify.constraint", "some documentation of this option"),
139+
("unify.delay", "some documentation of this option"),
140+
("unify.equal", "some documentation of this option"),
141+
("unify.head", "some documentation of this option"),
142+
("unify.hole", "some documentation of this option"),
143+
("unify.instantiate", "some documentation of this option"),
144+
("unify.invertible", "some documentation of this option"),
145+
("unify.meta", "some documentation of this option"),
146+
("unify.noeta", "some documentation of this option"),
147+
("unify.postpone", "some documentation of this option"),
148+
("unify.retry", "some documentation of this option"),
149+
("unify.search", "some documentation of this option"),
150+
("unify.unsolved", "some documentation of this option")
151+
]
152+
153+
public export
154+
KnownTopic : String -> Type
155+
KnownTopic s = IsJust (lookup s knownTopics)
156+
37157
||| An individual log level is a pair of a list of non-empty strings and a number.
38158
||| We keep the representation opaque to force users to call the smart constructor
39159
export
@@ -49,11 +169,24 @@ mkLogLevel' ps n = MkLogLevel (maybe [] forget ps) n
49169
||| The smart constructor makes sure that the empty string is mapped to the empty
50170
||| list. This bypasses the fact that the function `split` returns a non-empty
51171
||| list no matter what.
172+
|||
173+
||| However, invoking this function comes without guarantees that
174+
||| the passed string corresponds to a known topic. For this,
175+
||| use `mkLogLevel`.
176+
|||
177+
||| Use this function to create user defined loglevels, for instance, during
178+
||| elaborator reflection.
179+
export
180+
mkUnverifiedLogLevel : Bool -> (s : String) -> Nat -> LogLevel
181+
mkUnverifiedLogLevel False _ = mkLogLevel' Nothing
182+
mkUnverifiedLogLevel _ "" = mkLogLevel' Nothing
183+
mkUnverifiedLogLevel _ ps = mkLogLevel' (Just (split (== '.') ps))
184+
185+
||| Like `mkUnverifiedLogLevel` but with a compile time check that
186+
||| the passed string is a known topic.
52187
export
53-
mkLogLevel : Bool -> String -> Nat -> LogLevel
54-
mkLogLevel False _ = mkLogLevel' Nothing
55-
mkLogLevel _ "" = mkLogLevel' Nothing
56-
mkLogLevel _ ps = mkLogLevel' (Just (split (== '.') ps))
188+
mkLogLevel : Bool -> (s : String) -> {auto 0 _ : KnownTopic s} -> Nat -> LogLevel
189+
mkLogLevel b s = mkUnverifiedLogLevel b s
57190

58191
||| The unsafe constructor should only be used in places where the topic has already
59192
||| been appropriately processed.
@@ -99,7 +232,7 @@ parseLogLevel str = do
99232
ns = tail nns in
100233
case ns of
101234
[] => pure (MkLogLevel [], n)
102-
[ns] => pure (mkLogLevel True n, ns)
235+
[ns] => pure (mkUnverifiedLogLevel True n, ns)
103236
_ => Nothing
104237
lvl <- parsePositive n
105238
pure $ c (fromInteger lvl)

‎src/Core/Unify.idr

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1135,14 +1135,14 @@ mutual
11351135
dumpArg env (MkClosure opts loc lenv tm)
11361136
= do defs <- get Ctxt
11371137
empty <- clearDefs defs
1138-
logTerm "" 0 "Term: " tm
1138+
logTerm "unify" 20 "Term: " tm
11391139
nf <- evalClosure empty (MkClosure opts loc lenv tm)
1140-
logNF "" 0 " " env nf
1140+
logNF "unify" 20 " " env nf
11411141
dumpArg env cl
11421142
= do defs <- get Ctxt
11431143
empty <- clearDefs defs
11441144
nf <- evalClosure empty cl
1145-
logNF "" 0 " " env nf
1145+
logNF "unify" 20 " " env nf
11461146

11471147
export
11481148
unifyNoEta : {auto c : Ref Ctxt Defs} ->
@@ -1161,11 +1161,11 @@ mutual
11611161
-- may prove useful again...
11621162
{-
11631163
when (logging ust) $
1164-
do log "" 0 $ "Constructor " ++ show !(toFullNames x) ++ " " ++ show loc
1165-
log "" 0 "ARGUMENTS:"
1164+
do log "unify" 20 $ "Constructor " ++ show !(toFullNames x) ++ " " ++ show loc
1165+
log "unify" 20 "ARGUMENTS:"
11661166
defs <- get Ctxt
11671167
traverse_ (dumpArg env) xs
1168-
log "" 0 "WITH:"
1168+
log "unify" 20 "WITH:"
11691169
traverse_ (dumpArg env) ys
11701170
-}
11711171
unifyArgs mode loc env (map snd xs) (map snd ys)

‎src/Core/UnifyState.idr

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -718,7 +718,9 @@ dumpHole' lvl hole
718718
export
719719
dumpConstraints : {auto u : Ref UST UState} ->
720720
{auto c : Ref Ctxt Defs} ->
721-
(topics : String) -> (verbosity : Nat) ->
721+
(topics : String) ->
722+
{auto 0 _ : KnownTopic topics} ->
723+
(verbosity : Nat) ->
722724
(all : Bool) ->
723725
Core ()
724726
dumpConstraints str n all

‎src/Idris/IDEMode/Holes.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ import Idris.Pretty
99

1010
import Idris.IDEMode.Commands
1111

12-
import Libraries.Data.String.Extra
12+
import Libraries.Data.String.Extra as L
1313
import Libraries.Utils.Term
1414

1515
%default covering
@@ -150,7 +150,7 @@ prettyHole defs env fn args ty
150150
map (\premise => prettyRigHole premise.multiplicity
151151
<+> prettyImpBracket premise.isImplicit (prettyName premise.name <++> colon <++> prettyTerm premise.type))
152152
hdata.context) <+> hardline
153-
<+> (pretty $ replicate 30 '-') <+> hardline
153+
<+> (pretty $ L.replicate 30 '-') <+> hardline
154154
<+> pretty (nameRoot $ hdata.name) <++> colon <++> prettyTerm hdata.type
155155

156156
sexpPremise : HolePremise -> SExp

‎src/Idris/ProcessIdr.idr

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -238,11 +238,11 @@ processMod srcf ttcf msg sourcecode
238238

239239
hs <- traverse readHash imps
240240
defs <- get Ctxt
241-
log "" 5 $ "Current hash " ++ show (ifaceHash defs)
242-
log "" 5 $ show (moduleNS modh) ++ " hashes:\n" ++
241+
log "module.hash" 5 $ "Current hash " ++ show (ifaceHash defs)
242+
log "module.hash" 5 $ show (moduleNS modh) ++ " hashes:\n" ++
243243
show (sort (map snd hs))
244244
imphs <- readImportHashes ttcf
245-
log "" 5 $ "Old hashes from " ++ ttcf ++ ":\n" ++ show (sort imphs)
245+
log "module.hash" 5 $ "Old hashes from " ++ ttcf ++ ":\n" ++ show (sort imphs)
246246

247247
-- If the old hashes are the same as the hashes we've just
248248
-- read from the imports, and the source file is older than

‎src/TTImp/Elab/RunElab.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -67,14 +67,14 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp
6767
elabCon defs "LogMsg" [topic, verb, str]
6868
= do topic' <- evalClosure defs topic
6969
verb' <- evalClosure defs verb
70-
logC !(reify defs topic') !(reify defs verb') $
70+
unverifiedLogC !(reify defs topic') !(reify defs verb') $
7171
do str' <- evalClosure defs str
7272
reify defs str'
7373
scriptRet ()
7474
elabCon defs "LogTerm" [topic, verb, str, tm]
7575
= do topic' <- evalClosure defs topic
7676
verb' <- evalClosure defs verb
77-
logC !(reify defs topic') !(reify defs verb') $
77+
unverifiedLogC !(reify defs topic') !(reify defs verb') $
7878
do str' <- evalClosure defs str
7979
tm' <- evalClosure defs tm
8080
pure $ !(reify defs str') ++ ": " ++

‎src/TTImp/ProcessTransform.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,9 +27,9 @@ processTransform eopts nest env fc tn_in lhs rhs
2727
tidx <- resolveName tn
2828
(_, (vars' ** (sub', env', nest', lhstm, lhsty))) <-
2929
checkLHS True top True tidx eopts nest env fc lhs
30-
logTerm "" 3 "Transform LHS" lhstm
30+
logTerm "transform.lhs" 3 "Transform LHS" lhstm
3131
rhstm <- wrapError (InRHS fc tn_in) $
3232
checkTermSub tidx InExpr (InTrans :: eopts) nest' env' env sub' rhs (gnf env' lhsty)
3333
clearHoleLHS
34-
logTerm "" 3 "Transform RHS" rhstm
34+
logTerm "transform.rhs" 3 "Transform RHS" rhstm
3535
addTransform fc (MkTransform tn env' lhstm rhstm)

0 commit comments

Comments
 (0)