blob: ef0bae6d510b18ff567ce2be791452d2cff812eb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
module Obs.Logging
import System
import Text.Bounded
import public Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.Terminal
-- Logging Levels --------------------------------------------------------------
public export
data Level = Trace | Info | Debug | Warn | Error
export
Show Level where
show Trace = "trace"
show Info = "info"
show Debug = "debug"
show Warn = "warn"
show Error = "error"
levelToNat : Level -> Nat
levelToNat Trace = 4
levelToNat Info = 3
levelToNat Debug = 2
levelToNat Warn = 1
levelToNat Error = 0
export
Eq Level where
l == l' = levelToNat l == levelToNat l'
export
Ord Level where
compare l l' = compare (levelToNat l) (levelToNat l')
-- Logging Messages ------------------------------------------------------------
record Message (ann : Type) where
constructor MkMessage
lvl : Level
msg : Doc ann
bounds : Maybe Bounds
tags : List String
pretty : Message ann -> Doc ann
pretty msg =
let leader =
hsep $
[ fill 6 (pretty (show msg.lvl) <+> colon) ] ++
[ Doc.pretty $ concat {t = List} $
case msg.bounds of
Nothing => []
Just bounds =>
[ show (1 + bounds.startLine)
, ":"
, show bounds.startCol
, "--"
, show (1 + bounds.endLine)
, ":"
, show bounds.endCol
, ":"
]
] ++
map (\s => pretty s <+> colon) msg.tags
in group $ width (group leader <+> line) (\width => group $ indent (2 - width) msg.msg)
-- Logging Monad ---------------------------------------------------------------
export
data Logging : (ann, t : Type) -> Type where
Cont : (msg : Message ann) -> (l : Lazy (Logging ann t)) -> Logging ann t
Abort : Logging ann t
End : (v : t) -> Logging ann t
%name Logging l, l'
export
Functor (Logging ann) where
map f (Cont msg l) = Cont msg (map f l)
map f Abort = Abort
map f (End v) = End (f v)
export
Applicative (Logging ann) where
pure = End
(Cont msg f) <*> v = Cont msg (f <*> v)
Abort <*> v = Abort
(End f) <*> (Cont msg v) = Cont msg (End f <*> v)
(End f) <*> Abort = Abort
(End f) <*> (End v) = End (f v)
export
Monad (Logging ann) where
join (Cont msg l) = Cont msg (join l)
join Abort = Abort
join (End v) = v
-- Eliminators -----------------------------------------------------------------
export
discard : Logging ann a -> Maybe a
discard (Cont msg l) = discard l
discard Abort = Nothing
discard (End v) = Just v
export
logToTerminal : Level -> Logging AnsiStyle a -> IO a
logToTerminal lvl (Cont msg l) = do
() <- if msg.lvl <= lvl then putDoc (pretty msg) else pure ()
logToTerminal lvl l
logToTerminal lvl Abort = exitFailure
logToTerminal lvl (End v) = pure v
export
abort : Logging ann a
abort = Abort
mapMsg : (Message ann -> Message ann') -> Logging ann a -> Logging ann' a
mapMsg f (Cont msg l) = Cont (f msg) (mapMsg f l)
mapMsg f Abort = Abort
mapMsg f (End v) = End v
export
inScope : (tag : String) -> Logging ann a -> Logging ann a
inScope tag = mapMsg {tags $= (tag ::)}
export
inBounds : Bounds -> Logging ann a -> Logging ann a
inBounds bounds = mapMsg {bounds $= maybe (Just bounds) Just}
public export
interface Loggable (0 ann, ty : Type) where
log : Level -> ty -> Logging ann ()
export
trace : Loggable ann ty => ty -> Logging ann ()
trace = log Trace
export
info : Loggable ann ty => ty -> Logging ann ()
info = log Info
export
debug : Loggable ann ty => ty -> Logging ann ()
debug = log Debug
export
warn : Loggable ann ty => ty -> Logging ann ()
warn = log Warn
export
error : Loggable ann ty => ty -> Logging ann ()
error = log Error
export
fatal : Loggable ann ty => ty -> Logging ann a
fatal msg = do error msg; abort
export
Loggable ann (Doc ann) where
log lvl msg = Cont (MkMessage lvl msg Nothing []) $ End ()
export
Pretty x => Loggable ann x where
log lvl msg = log lvl $ pretty {ann = ann} msg
|
