@@ -0,0 +1,133 @@
1+-- ------------------------------------------------------------- [ Logging.idr ]
2+-- Module : Logging.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
15+
16+import Effects
17+import public Effect.Logging.Level
18+
19+%access public
20+
21+record LogRes (a : Type) where
22+ constructor MkLogRes
23+ lvl : Nat
24+ cats : List a
25+
26+instance (Show a) => Show (LogRes a) where
27+ show (MkLogRes l cs) = unwords ["Log Settings:", show l, show cs]
28+
29+instance (Eq a) => Eq (LogRes a) where
30+ (==) (MkLogRes x y) (MkLogRes x' y') = x' == x && y == y'
31+
32+instance Default (LogRes a) where
33+ default = MkLogRes Z Nil
34+
35+||| A Logging effect to log levels and categories.
36+data Logging : Effect where
37+ ||| Log a message.
38+ |||
39+ ||| @lvl The logging level it should appear at.
40+ ||| @cats The categories it should appear under.
41+ ||| @msg The message to log.
42+ Log : (Show a, Eq a) =>
43+ (lvl : Nat)
44+ -> (cats : List a)
45+ -> (msg : String)
46+ -> sig Logging () (LogRes a)
47+
48+ ||| Change the logging level.
49+ |||
50+ ||| @nlvl The new logging level
51+ SetLogLvl : (Show a, Eq a) =>
52+ (nlvl : Nat) ->
53+ sig Logging () (LogRes a) (LogRes a)
54+
55+ ||| Change the categories to show.
56+ |||
57+ ||| @ncats The new categories.
58+ SetLogCats : (Show a, Eq a) =>
59+ (ncats : List a) ->
60+ sig Logging () (LogRes a) (LogRes a)
61+
62+ ||| Initialise the logging.
63+ |||
64+ ||| @nlvl The new logging level.
65+ ||| @ncats The categories to show.
66+ InitLogger : (Show a, Eq a) =>
67+ (nlvl : Nat) ->
68+ (ncats : List a) ->
69+ sig Logging () (LogRes a) (LogRes a)
70+
71+instance Handler Logging IO where
72+ handle st (SetLogLvl nlvl) k = do
73+ let newSt = record {lvl = nlvl} st
74+ k () newSt
75+ handle st (SetLogCats newcs) k = do
76+ let newSt = record {cats = newcs} st
77+ k () newSt
78+
79+ handle st (InitLogger l cs) k = do
80+ let newSt = MkLogRes l cs
81+ k () newSt
82+
83+ handle st (Log l cs' msg) k = do
84+ case l <= lvl st of
85+ False => k () st
86+ True => do
87+ let res = and $ map (\x => elem x cs') (cats st)
88+ let prompt = if isNil (cats st)
89+ then unwords [show l, ":"]
90+ else unwords [show l, ":", show (cats st)]
91+ if res || isNil (cats st)
92+ then do
93+ printLn $ unwords [prompt, msg]
94+ k () st
95+ else k () st
96+
97+||| The Logging effect.
98+|||
99+||| @cTy The type used to differentiate categories.
100+LOG : (cTy : Type) -> EFFECT
101+LOG cTy = MkEff (LogRes cTy) Logging
102+
103+||| Change the logging level.
104+|||
105+||| @l The new logging level.
106+setLoglvl : (Eq a, Show a) => (l : Nat) -> Eff () [LOG a]
107+setLoglvl l = call $ SetLogLvl l
108+
109+||| Change the categories to show.
110+|||
111+||| @cs The new categories.
112+setLogCats : (Show a, Eq a) => (cs : List a) -> Eff () [LOG a]
113+setLogCats cs = call $ SetLogCats cs
114+
115+||| Initialise the Logger.
116+|||
117+||| @l The logging level.
118+||| @cs The categories to show.
119+initLogger : (Eq a, Show a) => (l : Nat)
120+ -> (cs : List a)
121+ -> Eff () [LOG a]
122+initLogger l cs = call $ InitLogger l cs
123+
124+||| Log the given message at the given level and assign it the list of categories.
125+|||
126+||| @l The logging level.
127+||| @cs The logging categories.
128+||| @m THe message to be logged.
129+log : (Show a, Eq a) => (l : Nat)
130+ -> (cs : List a) -> (m : String) -> Eff () [LOG a]
131+log l cs msg = call $ Log l cs msg
132+
133+-- --------------------------------------------------------------------- [ EOF ]