0 | module Core.Context.Log
  1 |
  2 | import public Core.Context
  3 | import Core.Options
  4 |
  5 | import Data.String
  6 | import Libraries.Data.StringMap
  7 |
  8 | import System.Clock
  9 |
 10 | %default covering
 11 |
 12 | -- if this function is called, then logging must be enabled.
 13 | %inline
 14 | export
 15 | logString : String -> Nat -> String -> Core ()
 16 | logString "" n msg = coreLift $ putStrLn
 17 |     $ "LOG " ++ show n ++ ": " ++ msg
 18 | logString str n msg = coreLift $ putStrLn
 19 |     $ "LOG " ++ str ++ ":" ++ show n ++ ": " ++ msg
 20 |
 21 | %inline
 22 | export
 23 | logString' : LogLevel -> String -> Core ()
 24 | logString' lvl =
 25 |   logString (fastConcat (intersperse "." (topics lvl)) ++ ":")
 26 |             (verbosity lvl)
 27 |
 28 | export
 29 | logging' : {auto c : Ref Ctxt Defs} ->
 30 |            LogLevel -> Core Bool
 31 | logging' lvl = do
 32 |     opts <- getSession
 33 |     pure $ verbosity lvl == 0 || (logEnabled opts && keepLog lvl (logLevel opts))
 34 |
 35 | export
 36 | unverifiedLogging : {auto c : Ref Ctxt Defs} ->
 37 |                     String -> Nat -> Core Bool
 38 | unverifiedLogging str Z = pure True
 39 | unverifiedLogging str n = do
 40 |     opts <- getSession
 41 |     pure $ logEnabled opts && keepLog (mkUnverifiedLogLevel str n) (logLevel opts)
 42 |
 43 | %inline
 44 | export
 45 | logging : {auto c : Ref Ctxt Defs} ->
 46 |           LogTopic -> Nat -> Core Bool
 47 | logging s n = unverifiedLogging s.topic n
 48 |
 49 | ||| Log message with a term, translating back to human readable names first.
 50 | export
 51 | logTerm : {vars : _} ->
 52 |           {auto c : Ref Ctxt Defs} ->
 53 |           LogTopic -> Nat -> Lazy String -> Term vars -> Core ()
 54 | logTerm s n msg tm
 55 |     = when !(logging s n)
 56 |         $ do tm' <- toFullNames tm
 57 |              logString s.topic n $ msg ++ ": " ++ show tm'
 58 |
 59 | export
 60 | log' : {auto c : Ref Ctxt Defs} ->
 61 |        LogLevel -> Lazy String -> Core ()
 62 | log' lvl msg
 63 |     = when !(logging' lvl)
 64 |         $ logString' lvl msg
 65 |
 66 | ||| Log a message with the given log level. Use increasingly
 67 | ||| high log level numbers for more granular logging.
 68 | |||
 69 | ||| If you want to use some `Core` computation to produce a message string, use `logC`.
 70 | ||| I.e. instead of `log "topic" 10 "message \{show !(toFullNames fn)}"` use
 71 | ||| `logC "topic" 10 $ do pure ""message \{show !(toFullNames fn)}""`.
 72 | ||| This will enfore that additional computation happends only when needed.
 73 | ||| `do` before `pure` in this case ensures the correct bounds.
 74 | export
 75 | log : {auto c : Ref Ctxt Defs} ->
 76 |       LogTopic -> Nat -> Lazy String -> Core ()
 77 | log s n msg
 78 |     = when !(logging s n)
 79 |         $ logString s.topic n msg
 80 |
 81 | export
 82 | unverifiedLogC : {auto c : Ref Ctxt Defs} ->
 83 |                  String -> Nat -> Core String -> Core ()
 84 | unverifiedLogC str n cmsg
 85 |     = when !(unverifiedLogging str n)
 86 |         $ do msg <- cmsg
 87 |              logString str n msg
 88 |
 89 | %inline
 90 | export
 91 | logC : {auto c : Ref Ctxt Defs} ->
 92 |        LogTopic -> Nat -> Core String -> Core ()
 93 | logC s = unverifiedLogC s.topic
 94 |
 95 | nano : Integer
 96 | nano = 1000000000
 97 |
 98 | micro : Integer
 99 | micro = 1000000
100 |
101 | export
102 | logTimeOver : Integer -> Core String -> Core a -> Core a
103 | logTimeOver nsecs str act
104 |     = do clock <- coreLift (clockTime Process)
105 |          let t = seconds clock * nano + nanoseconds clock
106 |          res <- act
107 |          clock <- coreLift (clockTime Process)
108 |          let t' = seconds clock * nano + nanoseconds clock
109 |          let time = t' - t
110 |          when (time > nsecs) $
111 |            assert_total $ -- We're not dividing by 0
112 |               do str' <- str
113 |                  coreLift $ putStrLn $ "TIMING " ++ str' ++ ": " ++
114 |                           show (time `div` nano) ++ "." ++
115 |                           addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
116 |                           "s"
117 |          pure res
118 |   where
119 |     addZeros : List Char -> String
120 |     addZeros [] = "000"
121 |     addZeros [x] = "00" ++ cast x
122 |     addZeros [x,y] = "0" ++ cast x ++ cast y
123 |     addZeros str = pack str
124 |
125 | export
126 | logTimeWhen : {auto c : Ref Ctxt Defs} ->
127 |               Bool -> Nat -> Lazy String -> Core a -> Core a
128 | logTimeWhen p lvl str act
129 |     = if p
130 |          then do clock <- coreLift (clockTime Process)
131 |                  let t = seconds clock * nano + nanoseconds clock
132 |                  res <- act
133 |                  clock <- coreLift (clockTime Process)
134 |                  let t' = seconds clock * nano + nanoseconds clock
135 |                  let time = t' - t
136 |                  assert_total $ -- We're not dividing by 0
137 |                     coreLift $ do
138 |                       let header = "TIMING " ++ replicate lvl '+' ++ ifThenElse (0 < lvl) " " ""
139 |                       putStrLn $ header ++ str ++ ": " ++
140 |                              show (time `div` nano) ++ "." ++
141 |                              addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
142 |                              "s"
143 |                  pure res
144 |          else act
145 |   where
146 |     addZeros : List Char -> String
147 |     addZeros [] = "000"
148 |     addZeros [x] = "00" ++ cast x
149 |     addZeros [x,y] = "0" ++ cast x ++ cast y
150 |     addZeros str = pack str
151 |
152 | logTimeRecord' : {auto c : Ref Ctxt Defs} ->
153 |                  String -> Core a -> Core a
154 | logTimeRecord' key act
155 |     = do clock <- coreLift (clockTime Process)
156 |          let t = seconds clock * nano + nanoseconds clock
157 |          res <- act
158 |          clock <- coreLift (clockTime Process)
159 |          let t' = seconds clock * nano + nanoseconds clock
160 |          let time = t' - t
161 |          defs <- get Ctxt
162 |          let tot = case lookup key (timings defs) of
163 |                         Nothing => 0
164 |                         Just (_, t) => t
165 |          put Ctxt ({ timings $= insert key (False, tot + time) } defs)
166 |          pure res
167 |
168 | -- for ad-hoc profiling, record the time the action takes and add it
169 | -- to the time for the given category
170 | export
171 | logTimeRecord : {auto c : Ref Ctxt Defs} ->
172 |                 String -> Core a -> Core a
173 | logTimeRecord key act
174 |     = do defs <- get Ctxt
175 |          -- Only record if we're not currently recording that key
176 |          case lookup key (timings defs) of
177 |               Just (True, t) => act
178 |               Just (False, t)
179 |                 => do put Ctxt ({ timings $= insert key (True, t) } defs)
180 |                       logTimeRecord' key act
181 |               Nothing
182 |                 => logTimeRecord' key act
183 |
184 | export
185 | showTimeRecord : {auto c : Ref Ctxt Defs} ->
186 |                  Core ()
187 | showTimeRecord
188 |     = do defs <- get Ctxt
189 |          traverse_ showTimeLog (toList (timings defs))
190 |   where
191 |     addZeros : List Char -> String
192 |     addZeros [] = "000"
193 |     addZeros [x] = "00" ++ cast x
194 |     addZeros [x,y] = "0" ++ cast x ++ cast y
195 |     addZeros str = pack str
196 |
197 |     showTimeLog : (String, (Bool, Integer)) -> Core ()
198 |     showTimeLog (key, (_, time))
199 |         = do coreLift $ putStr (key ++ ": ")
200 |              assert_total $ -- We're not dividing by 0
201 |                     coreLift $ putStrLn $ show (time `div` nano) ++ "." ++
202 |                                addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
203 |                                "s"
204 |
205 | export
206 | logTime : {auto c : Ref Ctxt Defs} ->
207 |           Nat -> Lazy String -> Core a -> Core a
208 | logTime lvl str act
209 |     = do opts <- getSession
210 |          logTimeWhen (maybe False (lvl <=) (logTimings opts)) lvl str act
211 |