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