-
Notifications
You must be signed in to change notification settings - Fork 389
/
Message.lean
282 lines (225 loc) · 12.8 KB
/
Message.lean
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
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
/-
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sebastian Ullrich, Leonardo de Moura
Message Type used by the Lean frontend
-/
import Lean.Data.Position
import Lean.Data.OpenDecl
import Lean.Syntax
import Lean.MetavarContext
import Lean.Environment
import Lean.Util.PPExt
import Lean.Util.PPGoal
namespace Lean
def mkErrorStringWithPos (fileName : String) (line col : Nat) (msg : String) : String :=
fileName ++ ":" ++ toString line ++ ":" ++ toString col ++ " " ++ toString msg
inductive MessageSeverity
| information | warning | error
structure MessageDataContext :=
(env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options)
structure NamingContext :=
(currNamespace : Name) (openDecls : List OpenDecl)
/- Structure message data. We use it for reporting errors, trace messages, etc. -/
inductive MessageData
| ofFormat : Format → MessageData
| ofSyntax : Syntax → MessageData
| ofExpr : Expr → MessageData
| ofLevel : Level → MessageData
| ofName : Name → MessageData
| ofGoal : MVarId → MessageData
/- `withContext ctx d` specifies the pretty printing context `(env, mctx, lctx, opts)` for the nested expressions in `d`. -/
| withContext : MessageDataContext → MessageData → MessageData
| withNamingContext : NamingContext → MessageData → MessageData
/- Lifted `Format.nest` -/
| nest : Nat → MessageData → MessageData
/- Lifted `Format.group` -/
| group : MessageData → MessageData
/- Lifted `Format.compose` -/
| compose : MessageData → MessageData → MessageData
/- Tagged sections. `Name` should be viewed as a "kind", and is used by `MessageData` inspector functions.
Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/
| tagged : Name → MessageData → MessageData
| node : Array MessageData → MessageData
namespace MessageData
instance : Inhabited MessageData := ⟨MessageData.ofFormat (arbitrary _)⟩
@[init] def stxMaxDepthOption : IO Unit :=
registerOption `syntaxMaxDepth { defValue := (2 : Nat), group := "", descr := "maximum depth when displaying syntax objects in messages" }
def getSyntaxMaxDepth (opts : Options) : Nat :=
opts.getNat `syntaxMaxDepth 2
private def sanitizeNames (ctx : MessageDataContext) : MessageDataContext :=
{ ctx with lctx := ctx.lctx.sanitizeNames ctx.opts }
def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext :=
{ env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts,
currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls }
partial def formatAux : NamingContext → Option MessageDataContext → MessageData → IO Format
| _, _, ofFormat fmt => pure fmt
| _, _, ofLevel u => pure $ fmt u
| _, _, ofName n => pure $ fmt n
| _, some ctx, ofSyntax s => pure $ s.formatStx (getSyntaxMaxDepth ctx.opts)
| _, none, ofSyntax s => pure $ s.formatStx
| _, none, ofExpr e => pure $ format (toString e)
| nCtx, some ctx, ofExpr e => ppExpr (mkPPContext nCtx ctx) e
| _, none, ofGoal mvarId => pure $ "goal " ++ format (mkMVar mvarId)
| nCtx, some ctx, ofGoal mvarId => ppGoal (mkPPContext nCtx ctx) mvarId
| nCtx, _, withContext ctx d => formatAux nCtx (some $ sanitizeNames ctx) d
| _, ctx, withNamingContext nCtx d => formatAux nCtx ctx d
| nCtx, ctx, tagged cls d => do d ← formatAux nCtx ctx d; pure $ Format.sbracket (format cls) ++ " " ++ d
| nCtx, ctx, nest n d => Format.nest n <$> formatAux nCtx ctx d
| nCtx, ctx, compose d₁ d₂ => do d₁ ← formatAux nCtx ctx d₁; d₂ ← formatAux nCtx ctx d₂; pure $ d₁ ++ d₂
| nCtx, ctx, group d => Format.group <$> formatAux nCtx ctx d
| nCtx, ctx, node ds => Format.nest 2 <$> ds.foldlM (fun r d => do d ← formatAux nCtx ctx d; pure $ r ++ Format.line ++ d) Format.nil
protected def format (msgData : MessageData) : IO Format :=
formatAux { currNamespace := Name.anonymous, openDecls := [] } none msgData
protected def toString (msgData : MessageData) : IO String := do
fmt ← msgData.format;
pure $ toString fmt
instance : HasAppend MessageData := ⟨compose⟩
instance hasCoeOfFormat : HasCoe Format MessageData := ⟨ofFormat⟩
instance hasCoeOfLevel : HasCoe Level MessageData := ⟨ofLevel⟩
instance hasCoeOfExpr : HasCoe Expr MessageData := ⟨ofExpr⟩
instance hasCoeOfName : HasCoe Name MessageData := ⟨ofName⟩
instance hasCoeOfSyntax : HasCoe Syntax MessageData := ⟨ofSyntax⟩
instance hasCoeOfOptExpr : HasCoe (Option Expr) MessageData :=
⟨fun o => match o with | none => "none" | some e => ofExpr e⟩
instance coeOfString : Coe String MessageData := ⟨ofFormat ∘ format⟩
instance coeOfFormat : Coe Format MessageData := ⟨ofFormat⟩
instance coeOfLevel : Coe Level MessageData := ⟨ofLevel⟩
instance coeOfExpr : Coe Expr MessageData := ⟨ofExpr⟩
instance coeOfName : Coe Name MessageData := ⟨ofName⟩
instance coeOfSyntax : Coe Syntax MessageData := ⟨ofSyntax⟩
instance coeOfOptExpr : Coe (Option Expr) MessageData :=
⟨fun o => match o with | none => "none" | some e => ofExpr e⟩
partial def arrayExpr.toMessageData (es : Array Expr) : Nat → MessageData → MessageData
| i, acc =>
if h : i < es.size then
let e := es.get ⟨i, h⟩;
let acc := if i == 0 then acc ++ ofExpr e else acc ++ ", " ++ ofExpr e;
arrayExpr.toMessageData (i+1) acc
else
acc ++ "]"
instance hasCoeOfArrayExpr : HasCoe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩
instance coeOfArrayExpr : Coe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩
def bracket (l : String) (f : MessageData) (r : String) : MessageData := group (nest l.length $ l ++ f ++ r)
def paren (f : MessageData) : MessageData := bracket "(" f ")"
def sbracket (f : MessageData) : MessageData := bracket "[" f "]"
def joinSep : List MessageData → MessageData → MessageData
| [], sep => Format.nil
| [a], sep => a
| a::as, sep => a ++ sep ++ joinSep as sep
def ofList: List MessageData → MessageData
| [] => "[]"
| xs => sbracket $ joinSep xs ("," ++ Format.line)
def ofArray (msgs : Array MessageData) : MessageData :=
ofList msgs.toList
instance hasCoeOfList : HasCoe (List MessageData) MessageData := ⟨ofList⟩
instance hasCoeOfListExpr : HasCoe (List Expr) MessageData := ⟨fun es => ofList $ es.map ofExpr⟩
instance coeOfList : Coe (List MessageData) MessageData := ⟨ofList⟩
instance coeOfListExpr : Coe (List Expr) MessageData := ⟨fun es => ofList $ es.map ofExpr⟩
end MessageData
structure Message :=
(fileName : String)
(pos : Position)
(endPos : Option Position := none)
(severity : MessageSeverity := MessageSeverity.error)
(caption : String := "")
(data : MessageData)
@[export lean_mk_message]
def mkMessageEx (fileName : String) (pos : Position) (endPos : Option Position) (severity : MessageSeverity) (caption : String) (text : String) : Message :=
{ fileName := fileName, pos := pos, endPos := endPos, severity := severity, caption := caption, data := text }
namespace Message
protected def toString (msg : Message) : IO String := do
str ← msg.data.toString;
pure $ mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column
((match msg.severity with
| MessageSeverity.information => ""
| MessageSeverity.warning => "warning: "
| MessageSeverity.error => "error: ") ++
(if msg.caption == "" then "" else msg.caption ++ ":\n") ++ str)
instance : Inhabited Message :=
⟨{ fileName := "", pos := ⟨0, 1⟩, data := arbitrary _}⟩
@[export lean_message_pos] def getPostEx (msg : Message) : Position := msg.pos
@[export lean_message_severity] def getSeverityEx (msg : Message) : MessageSeverity := msg.severity
@[export lean_message_string] unsafe def getMessageStringEx (msg : Message) : String :=
match unsafeIO (msg.data.toString) with -- hack: this is going to be deleted
| Except.ok msg => msg
| Except.error e => "error formatting message: " ++ toString e
end Message
structure MessageLog :=
(msgs : Std.PersistentArray Message := {})
namespace MessageLog
def empty : MessageLog := ⟨{}⟩
def isEmpty (log : MessageLog) : Bool :=
log.msgs.isEmpty
instance : Inhabited MessageLog := ⟨{}⟩
def add (msg : Message) (log : MessageLog) : MessageLog :=
⟨log.msgs.push msg⟩
protected def append (l₁ l₂ : MessageLog) : MessageLog :=
⟨l₁.msgs ++ l₂.msgs⟩
instance : HasAppend MessageLog :=
⟨MessageLog.append⟩
def hasErrors (log : MessageLog) : Bool :=
log.msgs.any $ fun m => match m.severity with
| MessageSeverity.error => true
| _ => false
def errorsToWarnings (log : MessageLog) : MessageLog :=
{ msgs := log.msgs.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }
def getInfoMessages (log : MessageLog) : MessageLog :=
{ msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.information => true | _ => false }
def forM {m : Type → Type} [Monad m] (log : MessageLog) (f : Message → m Unit) : m Unit :=
log.msgs.forM f
def toList (log : MessageLog) : List Message :=
(log.msgs.foldl (fun acc msg => msg :: acc) []).reverse
end MessageLog
def MessageData.nestD (msg : MessageData) : MessageData :=
MessageData.nest 2 msg
def indentD (msg : MessageData) : MessageData :=
MessageData.nestD (Format.line ++ msg)
def indentExpr (e : Expr) : MessageData :=
indentD e
namespace KernelException
private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData :=
MessageData.withContext { env := env, mctx := {}, lctx := lctx, opts := opts } msg
def toMessageData (e : KernelException) (opts : Options) : MessageData :=
match e with
| unknownConstant env constName => mkCtx env {} opts $ "(kernel) unknown constant " ++ constName
| alreadyDeclared env constName => mkCtx env {} opts $ "(kernel) constant has already been declared " ++ constName
| declTypeMismatch env decl givenType =>
let process (n : Name) (expectedType : Expr) : MessageData :=
"(kernel) declaration type mismatch " ++ n
++ Format.line ++ "has type" ++ indentExpr givenType
++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType;
match decl with
| Declaration.defnDecl { name := n, type := type, .. } => process n type
| Declaration.thmDecl { name := n, type := type, .. } => process n type
| _ => "(kernel) declaration type mismatch" -- TODO fix type checker, type mismatch for mutual decls does not have enough information
| declHasMVars env constName _ => mkCtx env {} opts $ "(kernel) declaration has metavariables " ++ constName
| declHasFVars env constName _ => mkCtx env {} opts $ "(kernel) declaration has free variables " ++ constName
| funExpected env lctx e => mkCtx env lctx opts $ "(kernel) function expected" ++ indentExpr e
| typeExpected env lctx e => mkCtx env lctx opts $ "(kernel) type expected" ++ indentExpr e
| letTypeMismatch env lctx n _ _ => mkCtx env lctx opts $ "(kernel) let-declaration type mismatch " ++ n
| exprTypeMismatch env lctx e _ => mkCtx env lctx opts $ "(kernel) type mismatch at " ++ indentExpr e
| appTypeMismatch env lctx e fnType argType =>
mkCtx env lctx opts $
"application type mismatch" ++ indentExpr e
++ Format.line ++ "argument has type" ++ indentExpr argType
++ Format.line ++ "but function has type" ++ indentExpr fnType
| invalidProj env lctx e => mkCtx env lctx opts $ "(kernel) invalid projection" ++ indentExpr e
| other msg => "(kernel) " ++ msg
end KernelException
class AddMessageContext (m : Type → Type) :=
(addMessageContext : MessageData → m MessageData)
export AddMessageContext (addMessageContext)
instance addMessageContextTrans (m n) [AddMessageContext m] [MonadLift m n] : AddMessageContext n :=
{ addMessageContext := fun msg => liftM (addMessageContext msg : m _) }
def addMessageContextPartial {m} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
env ← getEnv;
opts ← getOptions;
pure $ MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msgData
def addMessageContextFull {m} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
env ← getEnv;
mctx ← getMCtx;
lctx ← getLCtx;
opts ← getOptions;
pure $ MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData
end Lean