Mercurial > urweb

comparison src/elaborate.sml @ 6:38bf996e1c2e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Check for leftover kind unifs
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 16:44:39 -0500
parents 258261a53842
children a455a9f85cc3
comparison
equal deleted inserted replaced
5:258261a53842 6:38bf996e1c2e
259 checkKind env c1' k1 k; 259 checkKind env c1' k1 k;
260 checkKind env c2' k2 k; 260 checkKind env c2' k2 k;
261 ((L'.CConcat (c1', c2'), loc), k) 261 ((L'.CConcat (c1', c2'), loc), k)
262 end 262 end
263 263
264 fun kunifsRemain k =
265 case k of
266 L'.KUnif (_, ref NONE) => true
267 | _ => false
268
269 val kunifsInKind = U.Kind.exists kunifsRemain
270 val kunifsInCon = U.Con.exists {kind = kunifsRemain,
271 con = fn _ => false}
272
273 datatype decl_error =
274 KunifsRemainKind of ErrorMsg.span * L'.kind
275 | KunifsRemainCon of ErrorMsg.span * L'.con
276
277 fun declError env err =
278 case err of
279 KunifsRemainKind (loc, k) =>
280 (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in kind";
281 eprefaces' [("Kind", p_kind k)])
282 | KunifsRemainCon (loc, c) =>
283 (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in constructor";
284 eprefaces' [("Constructor", p_con env c)])
285
264 fun elabDecl env (d, loc) = 286 fun elabDecl env (d, loc) =
265 (resetKunif (); 287 (resetKunif ();
266 case d of 288 case d of
267 L.DCon (x, ko, c) => 289 L.DCon (x, ko, c) =>
268 let 290 let
272 294
273 val (c', ck) = elabCon env c 295 val (c', ck) = elabCon env c
274 val (env', n) = E.pushCNamed env x k' 296 val (env', n) = E.pushCNamed env x k'
275 in 297 in
276 checkKind env c' ck k'; 298 checkKind env c' ck k';
299
300 if kunifsInKind k' then
301 declError env (KunifsRemainKind (loc, k'))
302 else
303 ();
304
305 if kunifsInCon c' then
306 declError env (KunifsRemainCon (loc, c'))
307 else
308 ();
309
277 (env', 310 (env',
278 (L'.DCon (x, n, k', c'), loc)) 311 (L'.DCon (x, n, k', c'), loc))
279 end) 312 end)
280 313
281 fun elabFile env ds = 314 fun elabFile env ds =