git.iko.soy/Idris-dev
on master help sign in
Updated Logging Effect.
6422545Jan de Muijnck-Hughes
libs/effects/Effect/Logging.idrnew file+133
compare with master
unifiedsplit
@@ -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 ]
libs/effects/Effect/Logging/Default.idrdeleted−57
@@ -1,57 +0,0 @@
1−-- ------------------------------------------------------------- [ Default.idr ]
2−-- Module : Default.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.Default
15−
16−import Effects
17−import public Effect.Logging.Level
18−
19−import Control.IOExcept -- TODO Add IOExcept Logger.
20−
21−||| A Logging effect to log levels and categories.
22−data Logging : Effect where
23− Log : (Eq a, Show a) =>
24− (lvl : Nat)
25− -> (cats : List a)
26− -> (msg : String)
27− -> Logging () (Nat,List a) (\v => (Nat,List a))
28−
29−||| The Logging effect.
30−|||
31−||| @cTy The type used to differentiate categories.
32−LOG : (cTy : Type) -> EFFECT
33−LOG a = MkEff (Nat, List a) Logging
34−
35−instance Handler Logging IO where
36− handle (l,cs) (Log lvl cs' msg) k = do
37− case lvl <= l of
38− False => k () (l,cs)
39− True => do
40− let res = and $ map (\x => elem x cs') cs
41− let prompt = if isNil cs then "" else show cs
42− if res || isNil cs
43− then do
44− printLn $ unwords [show lvl, ":", prompt, ":", msg]
45− k () (l,cs)
46− else k () (l,cs)
47−
48−||| Log the given message at the given level and assign it the list of categories.
49−|||
50−||| @l The logging level.
51−||| @cs The logging categories.
52−||| @m THe message to be logged.
53−log : (Show a, Eq a) => (l : Nat)
54− -> (cs : List a) -> (m : String) -> Eff () [LOG a]
55−log lvl cs msg = call $ Log lvl cs msg
56−
57−-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effect/Logging/Simple.idr+14−5
@@ -21,9 +21,11 @@ import Control.IOExcept -- TODO Add IO Logging Handler
21||| A Logging effect that displays a logging message to be logged at a
21||| A Logging effect that displays a logging message to be logged at a
22||| certain level.
22||| certain level.
23data Logging : Effect where
23data Logging : Effect where
24+ SetLvl : (lvl : Nat)
25+ -> sig Logging () Nat Nat
24 Log : (lvl : Nat)
26 Log : (lvl : Nat)
25 -> (msg : String)
27 -> (msg : String)
26− -> Logging () Nat (\v => Nat)
28+ -> sig Logging () Nat
27
29
28||| A Logging Effect.
30||| A Logging Effect.
29LOG : EFFECT
31LOG : EFFECT
@@ -31,12 +33,19 @@ LOG = MkEff Nat Logging
31
33
32-- For logging in the IO context
34-- For logging in the IO context
33instance Handler Logging IO where
35instance Handler Logging IO where
36+ handle st (SetLvl newL) k = k () st
34− handle l (Log lvl msg) k = do
37+ handle st (Log lvl msg) k = do
35− case lvl <= l of
38+ case lvl <= st of
36− False => k () l
39+ False => k () st
37 True => do
40 True => do
38 printLn $ unwords [show lvl, ":", msg]
41 printLn $ unwords [show lvl, ":", msg]
39− k () l
42+ k () st
43+
44+||| Set the logging level.
45+|||
46+||| @l The new logging level.
47+setLogLvl : (l : Nat) -> Eff () [LOG]
48+setLogLvl l = call $ SetLvl l
40
49
41||| Log `msg` at the given level.
50||| Log `msg` at the given level.
42|||
51|||
libs/effects/effects.ipkg+1−1
@@ -16,5 +16,5 @@ modules = Effects
16 , Effect.System
16 , Effect.System
17 , Effect.Trans
17 , Effect.Trans
18 , Effect.Logging.Level
18 , Effect.Logging.Level
19+ , Effect.Logging
19 , Effect.Logging.Simple
20 , Effect.Logging.Simple
20− , Effect.Logging.Default
test/effects005/defaultlog.idr+7−2
@@ -1,5 +1,5 @@
1import Effects
1import Effects
2−import Effect.Logging.Default
2+import Effect.Logging
3
3
4func : Nat -> Eff () [LOG String]
4func : Nat -> Eff () [LOG String]
5func x = do
5func x = do
@@ -12,7 +12,12 @@ doubleFunc x = do
12 func x
12 func x
13 pure (x+x)
13 pure (x+x)
14
14
15+eMain : Eff () [LOG String]
16+eMain = do
17+ initLogger ALL ["NumOPS"]
18+ doubleFunc 3
19+
15main : IO ()
20main : IO ()
16main = do
21main = do
17− x <- runInit [(ALL,["NumOPS"])] (doubleFunc 3)
22+ x <- run eMain
18 printLn x
23 printLn x