0 | ||| Typeclass-based access to loggers from an environment.
  1 | |||
  2 | ||| `HasLog` provides a uniform way to extract and modify a `LogAction`
  3 | ||| within an environment type. Combined with `MonadReader`, this enables
  4 | ||| logging that is polymorphic over the monad - the concrete logger
  5 | ||| is determined by the environment.
  6 | |||
  7 | ||| `LoggerT` is a monad transformer that carries a `LogAction` in a
  8 | ||| reader environment. Use `usingLoggerT` to run a `LoggerT` computation
  9 | ||| with a concrete `LogAction`.
 10 | module Log4Types.HasLog
 11 |
 12 | import public Control.Monad.Reader.Interface
 13 | import Control.Monad.Reader.Reader
 14 | import public Control.Monad.Trans
 15 | import Log4Types.Core
 16 |
 17 | %default total
 18 |
 19 | ----------------------------------------------------------------------
 20 | -- HasLog interface
 21 | ----------------------------------------------------------------------
 22 |
 23 | ||| Interface for environment types that contain a LogAction.
 24 | |||
 25 | ||| The `m` parameter is the monad of the stored LogAction and should
 26 | ||| match the monad you're running in. This allows `logMsg` to directly
 27 | ||| execute the action without lifting.
 28 | public export
 29 | interface HasLog env msg (0 m : Type -> Type) where
 30 |   ||| Extract the LogAction from the environment.
 31 |   getLogAction : env -> LogAction m msg
 32 |   ||| Replace the LogAction in the environment.
 33 |   setLogAction : LogAction m msg -> env -> env
 34 |
 35 | ||| A LogAction is its own environment.
 36 | public export
 37 | HasLog (LogAction m msg) msg m where
 38 |   getLogAction = id
 39 |   setLogAction = const
 40 |
 41 | ----------------------------------------------------------------------
 42 | -- Logging functions
 43 | ----------------------------------------------------------------------
 44 |
 45 | ||| Log a message by extracting the action from the reader environment.
 46 | public export
 47 | logMsg : Monad m => MonadReader env m => HasLog env msg m => msg -> m ()
 48 | logMsg msg = do
 49 |   env <- ask
 50 |   unLogAction (getLogAction env) msg
 51 |
 52 | ||| Run a computation with a locally modified logger.
 53 | public export
 54 | withLog : Monad m => MonadReader env m => HasLog env msg m
 55 |        => (LogAction m msg -> LogAction m msg)
 56 |        -> m a -> m a
 57 | withLog f = local (\env => setLogAction (f (getLogAction env)) env)
 58 |
 59 | ----------------------------------------------------------------------
 60 | -- LoggerT
 61 | ----------------------------------------------------------------------
 62 |
 63 | ||| A monad transformer that carries a `LogAction` in a reader environment.
 64 | |||
 65 | ||| The stored `LogAction` is self-referential: it operates in `LoggerT msg m`,
 66 | ||| not in the inner monad `m`. This allows the action itself to use the
 67 | ||| full `LoggerT` capabilities.
 68 | |||
 69 | ||| Use `usingLoggerT` to run a `LoggerT` computation.
 70 | public export
 71 | record LoggerT (msg : Type) (m : Type -> Type) (a : Type) where
 72 |   constructor MkLoggerT
 73 |   unLoggerT : ReaderT (LogAction (LoggerT msg m) msg) m a
 74 |
 75 | public export
 76 | Functor m => Functor (LoggerT msg m) where
 77 |   map f (MkLoggerT r) = MkLoggerT (map f r)
 78 |
 79 | public export
 80 | Applicative m => Applicative (LoggerT msg m) where
 81 |   pure x = MkLoggerT (pure x)
 82 |   MkLoggerT f <*> MkLoggerT x = MkLoggerT (f <*> x)
 83 |
 84 | public export
 85 | Monad m => Monad (LoggerT msg m) where
 86 |   MkLoggerT m >>= f = MkLoggerT (m >>= unLoggerT . f)
 87 |
 88 | public export
 89 | MonadTrans (LoggerT msg) where
 90 |   lift = MkLoggerT . lift
 91 |
 92 | public export
 93 | HasIO m => HasIO (LoggerT msg m) where
 94 |   liftIO = MkLoggerT . liftIO
 95 |
 96 | public export
 97 | Monad m => MonadReader (LogAction (LoggerT msg m) msg) (LoggerT msg m) where
 98 |   ask = MkLoggerT ask
 99 |   local f (MkLoggerT m) = MkLoggerT (local f m)
100 |
101 | ||| Run a `LoggerT` computation with a concrete `LogAction`.
102 | |||
103 | ||| The provided `LogAction m msg` (operating in the inner monad) is
104 | ||| lifted to `LogAction (LoggerT msg m) msg` via `lift`.
105 | public export
106 | usingLoggerT : Monad m => LogAction m msg -> LoggerT msg m a -> m a
107 | usingLoggerT act (MkLoggerT r) =
108 |   runReaderT (hoistLogAction lift act) r
109 |