Merge pull request idris-lang#2376 from jfdm/logging-effect

Effectful Logging.

effects/Effect/Logging/Default.idr

@@ -0,0 +1,57 @@
+-- ------------------------------------------------------------- [ Default.idr ]
+-- Module    : Default.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.Default
+
+import Effects
+import public Effect.Logging.Level
+
+import Control.IOExcept -- TODO Add IOExcept Logger.
+
+||| A Logging effect to log levels and categories.
+data Logging : Effect where
+    Log : (Eq a, Show a) =>
+          (lvl : Nat)
+       -> (cats : List a)
+       -> (msg : String)
+       -> Logging () (Nat,List a) (\v => (Nat,List a))
+
+||| The Logging effect.
+|||
+||| @cTy The type used to differentiate categories.
+LOG : (cTy : Type) -> EFFECT
+LOG a = MkEff (Nat, List a) Logging
+
+instance Handler Logging IO where
+    handle (l,cs) (Log lvl cs' msg) k = do
+      case lvl <= l  of
+        False => k () (l,cs)
+        True  =>  do
+          let res = and $ map (\x => elem x cs') cs
+          let prompt = if isNil cs then "" else show cs
+          if res || isNil cs
+            then do
+              printLn $ unwords [show lvl, ":", prompt, ":", msg]
+              k () (l,cs)
+            else k () (l,cs)
+
+||| Log the given message at the given level 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 : Nat)
+    -> (cs : List a) -> (m : String) -> Eff () [LOG a]
+log lvl cs msg = call $ Log lvl cs msg
+
+-- --------------------------------------------------------------------- [ EOF ]

effects/Effect/Logging/Level.idr

@@ -0,0 +1,49 @@
+-- -------------------------------------------------------------- [ Levels.idr ]
+-- Module    : Levels.idr
+-- Copyright : (c) Jan de Muijnck-Hughes
+-- License   : see LICENSE
+-- --------------------------------------------------------------------- [ EOH ]
+||| Common aliases and definitions of Logging Levels.
+module Effect.Logging.Level
+
+%access public
+-- ---------------------------------------------- [ Nat Derived Logging Levels ]
+--
+-- Several aliases have been defined to aide in semantic use of the
+-- logging levels. These aliases have come from the Log4j family of
+-- loggers.
+
+||| No events will be logged.
+OFF : Nat
+OFF = 0
+
+||| A severe error that will prevent the application from continuing.
+FATAL : Nat
+FATAL = 1
+
+||| An error in the application, possibly recoverable.
+ERROR : Nat
+ERROR = 2
+
+||| An event that might possible lead to an error.
+WARN : Nat
+WARN = 3
+
+|||  An event for informational purposes.
+INFO : Nat
+INFO = 4
+
+||| A general debugging event.
+DEBUG : Nat
+DEBUG = 5
+
+||| A fine-grained debug message, typically capturing the flow through
+||| the application.
+TRACE : Nat
+TRACE = 6
+
+||| All events should be logged.
+ALL : Nat
+ALL = 7
+
+-- --------------------------------------------------------------------- [ EOF ]

effects/Effect/Logging/Simple.idr

@@ -0,0 +1,48 @@
+-- -------------------------------------------------------------- [ Simple.idr ]
+-- Module    : Logging.idr
+-- Copyright : (c) The Idris Community
+-- License   : see LICENSE
+--------------------------------------------------------------------- [ EOH ]
+
+||| A simple logging effect that allows messages to be logged at
+||| different numerical level. The higher the number the grater in
+||| verbosity the logging.
+|||
+||| In this effect the resource we are computing over is the logging
+||| level itself.
+|||
+module Effect.Logging.Simple
+
+import Effects
+import public Effect.Logging.Level
+
+import Control.IOExcept -- TODO Add IO Logging Handler
+
+||| A Logging effect that displays a logging message to be logged at a
+||| certain level.
+data Logging : Effect where
+    Log : (lvl : Nat)
+       -> (msg : String)
+       -> Logging () Nat (\v => Nat)
+
+||| A Logging Effect.
+LOG : EFFECT
+LOG = MkEff Nat Logging
+
+-- For logging in the IO context
+instance Handler Logging IO where
+    handle l (Log lvl msg) k = do
+      case lvl <= l  of
+        False   => k () l
+        True  =>  do
+          printLn $ unwords [show lvl, ":", msg]
+          k () l
+
+||| Log `msg` at the given level.
+|||
+||| @l The level to log.
+||| @m The message to log.
+log : (l : Nat) -> (m : String) -> Eff () [LOG]
+log lvl msg = call $ Log lvl msg
+
+-- --------------------------------------------------------------------- [ EOF ]

effects/effects.ipkg

@@ -1,9 +1,20 @@
 package effects
 
 opts    = "--nobasepkgs -i ../prelude -i ../base"
-modules = Effects, Effect.Default, Effect.Monad,
 
-          Effect.Exception, Effect.File, Effect.State,
-          Effect.Random, Effect.StdIO, Effect.Select,
-          Effect.Memory, Effect.System, Effect.Trans
+modules = Effects
+        , Effect.Default
+        , Effect.Monad
 
+        , Effect.Exception
+        , Effect.File
+        , Effect.State
+        , Effect.Random
+        , Effect.StdIO
+        , Effect.Select
+        , Effect.Memory
+        , Effect.System
+        , Effect.Trans
+        , Effect.Logging.Level
+        , Effect.Logging.Simple
+        , Effect.Logging.Default