Mercurial > urweb

comparison src/elab_err.sml @ 623:588b9d16b00a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents 6a0e54400805
children 12b73f3c108e
comparison
equal deleted inserted replaced
622:d64533157f40 623:588b9d16b00a
34 structure U = ElabUtil 34 structure U = ElabUtil
35 35
36 open Print 36 open Print
37 structure P = ElabPrint 37 structure P = ElabPrint
38 38
39 val simplCon = U.Con.mapB {kind = fn k => k, 39 val simplCon = U.Con.mapB {kind = fn _ => fn k => k,
40 con = fn env => fn c => 40 con = fn env => fn c =>
41 let 41 let
42 val c = (c, ErrorMsg.dummySpan) 42 val c = (c, ErrorMsg.dummySpan)
43 val (c', _) = Disjoint.hnormCon (env, Disjoint.empty) c 43 val (c', _) = Disjoint.hnormCon (env, Disjoint.empty) c
44 in 44 in
45 (*prefaces "simpl" [("c", P.p_con env c), 45 (*prefaces "simpl" [("c", P.p_con env c),
46 ("c'", P.p_con env c')];*) 46 ("c'", P.p_con env c')];*)
47 #1 c' 47 #1 c'
48 end, 48 end,
49 bind = fn (env, U.Con.Rel (x, k)) => E.pushCRel env x k 49 bind = fn (env, U.Con.RelC (x, k)) => E.pushCRel env x k
50 | (env, U.Con.Named (x, n, k)) => E.pushCNamedAs env x n k NONE} 50 | (env, U.Con.NamedC (x, n, k)) => E.pushCNamedAs env x n k NONE
51 | (env, _) => env}
51 52
52 val p_kind = P.p_kind 53 val p_kind = P.p_kind
54
55 datatype kind_error =
56 UnboundKind of ErrorMsg.span * string
57
58 fun kindError env err =
59 case err of
60 UnboundKind (loc, s) =>
61 ErrorMsg.errorAt loc ("Unbound kind variable " ^ s)
53 62
54 datatype kunify_error = 63 datatype kunify_error =
55 KOccursCheckFailed of kind * kind 64 KOccursCheckFailed of kind * kind
56 | KIncompatible of kind * kind 65 | KIncompatible of kind * kind
57 66
58 fun kunifyError err = 67 fun kunifyError env err =
59 case err of 68 case err of
60 KOccursCheckFailed (k1, k2) => 69 KOccursCheckFailed (k1, k2) =>
61 eprefaces "Kind occurs check failed" 70 eprefaces "Kind occurs check failed"
62 [("Kind 1", p_kind k1), 71 [("Kind 1", p_kind env k1),
63 ("Kind 2", p_kind k2)] 72 ("Kind 2", p_kind env k2)]
64 | KIncompatible (k1, k2) => 73 | KIncompatible (k1, k2) =>
65 eprefaces "Incompatible kinds" 74 eprefaces "Incompatible kinds"
66 [("Kind 1", p_kind k1), 75 [("Kind 1", p_kind env k1),
67 ("Kind 2", p_kind k2)] 76 ("Kind 2", p_kind env k2)]
68 77
69 78
70 fun p_con env c = P.p_con env (simplCon env c) 79 fun p_con env c = P.p_con env (simplCon env c)
71 80
72 datatype con_error = 81 datatype con_error =
87 | UnboundStrInCon (loc, s) => 96 | UnboundStrInCon (loc, s) =>
88 ErrorMsg.errorAt loc ("Unbound structure " ^ s) 97 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
89 | WrongKind (c, k1, k2, kerr) => 98 | WrongKind (c, k1, k2, kerr) =>
90 (ErrorMsg.errorAt (#2 c) "Wrong kind"; 99 (ErrorMsg.errorAt (#2 c) "Wrong kind";
91 eprefaces' [("Constructor", p_con env c), 100 eprefaces' [("Constructor", p_con env c),
92 ("Have kind", p_kind k1), 101 ("Have kind", p_kind env k1),
93 ("Need kind", p_kind k2)]; 102 ("Need kind", p_kind env k2)];
94 kunifyError kerr) 103 kunifyError env kerr)
95 | DuplicateField (loc, s) => 104 | DuplicateField (loc, s) =>
96 ErrorMsg.errorAt loc ("Duplicate record field " ^ s) 105 ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
97 | ProjBounds (c, n) => 106 | ProjBounds (c, n) =>
98 (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection"; 107 (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
99 eprefaces' [("Constructor", p_con env c), 108 eprefaces' [("Constructor", p_con env c),
100 ("Index", Print.PD.string (Int.toString n))]) 109 ("Index", Print.PD.string (Int.toString n))])
101 | ProjMismatch (c, k) => 110 | ProjMismatch (c, k) =>
102 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor"; 111 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
103 eprefaces' [("Constructor", p_con env c), 112 eprefaces' [("Constructor", p_con env c),
104 ("Kind", p_kind k)]) 113 ("Kind", p_kind env k)])
105 114
106 115
107 datatype cunify_error = 116 datatype cunify_error =
108 CKind of kind * kind * kunify_error 117 CKind of kind * kind * kunify_error
109 | COccursCheckFailed of con * con 118 | COccursCheckFailed of con * con
114 123
115 fun cunifyError env err = 124 fun cunifyError env err =
116 case err of 125 case err of
117 CKind (k1, k2, kerr) => 126 CKind (k1, k2, kerr) =>
118 (eprefaces "Kind unification failure" 127 (eprefaces "Kind unification failure"
119 [("Kind 1", p_kind k1), 128 [("Kind 1", p_kind env k1),
120 ("Kind 2", p_kind k2)]; 129 ("Kind 2", p_kind env k2)];
121 kunifyError kerr) 130 kunifyError env kerr)
122 | COccursCheckFailed (c1, c2) => 131 | COccursCheckFailed (c1, c2) =>
123 eprefaces "Constructor occurs check failed" 132 eprefaces "Constructor occurs check failed"
124 [("Con 1", p_con env c1), 133 [("Con 1", p_con env c1),
125 ("Con 2", p_con env c2)] 134 ("Con 2", p_con env c2)]
126 | CIncompatible (c1, c2) => 135 | CIncompatible (c1, c2) =>
131 eprefaces "Differing constructor function explicitness" 140 eprefaces "Differing constructor function explicitness"
132 [("Con 1", p_con env c1), 141 [("Con 1", p_con env c1),
133 ("Con 2", p_con env c2)] 142 ("Con 2", p_con env c2)]
134 | CKindof (k, c, expected) => 143 | CKindof (k, c, expected) =>
135 eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")") 144 eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
136 [("Kind", p_kind k), 145 [("Kind", p_kind env k),
137 ("Con", p_con env c)] 146 ("Con", p_con env c)]
138 | CRecordFailure (c1, c2) => 147 | CRecordFailure (c1, c2) =>
139 eprefaces "Can't unify record constructors" 148 eprefaces "Can't unify record constructors"
140 [("Summary 1", p_con env c1), 149 [("Summary 1", p_con env c1),
141 ("Summary 2", p_con env c2)] 150 ("Summary 2", p_con env c2)]
265 eprefaces' [("Item", p_sgn_item env sgi)]) 274 eprefaces' [("Item", p_sgn_item env sgi)])
266 | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) => 275 | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
267 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:"; 276 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
268 eprefaces' [("Have", p_sgn_item env sgi1), 277 eprefaces' [("Have", p_sgn_item env sgi1),
269 ("Need", p_sgn_item env sgi2), 278 ("Need", p_sgn_item env sgi2),
270 ("Kind 1", p_kind k1), 279 ("Kind 1", p_kind env k1),
271 ("Kind 2", p_kind k2)]; 280 ("Kind 2", p_kind env k2)];
272 kunifyError kerr) 281 kunifyError env kerr)
273 | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) => 282 | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
274 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:"; 283 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
275 eprefaces' [("Have", p_sgn_item env sgi1), 284 eprefaces' [("Have", p_sgn_item env sgi1),
276 ("Need", p_sgn_item env sgi2), 285 ("Need", p_sgn_item env sgi2),
277 ("Con 1", p_con env c1), 286 ("Con 1", p_con env c1),
294 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'"; 303 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
295 eprefaces' [("Signature", p_sgn env sgn), 304 eprefaces' [("Signature", p_sgn env sgn),
296 ("Field", PD.string x)]) 305 ("Field", PD.string x)])
297 | WhereWrongKind (k1, k2, kerr) => 306 | WhereWrongKind (k1, k2, kerr) =>
298 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'"; 307 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
299 eprefaces' [("Have", p_kind k1), 308 eprefaces' [("Have", p_kind env k1),
300 ("Need", p_kind k2)]; 309 ("Need", p_kind env k2)];
301 kunifyError kerr) 310 kunifyError env kerr)
302 | NotIncludable sgn => 311 | NotIncludable sgn =>
303 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'"; 312 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
304 eprefaces' [("Signature", p_sgn env sgn)]) 313 eprefaces' [("Signature", p_sgn env sgn)])
305 | DuplicateCon (loc, s) => 314 | DuplicateCon (loc, s) =>
306 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature") 315 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
335 | UnOpenable sgn => 344 | UnOpenable sgn =>
336 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure"; 345 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
337 eprefaces' [("Signature", p_sgn env sgn)]) 346 eprefaces' [("Signature", p_sgn env sgn)])
338 | NotType (k, (k1, k2, ue)) => 347 | NotType (k, (k1, k2, ue)) =>
339 (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'"; 348 (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
340 eprefaces' [("Kind", p_kind k), 349 eprefaces' [("Kind", p_kind env k),
341 ("Subkind 1", p_kind k1), 350 ("Subkind 1", p_kind env k1),
342 ("Subkind 2", p_kind k2)]; 351 ("Subkind 2", p_kind env k2)];
343 kunifyError ue) 352 kunifyError env ue)
344 | DuplicateConstructor (x, loc) => 353 | DuplicateConstructor (x, loc) =>
345 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x) 354 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
346 | NotDatatype loc => 355 | NotDatatype loc =>
347 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype" 356 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
348 357