Mercurial > urweb

comparison src/elab_err.sml @ 1719:0bafdfae2ac7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Saving proper environments, to use in displaying nested error messages
author Adam Chlipala <adam@chlipala.net>
date Sat, 21 Apr 2012 14:57:00 -0400
parents d6c45026240d
children fca4a6d05ac1
comparison
equal deleted inserted replaced
1718:dd12d6d9e9a7 1719:0bafdfae2ac7
1 (* Copyright (c) 2008-2010, Adam Chlipala 1 (* Copyright (c) 2008-2010, 2012, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
70 70
71 datatype con_error = 71 datatype con_error =
72 UnboundCon of ErrorMsg.span * string 72 UnboundCon of ErrorMsg.span * string
73 | UnboundDatatype of ErrorMsg.span * string 73 | UnboundDatatype of ErrorMsg.span * string
74 | UnboundStrInCon of ErrorMsg.span * string 74 | UnboundStrInCon of ErrorMsg.span * string
75 | WrongKind of con * kind * kind * kunify_error 75 | WrongKind of con * kind * kind * E.env * kunify_error
76 | DuplicateField of ErrorMsg.span * string 76 | DuplicateField of ErrorMsg.span * string
77 | ProjBounds of con * int 77 | ProjBounds of con * int
78 | ProjMismatch of con * kind 78 | ProjMismatch of con * kind
79 79
80 fun conError env err = 80 fun conError env err =
83 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s) 83 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
84 | UnboundDatatype (loc, s) => 84 | UnboundDatatype (loc, s) =>
85 ErrorMsg.errorAt loc ("Unbound datatype " ^ s) 85 ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
86 | UnboundStrInCon (loc, s) => 86 | UnboundStrInCon (loc, s) =>
87 ErrorMsg.errorAt loc ("Unbound structure " ^ s) 87 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
88 | WrongKind (c, k1, k2, kerr) => 88 | WrongKind (c, k1, k2, env', kerr) =>
89 (ErrorMsg.errorAt (#2 c) "Wrong kind"; 89 (ErrorMsg.errorAt (#2 c) "Wrong kind";
90 eprefaces' [("Constructor", p_con env c), 90 eprefaces' [("Constructor", p_con env c),
91 ("Have kind", p_kind env k1), 91 ("Have kind", p_kind env k1),
92 ("Need kind", p_kind env k2)]; 92 ("Need kind", p_kind env k2)];
93 kunifyError env kerr) 93 kunifyError env' kerr)
94 | DuplicateField (loc, s) => 94 | DuplicateField (loc, s) =>
95 ErrorMsg.errorAt loc ("Duplicate record field " ^ s) 95 ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
96 | ProjBounds (c, n) => 96 | ProjBounds (c, n) =>
97 (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection"; 97 (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
98 eprefaces' [("Constructor", p_con env c), 98 eprefaces' [("Constructor", p_con env c),
101 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor"; 101 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
102 eprefaces' [("Constructor", p_con env c), 102 eprefaces' [("Constructor", p_con env c),
103 ("Kind", p_kind env k)]) 103 ("Kind", p_kind env k)])
104 104
105 datatype cunify_error = 105 datatype cunify_error =
106 CKind of kind * kind * kunify_error 106 CKind of kind * kind * E.env * kunify_error
107 | COccursCheckFailed of con * con 107 | COccursCheckFailed of con * con
108 | CIncompatible of con * con 108 | CIncompatible of con * con
109 | CExplicitness of con * con 109 | CExplicitness of con * con
110 | CKindof of kind * con * string 110 | CKindof of kind * con * string
111 | CRecordFailure of con * con * (con * con * con * cunify_error option) option 111 | CRecordFailure of con * con * (con * con * con * (E.env * cunify_error) option) option
112 | TooLifty of ErrorMsg.span * ErrorMsg.span 112 | TooLifty of ErrorMsg.span * ErrorMsg.span
113 | TooUnify of con * con 113 | TooUnify of con * con
114 | TooDeep 114 | TooDeep
115 | CScope of con * con 115 | CScope of con * con
116 116
117 fun cunifyError env err = 117 fun cunifyError env err : unit =
118 case err of 118 case err of
119 CKind (k1, k2, kerr) => 119 CKind (k1, k2, env', kerr) =>
120 (eprefaces "Kind unification failure" 120 (eprefaces "Kind unification failure"
121 [("Have", p_kind env k1), 121 [("Have", p_kind env k1),
122 ("Need", p_kind env k2)]; 122 ("Need", p_kind env k2)];
123 kunifyError env kerr) 123 kunifyError env' kerr)
124 | COccursCheckFailed (c1, c2) => 124 | COccursCheckFailed (c1, c2) =>
125 eprefaces "Constructor occurs check failed" 125 eprefaces "Constructor occurs check failed"
126 [("Have", p_con env c1), 126 [("Have", p_con env c1),
127 ("Need", p_con env c2)] 127 ("Need", p_con env c2)]
128 | CIncompatible (c1, c2) => 128 | CIncompatible (c1, c2) =>
146 | SOME (nm, t1, t2, _) => 146 | SOME (nm, t1, t2, _) =>
147 [("Field", p_con env nm), 147 [("Field", p_con env nm),
148 ("Value 1", p_con env t1), 148 ("Value 1", p_con env t1),
149 ("Value 2", p_con env t2)])); 149 ("Value 2", p_con env t2)]));
150 case fo of 150 case fo of
151 SOME (_, _, _, SOME err') => cunifyError env err' 151 SOME (_, _, _, SOME (env', err')) => cunifyError env' err'
152 | _ => ()) 152 | _ => ())
153 | TooLifty (loc1, loc2) => 153 | TooLifty (loc1, loc2) =>
154 (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings"; 154 (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings";
155 eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))]) 155 eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))])
156 | TooUnify (c1, c2) => 156 | TooUnify (c1, c2) =>
164 ("Need", p_con env c2)] 164 ("Need", p_con env c2)]
165 165
166 datatype exp_error = 166 datatype exp_error =
167 UnboundExp of ErrorMsg.span * string 167 UnboundExp of ErrorMsg.span * string
168 | UnboundStrInExp of ErrorMsg.span * string 168 | UnboundStrInExp of ErrorMsg.span * string
169 | Unify of exp * con * con * cunify_error 169 | Unify of exp * con * con * E.env * cunify_error
170 | Unif of string * ErrorMsg.span * con 170 | Unif of string * ErrorMsg.span * con
171 | WrongForm of string * exp * con 171 | WrongForm of string * exp * con
172 | IncompatibleCons of con * con 172 | IncompatibleCons of con * con
173 | DuplicatePatternVariable of ErrorMsg.span * string 173 | DuplicatePatternVariable of ErrorMsg.span * string
174 | PatUnify of pat * con * con * cunify_error 174 | PatUnify of pat * con * con * E.env * cunify_error
175 | UnboundConstructor of ErrorMsg.span * string list * string 175 | UnboundConstructor of ErrorMsg.span * string list * string
176 | PatHasArg of ErrorMsg.span 176 | PatHasArg of ErrorMsg.span
177 | PatHasNoArg of ErrorMsg.span 177 | PatHasNoArg of ErrorMsg.span
178 | Inexhaustive of ErrorMsg.span * pat 178 | Inexhaustive of ErrorMsg.span * pat
179 | DuplicatePatField of ErrorMsg.span * string 179 | DuplicatePatField of ErrorMsg.span * string
195 case err of 195 case err of
196 UnboundExp (loc, s) => 196 UnboundExp (loc, s) =>
197 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) 197 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
198 | UnboundStrInExp (loc, s) => 198 | UnboundStrInExp (loc, s) =>
199 ErrorMsg.errorAt loc ("Unbound structure " ^ s) 199 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
200 | Unify (e, c1, c2, uerr) => 200 | Unify (e, c1, c2, env', uerr) =>
201 (ErrorMsg.errorAt (#2 e) "Unification failure"; 201 (ErrorMsg.errorAt (#2 e) "Unification failure";
202 eprefaces' [("Expression", p_exp env e), 202 eprefaces' [("Expression", p_exp env e),
203 ("Have con", p_con env c1), 203 ("Have con", p_con env c1),
204 ("Need con", p_con env c2)]; 204 ("Need con", p_con env c2)];
205 cunifyError env uerr) 205 cunifyError env' uerr)
206 | Unif (action, loc, c) => 206 | Unif (action, loc, c) =>
207 (ErrorMsg.errorAt loc ("Unification variable blocks " ^ action); 207 (ErrorMsg.errorAt loc ("Unification variable blocks " ^ action);
208 eprefaces' [("Con", p_con env c)]) 208 eprefaces' [("Con", p_con env c)])
209 | WrongForm (variety, e, t) => 209 | WrongForm (variety, e, t) =>
210 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety); 210 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
214 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors"; 214 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
215 eprefaces' [("Have", p_con env c1), 215 eprefaces' [("Have", p_con env c1),
216 ("Need", p_con env c2)]) 216 ("Need", p_con env c2)])
217 | DuplicatePatternVariable (loc, s) => 217 | DuplicatePatternVariable (loc, s) =>
218 ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s) 218 ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
219 | PatUnify (p, c1, c2, uerr) => 219 | PatUnify (p, c1, c2, env', uerr) =>
220 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern"; 220 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
221 eprefaces' [("Pattern", p_pat env p), 221 eprefaces' [("Pattern", p_pat env p),
222 ("Have con", p_con env c1), 222 ("Have con", p_con env c1),
223 ("Need con", p_con env c2)]; 223 ("Need con", p_con env c2)];
224 cunifyError env uerr) 224 cunifyError env' uerr)
225 | UnboundConstructor (loc, ms, s) => 225 | UnboundConstructor (loc, ms, s) =>
226 ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern") 226 ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
227 | PatHasArg loc => 227 | PatHasArg loc =>
228 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument" 228 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
229 | PatHasNoArg loc => 229 | PatHasNoArg loc =>
327 eprefaces' [("Decl", p_decl env d)]) 327 eprefaces' [("Decl", p_decl env d)])
328 328
329 datatype sgn_error = 329 datatype sgn_error =
330 UnboundSgn of ErrorMsg.span * string 330 UnboundSgn of ErrorMsg.span * string
331 | UnmatchedSgi of ErrorMsg.span * sgn_item 331 | UnmatchedSgi of ErrorMsg.span * sgn_item
332 | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * kunify_error 332 | SgiWrongKind of ErrorMsg.span * sgn_item * kind * sgn_item * kind * E.env * kunify_error
333 | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * cunify_error 333 | SgiWrongCon of ErrorMsg.span * sgn_item * con * sgn_item * con * E.env * cunify_error
334 | SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item 334 | SgiMismatchedDatatypes of ErrorMsg.span * sgn_item * sgn_item
335 * (con * con * cunify_error) option 335 * (con * con * E.env * cunify_error) option
336 | SgnWrongForm of ErrorMsg.span * sgn * sgn 336 | SgnWrongForm of ErrorMsg.span * sgn * sgn
337 | UnWhereable of sgn * string 337 | UnWhereable of sgn * string
338 | WhereWrongKind of kind * kind * kunify_error 338 | WhereWrongKind of kind * kind * E.env * kunify_error
339 | NotIncludable of sgn 339 | NotIncludable of sgn
340 | DuplicateCon of ErrorMsg.span * string 340 | DuplicateCon of ErrorMsg.span * string
341 | DuplicateVal of ErrorMsg.span * string 341 | DuplicateVal of ErrorMsg.span * string
342 | DuplicateSgn of ErrorMsg.span * string 342 | DuplicateSgn of ErrorMsg.span * string
343 | DuplicateStr of ErrorMsg.span * string 343 | DuplicateStr of ErrorMsg.span * string
351 UnboundSgn (loc, s) => 351 UnboundSgn (loc, s) =>
352 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s) 352 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
353 | UnmatchedSgi (loc, sgi) => 353 | UnmatchedSgi (loc, sgi) =>
354 (ErrorMsg.errorAt loc "Unmatched signature item"; 354 (ErrorMsg.errorAt loc "Unmatched signature item";
355 eprefaces' [("Item", p_sgn_item env sgi)]) 355 eprefaces' [("Item", p_sgn_item env sgi)])
356 | SgiWrongKind (loc, sgi1, k1, sgi2, k2, kerr) => 356 | SgiWrongKind (loc, sgi1, k1, sgi2, k2, env', kerr) =>
357 (ErrorMsg.errorAt loc "Kind unification failure in signature matching:"; 357 (ErrorMsg.errorAt loc "Kind unification failure in signature matching:";
358 eprefaces' [("Have", p_sgn_item env sgi1), 358 eprefaces' [("Have", p_sgn_item env sgi1),
359 ("Need", p_sgn_item env sgi2), 359 ("Need", p_sgn_item env sgi2),
360 ("Kind 1", p_kind env k1), 360 ("Kind 1", p_kind env k1),
361 ("Kind 2", p_kind env k2)]; 361 ("Kind 2", p_kind env k2)];
362 kunifyError env kerr) 362 kunifyError env' kerr)
363 | SgiWrongCon (loc, sgi1, c1, sgi2, c2, cerr) => 363 | SgiWrongCon (loc, sgi1, c1, sgi2, c2, env', cerr) =>
364 (ErrorMsg.errorAt loc "Constructor unification failure in signature matching:"; 364 (ErrorMsg.errorAt loc "Constructor unification failure in signature matching:";
365 eprefaces' [("Have", p_sgn_item env sgi1), 365 eprefaces' [("Have", p_sgn_item env sgi1),
366 ("Need", p_sgn_item env sgi2), 366 ("Need", p_sgn_item env sgi2),
367 ("Con 1", p_con env c1), 367 ("Con 1", p_con env c1),
368 ("Con 2", p_con env c2)]; 368 ("Con 2", p_con env c2)];
369 cunifyError env cerr) 369 cunifyError env' cerr)
370 | SgiMismatchedDatatypes (loc, sgi1, sgi2, cerro) => 370 | SgiMismatchedDatatypes (loc, sgi1, sgi2, cerro) =>
371 (ErrorMsg.errorAt loc "Mismatched 'datatype' specifications:"; 371 (ErrorMsg.errorAt loc "Mismatched 'datatype' specifications:";
372 eprefaces' [("Have", p_sgn_item env sgi1), 372 eprefaces' [("Have", p_sgn_item env sgi1),
373 ("Need", p_sgn_item env sgi2)]; 373 ("Need", p_sgn_item env sgi2)];
374 Option.app (fn (c1, c2, ue) => 374 Option.app (fn (c1, c2, env', ue) =>
375 (eprefaces "Unification error" 375 (eprefaces "Unification error"
376 [("Con 1", p_con env c1), 376 [("Con 1", p_con env' c1),
377 ("Con 2", p_con env c2)]; 377 ("Con 2", p_con env' c2)];
378 cunifyError env ue)) cerro) 378 cunifyError env' ue)) cerro)
379 | SgnWrongForm (loc, sgn1, sgn2) => 379 | SgnWrongForm (loc, sgn1, sgn2) =>
380 (ErrorMsg.errorAt loc "Incompatible signatures:"; 380 (ErrorMsg.errorAt loc "Incompatible signatures:";
381 eprefaces' [("Sig 1", p_sgn env sgn1), 381 eprefaces' [("Sig 1", p_sgn env sgn1),
382 ("Sig 2", p_sgn env sgn2)]) 382 ("Sig 2", p_sgn env sgn2)])
383 | UnWhereable (sgn, x) => 383 | UnWhereable (sgn, x) =>
384 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'"; 384 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
385 eprefaces' [("Signature", p_sgn env sgn), 385 eprefaces' [("Signature", p_sgn env sgn),
386 ("Field", PD.string x)]) 386 ("Field", PD.string x)])
387 | WhereWrongKind (k1, k2, kerr) => 387 | WhereWrongKind (k1, k2, env', kerr) =>
388 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'"; 388 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
389 eprefaces' [("Have", p_kind env k1), 389 eprefaces' [("Have", p_kind env k1),
390 ("Need", p_kind env k2)]; 390 ("Need", p_kind env k2)];
391 kunifyError env kerr) 391 kunifyError env' kerr)
392 | NotIncludable sgn => 392 | NotIncludable sgn =>
393 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'"; 393 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
394 eprefaces' [("Signature", p_sgn env sgn)]) 394 eprefaces' [("Signature", p_sgn env sgn)])
395 | DuplicateCon (loc, s) => 395 | DuplicateCon (loc, s) =>
396 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature") 396 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
407 datatype str_error = 407 datatype str_error =
408 UnboundStr of ErrorMsg.span * string 408 UnboundStr of ErrorMsg.span * string
409 | NotFunctor of sgn 409 | NotFunctor of sgn
410 | FunctorRebind of ErrorMsg.span 410 | FunctorRebind of ErrorMsg.span
411 | UnOpenable of sgn 411 | UnOpenable of sgn
412 | NotType of ErrorMsg.span * kind * (kind * kind * kunify_error) 412 | NotType of ErrorMsg.span * kind * (kind * kind * E.env * kunify_error)
413 | DuplicateConstructor of string * ErrorMsg.span 413 | DuplicateConstructor of string * ErrorMsg.span
414 | NotDatatype of ErrorMsg.span 414 | NotDatatype of ErrorMsg.span
415 415
416 fun strError env err = 416 fun strError env err =
417 case err of 417 case err of
423 | FunctorRebind loc => 423 | FunctorRebind loc =>
424 ErrorMsg.errorAt loc "Attempt to rebind functor" 424 ErrorMsg.errorAt loc "Attempt to rebind functor"
425 | UnOpenable sgn => 425 | UnOpenable sgn =>
426 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure"; 426 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
427 eprefaces' [("Signature", p_sgn env sgn)]) 427 eprefaces' [("Signature", p_sgn env sgn)])
428 | NotType (loc, k, (k1, k2, ue)) => 428 | NotType (loc, k, (k1, k2, env', ue)) =>
429 (ErrorMsg.errorAt loc "'val' type kind is not 'Type'"; 429 (ErrorMsg.errorAt loc "'val' type kind is not 'Type'";
430 eprefaces' [("Kind", p_kind env k), 430 eprefaces' [("Kind", p_kind env k),
431 ("Subkind 1", p_kind env k1), 431 ("Subkind 1", p_kind env k1),
432 ("Subkind 2", p_kind env k2)]; 432 ("Subkind 2", p_kind env k2)];
433 kunifyError env ue) 433 kunifyError env' ue)
434 | DuplicateConstructor (x, loc) => 434 | DuplicateConstructor (x, loc) =>
435 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x) 435 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
436 | NotDatatype loc => 436 | NotDatatype loc =>
437 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype" 437 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
438 438