git.iko.soy/Idris-dev
on cd58dfb help sign in
Idris-dev/libs/effects/Effect/Logging/Level.idr
81 lines 2.5 kB history raw
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.
15module Effect.Logging.Level
17%access public export
18%default total
20-- ---------------------------------------------------- [ Log Level Definition ]
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.
28data LogLevel : Nat -> Type where
29 ||| Log No Events
30 OFF : LogLevel 0
32 ||| A fine-grained debug message, typically capturing the flow through
33 ||| the application.
34 TRACE : LogLevel 10
36 ||| A general debugging event.
37 DEBUG : LogLevel 20
39 ||| An event for informational purposes.
40 INFO : LogLevel 30
42 ||| An event that might possible lead to an error.
43 WARN : LogLevel 40
45 ||| An error in the application, possibly recoverable.
46 ERROR : LogLevel 50
48 ||| A severe error that will prevent the application from continuing.
49 FATAL : LogLevel 60
51 ||| All events should be logged.
52 ALL : LogLevel 70
54 ||| User defined logging level.
55 CUSTOM : (n : Nat) -> {auto prf : LTE n 70} -> LogLevel n
57implementation Cast (LogLevel n) Nat where
58 cast {n} _ = n
60implementation Show (LogLevel n) where
61 showPrec d OFF = "OFF"
62 showPrec d TRACE = "TRACE"
63 showPrec d DEBUG = "DEBUG"
64 showPrec d INFO = "INFO"
65 showPrec d WARN = "WARN"
66 showPrec d FATAL = "FATAL"
67 showPrec d ERROR = "ERROR"
68 showPrec d ALL = "ALL"
69 showPrec d (CUSTOM n) = showCon d "CUSTOM" $ showArg n
71implementation 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
77||| Compare to logging levels.
78cmpLevel : LogLevel a -> LogLevel b -> Ordering
79cmpLevel {a} {b} _ _ = compare a b
81-- --------------------------------------------------------------------- [ EOF ]