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
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
|
(* Copyright (c) 2008, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* - Redistributions of source code must retain the above copyright notice,
* this list of conditions and the following disclaimer.
* - Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
* - The names of contributors may not be used to endorse or promote products
* derived from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
* ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
* LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
* CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
* SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
* CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
* ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
* POSSIBILITY OF SUCH DAMAGE.
*)
structure ElabErr :> ELAB_ERR = struct
structure L = Source
open Elab
structure E = ElabEnv
structure U = ElabUtil
open Print
structure P = ElabPrint
val simplCon = U.Con.mapB {kind = fn _ => fn k => k,
con = fn env => fn c =>
let
val c = (c, ErrorMsg.dummySpan)
val c' = ElabOps.hnormCon env c
in
(*prefaces "simpl" [("c", P.p_con env c),
("c'", P.p_con env c')];*)
#1 c'
end,
bind = fn (env, U.Con.RelC (x, k)) => E.pushCRel env x k
| (env, U.Con.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co
| (env, _) => env}
val p_kind = P.p_kind
datatype kind_error =
UnboundKind of ErrorMsg.span * string
fun kindError env err =
case err of
UnboundKind (loc, s) =>
ErrorMsg.errorAt loc ("Unbound kind variable " ^ s)
datatype kunify_error =
KOccursCheckFailed of kind * kind
| KIncompatible of kind * kind
fun kunifyError env err =
case err of
KOccursCheckFailed (k1, k2) =>
eprefaces "Kind occurs check failed"
[("Kind 1", p_kind env k1),
("Kind 2", p_kind env k2)]
| KIncompatible (k1, k2) =>
eprefaces "Incompatible kinds"
[("Kind 1", p_kind env k1),
("Kind 2", p_kind env k2)]
fun p_con env c = P.p_con env (simplCon env c)
datatype con_error =
UnboundCon of ErrorMsg.span * string
| UnboundDatatype of ErrorMsg.span * string
| UnboundStrInCon of ErrorMsg.span * string
| WrongKind of con * kind * kind * kunify_error
| DuplicateField of ErrorMsg.span * string
| ProjBounds of con * int
| ProjMismatch of con * kind
fun conError env err =
case err of
UnboundCon (loc, s) =>
ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
| UnboundDatatype (loc, s) =>
ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
| UnboundStrInCon (loc, s) =>
ErrorMsg.errorAt loc ("Unbound structure " ^ s)
| WrongKind (c, k1, k2, kerr) =>
(ErrorMsg.errorAt (#2 c) "Wrong kind";
eprefaces' [("Constructor", p_con env c),
("Have kind", p_kind env k1),
("Need kind", p_kind env k2)];
kunifyError env kerr)
| DuplicateField (loc, s) =>
ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
| ProjBounds (c, n) =>
(ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
eprefaces' [("Constructor", p_con env c),
("Index", Print.PD.string (Int.toString n))])
| ProjMismatch (c, k) =>
(ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
eprefaces' [("Constructor", p_con env c),
("Kind", p_kind env k)])
datatype cunify_error =
CKind of kind * kind * kunify_error
| COccursCheckFailed of con * con
| CIncompatible of con * con
| CExplicitness of con * con
| CKindof of kind * con * string
| CRecordFailure of con * con
fun cunifyError env err =
case err of
CKind (k1, k2, kerr) =>
(eprefaces "Kind unification failure"
[("Kind 1", p_kind env k1),
("Kind 2", p_kind env k2)];
kunifyError env kerr)
| COccursCheckFailed (c1, c2) =>
eprefaces "Constructor occurs check failed"
[("Con 1", p_con env c1),
("Con 2", p_con env c2)]
| CIncompatible (c1, c2) =>
eprefaces "Incompatible constructors"
[("Con 1", p_con env c1),
("Con 2", p_con env c2)]
| CExplicitness (c1, c2) =>
eprefaces "Differing constructor function explicitness"
[("Con 1", p_con env c1),
("Con 2", p_con env c2)]
| CKindof (k, c, expected) =>
eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
[("Kind", p_kind env k),
("Con", p_con env c)]
| CRecordFailure (c1, c2) =>
eprefaces "Can't unify record constructors"
[("Summary 1", p_con env c1),
("Summary 2", p_con env c2)]
datatype exp_error =
UnboundExp of ErrorMsg.span * string
| UnboundStrInExp of ErrorMsg.span * string
| Unify of exp * con * con * cunify_error
| Unif of string * ErrorMsg.span * con
| WrongForm of string * exp * con
| IncompatibleCons of con * con
| DuplicatePatternVariable of ErrorMsg.span * string
| PatUnify of pat * con * con * cunify_error
| UnboundConstructor of ErrorMsg.span * string list * string
| PatHasArg of ErrorMsg.span
| PatHasNoArg of ErrorMsg.span
| Inexhaustive of ErrorMsg.span * pat
| DuplicatePatField of ErrorMsg.span * string
| Unresolvable of ErrorMsg.span * con
| OutOfContext of ErrorMsg.span * (exp * con) option
| IllegalRec of string * exp
val p_exp = P.p_exp
val p_pat = P.p_pat
fun expError env err =
case err of
UnboundExp (loc, s) =>
ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
| UnboundStrInExp (loc, s) =>
ErrorMsg.errorAt loc ("Unbound structure " ^ s)
| Unify (e, c1, c2, uerr) =>
(ErrorMsg.errorAt (#2 e) "Unification failure";
eprefaces' [("Expression", p_exp env e),
("Have con", p_con env c1),
("Need con", p_con env c2)];
cunifyError env uerr)
| Unif (action, loc, c) =>
(ErrorMsg.errorAt loc ("Unification variable blocks " ^ action);
eprefaces' [("Con", p_con env c)])
| WrongForm (variety, e, t) =>
(ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
eprefaces' [("Expression", p_exp env e),
("Type", p_con env t)])
| IncompatibleCons (c1, c2) =>
(ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
eprefaces' [("Con 1", p_con env c1),
("Con 2", p_con env c2)])
| DuplicatePatternVariable (loc, s) =>
ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
| PatUnify (p, c1, c2, uerr) =>
(ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
eprefaces' [("Pattern", p_pat env p),
("Have con", p_con env c1),
("Need con", p_con env c2)];
cunifyError env uerr)
| UnboundConstructor (loc, ms, s) =>
ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
| PatHasArg loc =>
ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
| PatHasNoArg loc =>
ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
| Inexhaustive (loc, p) =>
(ErrorMsg.errorAt loc "Inexhaustive 'case'";
eprefaces' [("Missed case", p_pat env p)])
| DuplicatePatField (loc, s) =>
ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
| OutOfContext (loc, co) =>
(ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
("Type", p_con env c)]) co)
| Unresolvable (loc, c) =>
(ErrorMsg.errorAt loc "Can't resolve type class instance";
eprefaces' [("Class constraint", p_con env c)(*,
("Class database", p_list (fn (c, rules) =>
box [P.p_con env c,
PD.string ":",
space,
p_list (fn (c, e) =>
box [p_exp env e,
PD.string ":",
space,
P.p_con env c]) rules])
(E.listClasses env))*)])
| IllegalRec (x, e) =>
(ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
eprefaces' [("Variable", PD.string x),
("Expression", p_exp env e)])
datatype decl_error =
KunifsRemain of decl list
| CunifsRemain of decl list
| Nonpositive of decl
fun lspan [] = ErrorMsg.dummySpan
| lspan ((_, loc) :: _) = loc
val p_decl = P.p_decl
fun declError env err =
case err of
KunifsRemain ds =>
(ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
| CunifsRemain ds =>
(ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
| Nonpositive d =>
(ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
eprefaces' [("Decl", p_decl env d)])
datatype sgn_error =
UnboundSgn of ErrorMsg.span * string
| UnmatchedSgi of ErrorMsg.span * sgn_item
| SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * kunify_error
| SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * cunify_error
| SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item
* (con * con * cunify_error) option
| SgnWrongForm of ErrorMsg.span * sgn * sgn
| UnWhereable of sgn * string
| WhereWrongKind of kind * kind * kunify_error
| NotIncludable of sgn
| DuplicateCon of ErrorMsg.span * string
| DuplicateVal of ErrorMsg.span * string
| DuplicateSgn of ErrorMsg.span * string
| DuplicateStr of ErrorMsg.span * string
| NotConstraintsable of sgn
val p_sgn_item = P.p_sgn_item
val p_sgn = P.p_sgn
fun sgnError env err =
case err of
UnboundSgn (loc, s) =>
ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
| UnmatchedSgi (loc, sgi) =>
(ErrorMsg.errorAt loc "Unmatched signature item";
eprefaces' [("Item", p_sgn_item env sgi)])
| SgiWrongKind (loc, sgi1, k1, sgi2, k2, kerr) =>
(ErrorMsg.errorAt loc "Kind unification failure in signature matching:";
eprefaces' [("Have", p_sgn_item env sgi1),
("Need", p_sgn_item env sgi2),
("Kind 1", p_kind env k1),
("Kind 2", p_kind env k2)];
kunifyError env kerr)
| SgiWrongCon (loc, sgi1, c1, sgi2, c2, cerr) =>
(ErrorMsg.errorAt loc "Constructor unification failure in signature matching:";
eprefaces' [("Have", p_sgn_item env sgi1),
("Need", p_sgn_item env sgi2),
("Con 1", p_con env c1),
("Con 2", p_con env c2)];
cunifyError env cerr)
| SgiMismatchedDatatypes (loc, sgi1, sgi2, cerro) =>
(ErrorMsg.errorAt loc "Mismatched 'datatype' specifications:";
eprefaces' [("Have", p_sgn_item env sgi1),
("Need", p_sgn_item env sgi2)];
Option.app (fn (c1, c2, ue) =>
(eprefaces "Unification error"
[("Con 1", p_con env c1),
("Con 2", p_con env c2)];
cunifyError env ue)) cerro)
| SgnWrongForm (loc, sgn1, sgn2) =>
(ErrorMsg.errorAt loc "Incompatible signatures:";
eprefaces' [("Sig 1", p_sgn env sgn1),
("Sig 2", p_sgn env sgn2)])
| UnWhereable (sgn, x) =>
(ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
eprefaces' [("Signature", p_sgn env sgn),
("Field", PD.string x)])
| WhereWrongKind (k1, k2, kerr) =>
(ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
eprefaces' [("Have", p_kind env k1),
("Need", p_kind env k2)];
kunifyError env kerr)
| NotIncludable sgn =>
(ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
eprefaces' [("Signature", p_sgn env sgn)])
| DuplicateCon (loc, s) =>
ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
| DuplicateVal (loc, s) =>
ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
| DuplicateSgn (loc, s) =>
ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
| DuplicateStr (loc, s) =>
ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
| NotConstraintsable sgn =>
(ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
eprefaces' [("Signature", p_sgn env sgn)])
datatype str_error =
UnboundStr of ErrorMsg.span * string
| NotFunctor of sgn
| FunctorRebind of ErrorMsg.span
| UnOpenable of sgn
| NotType of ErrorMsg.span * kind * (kind * kind * kunify_error)
| DuplicateConstructor of string * ErrorMsg.span
| NotDatatype of ErrorMsg.span
fun strError env err =
case err of
UnboundStr (loc, s) =>
ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
| NotFunctor sgn =>
(ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
eprefaces' [("Signature", p_sgn env sgn)])
| FunctorRebind loc =>
ErrorMsg.errorAt loc "Attempt to rebind functor"
| UnOpenable sgn =>
(ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
eprefaces' [("Signature", p_sgn env sgn)])
| NotType (loc, k, (k1, k2, ue)) =>
(ErrorMsg.errorAt loc "'val' type kind is not 'Type'";
eprefaces' [("Kind", p_kind env k),
("Subkind 1", p_kind env k1),
("Subkind 2", p_kind env k2)];
kunifyError env ue)
| DuplicateConstructor (x, loc) =>
ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
| NotDatatype loc =>
ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
end
|
