@@ -14,23 +14,81 @@
1414module Effect.Logging
1515
1616import Effects
17−import public Effect.Logging.Level
1817
1918%access public
2019
20+-- ---------------------------------------------------- [ Log Level Definition ]
21+
22+||| Logging levels are natural numbers wrapped in a data type for
23+||| convenience.
24+|||
25+||| Several aliases have been defined to aide in semantic use of the
26+||| logging levels. These aliases have come from the Log4j/Python
27+||| family of loggers.
28+data LogLevel : Nat -> Type where
29+ ||| Log No Events
30+ OFF : LogLevel 0
31+
32+ ||| A fine-grained debug message, typically capturing the flow through
33+ ||| the application.
34+ TRACE : LogLevel 10
35+
36+ ||| A general debugging event.
37+ DEBUG : LogLevel 20
38+
39+ ||| An event for informational purposes.
40+ INFO : LogLevel 30
41+
42+ ||| An event that might possible lead to an error.
43+ WARN : LogLevel 40
44+
45+ ||| A severe error that will prevent the application from continuing.
46+ FATAL : LogLevel 50
47+
48+ ||| An error in the application, possibly recoverable.
49+ ERROR : LogLevel 60
50+
51+ ||| All events should be logged.
52+ ALL : LogLevel 70
53+
54+ ||| User defined logging level.
55+ CUSTOM : (n : Nat) -> {auto prf : LTE n 70} -> LogLevel n
56+
57+instance Cast (LogLevel n) Nat where
58+ cast {n} _ = n
59+
60+instance Show (LogLevel n) where
61+ show OFF = "OFF"
62+ show TRACE = "TRACE"
63+ show DEBUG = "DEBUG"
64+ show INFO = "INFO"
65+ show WARN = "WARN"
66+ show FATAL = "FATAL"
67+ show ERROR = "ERROR"
68+ show ALL = "ALL"
69+ show (CUSTOM n) = unwords ["CUSTOM", show n]
70+
71+instance Eq (LogLevel n) where
72+ (==) x y = lvlEq x y
73+ where
74+ lvlEq : LogLevel a -> LogLevel b -> Bool
75+ lvlEq {a} {b} _ _ = a == b
76+
77+cmpLevel : LogLevel a -> LogLevel b -> Ordering
78+cmpLevel {a} {b} _ _ = compare a b
79+
80+||| The Logging details, this is the resource that the effect is
81+||| defined over.
2182record LogRes (a : Type) where
2283 constructor MkLogRes
23− lvl : Nat
84+ lvl : LogLevel n
2485 cats : List a
2586
2687instance (Show a) => Show (LogRes a) where
2788 show (MkLogRes l cs) = unwords ["Log Settings:", show l, show cs]
2889
29−instance (Eq a) => Eq (LogRes a) where
30− (==) (MkLogRes x y) (MkLogRes x' y') = x' == x && y == y'
31−
3290instance Default (LogRes a) where
33− default = MkLogRes Z Nil
91+ default = MkLogRes OFF Nil
3492
3593||| A Logging effect to log levels and categories.
3694data Logging : Effect where
@@ -40,7 +98,7 @@ data Logging : Effect where
4098 ||| @cats The categories it should appear under.
4199 ||| @msg The message to log.
42100 Log : (Show a, Eq a) =>
43− (lvl : Nat)
101+ (lvl : LogLevel n)
44102 -> (cats : List a)
45103 -> (msg : String)
46104 -> sig Logging () (LogRes a)
@@ -49,7 +107,7 @@ data Logging : Effect where
49107 |||
50108 ||| @nlvl The new logging level
51109 SetLogLvl : (Show a, Eq a) =>
52− (nlvl : Nat) ->
110+ (nlvl : LogLevel n) ->
53111 sig Logging () (LogRes a) (LogRes a)
54112
55113 ||| Change the categories to show.
@@ -64,7 +122,7 @@ data Logging : Effect where
64122 ||| @nlvl The new logging level.
65123 ||| @ncats The categories to show.
66124 InitLogger : (Show a, Eq a) =>
67− (nlvl : Nat) ->
125+ (nlvl : LogLevel n) ->
68126 (ncats : List a) ->
69127 sig Logging () (LogRes a) (LogRes a)
70128
@@ -81,16 +139,16 @@ instance Handler Logging IO where
81139 k () newSt
82140
83141 handle st (Log l cs' msg) k = do
84− case l <= lvl st of
85− False => k () st
86− True => do
142+ case cmpLevel l (lvl st) of
143+ GT => k () st
144+ otherwise => do
87145 let res = and $ map (\x => elem x cs') (cats st)
88146 let prompt = if isNil (cats st)
89147 then unwords [show l, ":"]
90148 else unwords [show l, ":", show (cats st)]
91149 if res || isNil (cats st)
92150 then do
93− printLn $ unwords [prompt, msg]
151+ putStrLn $ unwords [prompt, msg]
94152 k () st
95153 else k () st
96154
@@ -103,7 +161,7 @@ LOG cTy = MkEff (LogRes cTy) Logging
103161||| Change the logging level.
104162|||
105163||| @l The new logging level.
106−setLoglvl : (Eq a, Show a) => (l : Nat) -> Eff () [LOG a]
164+setLoglvl : (Eq a, Show a) => (l : LogLevel n) -> Eff () [LOG a]
107165setLoglvl l = call $ SetLogLvl l
108166
109167||| Change the categories to show.
@@ -116,7 +174,7 @@ setLogCats cs = call $ SetLogCats cs
116174|||
117175||| @l The logging level.
118176||| @cs The categories to show.
119−initLogger : (Eq a, Show a) => (l : Nat)
177+initLogger : (Eq a, Show a) => (l : LogLevel n)
120178 -> (cs : List a)
121179 -> Eff () [LOG a]
122180initLogger l cs = call $ InitLogger l cs
@@ -126,8 +184,37 @@ initLogger l cs = call $ InitLogger l cs
126184||| @l The logging level.
127185||| @cs The logging categories.
128186||| @m THe message to be logged.
129−log : (Show a, Eq a) => (l : Nat)
187+log : (Show a, Eq a) => (l : Nat) -> {auto prf : LTE l 70}
130188 -> (cs : List a) -> (m : String) -> Eff () [LOG a]
131−log l cs msg = call $ Log l cs msg
189+log l cs msg = call $ Log (getProof lvl) cs msg
190+ where
191+ lvl : (n ** LogLevel n)
192+ lvl = case cast {to=String} (cast {to=Int} l) of
193+ "0" => (_ ** OFF)
194+ "10" => (_ ** TRACE)
195+ "20" => (_ ** DEBUG)
196+ "30" => (_ ** INFO)
197+ "40" => (_ ** WARN)
198+ "50" => (_ ** FATAL)
199+ "60" => (_ ** ERROR)
200+ _ => (_ ** CUSTOM l)
201+
202+trace : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
203+trace cs msg = call $ Log TRACE cs msg
204+
205+debug : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
206+debug cs msg = call $ Log DEBUG cs msg
207+
208+info : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
209+info cs msg = call $ Log INFO cs msg
210+
211+warn : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
212+warn cs msg = call $ Log WARN cs msg
213+
214+fatal : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
215+fatal cs msg = call $ Log FATAL cs msg
216+
217+error : (Show a, Eq a) => List a -> String -> Eff () [LOG a]
218+error cs msg = call $ Log ERROR cs msg
132219
133220-- --------------------------------------------------------------------- [ EOF ]