Category.idr

-- ------------------------------------------------------------ [ Category.idr ]
-- Module    : Category.idr
-- Copyright : (c) The Idris Community
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A logging effect that allows messages to be logged using both
||| numerical levels and user specified categories. The higher the
||| logging level the grater in verbosity the logging.
|||
||| In this effect the resource we are computing over is the logging
||| level itself and the list of categories to show.
module Effect.Logging.Category

import Effects
import public Effect.Logging.Level

%access public

-- -------------------------------------------------------- [ Logging Resource ]

||| The Logging details, this is the resource that the effect is
||| defined over.
record LogRes (a : Type) where
  constructor MkLogRes
  getLevel      : LogLevel n
  getCategories : List a

implementation Default (LogRes a) where
  default = MkLogRes OFF Nil

-- ------------------------------------------------------- [ Effect Definition ]

||| A Logging effect to log levels and categories.
data Logging : Effect where
    ||| Log a message.
    |||
    ||| @lvl  The logging level it should appear at.
    ||| @cats The categories it should appear under.
    ||| @msg  The message to log.
    Log : (Show a, Eq a) =>
          (lvl : LogLevel n)
       -> (cats : List a)
       -> (msg : String)
       -> sig Logging () (LogRes a)

    ||| Change the logging level.
    |||
    ||| @nlvl The new logging level
    SetLogLvl : (Show a, Eq a) =>
                (nlvl : LogLevel n) ->
                sig Logging () (LogRes a) (LogRes a)

    ||| Change the categories to show.
    |||
    ||| @ncats The new categories.
    SetLogCats : (Show a, Eq a) =>
                 (ncats : List a) ->
                 sig Logging () (LogRes a) (LogRes a)

    ||| Initialise the logging.
    |||
    ||| @nlvl  The new logging level.
    ||| @ncats The categories to show.
    InitLogger : (Show a, Eq a) =>
                 (nlvl  : LogLevel n) ->
                 (ncats : List a) ->
                 sig Logging () (LogRes a) (LogRes a)

-- -------------------------------------------------------------- [ IO Handler ]

implementation Handler Logging IO where
    handle st (SetLogLvl  nlvl)  k = do
        let newSt = record {getLevel = nlvl}  st
        k () newSt
    handle st (SetLogCats newcs) k = do
        let newSt = record {getCategories = newcs} st
        k () newSt

    handle st  (InitLogger l cs) k = do
        let newSt = MkLogRes l cs
        k () newSt

    handle st (Log l cs' msg) k = do
      case cmpLevel l (getLevel st) of
        GT        => k () st
        otherwise =>  do
          let res = and $ map (\x => elem x cs') (getCategories st)
          let prompt = if isNil (getCategories st)
                         then unwords [show l, ":"]
                         else unwords [show l, ":", show (getCategories st), ":"]
          if res || isNil (getCategories st)
            then do
              putStrLn $ unwords [prompt, msg]
              k () st
            else k () st


-- ------------------------------------------------------- [ Effect Descriptor ]

||| The Logging effect.
|||
||| @a The type used to differentiate categories.
LOG : (a : Type) -> EFFECT
LOG a = MkEff (LogRes a) Logging

-- ----------------------------------------------------------- [ Effectful API ]

||| Change the logging level.
|||
||| @l  The new logging level.
setLoglvl : (Show a, Eq a) => (l : LogLevel n) -> Eff () [LOG a]
setLoglvl l = call $ SetLogLvl l

||| Change the categories to show.
|||
||| @cs The new categories.
setLogCats : (Show a, Eq a) => (cs : List a) -> Eff () [LOG a]
setLogCats cs = call $ SetLogCats cs

||| Initialise the Logger.
|||
||| @l  The logging level.
||| @cs The categories to show.
initLogger : (Show a, Eq a) => (l : LogLevel n)
                            -> (cs : List a)
                            -> Eff () [LOG a]
initLogger l cs = call $ InitLogger l cs

||| Log the given message at the given level indicated by a natural number and assign it the list of categories.
|||
||| @l The logging level.
||| @cs The logging categories.
||| @m THe message to be logged.
log : (Show a, Eq a) => (l : LogLevel n)
                     -> (cs : List a)
                     -> (m : String)
                     -> Eff () [LOG a]
log l cs msg = call $ Log l cs msg

||| Log the given message at the given level indicated by a natural number and assign it the list of categories.
|||
||| @l The logging level.
||| @cs The logging categories.
||| @m THe message to be logged.
logN : (Show a, Eq a) => (l : Nat)
                      -> {auto prf : LTE l 70}
                      -> (cs : List a)
                      -> (m : String)
                      -> Eff () [LOG a]
logN l cs msg = call $ Log (getProof lvl) cs msg
  where
    lvl : (n ** LogLevel n)
    lvl = case cast {to=String} (cast {to=Int} l) of
            "0"  => (_ ** OFF)
            "10" => (_ ** TRACE)
            "20" => (_ ** DEBUG)
            "30" => (_ ** INFO)
            "40" => (_ ** WARN)
            "50" => (_ ** FATAL)
            "60" => (_ ** ERROR)
            _    => (_ ** CUSTOM l)

trace : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
trace cs msg = call $ Log TRACE cs msg

debug : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
debug cs msg = call $ Log DEBUG cs msg

info : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
info cs msg = call $ Log INFO cs msg

warn : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
warn cs msg = call $ Log WARN cs msg

fatal : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
fatal cs msg = call $ Log FATAL cs msg

error : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
error cs msg = call $ Log ERROR cs msg

-- --------------------------------------------------------------------- [ EOF ]