@@ -0,0 +1,184 @@
1+-- ------------------------------------------------------------ [ Category.idr ]
2+-- Module : Category.idr
3+-- Copyright : (c) The Idris Community
4+-- License : see LICENSE
5+-- --------------------------------------------------------------------- [ EOH ]
6+||| A logging effect that allows messages to be logged using both
7+||| numerical levels and user specified categories. The higher the
8+||| logging level the grater in verbosity the logging.
9+|||
10+||| In this effect the resource we are computing over is the logging
11+||| level itself and the list of categories to show.
12+module Effect.Logging.Category
13+
14+import Effects
15+import public Effect.Logging.Level
16+
17+%access public
18+
19+-- -------------------------------------------------------- [ Logging Resource ]
20+
21+||| The Logging details, this is the resource that the effect is
22+||| defined over.
23+record LogRes (a : Type) where
24+ constructor MkLogRes
25+ getLevel : LogLevel n
26+ getCategories : List a
27+
28+instance (Show a) => Show (LogRes a) where
29+ show (MkLogRes l cs) = unwords ["Log Settings:", show l, show cs]
30+
31+instance Default (LogRes a) where
32+ default = MkLogRes OFF Nil
33+
34+-- ------------------------------------------------------- [ Effect Definition ]
35+
36+||| A Logging effect to log levels and categories.
37+data Logging : Effect where
38+ ||| Log a message.
39+ |||
40+ ||| @lvl The logging level it should appear at.
41+ ||| @cats The categories it should appear under.
42+ ||| @msg The message to log.
43+ Log : (Show a, Eq a) =>
44+ (lvl : LogLevel n)
45+ -> (cats : List a)
46+ -> (msg : String)
47+ -> sig Logging () (LogRes a)
48+
49+ ||| Change the logging level.
50+ |||
51+ ||| @nlvl The new logging level
52+ SetLogLvl : (Show a, Eq a) =>
53+ (nlvl : LogLevel n) ->
54+ sig Logging () (LogRes a) (LogRes a)
55+
56+ ||| Change the categories to show.
57+ |||
58+ ||| @ncats The new categories.
59+ SetLogCats : (Show a, Eq a) =>
60+ (ncats : List a) ->
61+ sig Logging () (LogRes a) (LogRes a)
62+
63+ ||| Initialise the logging.
64+ |||
65+ ||| @nlvl The new logging level.
66+ ||| @ncats The categories to show.
67+ InitLogger : (Show a, Eq a) =>
68+ (nlvl : LogLevel n) ->
69+ (ncats : List a) ->
70+ sig Logging () (LogRes a) (LogRes a)
71+
72+-- -------------------------------------------------------------- [ IO Handler ]
73+
74+instance Handler Logging IO where
75+ handle st (SetLogLvl nlvl) k = do
76+ let newSt = record {getLevel = nlvl} st
77+ k () newSt
78+ handle st (SetLogCats newcs) k = do
79+ let newSt = record {getCategories = newcs} st
80+ k () newSt
81+
82+ handle st (InitLogger l cs) k = do
83+ let newSt = MkLogRes l cs
84+ k () newSt
85+
86+ handle st (Log l cs' msg) k = do
87+ case cmpLevel l (getLevel st) of
88+ GT => k () st
89+ otherwise => do
90+ let res = and $ map (\x => elem x cs') (getCategories st)
91+ let prompt = if isNil (getCategories st)
92+ then unwords [show l, ":"]
93+ else unwords [show l, ":", show (getCategories st), ":"]
94+ if res || isNil (getCategories st)
95+ then do
96+ putStrLn $ unwords [prompt, msg]
97+ k () st
98+ else k () st
99+
100+
101+-- ------------------------------------------------------- [ Effect Descriptor ]
102+
103+||| The Logging effect.
104+|||
105+||| @a The type used to differentiate categories.
106+LOG : (a : Type) -> EFFECT
107+LOG a = MkEff (LogRes a) Logging
108+
109+-- ----------------------------------------------------------- [ Effectful API ]
110+
111+||| Change the logging level.
112+|||
113+||| @l The new logging level.
114+setLoglvl : (Show a, Eq a) => (l : LogLevel n) -> Eff () [LOG a]
115+setLoglvl l = call $ SetLogLvl l
116+
117+||| Change the categories to show.
118+|||
119+||| @cs The new categories.
120+setLogCats : (Show a, Eq a) => (cs : List a) -> Eff () [LOG a]
121+setLogCats cs = call $ SetLogCats cs
122+
123+||| Initialise the Logger.
124+|||
125+||| @l The logging level.
126+||| @cs The categories to show.
127+initLogger : (Show a, Eq a) => (l : LogLevel n)
128+ -> (cs : List a)
129+ -> Eff () [LOG a]
130+initLogger l cs = call $ InitLogger l cs
131+
132+||| Log the given message at the given level indicated by a natural number and assign it the list of categories.
133+|||
134+||| @l The logging level.
135+||| @cs The logging categories.
136+||| @m THe message to be logged.
137+log : (Show a, Eq a) => (l : LogLevel n)
138+ -> (cs : List a)
139+ -> (m : String)
140+ -> Eff () [LOG a]
141+log l cs msg = call $ Log l cs msg
142+
143+||| Log the given message at the given level indicated by a natural number and assign it the list of categories.
144+|||
145+||| @l The logging level.
146+||| @cs The logging categories.
147+||| @m THe message to be logged.
148+logN : (Show a, Eq a) => (l : Nat)
149+ -> {auto prf : LTE l 70}
150+ -> (cs : List a)
151+ -> (m : String)
152+ -> Eff () [LOG a]
153+logN l cs msg = call $ Log (getProof lvl) cs msg
154+ where
155+ lvl : (n ** LogLevel n)
156+ lvl = case cast {to=String} (cast {to=Int} l) of
157+ "0" => (_ ** OFF)
158+ "10" => (_ ** TRACE)
159+ "20" => (_ ** DEBUG)
160+ "30" => (_ ** INFO)
161+ "40" => (_ ** WARN)
162+ "50" => (_ ** FATAL)
163+ "60" => (_ ** ERROR)
164+ _ => (_ ** CUSTOM l)
165+
166+trace : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
167+trace cs msg = call $ Log TRACE cs msg
168+
169+debug : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
170+debug cs msg = call $ Log DEBUG cs msg
171+
172+info : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
173+info cs msg = call $ Log INFO cs msg
174+
175+warn : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
176+warn cs msg = call $ Log WARN cs msg
177+
178+fatal : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
179+fatal cs msg = call $ Log FATAL cs msg
180+
181+error : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
182+error cs msg = call $ Log ERROR cs msg
183+
184+-- --------------------------------------------------------------------- [ EOF ]