git.iko.soy/Idris-dev
on master help sign in
Merge branch 'jfdm-effLogging-updates'
eb38173Edwin Brady
CHANGELOG+2
compare with master
unifiedsplit
@@ -14,6 +14,8 @@ such, the (-) operator and 'abs' have been moved there from 'Num'.
14* A special version of (-) on 'Nat' requires that the second argument is
14* A special version of (-) on 'Nat' requires that the second argument is
15smaller than or equal to the first. 'minus' retains the old behaviour,
15smaller than or equal to the first. 'minus' retains the old behaviour,
16returning Z if there is an underflow.
16returning Z if there is an underflow.
17+* New Logging Effects have been added to facilitate logging of effectful
18+ programmes.
17
19
18Tool updates
20Tool updates
19------------
21------------
libs/effects/Effect/Logging/Category.idrnew file+184
@@ -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 ]
libs/effects/Effect/Logging/Default.idr+97−36
@@ -2,56 +2,117 @@
2-- Module : Default.idr
2-- Module : Default.idr
3-- Copyright : (c) The Idris Community
3-- Copyright : (c) The Idris Community
4-- License : see LICENSE
4-- License : see LICENSE
5−-- --------------------------------------------------------------------- [ EOH ]
5+--------------------------------------------------------------------- [ EOH ]
6−
7−||| A logging effect that allows messages to be logged using both
6+||| The default logging effect that allows messages to be logged at
8−||| numerical levels and user specified categories. The higher the
7+||| different numerical levels. The higher the number the greater in
9−||| logging level the grater in verbosity the logging.
8+||| verbosity the logging.
10|||
9|||
11||| In this effect the resource we are computing over is the logging
10||| In this effect the resource we are computing over is the logging
12−||| level itself and the list of categories to show.
11+||| level itself.
13|||
12|||
14module Effect.Logging.Default
13module Effect.Logging.Default
15
14
16import Effects
15import Effects
17import public Effect.Logging.Level
16import public Effect.Logging.Level
18
17
19−import Control.IOExcept -- TODO Add IOExcept Logger.
18+%access public
19+
20+-- ------------------------------------------------------------ [ The Resource ]
21+
22+||| The resource that the log effect is defined over.
23+record LogRes where
24+ constructor MkLogRes
25+ getLevel : LogLevel n
20
26
21−||| A Logging effect to log levels and categories.
27+instance Default LogRes where
28+ default = MkLogRes OFF
29+
30+-- ------------------------------------------------------ [ The Logging Effect ]
31+
32+||| A Logging effect that displays a logging message to be logged at a
33+||| certain level.
22data Logging : Effect where
34data Logging : Effect where
23− Log : (Eq a, Show a) =>
35+ ||| Change the logging level.
24− (lvl : Nat)
36+ |||
25− -> (cats : List a)
37+ ||| @lvl The new logging level.
38+ SetLvl : (lvl : LogLevel n)
39+ -> sig Logging () (LogRes) (LogRes)
40+
41+ ||| Log a message.
42+ |||
43+ ||| @lvl The logging level it should appear at.
44+ ||| @msg The message to log.
45+ Log : (lvl : LogLevel n)
26 -> (msg : String)
46 -> (msg : String)
27− -> Logging () (Nat,List a) (\v => (Nat,List a))
47+ -> sig Logging () (LogRes)
28
48
29−||| The Logging effect.
49+-- -------------------------------------------------------------- [ IO Handler ]
30−|||
31−||| @cTy The type used to differentiate categories.
32−LOG : (cTy : Type) -> EFFECT
33−LOG a = MkEff (Nat, List a) Logging
34
50
51+-- For logging in the IO context
35instance Handler Logging IO where
52instance Handler Logging IO where
53+ handle st (SetLvl newLvl) k = k () (MkLogRes newLvl)
36− handle (l,cs) (Log lvl cs' msg) k = do
54+ handle st (Log lvl msg) k = do
37− case lvl <= l of
55+ case cmpLevel lvl (getLevel st) of
38− False => k () (l,cs)
56+ GT => k () st
39− True => do
57+ otherwise => 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]
58+ putStrLn $ unwords [show lvl, ":", msg]
45− k () (l,cs)
59+ k () st
46− else k () (l,cs)
60+
47−
61+-- ------------------------------------------------------- [ Effect Descriptor ]
48−||| Log the given message at the given level and assign it the list of categories.
62+
63+||| A Logging Effect.
64+LOG : EFFECT
65+LOG = MkEff (LogRes) Logging
66+
67+-- ----------------------------------------------------------- [ Effectful API ]
68+
69+||| Set the logging level.
49|||
70|||
50−||| @l The logging level.
71+||| @l The new logging level.
51−||| @cs The logging categories.
72+setLogLvl : (l : LogLevel n) -> Eff () [LOG]
73+setLogLvl l = call $ SetLvl l
74+
75+||| Log `msg` at the given level specified as a natural number.
76+|||
77+||| @l The level to log.
52−||| @m THe message to be logged.
78+||| @m The message to log.
53−log : (Show a, Eq a) => (l : Nat)
79+log : (l : LogLevel n) -> (m : String) -> Eff () [LOG]
80+log l msg = call $ Log l msg
81+
82+||| Log `msg` at the given level specified as a natural number.
83+|||
84+||| @l The level to log.
85+||| @m The message to log.
86+logN : (l : Nat) -> {auto prf : LTE l 70} -> (m : String) -> Eff () [LOG]
87+logN l msg = call $ Log (getProof lvl) msg
88+ where
89+ lvl : (n ** LogLevel n)
90+ lvl = case cast {to=String} (cast {to=Int} l) of
91+ "0" => (_ ** OFF)
92+ "10" => (_ ** TRACE)
93+ "20" => (_ ** DEBUG)
94+ "30" => (_ ** INFO)
95+ "40" => (_ ** WARN)
96+ "50" => (_ ** FATAL)
97+ "60" => (_ ** ERROR)
98+ _ => (_ ** CUSTOM l)
99+
100+trace : String -> Eff () [LOG]
101+trace msg = call $ Log TRACE msg
102+
103+debug : String -> Eff () [LOG]
104+debug msg = call $ Log DEBUG msg
105+
54− -> (cs : List a) -> (m : String) -> Eff () [LOG a]
106+info : String -> Eff () [LOG]
107+info msg = call $ Log INFO msg
108+
109+warn : String -> Eff () [LOG]
110+warn msg = call $ Log WARN msg
111+
112+fatal : String -> Eff () [LOG]
55−log lvl cs msg = call $ Log lvl cs msg
113+fatal msg = call $ Log FATAL msg
114+
115+error : String -> Eff () [LOG]
116+error msg = call $ Log ERROR msg
56
117
57-- --------------------------------------------------------------------- [ EOF ]
118-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effect/Logging/Level.idr+74−42
@@ -1,49 +1,81 @@
1−-- -------------------------------------------------------------- [ Levels.idr ]
1+-- --------------------------------------------------------------- [ Level.idr ]
2−-- Module : Levels.idr
2+-- Module : Level.idr
3−-- Copyright : (c) Jan de Muijnck-Hughes
3+-- Copyright : (c) The Idris Community
4-- License : see LICENSE
4-- License : see LICENSE
5-- --------------------------------------------------------------------- [ EOH ]
5-- --------------------------------------------------------------------- [ EOH ]
6−||| Common aliases and definitions of Logging Levels.
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.
7module Effect.Logging.Level
15module Effect.Logging.Level
8
16
9%access public
17%access public
10−-- ---------------------------------------------- [ Nat Derived Logging Levels ]
18+%default total
11−--
19+
20+-- ---------------------------------------------------- [ Log Level Definition ]
21+
22+||| Logging levels are natural numbers wrapped in a data type for
23+||| convenience.
24+|||
12−-- Several aliases have been defined to aide in semantic use of the
25+||| Several aliases have been defined to aide in semantic use of the
13−-- logging levels. These aliases have come from the Log4j family of
26+||| logging levels. These aliases have come from the Log4j/Python
14−-- loggers.
27+||| family of loggers.
15−
28+data LogLevel : Nat -> Type where
16−||| No events will be logged.
29+ ||| Log No Events
17−OFF : Nat
30+ OFF : LogLevel 0
18−OFF = 0
31+
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
32+ ||| A fine-grained debug message, typically capturing the flow through
41−||| the application.
33+ ||| the application.
42−TRACE : Nat
34+ TRACE : LogLevel 10
43−TRACE = 6
35+
44−
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+
45−||| All events should be logged.
51+ ||| All events should be logged.
46−ALL : Nat
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"
47−ALL = 7
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
48
80
49-- --------------------------------------------------------------------- [ EOF ]
81-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effect/Logging/Simple.idrdeleted−48
@@ -1,48 +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−import public Effect.Logging.Level
18−
19−import Control.IOExcept -- TODO Add IO Logging Handler
20−
21−||| A Logging effect that displays a logging message to be logged at a
22−||| certain level.
23−data Logging : Effect where
24− Log : (lvl : Nat)
25− -> (msg : String)
26− -> Logging () Nat (\v => Nat)
27−
28−||| A Logging Effect.
29−LOG : EFFECT
30−LOG = MkEff Nat Logging
31−
32−-- For logging in the IO context
33−instance Handler Logging IO where
34− handle l (Log lvl msg) k = do
35− case lvl <= l of
36− False => k () l
37− True => do
38− printLn $ unwords [show lvl, ":", msg]
39− k () l
40−
41−||| Log `msg` at the given level.
42−|||
43−||| @l The level to log.
44−||| @m The message to log.
45−log : (l : Nat) -> (m : String) -> Eff () [LOG]
46−log lvl msg = call $ Log lvl msg
47−
48−-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effects.idr+9−9
@@ -25,7 +25,7 @@ data EFFECT : Type where
25 MkEff : Type -> Effect -> EFFECT
25 MkEff : Type -> Effect -> EFFECT
26
26
27-- 'sig' gives the signature for an effect. There are four versions
27-- 'sig' gives the signature for an effect. There are four versions
28−-- depending on whether there is no resource needed,
28+-- depending on whether there is no resource needed,
29-- no state change, a non-dependent change,
29-- no state change, a non-dependent change,
30-- or a dependent change. These are easily disambiguated by type.
30-- or a dependent change. These are easily disambiguated by type.
31
31
@@ -42,7 +42,7 @@ namespace UpdateEffect
42 sig e r e_in e_out = e r e_in (\v => e_out)
42 sig e r e_in e_out = e r e_in (\v => e_out)
43
43
44namespace DepUpdateEffect
44namespace DepUpdateEffect
45− sig : Effect ->
45+ sig : Effect ->
46 (ret : Type) -> (res_in : Type) -> (res_out : ret -> Type) -> Type
46 (ret : Type) -> (res_in : Type) -> (res_out : ret -> Type) -> Type
47 sig e r e_in e_out = e r e_in e_out
47 sig e r e_in e_out = e r e_in e_out
48
48
@@ -193,17 +193,17 @@ namespace TransEff
193 Eff : (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
193 Eff : (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
194 Eff x es ce = {m : Type -> Type} -> EffM m x es (\_ => ce)
194 Eff x es ce = {m : Type -> Type} -> EffM m x es (\_ => ce)
195
195
196− EffT : (m : Type -> Type) ->
196+ EffT : (m : Type -> Type) ->
197 (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
197 (x : Type) -> (es : List EFFECT) -> (ce : List EFFECT) -> Type
198 EffT m x es ce = EffM m x es (\_ => ce)
198 EffT m x es ce = EffM m x es (\_ => ce)
199
199
200namespace DepEff
200namespace DepEff
201 -- Dependent effects, updates dependent on result
201 -- Dependent effects, updates dependent on result
202− Eff : (x : Type) -> (es : List EFFECT)
202+ Eff : (x : Type) -> (es : List EFFECT)
203 -> (ce : x -> List EFFECT) -> Type
203 -> (ce : x -> List EFFECT) -> Type
204 Eff x es ce = {m : Type -> Type} -> EffM m x es ce
204 Eff x es ce = {m : Type -> Type} -> EffM m x es ce
205
205
206− EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT)
206+ EffT : (m : Type -> Type) -> (x : Type) -> (es : List EFFECT)
207 -> (ce : x -> List EFFECT) -> Type
207 -> (ce : x -> List EFFECT) -> Type
208 EffT m x es ce = EffM m x es ce
208 EffT m x es ce = EffM m x es ce
209
209
@@ -269,7 +269,7 @@ eff env (callP prf effP) k = execEff env prf effP k
269eff env (liftP prf effP) k
269eff env (liftP prf effP) k
270 = let env' = dropEnv env prf in
270 = let env' = dropEnv env prf in
271 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
271 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
272−eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k
272+eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k
273 = eff (res :: env) effP (\p', (val :: envk) => k p' envk)
273 = eff (res :: env) effP (\p', (val :: envk) => k p' envk)
274-- FIXME:
274-- FIXME:
275-- xs is needed explicitly because otherwise the pattern binding for
275-- xs is needed explicitly because otherwise the pattern binding for
@@ -313,7 +313,7 @@ lift e {prf} = liftP prf e
313|||
313|||
314||| @prog The effectful program to run.
314||| @prog The effectful program to run.
315%no_implicit
315%no_implicit
316−run : Applicative m =>
316+run : Applicative m =>
317 (prog : EffM m a xs xs') -> {default MkDefaultEnv env : Env m xs} ->
317 (prog : EffM m a xs xs') -> {default MkDefaultEnv env : Env m xs} ->
318 m a
318 m a
319run prog {env} = eff env prog (\r, env => pure r)
319run prog {env} = eff env prog (\r, env => pure r)
@@ -325,8 +325,8 @@ run prog {env} = eff env prog (\r, env => pure r)
325|||
325|||
326||| @prog The effectful program to run.
326||| @prog The effectful program to run.
327%no_implicit
327%no_implicit
328−runPure : (prog : EffM id a xs xs') ->
328+runPure : (prog : EffM id a xs xs') ->
329− {default MkDefaultEnv env : Env id xs} -> a
329+ {default MkDefaultEnv env : Env id xs} -> a
330runPure prog {env} = eff env prog (\r, env => r)
330runPure prog {env} = eff env prog (\r, env => r)
331
331
332||| Run an effectful program in a given context `m` with a default value for the environment.
332||| Run an effectful program in a given context `m` with a default value for the environment.
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.Simple
20 , Effect.Logging.Default
19 , Effect.Logging.Default
20+ , Effect.Logging.Category
test/effects005/categoryLogger.idrnew file+23
@@ -0,0 +1,23 @@
1+import Effects
2+import Effect.Logging.Category
3+
4+func : Nat -> Eff () [LOG String]
5+func x = do
6+ warn Nil $ unwords ["I do nothing with", show x]
7+ pure ()
8+
9+doubleFunc : Nat -> Eff Nat [LOG String]
10+doubleFunc x = do
11+ logN 40 ["NumOPS"] $ unwords ["Doing the double with", show x ]
12+ func x
13+ pure (x+x)
14+
15+eMain : Eff Nat [LOG String]
16+eMain = do
17+ initLogger ALL ["NumOPS"]
18+ doubleFunc 3
19+
20+main : IO ()
21+main = do
22+ x <- run eMain
23+ printLn x
test/effects005/defaultLogger.idrnew file+14
@@ -0,0 +1,14 @@
1+import Effects
2+import Effect.Logging.Default
3+
4+doubleFunc : Nat -> Eff Nat [LOG]
5+doubleFunc x = do
6+ warn $ unwords ["Doing the double with", show x ]
7+ pure (x+x)
8+
9+main : IO ()
10+main = do
11+ x <- runInit [MkLogRes ALL] (doubleFunc 3)
12+ printLn x
13+ y <- run (doubleFunc 4)
14+ printLn y
test/effects005/defaultlog.idrdeleted−18
@@ -1,18 +0,0 @@
1−import Effects
2−import Effect.Logging.Default
3−
4−func : Nat -> Eff () [LOG String]
5−func x = do
6− log WARN Nil $ unwords ["I do nothing with", show x]
7− pure ()
8−
9−doubleFunc : Nat -> Eff Nat [LOG String]
10−doubleFunc x = do
11− log WARN ["NumOPS"] $ unwords ["Doing the double with", show x ]
12− func x
13− pure (x+x)
14−
15−main : IO ()
16−main = do
17− x <- runInit [(ALL,["NumOPS"])] (doubleFunc 3)
18− printLn x
test/effects005/expected+2−2
@@ -1,5 +1,5 @@
1−"3 : Doing the double with 3"
1+WARN : 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/run+4−4
@@ -1,6 +1,6 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2−idris $@ simplelog.idr -o simple -p effects
3−./simple
4−idris $@ defaultlog.idr -o default -p effects
2+idris $@ defaultLogger.idr -o default -p effects
5./default
3./default
4+idris $@ categoryLogger.idr -o category -p effects
5+./category
6−rm -f simple default *.ibc
6+rm -f default category *.ibc
test/effects005/simplelog.idrdeleted−14
@@ -1,14 +0,0 @@
1−import Effects
2−import Effect.Logging.Simple
3−
4−doubleFunc : Nat -> Eff Nat [LOG]
5−doubleFunc x = do
6− log WARN $ unwords ["Doing the double with", show x ]
7− pure (x+x)
8−
9−main : IO ()
10−main = do
11− x <- runInit [ALL] (doubleFunc 3)
12− printLn x
13− y <- runInit [OFF] (doubleFunc 4)
14− printLn y