git.iko.soy/Idris-dev
on master help sign in
Renamed Logging Effects, improved simple logger

+ Renamed the simple logging effect to default as it is composable accross effectful programs. + Simple logger uses same levels as category loggerl. + The category logger is now category.

commit40481dc6e653dc0a07163671c4fc71e27b1d1b0a authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateWed 26 Aug 2015, 21:32 (11 years ago) parentd57d929
5 files changed+216−129
compare with master
unifiedsplit
libs/effects/Effect/Logging.idr → libs/effects/Effect/Logging/Category.idr+23−73 libs/effects/Effect/Logging/Default.idr+109 libs/effects/Effect/Logging/Level.idr+81 libs/effects/Effect/Logging/Simple.idr−54 libs/effects/effects.ipkg+3−2
libs/effects/Effect/Logging.idr → libs/effects/Effect/Logging/Category.idrrenamed+23−73
@@ -1,88 +1,29 @@
1−-- ------------------------------------------------------------- [ Logging.idr ]
2−-- Module : Logging.idr
1+-- ------------------------------------------------------------ [ Category.idr ]
2+-- Module : Category.idr
33-- Copyright : (c) The Idris Community
44-- License : see LICENSE
55-- --------------------------------------------------------------------- [ EOH ]
6−
76||| A logging effect that allows messages to be logged using both
87||| numerical levels and user specified categories. The higher the
98||| logging level the grater in verbosity the logging.
109|||
1110||| In this effect the resource we are computing over is the logging
1211||| level itself and the list of categories to show.
13−|||
14−module Effect.Logging
12+module Effect.Logging.Category
1513
1614import Effects
15+import public Effect.Logging.Level
1716
1817%access public
1918
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− ||| An error in the application, possibly recoverable.
46− ERROR : LogLevel 50
47−
48− ||| A severe error that will prevent the application from continuing.
49− FATAL : 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
19+-- -------------------------------------------------------- [ Logging Resource ]
7920
8021||| The Logging details, this is the resource that the effect is
8122||| defined over.
8223record LogRes (a : Type) where
8324 constructor MkLogRes
84− lvl : LogLevel n
85− cats : List a
25+ getLevel : LogLevel n
26+ getCategories : List a
8627
8728instance (Show a) => Show (LogRes a) where
8829 show (MkLogRes l cs) = unwords ["Log Settings:", show l, show cs]
@@ -90,6 +31,8 @@ instance (Show a) => Show (LogRes a) where
9031instance Default (LogRes a) where
9132 default = MkLogRes OFF Nil
9233
34+-- ------------------------------------------------------- [ Effect Definition ]
35+
9336||| A Logging effect to log levels and categories.
9437data Logging : Effect where
9538 ||| Log a message.
@@ -126,12 +69,14 @@ data Logging : Effect where
12669 (ncats : List a) ->
12770 sig Logging () (LogRes a) (LogRes a)
12871
72+-- -------------------------------------------------------------- [ IO Handler ]
73+
12974instance Handler Logging IO where
13075 handle st (SetLogLvl nlvl) k = do
131− let newSt = record {lvl = nlvl} st
76+ let newSt = record {getLevel = nlvl} st
13277 k () newSt
13378 handle st (SetLogCats newcs) k = do
134− let newSt = record {cats = newcs} st
79+ let newSt = record {getCategories = newcs} st
13580 k () newSt
13681
13782 handle st (InitLogger l cs) k = do
@@ -139,25 +84,30 @@ instance Handler Logging IO where
13984 k () newSt
14085
14186 handle st (Log l cs' msg) k = do
142− case cmpLevel l (lvl st) of
87+ case cmpLevel l (getLevel st) of
14388 GT => k () st
14489 otherwise => do
145− let res = and $ map (\x => elem x cs') (cats st)
146− let prompt = if isNil (cats st)
90+ let res = and $ map (\x => elem x cs') (getCategories st)
91+ let prompt = if isNil (getCategories st)
14792 then unwords [show l, ":"]
148− else unwords [show l, ":", show (cats st), ":"]
149− if res || isNil (cats st)
93+ else unwords [show l, ":", show (getCategories st), ":"]
94+ if res || isNil (getCategories st)
15095 then do
15196 putStrLn $ unwords [prompt, msg]
15297 k () st
15398 else k () st
15499
100+
101+-- ------------------------------------------------------- [ Effect Descriptor ]
102+
155103||| The Logging effect.
156104|||
157105||| @cTy The type used to differentiate categories.
158106LOG : (cTy : Type) -> EFFECT
159107LOG cTy = MkEff (LogRes cTy) Logging
160108
109+-- ----------------------------------------------------------- [ Effectful API ]
110+
161111||| Change the logging level.
162112|||
163113||| @l The new logging level.
libs/effects/Effect/Logging/Default.idrnew file+109
@@ -0,0 +1,109 @@
1+-- ------------------------------------------------------------- [ Default.idr ]
2+-- Module : Default.idr
3+-- Copyright : (c) The Idris Community
4+-- License : see LICENSE
5+--------------------------------------------------------------------- [ EOH ]
6+||| The default logging effect that allows messages to be logged at
7+||| different numerical levels. The higher the number the greater in
8+||| verbosity the logging.
9+|||
10+||| In this effect the resource we are computing over is the logging
11+||| level itself.
12+|||
13+module Effect.Logging.Default
14+
15+import Effects
16+import public Effect.Logging.Level
17+
18+-- ------------------------------------------------------------ [ The Resource ]
19+
20+||| The resource that the log effect is defined over.
21+record LogRes where
22+ constructor MkLogRes
23+ getLevel : LogLevel n
24+
25+instance Default LogRes where
26+ default = MkLogRes OFF
27+
28+-- ------------------------------------------------------ [ The Logging Effect ]
29+
30+||| A Logging effect that displays a logging message to be logged at a
31+||| certain level.
32+data Logging : Effect where
33+ ||| Change the logging level.
34+ |||
35+ ||| @lvl The new logging level.
36+ SetLvl : (lvl : LogLevel n)
37+ -> sig Logging () (LogRes) (LogRes)
38+
39+ ||| Log a message.
40+ |||
41+ ||| @lvl The logging level it should appear at.
42+ ||| @msg The message to log.
43+ Log : (lvl : LogLevel n)
44+ -> (msg : String)
45+ -> sig Logging () (LogRes)
46+
47+-- -------------------------------------------------------------- [ IO Handler ]
48+
49+-- For logging in the IO context
50+instance Handler Logging IO where
51+ handle st (SetLvl newLvl) k = k () (MkLogRes newLvl)
52+ handle st (Log lvl msg) k = do
53+ case cmpLevel lvl (getLevel st) of
54+ GT => k () st
55+ otherwise => do
56+ putStrLn $ unwords [show lvl, ":", msg]
57+ k () st
58+
59+-- ------------------------------------------------------- [ Effect Descriptor ]
60+
61+||| A Logging Effect.
62+LOG : EFFECT
63+LOG = MkEff (LogRes) Logging
64+
65+-- ----------------------------------------------------------- [ Effectful API ]
66+
67+||| Set the logging level.
68+|||
69+||| @l The new logging level.
70+setLogLvl : (l : LogLevel n) -> Eff () [LOG]
71+setLogLvl l = call $ SetLvl l
72+
73+||| Log `msg` at the given level.
74+|||
75+||| @l The level to log.
76+||| @m The message to log.
77+log : (l : Nat) -> {auto prf : LTE l 70} -> (m : String) -> Eff () [LOG]
78+log l msg = call $ Log (getProof lvl) msg
79+ where
80+ lvl : (n ** LogLevel n)
81+ lvl = case cast {to=String} (cast {to=Int} l) of
82+ "0" => (_ ** OFF)
83+ "10" => (_ ** TRACE)
84+ "20" => (_ ** DEBUG)
85+ "30" => (_ ** INFO)
86+ "40" => (_ ** WARN)
87+ "50" => (_ ** FATAL)
88+ "60" => (_ ** ERROR)
89+ _ => (_ ** CUSTOM l)
90+
91+trace : String -> Eff () [LOG]
92+trace msg = call $ Log TRACE msg
93+
94+debug : String -> Eff () [LOG]
95+debug msg = call $ Log DEBUG msg
96+
97+info : String -> Eff () [LOG]
98+info msg = call $ Log INFO msg
99+
100+warn : String -> Eff () [LOG]
101+warn msg = call $ Log WARN msg
102+
103+fatal : String -> Eff () [LOG]
104+fatal msg = call $ Log FATAL msg
105+
106+error : String -> Eff () [LOG]
107+error msg = call $ Log ERROR msg
108+
109+-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effect/Logging/Level.idrnew file+81
@@ -0,0 +1,81 @@
1+-- --------------------------------------------------------------- [ Level.idr ]
2+-- Module : Level.idr
3+-- Copyright : (c) The Idris Community
4+-- License : see LICENSE
5+-- --------------------------------------------------------------------- [ EOH ]
6+||| A dependently typed logging level representation where logging
7+||| levels are based on a Natural number range [0,70].
8+|||
9+||| The `LogLevel` type allows for semantic constructors to be used
10+||| for the majority of logging levels, with an option for custom
11+||| levels to be defined.
12+|||
13+||| The logging level design comes from the Log4j/Python family of
14+||| loggers.
15+module Effect.Logging.Level
16+
17+%access public
18+%default total
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+ ||| An error in the application, possibly recoverable.
46+ ERROR : LogLevel 50
47+
48+ ||| A severe error that will prevent the application from continuing.
49+ FATAL : 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+||| Compare to logging levels.
78+cmpLevel : LogLevel a -> LogLevel b -> Ordering
79+cmpLevel {a} {b} _ _ = compare a b
80+
81+-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effect/Logging/Simple.idrdeleted−54
@@ -1,54 +0,0 @@
1−-- -------------------------------------------------------------- [ Simple.idr ]
2−-- Module : Logging.idr
3−-- Copyright : (c) The Idris Community
4−-- License : see LICENSE
5−--------------------------------------------------------------------- [ EOH ]
6−
7−||| A simple logging effect that allows messages to be logged at
8−||| different numerical level. The higher the number the grater in
9−||| verbosity the logging.
10−|||
11−||| In this effect the resource we are computing over is the logging
12−||| level itself.
13−|||
14−module Effect.Logging.Simple
15−
16−import Effects
17−
18−||| A Logging effect that displays a logging message to be logged at a
19−||| certain level.
20−data Logging : Effect where
21− SetLvl : (lvl : Nat)
22− -> sig Logging () Nat Nat
23− Log : (lvl : Nat)
24− -> (msg : String)
25− -> sig Logging () Nat
26−
27−||| A Logging Effect.
28−LOG : EFFECT
29−LOG = MkEff Nat Logging
30−
31−-- For logging in the IO context
32−instance Handler Logging IO where
33− handle st (SetLvl newL) k = k () st
34− handle st (Log lvl msg) k = do
35− case lvl <= st of
36− False => k () st
37− True => do
38− putStrLn $ unwords [show lvl, ":", msg]
39− k () st
40−
41−||| Set the logging level.
42−|||
43−||| @l The new logging level.
44−setLogLvl : (l : Nat) -> Eff () [LOG]
45−setLogLvl l = call $ SetLvl l
46−
47−||| Log `msg` at the given level.
48−|||
49−||| @l The level to log.
50−||| @m The message to log.
51−log : (l : Nat) -> (m : String) -> Eff () [LOG]
52−log lvl msg = call $ Log lvl msg
53−
54−-- --------------------------------------------------------------------- [ EOF ]
libs/effects/effects.ipkg+3−2
@@ -15,5 +15,6 @@ modules = Effects
1515 , Effect.Memory
1616 , Effect.System
1717 , Effect.Trans
18− , Effect.Logging
19− , Effect.Logging.Simple
18+ , Effect.Logging.Level
19+ , Effect.Logging.Default
20+ , Effect.Logging.Category