git.iko.soy/Idris-dev
on master help sign in
Rewrote Default Logger and Simple Logger
2df4ef6Jan de Muijnck-Hughes
CHANGELOG+2
compare with master
unifiedsplit
@@ -30,6 +30,8 @@ New in 0.9.19:
30* Major improvements to reflected elaboration scripts, including the ability to run
30* Major improvements to reflected elaboration scripts, including the ability to run
31 them in a declaration context and many bug fixes.
31 them in a declaration context and many bug fixes.
32* "decl syntax" rules to allow syntax extensions at the declaration level
32* "decl syntax" rules to allow syntax extensions at the declaration level
33+* New Logging Effects have been added to facilitate logging of effectful
34+ programmes.
33
35
34New in 0.9.18:
36New in 0.9.18:
35--------------
37--------------
libs/effects/Effect/Logging.idr+104−17
@@ -14,23 +14,81 @@
14module Effect.Logging
14module Effect.Logging
15
15
16import Effects
16import Effects
17−import public Effect.Logging.Level
18
17
19%access public
18%access public
20
19
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.
21record LogRes (a : Type) where
82record LogRes (a : Type) where
22 constructor MkLogRes
83 constructor MkLogRes
23− lvl : Nat
84+ lvl : LogLevel n
24 cats : List a
85 cats : List a
25
86
26instance (Show a) => Show (LogRes a) where
87instance (Show a) => Show (LogRes a) where
27 show (MkLogRes l cs) = unwords ["Log Settings:", show l, show cs]
88 show (MkLogRes l cs) = unwords ["Log Settings:", show l, show cs]
28
89
29−instance (Eq a) => Eq (LogRes a) where
30− (==) (MkLogRes x y) (MkLogRes x' y') = x' == x && y == y'
31−
32instance Default (LogRes a) where
90instance Default (LogRes a) where
33− default = MkLogRes Z Nil
91+ default = MkLogRes OFF Nil
34
92
35||| A Logging effect to log levels and categories.
93||| A Logging effect to log levels and categories.
36data Logging : Effect where
94data Logging : Effect where
@@ -40,7 +98,7 @@ data Logging : Effect where
40 ||| @cats The categories it should appear under.
98 ||| @cats The categories it should appear under.
41 ||| @msg The message to log.
99 ||| @msg The message to log.
42 Log : (Show a, Eq a) =>
100 Log : (Show a, Eq a) =>
43− (lvl : Nat)
101+ (lvl : LogLevel n)
44 -> (cats : List a)
102 -> (cats : List a)
45 -> (msg : String)
103 -> (msg : String)
46 -> sig Logging () (LogRes a)
104 -> sig Logging () (LogRes a)
@@ -49,7 +107,7 @@ data Logging : Effect where
49 |||
107 |||
50 ||| @nlvl The new logging level
108 ||| @nlvl The new logging level
51 SetLogLvl : (Show a, Eq a) =>
109 SetLogLvl : (Show a, Eq a) =>
52− (nlvl : Nat) ->
110+ (nlvl : LogLevel n) ->
53 sig Logging () (LogRes a) (LogRes a)
111 sig Logging () (LogRes a) (LogRes a)
54
112
55 ||| Change the categories to show.
113 ||| Change the categories to show.
@@ -64,7 +122,7 @@ data Logging : Effect where
64 ||| @nlvl The new logging level.
122 ||| @nlvl The new logging level.
65 ||| @ncats The categories to show.
123 ||| @ncats The categories to show.
66 InitLogger : (Show a, Eq a) =>
124 InitLogger : (Show a, Eq a) =>
67− (nlvl : Nat) ->
125+ (nlvl : LogLevel n) ->
68 (ncats : List a) ->
126 (ncats : List a) ->
69 sig Logging () (LogRes a) (LogRes a)
127 sig Logging () (LogRes a) (LogRes a)
70
128
@@ -81,16 +139,16 @@ instance Handler Logging IO where
81 k () newSt
139 k () newSt
82
140
83 handle st (Log l cs' msg) k = do
141 handle st (Log l cs' msg) k = do
84− case l <= lvl st of
142+ case cmpLevel l (lvl st) of
85− False => k () st
143+ GT => k () st
86− True => do
144+ otherwise => do
87 let res = and $ map (\x => elem x cs') (cats st)
145 let res = and $ map (\x => elem x cs') (cats st)
88 let prompt = if isNil (cats st)
146 let prompt = if isNil (cats st)
89 then unwords [show l, ":"]
147 then unwords [show l, ":"]
90 else unwords [show l, ":", show (cats st)]
148 else unwords [show l, ":", show (cats st)]
91 if res || isNil (cats st)
149 if res || isNil (cats st)
92 then do
150 then do
93− printLn $ unwords [prompt, msg]
151+ putStrLn $ unwords [prompt, msg]
94 k () st
152 k () st
95 else k () st
153 else k () st
96
154
@@ -103,7 +161,7 @@ LOG cTy = MkEff (LogRes cTy) Logging
103||| Change the logging level.
161||| Change the logging level.
104|||
162|||
105||| @l The new logging level.
163||| @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]
107setLoglvl l = call $ SetLogLvl l
165setLoglvl l = call $ SetLogLvl l
108
166
109||| Change the categories to show.
167||| Change the categories to show.
@@ -116,7 +174,7 @@ setLogCats cs = call $ SetLogCats cs
116|||
174|||
117||| @l The logging level.
175||| @l The logging level.
118||| @cs The categories to show.
176||| @cs The categories to show.
119−initLogger : (Eq a, Show a) => (l : Nat)
177+initLogger : (Eq a, Show a) => (l : LogLevel n)
120 -> (cs : List a)
178 -> (cs : List a)
121 -> Eff () [LOG a]
179 -> Eff () [LOG a]
122initLogger l cs = call $ InitLogger l cs
180initLogger l cs = call $ InitLogger l cs
@@ -126,8 +184,37 @@ initLogger l cs = call $ InitLogger l cs
126||| @l The logging level.
184||| @l The logging level.
127||| @cs The logging categories.
185||| @cs The logging categories.
128||| @m THe message to be logged.
186||| @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}
130 -> (cs : List a) -> (m : String) -> Eff () [LOG a]
188 -> (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
132
219
133-- --------------------------------------------------------------------- [ EOF ]
220-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effect/Logging/Level.idrdeleted−49
@@ -1,49 +0,0 @@
1−-- -------------------------------------------------------------- [ Levels.idr ]
2−-- Module : Levels.idr
3−-- Copyright : (c) Jan de Muijnck-Hughes
4−-- License : see LICENSE
5−-- --------------------------------------------------------------------- [ EOH ]
6−||| Common aliases and definitions of Logging Levels.
7−module Effect.Logging.Level
8−
9−%access public
10−-- ---------------------------------------------- [ Nat Derived Logging Levels ]
11−--
12−-- Several aliases have been defined to aide in semantic use of the
13−-- logging levels. These aliases have come from the Log4j family of
14−-- loggers.
15−
16−||| No events will be logged.
17−OFF : Nat
18−OFF = 0
19−
20−||| A severe error that will prevent the application from continuing.
21−FATAL : Nat
22−FATAL = 1
23−
24−||| An error in the application, possibly recoverable.
25−ERROR : Nat
26−ERROR = 2
27−
28−||| An event that might possible lead to an error.
29−WARN : Nat
30−WARN = 3
31−
32−||| An event for informational purposes.
33−INFO : Nat
34−INFO = 4
35−
36−||| A general debugging event.
37−DEBUG : Nat
38−DEBUG = 5
39−
40−||| A fine-grained debug message, typically capturing the flow through
41−||| the application.
42−TRACE : Nat
43−TRACE = 6
44−
45−||| All events should be logged.
46−ALL : Nat
47−ALL = 7
48−
49−-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effect/Logging/Simple.idr+1−4
@@ -14,9 +14,6 @@
14module Effect.Logging.Simple
14module Effect.Logging.Simple
15
15
16import Effects
16import Effects
17−import public Effect.Logging.Level
18−
19−import Control.IOExcept -- TODO Add IO Logging Handler
20
17
21||| A Logging effect that displays a logging message to be logged at a
18||| A Logging effect that displays a logging message to be logged at a
22||| certain level.
19||| certain level.
@@ -38,7 +35,7 @@ instance Handler Logging IO where
38 case lvl <= st of
35 case lvl <= st of
39 False => k () st
36 False => k () st
40 True => do
37 True => do
41− printLn $ unwords [show lvl, ":", msg]
38+ putStrLn $ unwords [show lvl, ":", msg]
42 k () st
39 k () st
43
40
44||| Set the logging level.
41||| Set the logging level.
libs/effects/effects.ipkg−1
@@ -15,6 +15,5 @@ modules = Effects
15 , Effect.Memory
15 , Effect.Memory
16 , Effect.System
16 , Effect.System
17 , Effect.Trans
17 , Effect.Trans
18− , Effect.Logging.Level
19 , Effect.Logging
18 , Effect.Logging
20 , Effect.Logging.Simple
19 , Effect.Logging.Simple
test/effects005/defaultlog.idr+3−3
@@ -3,16 +3,16 @@ import Effect.Logging
3
3
4func : Nat -> Eff () [LOG String]
4func : Nat -> Eff () [LOG String]
5func x = do
5func x = do
6− log WARN Nil $ unwords ["I do nothing with", show x]
6+ warn Nil $ unwords ["I do nothing with", show x]
7 pure ()
7 pure ()
8
8
9doubleFunc : Nat -> Eff Nat [LOG String]
9doubleFunc : Nat -> Eff Nat [LOG String]
10doubleFunc x = do
10doubleFunc x = do
11− log WARN ["NumOPS"] $ unwords ["Doing the double with", show x ]
11+ log 40 ["NumOPS"] $ unwords ["Doing the double with", show x ]
12 func x
12 func x
13 pure (x+x)
13 pure (x+x)
14
14
15−eMain : Eff () [LOG String]
15+eMain : Eff Nat [LOG String]
16eMain = do
16eMain = do
17 initLogger ALL ["NumOPS"]
17 initLogger ALL ["NumOPS"]
18 doubleFunc 3
18 doubleFunc 3
test/effects005/expected+2−2
@@ -1,5 +1,5 @@
1−"3 : Doing the double with 3"
1+3 : Doing the double with 3
26
26
38
38
4−"3 : [\"NumOPS\"] : Doing the double with 3"
4+WARN : ["NumOPS"] : Doing the double with 3
56
56
test/effects005/simplelog.idr+3−3
@@ -3,12 +3,12 @@ import Effect.Logging.Simple
3
3
4doubleFunc : Nat -> Eff Nat [LOG]
4doubleFunc : Nat -> Eff Nat [LOG]
5doubleFunc x = do
5doubleFunc x = do
6− log WARN $ unwords ["Doing the double with", show x ]
6+ log 3 $ unwords ["Doing the double with", show x ]
7 pure (x+x)
7 pure (x+x)
8
8
9main : IO ()
9main : IO ()
10main = do
10main = do
11− x <- runInit [ALL] (doubleFunc 3)
11+ x <- runInit [7] (doubleFunc 3)
12 printLn x
12 printLn x
13− y <- runInit [OFF] (doubleFunc 4)
13+ y <- runInit [0] (doubleFunc 4)
14 printLn y
14 printLn y