Mercurial > urweb

comparison src/elab_err.sml @ 329:eec65c11d3e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
foldTR2
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 10:30:45 -0400
parents
children 075b36dbb1a4
comparison
equal deleted inserted replaced
328:58f1260f293f 329:eec65c11d3e2
1 (* Copyright (c) 2008, Adam Chlipala
2 * All rights reserved.
3 *
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met:
6 *
7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission.
14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE.
26 *)
27
28 structure ElabErr :> ELAB_ERR = struct
29
30 structure L = Source
31 open Elab
32
33 structure E = ElabEnv
34 structure U = ElabUtil
35
36 open Print
37 structure P = ElabPrint
38
39 val simplCon = U.Con.mapB {kind = fn k => k,
40 con = fn env => fn c =>
41 let
42 val c = (c, ErrorMsg.dummySpan)
43 val (c', _) = Disjoint.hnormCon (env, Disjoint.empty) c
44 in
45 (*prefaces "simpl" [("c", P.p_con env c),
46 ("c'", P.p_con env c')];*)
47 #1 c'
48 end,
49 bind = fn (env, U.Con.Rel (x, k)) => E.pushCRel env x k
50 | (env, U.Con.Named (x, n, k)) => E.pushCNamedAs env x n k NONE}
51
52 val p_kind = P.p_kind
53
54 datatype kunify_error =
55 KOccursCheckFailed of kind * kind
56 | KIncompatible of kind * kind
57
58 fun kunifyError err =
59 case err of
60 KOccursCheckFailed (k1, k2) =>
61 eprefaces "Kind occurs check failed"
62 [("Kind 1", p_kind k1),
63 ("Kind 2", p_kind k2)]
64 | KIncompatible (k1, k2) =>
65 eprefaces "Incompatible kinds"
66 [("Kind 1", p_kind k1),
67 ("Kind 2", p_kind k2)]
68
69
70 fun p_con env c = P.p_con env (simplCon env c)
71
72 datatype con_error =
73 UnboundCon of ErrorMsg.span * string
74 | UnboundDatatype of ErrorMsg.span * string
75 | UnboundStrInCon of ErrorMsg.span * string
76 | WrongKind of con * kind * kind * kunify_error
77 | DuplicateField of ErrorMsg.span * string
78 | ProjBounds of con * int
79 | ProjMismatch of con * kind
80
81 fun conError env err =
82 case err of
83 UnboundCon (loc, s) =>
84 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
85 | UnboundDatatype (loc, s) =>
86 ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
87 | UnboundStrInCon (loc, s) =>
88 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
89 | WrongKind (c, k1, k2, kerr) =>
90 (ErrorMsg.errorAt (#2 c) "Wrong kind";
91 eprefaces' [("Constructor", p_con env c),
92 ("Have kind", p_kind k1),
93 ("Need kind", p_kind k2)];
94 kunifyError kerr)
95 | DuplicateField (loc, s) =>
96 ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
97 | ProjBounds (c, n) =>
98 (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
99 eprefaces' [("Constructor", p_con env c),
100 ("Index", Print.PD.string (Int.toString n))])
101 | ProjMismatch (c, k) =>
102 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
103 eprefaces' [("Constructor", p_con env c),
104 ("Kind", p_kind k)])
105
106
107 datatype cunify_error =
108 CKind of kind * kind * kunify_error
109 | COccursCheckFailed of con * con
110 | CIncompatible of con * con
111 | CExplicitness of con * con
112 | CKindof of kind * con
113 | CRecordFailure of con * con
114
115 fun cunifyError env err =
116 case err of
117 CKind (k1, k2, kerr) =>
118 (eprefaces "Kind unification failure"
119 [("Kind 1", p_kind k1),
120 ("Kind 2", p_kind k2)];
121 kunifyError kerr)
122 | COccursCheckFailed (c1, c2) =>
123 eprefaces "Constructor occurs check failed"
124 [("Con 1", p_con env c1),
125 ("Con 2", p_con env c2)]
126 | CIncompatible (c1, c2) =>
127 eprefaces "Incompatible constructors"
128 [("Con 1", p_con env c1),
129 ("Con 2", p_con env c2)]
130 | CExplicitness (c1, c2) =>
131 eprefaces "Differing constructor function explicitness"
132 [("Con 1", p_con env c1),
133 ("Con 2", p_con env c2)]
134 | CKindof (k, c) =>
135 eprefaces "Unexpected kind for kindof calculation"
136 [("Kind", p_kind k),
137 ("Con", p_con env c)]
138 | CRecordFailure (c1, c2) =>
139 eprefaces "Can't unify record constructors"
140 [("Summary 1", p_con env c1),
141 ("Summary 2", p_con env c2)]
142
143 datatype exp_error =
144 UnboundExp of ErrorMsg.span * string
145 | UnboundStrInExp of ErrorMsg.span * string
146 | Unify of exp * con * con * cunify_error
147 | Unif of string * con
148 | WrongForm of string * exp * con
149 | IncompatibleCons of con * con
150 | DuplicatePatternVariable of ErrorMsg.span * string
151 | PatUnify of pat * con * con * cunify_error
152 | UnboundConstructor of ErrorMsg.span * string list * string
153 | PatHasArg of ErrorMsg.span
154 | PatHasNoArg of ErrorMsg.span
155 | Inexhaustive of ErrorMsg.span
156 | DuplicatePatField of ErrorMsg.span * string
157 | Unresolvable of ErrorMsg.span * con
158 | OutOfContext of ErrorMsg.span * (exp * con) option
159 | IllegalRec of string * exp
160
161 val p_exp = P.p_exp
162 val p_pat = P.p_pat
163
164 fun expError env err =
165 case err of
166 UnboundExp (loc, s) =>
167 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
168 | UnboundStrInExp (loc, s) =>
169 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
170 | Unify (e, c1, c2, uerr) =>
171 (ErrorMsg.errorAt (#2 e) "Unification failure";
172 eprefaces' [("Expression", p_exp env e),
173 ("Have con", p_con env c1),
174 ("Need con", p_con env c2)];
175 cunifyError env uerr)
176 | Unif (action, c) =>
177 (ErrorMsg.errorAt (#2 c) ("Unification variable blocks " ^ action);
178 eprefaces' [("Con", p_con env c)])
179 | WrongForm (variety, e, t) =>
180 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
181 eprefaces' [("Expression", p_exp env e),
182 ("Type", p_con env t)])
183 | IncompatibleCons (c1, c2) =>
184 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
185 eprefaces' [("Con 1", p_con env c1),
186 ("Con 2", p_con env c2)])
187 | DuplicatePatternVariable (loc, s) =>
188 ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
189 | PatUnify (p, c1, c2, uerr) =>
190 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
191 eprefaces' [("Pattern", p_pat env p),
192 ("Have con", p_con env c1),
193 ("Need con", p_con env c2)];
194 cunifyError env uerr)
195 | UnboundConstructor (loc, ms, s) =>
196 ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
197 | PatHasArg loc =>
198 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
199 | PatHasNoArg loc =>
200 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
201 | Inexhaustive loc =>
202 ErrorMsg.errorAt loc "Inexhaustive 'case'"
203 | DuplicatePatField (loc, s) =>
204 ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
205 | OutOfContext (loc, co) =>
206 (ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
207 Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
208 ("Type", p_con env c)]) co)
209 | Unresolvable (loc, c) =>
210 (ErrorMsg.errorAt loc "Can't resolve type class instance";
211 eprefaces' [("Class constraint", p_con env c)])
212 | IllegalRec (x, e) =>
213 (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
214 eprefaces' [("Variable", PD.string x),
215 ("Expression", p_exp env e)])
216
217
218 datatype decl_error =
219 KunifsRemain of decl list
220 | CunifsRemain of decl list
221 | Nonpositive of decl
222
223 fun lspan [] = ErrorMsg.dummySpan
224 | lspan ((_, loc) :: _) = loc
225
226 val p_decl = P.p_decl
227
228 fun declError env err =
229 case err of
230 KunifsRemain ds =>
231 (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
232 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
233 | CunifsRemain ds =>
234 (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
235 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
236 | Nonpositive d =>
237 (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
238 eprefaces' [("Decl", p_decl env d)])
239
240 datatype sgn_error =
241 UnboundSgn of ErrorMsg.span * string
242 | UnmatchedSgi of sgn_item
243 | SgiWrongKind of sgn_item * kind * sgn_item * kind * kunify_error
244 | SgiWrongCon of sgn_item * con * sgn_item * con * cunify_error
245 | SgiMismatchedDatatypes of sgn_item * sgn_item * (con * con * cunify_error) option
246 | SgnWrongForm of sgn * sgn
247 | UnWhereable of sgn * string
248 | WhereWrongKind of kind * kind * kunify_error
249 | NotIncludable of sgn
250 | DuplicateCon of ErrorMsg.span * string
251 | DuplicateVal of ErrorMsg.span * string
252 | DuplicateSgn of ErrorMsg.span * string
253 | DuplicateStr of ErrorMsg.span * string
254 | NotConstraintsable of sgn
255
256 val p_sgn_item = P.p_sgn_item
257 val p_sgn = P.p_sgn
258
259 fun sgnError env err =
260 case err of
261 UnboundSgn (loc, s) =>
262 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
263 | UnmatchedSgi (sgi as (_, loc)) =>
264 (ErrorMsg.errorAt loc "Unmatched signature item";
265 eprefaces' [("Item", p_sgn_item env sgi)])
266 | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
267 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
268 eprefaces' [("Have", p_sgn_item env sgi1),
269 ("Need", p_sgn_item env sgi2),
270 ("Kind 1", p_kind k1),
271 ("Kind 2", p_kind k2)];
272 kunifyError kerr)
273 | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
274 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
275 eprefaces' [("Have", p_sgn_item env sgi1),
276 ("Need", p_sgn_item env sgi2),
277 ("Con 1", p_con env c1),
278 ("Con 2", p_con env c2)];
279 cunifyError env cerr)
280 | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
281 (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
282 eprefaces' [("Have", p_sgn_item env sgi1),
283 ("Need", p_sgn_item env sgi2)];
284 Option.app (fn (c1, c2, ue) =>
285 (eprefaces "Unification error"
286 [("Con 1", p_con env c1),
287 ("Con 2", p_con env c2)];
288 cunifyError env ue)) cerro)
289 | SgnWrongForm (sgn1, sgn2) =>
290 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
291 eprefaces' [("Sig 1", p_sgn env sgn1),
292 ("Sig 2", p_sgn env sgn2)])
293 | UnWhereable (sgn, x) =>
294 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
295 eprefaces' [("Signature", p_sgn env sgn),
296 ("Field", PD.string x)])
297 | WhereWrongKind (k1, k2, kerr) =>
298 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
299 eprefaces' [("Have", p_kind k1),
300 ("Need", p_kind k2)];
301 kunifyError kerr)
302 | NotIncludable sgn =>
303 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
304 eprefaces' [("Signature", p_sgn env sgn)])
305 | DuplicateCon (loc, s) =>
306 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
307 | DuplicateVal (loc, s) =>
308 ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
309 | DuplicateSgn (loc, s) =>
310 ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
311 | DuplicateStr (loc, s) =>
312 ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
313 | NotConstraintsable sgn =>
314 (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
315 eprefaces' [("Signature", p_sgn env sgn)])
316
317 datatype str_error =
318 UnboundStr of ErrorMsg.span * string
319 | NotFunctor of sgn
320 | FunctorRebind of ErrorMsg.span
321 | UnOpenable of sgn
322 | NotType of kind * (kind * kind * kunify_error)
323 | DuplicateConstructor of string * ErrorMsg.span
324 | NotDatatype of ErrorMsg.span
325
326 fun strError env err =
327 case err of
328 UnboundStr (loc, s) =>
329 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
330 | NotFunctor sgn =>
331 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
332 eprefaces' [("Signature", p_sgn env sgn)])
333 | FunctorRebind loc =>
334 ErrorMsg.errorAt loc "Attempt to rebind functor"
335 | UnOpenable sgn =>
336 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
337 eprefaces' [("Signature", p_sgn env sgn)])
338 | NotType (k, (k1, k2, ue)) =>
339 (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
340 eprefaces' [("Kind", p_kind k),
341 ("Subkind 1", p_kind k1),
342 ("Subkind 2", p_kind k2)];
343 kunifyError ue)
344 | DuplicateConstructor (x, loc) =>
345 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
346 | NotDatatype loc =>
347 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
348
349 end