blob: 07617758010dd85b19546e65aeda90540ab66e3d (
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
|
module Obs.Logging
import Data.List.Lazy
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
tags : List String
pretty : Message ann -> Doc ann
pretty msg =
hsep $
[ fill 6 (pretty (show msg.lvl) <+> colon) ] ++
reverse (map (\s => pretty s <+> colon) msg.tags) ++
[ align msg.msg ]
-- Logging Monad ---------------------------------------------------------------
export
record Logging (ann, t : Type) where
constructor MkLogging
out : Maybe t
msgs : LazyList (Message ann)
export
Functor (Logging ann) where
map f = {out $= map f}
export
Applicative (Logging ann) where
pure v = MkLogging {out = pure v, msgs = []}
f <*> v = MkLogging {out = f.out <*> v.out, msgs = f.msgs ++ v.msgs}
export
Monad (Logging ann) where
(MkLogging Nothing msgs) >>= f = MkLogging Nothing msgs
(MkLogging (Just v) msgs) >>= f = {msgs $= (msgs ++)} (f v)
-- -- Eliminators -----------------------------------------------------------------
export
discard : Logging ann a -> Maybe a
discard = out
export
logToTerminal : Level -> Logging AnsiStyle a -> IO a
logToTerminal lvl log = do
Lazy.for_ (filter (\msg => msg.lvl <= lvl) log.msgs) (putDoc . pretty)
case log.out of
Just v => pure v
Nothing => exitFailure
export
abort : Logging ann a
abort = MkLogging Nothing []
export
inScope : (tag : String) -> Logging ann a -> Logging ann a
inScope tag = {msgs $= map {tags $= (tag ::)}}
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 = MkLogging (pure ()) [MkMessage lvl msg []]
export
Pretty x => Loggable ann x where
log lvl msg = log lvl $ pretty {ann = ann} msg
export
Loggable ann x => Loggable ann (WithBounds x) where
log lvl msg =
let f : Logging ann () -> Logging ann ()
f = case msg.isIrrelevant of
True => id
False => inScope $
show (1 + msg.bounds.startLine) ++
":" ++
show msg.bounds.startCol ++
"--" ++
show (1 + msg.bounds.endLine) ++
":" ++
show msg.bounds.endCol
in f (log lvl msg.val)
|
