0 | ||| The fundamental LogAction type and combinators.
  1 | |||
  2 | ||| A `LogAction m msg` is a first-class logging value: a function that
  3 | ||| consumes a message of type `msg` in some monadic context `m`.
  4 | ||| LogActions compose via Semigroup (fan-out to multiple destinations),
  5 | ||| transform via Contravariant (adapt message types), and filter via
  6 | ||| predicates.
  7 | module Log4Types.Core.Action
  8 |
  9 | import Data.Contravariant
 10 |
 11 | %default total
 12 |
 13 | ----------------------------------------------------------------------
 14 | -- Core type
 15 | ----------------------------------------------------------------------
 16 |
 17 | ||| A logging action that consumes messages of type `msg` in context `m`.
 18 | |||
 19 | ||| This is the central type of log4types. A LogAction is a first-class
 20 | ||| value that can be composed, transformed, and passed around.
 21 | public export
 22 | record LogAction (m : Type -> Type) (msg : Type) where
 23 |   constructor MkLogAction
 24 |   unLogAction : msg -> m ()
 25 |
 26 | ----------------------------------------------------------------------
 27 | -- Execution
 28 | ----------------------------------------------------------------------
 29 |
 30 | public export infixl 5 <&
 31 | public export infixr 5 &>
 32 |
 33 | ||| Execute a log action on a message.
 34 | |||
 35 | ||| ```idris
 36 | ||| logStringStdout <& "hello"
 37 | ||| ```
 38 | public export
 39 | (<&) : LogAction m msg -> msg -> m ()
 40 | (<&) = unLogAction
 41 |
 42 | ||| Execute a log action on a message (flipped).
 43 | public export
 44 | (&>) : msg -> LogAction m msg -> m ()
 45 | (&>) = flip (<&)
 46 |
 47 | ----------------------------------------------------------------------
 48 | -- Contravariant
 49 | ----------------------------------------------------------------------
 50 |
 51 | ||| Transform the message type before logging.
 52 | |||
 53 | ||| If you can log `b` and you have `a -> b`, you can log `a`.
 54 | public export
 55 | cmap : (a -> b) -> LogAction m b -> LogAction m a
 56 | cmap f (MkLogAction act) = MkLogAction (act . f)
 57 |
 58 | public export
 59 | Contravariant (LogAction m) where
 60 |   contramap = cmap
 61 |
 62 | ||| Transform the message type using a monadic computation.
 63 | |||
 64 | ||| Like `cmap` but the transformation can perform effects.
 65 | ||| Useful for enriching messages with timestamps, thread IDs, etc.
 66 | public export
 67 | cmapM : Monad m => (a -> m b) -> LogAction m b -> LogAction m a
 68 | cmapM f (MkLogAction act) = MkLogAction (\a => f a >>= act)
 69 |
 70 | ----------------------------------------------------------------------
 71 | -- Composition
 72 | ----------------------------------------------------------------------
 73 |
 74 | ||| Combine two log actions: both receive the same message.
 75 | public export
 76 | Applicative m => Semigroup (LogAction m msg) where
 77 |   MkLogAction a1 <+> MkLogAction a2 = MkLogAction $ \msg => a1 msg *> a2 msg
 78 |
 79 | ||| The silent log action that discards all messages.
 80 | public export
 81 | Applicative m => Monoid (LogAction m msg) where
 82 |   neutral = MkLogAction $ \_ => pure ()
 83 |
 84 | ----------------------------------------------------------------------
 85 | -- Filtering
 86 | ----------------------------------------------------------------------
 87 |
 88 | ||| Only log messages satisfying a predicate.
 89 | public export
 90 | cfilter : Applicative m => (msg -> Bool) -> LogAction m msg -> LogAction m msg
 91 | cfilter p (MkLogAction act) = MkLogAction $ \msg =>
 92 |   if p msg then act msg else pure ()
 93 |
 94 | ||| Only log messages satisfying a monadic predicate.
 95 | public export
 96 | cfilterM : Monad m => (msg -> m Bool) -> LogAction m msg -> LogAction m msg
 97 | cfilterM p (MkLogAction act) = MkLogAction $ \msg => do
 98 |   ok <- p msg
 99 |   if ok then act msg else pure ()
100 |
101 | ||| Transform and filter: only log when the function returns Just.
102 | public export
103 | cmapMaybe : Applicative m => (a -> Maybe b) -> LogAction m b -> LogAction m a
104 | cmapMaybe f (MkLogAction act) = MkLogAction $ \a =>
105 |   case f a of
106 |     Just b  => act b
107 |     Nothing => pure ()
108 |
109 | ----------------------------------------------------------------------
110 | -- Divisible
111 | ----------------------------------------------------------------------
112 |
113 | ||| Split a message into two parts and log each to a different action.
114 | |||
115 | ||| Contravariant analogue of Applicative: if you can split `a` into
116 | ||| `(b, c)` and log each independently, you can log `a`.
117 | public export
118 | divide : Applicative m
119 |       => (a -> (b, c))
120 |       -> LogAction m b
121 |       -> LogAction m c
122 |       -> LogAction m a
123 | divide f (MkLogAction actB) (MkLogAction actC) = MkLogAction $ \a =>
124 |   let (b, c) = f a in actB b *> actC c
125 |
126 | ----------------------------------------------------------------------
127 | -- Decidable
128 | ----------------------------------------------------------------------
129 |
130 | ||| Route a message to one of two loggers based on a decision function.
131 | |||
132 | ||| Contravariant analogue of Alternative: if you can decide whether
133 | ||| `a` is a `b` or a `c`, and log each, you can log `a`.
134 | public export
135 | choose : Applicative m
136 |       => (a -> Either b c)
137 |       -> LogAction m b
138 |       -> LogAction m c
139 |       -> LogAction m a
140 | choose f (MkLogAction actB) (MkLogAction actC) = MkLogAction $ \a =>
141 |   case f a of
142 |     Left  b => actB b
143 |     Right c => actC c
144 |
145 | ----------------------------------------------------------------------
146 | -- Monad transformation
147 | ----------------------------------------------------------------------
148 |
149 | ||| Transform the monadic context of a LogAction via a natural transformation.
150 | public export
151 | hoistLogAction : ({0 x : Type} -> m x -> n x) -> LogAction m a -> LogAction n a
152 | hoistLogAction nat (MkLogAction act) = MkLogAction (nat . act)
153 |