0 | module IO.Async.Logging
  1 |
  2 | import IO.Async.Core
  3 | import Derive.Prelude
  4 |
  5 | %default total
  6 | %language ElabReflection
  7 |
  8 | public export
  9 | data LogLevel = Trace | Debug | Info | Warn | Error | Fatal
 10 |
 11 | %runElab derive "LogLevel" [Show,Eq,Ord]
 12 |
 13 | export
 14 | Interpolation LogLevel where interpolate = toLower . show
 15 |
 16 | public export
 17 | record Logger (0 e : Type) where
 18 |   constructor MkLogger
 19 |   logML : LogLevel -> Lazy (List String) -> Async e [] ()
 20 |
 21 | ||| Only log message of at least the given logging level.
 22 | export
 23 | filter : LogLevel -> Logger e -> Logger e
 24 | filter lvl x = MkLogger $ \l,s => case l >= lvl of
 25 |   True  => x.logML l s
 26 |   False => pure ()
 27 |
 28 | export
 29 | Semigroup (Logger e) where
 30 |   x <+> y = MkLogger $ \l,s => x.logML l s >> y.logML l s
 31 |
 32 | export
 33 | Monoid (Logger e) where
 34 |   neutral = MkLogger $ \_,_ => pure ()
 35 |
 36 | parameters {auto lg  : Logger e}
 37 |
 38 |   export
 39 |   logML : LogLevel -> Lazy (List String) -> Async e es ()
 40 |   logML l ss = weakenErrors $ lg.logML l ss 
 41 |
 42 |   export %inline
 43 |   log : LogLevel -> Lazy String -> Async e es ()
 44 |   log l s = logML l [s]
 45 |   
 46 |   export %inline
 47 |   trace : Lazy String -> Async e es ()
 48 |   trace = log Trace
 49 |   
 50 |   export %inline
 51 |   debug : Lazy String -> Async e es ()
 52 |   debug = log Debug
 53 |   
 54 |   export %inline
 55 |   info : Lazy String -> Async e es ()
 56 |   info = log Info
 57 |   
 58 |   export %inline
 59 |   warn : Lazy String -> Async e es ()
 60 |   warn = log Warn
 61 |   
 62 |   export %inline
 63 |   error : Lazy String -> Async e es ()
 64 |   error = log Error
 65 |   
 66 |   export %inline
 67 |   fatal : Lazy String -> Async e es ()
 68 |   fatal = log Fatal
 69 |   
 70 |   export %inline
 71 |   traceML : Lazy (List String) -> Async e es ()
 72 |   traceML = logML Trace
 73 |   
 74 |   export %inline
 75 |   debugML : Lazy (List String) -> Async e es ()
 76 |   debugML = logML Debug
 77 |   
 78 |   export %inline
 79 |   infoML : Lazy (List String) -> Async e es ()
 80 |   infoML = logML Info
 81 |   
 82 |   export %inline
 83 |   warnML : Lazy (List String) -> Async e es ()
 84 |   warnML = logML Warn
 85 |   
 86 |   export %inline
 87 |   errorML : Lazy (List String) -> Async e es ()
 88 |   errorML = logML Error
 89 |   
 90 |   export %inline
 91 |   fatalML : Lazy (List String) -> Async e es ()
 92 |   fatalML = logML Fatal
 93 |   
 94 |   export %inline
 95 |   ierror : Interpolation a => a -> Async e es ()
 96 |   ierror x = error (interpolate x)
 97 |   
 98 |   export %inline
 99 |   ifatal : Interpolation a => a -> Async e es ()
100 |   ifatal x = fatal (interpolate x)
101 |
102 | --------------------------------------------------------------------------------
103 | -- Loggable
104 | --------------------------------------------------------------------------------
105 |
106 | public export
107 | interface Loggable e t where
108 |   logLoggable : {0 es : _} -> t -> Async e es ()
109 |
110 | parameters {0 es     : List Type}
111 |            {auto lgs : All (Loggable e) es}
112 |
113 |   export
114 |   unerr : (dflt : t) -> Async e es t -> Async e [] t
115 |   unerr dflt = handle (mapProperty (\_,v => logLoggable v $> dflt) lgs)
116 |
117 |   export %inline
118 |   unerrMaybe : Async e es t -> Async e [] (Maybe t)
119 |   unerrMaybe = unerr Nothing . map Just
120 |
121 |   export %inline
122 |   logErrs : Async e es () -> Async e [] ()
123 |   logErrs = unerr ()
124 |