@@ -0,0 +1,57 @@
1+-- ------------------------------------------------------------- [ Default.idr ]
2+-- Module : Default.idr
3+-- Copyright : (c) The Idris Community
4+-- License : see LICENSE
5+-- --------------------------------------------------------------------- [ EOH ]
6+
7+||| A logging effect that allows messages to be logged using both
8+||| numerical levels and user specified categories. The higher the
9+||| logging level the grater in verbosity the logging.
10+|||
11+||| In this effect the resource we are computing over is the logging
12+||| level itself and the list of categories to show.
13+|||
14+module Effect.Logging.Default
15+
16+import Effects
17+import public Effect.Logging.Level
18+
19+import Control.IOExcept -- TODO Add IOExcept Logger.
20+
21+||| A Logging effect to log levels and categories.
22+data Logging : Effect where
23+ Log : (Eq a, Show a) =>
24+ (lvl : Nat)
25+ -> (cats : List a)
26+ -> (msg : String)
27+ -> Logging () (Nat,List a) (\v => (Nat,List a))
28+
29+||| The Logging effect.
30+|||
31+||| @cTy The type used to differentiate categories.
32+LOG : (cTy : Type) -> EFFECT
33+LOG a = MkEff (Nat, List a) Logging
34+
35+instance Handler Logging IO where
36+ handle (l,cs) (Log lvl cs' msg) k = do
37+ case lvl <= l of
38+ False => k () (l,cs)
39+ True => do
40+ let res = and $ map (\x => elem x cs') cs
41+ let prompt = if isNil cs then "" else show cs
42+ if res || isNil cs
43+ then do
44+ printLn $ unwords [show lvl, ":", prompt, ":", msg]
45+ k () (l,cs)
46+ else k () (l,cs)
47+
48+||| Log the given message at the given level and assign it the list of categories.
49+|||
50+||| @l The logging level.
51+||| @cs The logging categories.
52+||| @m THe message to be logged.
53+log : (Show a, Eq a) => (l : Nat)
54+ -> (cs : List a) -> (m : String) -> Eff () [LOG a]
55+log lvl cs msg = call $ Log lvl cs msg
56+
57+-- --------------------------------------------------------------------- [ EOF ]