
  0 | ||| Asynchronous logging: a background fiber drains a bounded channel
  1 | ||| and runs the underlying `LogAction` off the application's critical
  2 | ||| path, so a log call costs a channel write instead of backend IO.
  3 | module Log4Types.Async
  4 | 
  5 | import IO.Async
  6 | import IO.Async.Channel
  7 | import Log4Types.Core
  8 | 
  9 | %default total
 10 | 
 11 | ||| Configuration for the background log worker.
 12 | public export
 13 | record AsyncConfig where
 14 |   constructor MkAsyncConfig
 15 |   ||| Maximum messages buffered in the channel. When full, log calls
 16 |   ||| block the calling fiber until the worker catches up.
 17 |   capacity : Nat
 18 | 
 19 | ||| Sensible default: a 1024-message buffer.
 20 | public export
 21 | defaultAsyncConfig : AsyncConfig
 22 | defaultAsyncConfig = MkAsyncConfig 1024
 23 | 
 24 | covering
 25 | drain : LogAction IO msg -> Channel msg -> Async e [] ()
 26 | drain underlying chan = do
 27 |   Just m <- receive chan
 28 |     | Nothing => pure ()
 29 |   liftIO (underlying <& m)
 30 |   drain underlying chan
 31 | 
 32 | ||| Run a computation with an async-backed `LogAction`.
 33 | |||
 34 | ||| A background fiber drains a bounded channel and runs `underlying`
 35 | ||| on each message. The `LogAction` handed to the continuation
 36 | ||| enqueues in roughly constant time, blocking only when the channel
 37 | ||| is full. On scope exit the channel is closed and every pending
 38 | ||| message is flushed before returning.
 39 | export covering
 40 | withAsyncLogger
 41 |   :  (config     : AsyncConfig)
 42 |   -> (underlying : LogAction IO msg)
 43 |   -> (LogAction (Async e []) msg -> Async e [] a)
 44 |   -> Async e [] a
 45 | withAsyncLogger config underlying k = do
 46 |   chan <- channel config.capacity
 47 |   fib  <- start (drain underlying chan)
 48 |   res  <- k (MkLogAction $ \m => ignore (send chan m))
 49 |   close chan
 50 |   ignore (join fib)
 51 |   pure res
 52 |