Mercurial > urweb
comparison src/elab_err.sml @ 1719:0bafdfae2ac7
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 |