Mercurial > urweb

comparison src/elab_err.sml @ 1000:5d7e05b4a5c0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Better subSgn error locations
author Adam Chlipala <adamc@hcoop.net>
date Thu, 15 Oct 2009 14:27:38 -0400
parents 1c2f335297b7
children 26197c957ad6
comparison
equal deleted inserted replaced
999:8d821baac99e 1000:5d7e05b4a5c0
257 (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)"; 257 (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
258 eprefaces' [("Decl", p_decl env d)]) 258 eprefaces' [("Decl", p_decl env d)])
259 259
260 datatype sgn_error = 260 datatype sgn_error =
261 UnboundSgn of ErrorMsg.span * string 261 UnboundSgn of ErrorMsg.span * string
262 | UnmatchedSgi of sgn_item 262 | UnmatchedSgi of ErrorMsg.span * sgn_item
263 | SgiWrongKind of sgn_item * kind * sgn_item * kind * kunify_error 263 | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * kunify_error
264 | SgiWrongCon of sgn_item * con * sgn_item * con * cunify_error 264 | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * cunify_error
265 | SgiMismatchedDatatypes of sgn_item * sgn_item * (con * con * cunify_error) option 265 | SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item
266 | SgnWrongForm of sgn * sgn 266 * (con * con * cunify_error) option
267 | SgnWrongForm of ErrorMsg.span * sgn * sgn
267 | UnWhereable of sgn * string 268 | UnWhereable of sgn * string
268 | WhereWrongKind of kind * kind * kunify_error 269 | WhereWrongKind of kind * kind * kunify_error
269 | NotIncludable of sgn 270 | NotIncludable of sgn
270 | DuplicateCon of ErrorMsg.span * string 271 | DuplicateCon of ErrorMsg.span * string
271 | DuplicateVal of ErrorMsg.span * string 272 | DuplicateVal of ErrorMsg.span * string
278 279
279 fun sgnError env err = 280 fun sgnError env err =
280 case err of 281 case err of
281 UnboundSgn (loc, s) => 282 UnboundSgn (loc, s) =>
282 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s) 283 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
283 | UnmatchedSgi (sgi as (_, loc)) => 284 | UnmatchedSgi (loc, sgi) =>
284 (ErrorMsg.errorAt loc "Unmatched signature item"; 285 (ErrorMsg.errorAt loc "Unmatched signature item";
285 eprefaces' [("Item", p_sgn_item env sgi)]) 286 eprefaces' [("Item", p_sgn_item env sgi)])
286 | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) => 287 | SgiWrongKind (loc, sgi1, k1, sgi2, k2, kerr) =>
287 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:"; 288 (ErrorMsg.errorAt loc "Kind unification failure in signature matching:";
288 eprefaces' [("Have", p_sgn_item env sgi1), 289 eprefaces' [("Have", p_sgn_item env sgi1),
289 ("Need", p_sgn_item env sgi2), 290 ("Need", p_sgn_item env sgi2),
290 ("Kind 1", p_kind env k1), 291 ("Kind 1", p_kind env k1),
291 ("Kind 2", p_kind env k2)]; 292 ("Kind 2", p_kind env k2)];
292 kunifyError env kerr) 293 kunifyError env kerr)
293 | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) => 294 | SgiWrongCon (loc, sgi1, c1, sgi2, c2, cerr) =>
294 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:"; 295 (ErrorMsg.errorAt loc "Constructor unification failure in signature matching:";
295 eprefaces' [("Have", p_sgn_item env sgi1), 296 eprefaces' [("Have", p_sgn_item env sgi1),
296 ("Need", p_sgn_item env sgi2), 297 ("Need", p_sgn_item env sgi2),
297 ("Con 1", p_con env c1), 298 ("Con 1", p_con env c1),
298 ("Con 2", p_con env c2)]; 299 ("Con 2", p_con env c2)];
299 cunifyError env cerr) 300 cunifyError env cerr)
300 | SgiMismatchedDatatypes (sgi1, sgi2, cerro) => 301 | SgiMismatchedDatatypes (loc, sgi1, sgi2, cerro) =>
301 (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:"; 302 (ErrorMsg.errorAt loc "Mismatched 'datatype' specifications:";
302 eprefaces' [("Have", p_sgn_item env sgi1), 303 eprefaces' [("Have", p_sgn_item env sgi1),
303 ("Need", p_sgn_item env sgi2)]; 304 ("Need", p_sgn_item env sgi2)];
304 Option.app (fn (c1, c2, ue) => 305 Option.app (fn (c1, c2, ue) =>
305 (eprefaces "Unification error" 306 (eprefaces "Unification error"
306 [("Con 1", p_con env c1), 307 [("Con 1", p_con env c1),
307 ("Con 2", p_con env c2)]; 308 ("Con 2", p_con env c2)];
308 cunifyError env ue)) cerro) 309 cunifyError env ue)) cerro)
309 | SgnWrongForm (sgn1, sgn2) => 310 | SgnWrongForm (loc, sgn1, sgn2) =>
310 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:"; 311 (ErrorMsg.errorAt loc "Incompatible signatures:";
311 eprefaces' [("Sig 1", p_sgn env sgn1), 312 eprefaces' [("Sig 1", p_sgn env sgn1),
312 ("Sig 2", p_sgn env sgn2)]) 313 ("Sig 2", p_sgn env sgn2)])
313 | UnWhereable (sgn, x) => 314 | UnWhereable (sgn, x) =>
314 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'"; 315 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
315 eprefaces' [("Signature", p_sgn env sgn), 316 eprefaces' [("Signature", p_sgn env sgn),