Mercurial > urweb

comparison src/elaborate.sml @ 10:dde5c52e5e5e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of elaborating expressions
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 13:59:03 -0400
parents 14b533dbe6cc
children e97c6d335869
comparison
equal deleted inserted replaced
9:14b533dbe6cc 10:dde5c52e5e5e
137 val ktype = (L'.KType, dummy) 137 val ktype = (L'.KType, dummy)
138 val kname = (L'.KName, dummy) 138 val kname = (L'.KName, dummy)
139 139
140 val cerror = (L'.CError, dummy) 140 val cerror = (L'.CError, dummy)
141 val kerror = (L'.KError, dummy) 141 val kerror = (L'.KError, dummy)
142 val eerror = (L'.EError, dummy)
142 143
143 local 144 local
144 val count = ref 0 145 val count = ref 0
145 in 146 in
146 147
158 (L'.KUnif (s, ref NONE), dummy) 159 (L'.KUnif (s, ref NONE), dummy)
159 end 160 end
160 161
161 end 162 end
162 163
164 local
165 val count = ref 0
166 in
167
168 fun resetCunif () = count := 0
169
170 fun cunif k =
171 let
172 val n = !count
173 val s = if n <= 26 then
174 str (chr (ord #"A" + n))
175 else
176 "U" ^ Int.toString (n - 26)
177 in
178 count := n + 1;
179 (L'.CUnif (k, s, ref NONE), dummy)
180 end
181
182 end
183
163 fun elabCon env (c, loc) = 184 fun elabCon env (c, loc) =
164 case c of 185 case c of
165 L.CAnnot (c, k) => 186 L.CAnnot (c, k) =>
166 let 187 let
167 val k' = elabKind k 188 val k' = elabKind k
262 283
263 fun kunifsRemain k = 284 fun kunifsRemain k =
264 case k of 285 case k of
265 L'.KUnif (_, ref NONE) => true 286 L'.KUnif (_, ref NONE) => true
266 | _ => false 287 | _ => false
288 fun cunifsRemain c =
289 case c of
290 L'.CUnif (_, _, ref NONE) => true
291 | _ => false
267 292
268 val kunifsInKind = U.Kind.exists kunifsRemain 293 val kunifsInKind = U.Kind.exists kunifsRemain
269 val kunifsInCon = U.Con.exists {kind = kunifsRemain, 294 val kunifsInCon = U.Con.exists {kind = kunifsRemain,
270 con = fn _ => false} 295 con = fn _ => false}
296 val kunifsInExp = U.Exp.exists {kind = kunifsRemain,
297 con = fn _ => false,
298 exp = fn _ => false}
299
300 val cunifsInCon = U.Con.exists {kind = fn _ => false,
301 con = cunifsRemain}
302 val cunifsInExp = U.Exp.exists {kind = fn _ => false,
303 con = cunifsRemain,
304 exp = fn _ => false}
305
306 fun occursCon r =
307 U.Con.exists {kind = fn _ => false,
308 con = fn L'.CUnif (_, _, r') => r = r'
309 | _ => false}
310
311 datatype cunify_error =
312 CKind of L'.kind * L'.kind * kunify_error
313 | COccursCheckFailed of L'.con * L'.con
314 | CIncompatible of L'.con * L'.con
315 | CExplicitness of L'.con * L'.con
316
317 exception CUnify' of cunify_error
318
319 fun cunifyError env err =
320 case err of
321 CKind (k1, k2, kerr) =>
322 (eprefaces "Kind unification failure"
323 [("Kind 1", p_kind k1),
324 ("Kind 2", p_kind k2)];
325 kunifyError kerr)
326 | COccursCheckFailed (c1, c2) =>
327 eprefaces "Constructor occurs check failed"
328 [("Con 1", p_con env c1),
329 ("Con 2", p_con env c2)]
330 | CIncompatible (c1, c2) =>
331 eprefaces "Incompatible constructors"
332 [("Con 1", p_con env c1),
333 ("Con 2", p_con env c2)]
334 | CExplicitness (c1, c2) =>
335 eprefaces "Differing constructor function explicitness"
336 [("Con 1", p_con env c1),
337 ("Con 2", p_con env c2)]
338
339 fun unifyCons' env (c1All as (c1, _)) (c2All as (c2, _)) =
340 let
341 fun err f = raise CUnify' (f (c1All, c2All))
342 in
343 case (c1, c2) of
344 (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
345 (unifyCons' env d1 d2;
346 unifyCons' env r1 r2)
347 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
348 if expl1 <> expl2 then
349 err CExplicitness
350 else
351 (unifyKinds d1 d2;
352 unifyCons' (E.pushCRel env x1 d1) r1 r2)
353 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2
354
355 | (L'.CRel n1, L'.CRel n2) =>
356 if n1 = n2 then
357 ()
358 else
359 err CIncompatible
360 | (L'.CNamed n1, L'.CNamed n2) =>
361 if n1 = n2 then
362 ()
363 else
364 err CIncompatible
365
366 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
367 (unifyCons' env d1 d2;
368 unifyCons' env r1 r2)
369 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
370 (unifyKinds k1 k2;
371 unifyCons' (E.pushCRel env x1 k1) c1 c2)
372
373 | (L'.CName n1, L'.CName n2) =>
374 if n1 = n2 then
375 ()
376 else
377 err CIncompatible
378
379 | (L'.CRecord (k1, rs1), L'.CRecord (k2, rs2)) =>
380 (unifyKinds k1 k2;
381 ((ListPair.appEq (fn ((n1, v1), (n2, v2)) =>
382 (unifyCons' env n1 n2;
383 unifyCons' env v1 v2)) (rs1, rs2))
384 handle ListPair.UnequalLengths => err CIncompatible))
385 | (L'.CConcat (d1, r1), L'.CConcat (d2, r2)) =>
386 (unifyCons' env d1 d2;
387 unifyCons' env r1 r2)
388
389
390 | (L'.CError, _) => ()
391 | (_, L'.CError) => ()
392
393 | (L'.CUnif (_, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All
394 | (_, L'.CUnif (_, _, ref (SOME c2All))) => unifyCons' env c1All c2All
395
396 | (L'.CUnif (k1, _, r1), L'.CUnif (k2, _, r2)) =>
397 if r1 = r2 then
398 ()
399 else
400 (unifyKinds k1 k2;
401 r1 := SOME c2All)
402
403 | (L'.CUnif (_, _, r), _) =>
404 if occursCon r c2All then
405 err COccursCheckFailed
406 else
407 r := SOME c2All
408 | (_, L'.CUnif (_, _, r)) =>
409 if occursCon r c1All then
410 err COccursCheckFailed
411 else
412 r := SOME c1All
413
414 | _ => err CIncompatible
415 end
416
417 exception CUnify of L'.con * L'.con * cunify_error
418
419 fun unifyCons env c1 c2 =
420 unifyCons' env c1 c2
421 handle CUnify' err => raise CUnify (c1, c2, err)
422 | KUnify args => raise CUnify (c1, c2, CKind args)
423
424 datatype exp_error =
425 UnboundExp of ErrorMsg.span * string
426 | Unify of L'.exp * L'.con * L'.con * cunify_error
427
428 fun expError env err =
429 case err of
430 UnboundExp (loc, s) =>
431 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
432 | Unify (e, c1, c2, uerr) =>
433 (ErrorMsg.errorAt (#2 e) "Unification failure";
434 eprefaces' [("Expression", p_exp env e),
435 ("Have con", p_con env c1),
436 ("Need con", p_con env c2)];
437 cunifyError env uerr)
438
439 fun checkCon env e c1 c2 =
440 unifyCons env c1 c2
441 handle CUnify (c1, c2, err) =>
442 expError env (Unify (e, c1, c2, err))
443
444 fun elabExp env (e, loc) =
445 case e of
446 L.EAnnot (e, t) =>
447 let
448 val (e', et) = elabExp env e
449 val (t', _) = elabCon env t
450 in
451 checkCon env e' et t';
452 (e', t')
453 end
454
455 | L.EVar s =>
456 (case E.lookupE env s of
457 E.NotBound =>
458 (expError env (UnboundExp (loc, s));
459 (eerror, cerror))
460 | E.Rel (n, t) => ((L'.ERel n, loc), t)
461 | E.Named (n, t) => ((L'.ENamed n, loc), t))
462 | L.EApp (e1, e2) =>
463 let
464 val (e1', t1) = elabExp env e1
465 val (e2', t2) = elabExp env e2
466
467 val dom = cunif ktype
468 val ran = cunif ktype
469 val t = (L'.TFun (dom, ran), dummy)
470 in
471 checkCon env e1' t1 t;
472 checkCon env e2' t2 dom;
473 ((L'.EApp (e1', e2'), loc), ran)
474 end
475 | L.EAbs (x, to, e) =>
476 let
477 val t' = case to of
478 NONE => cunif ktype
479 | SOME t =>
480 let
481 val (t', tk) = elabCon env t
482 in
483 checkKind env t' tk ktype;
484 t'
485 end
486 val (e', et) = elabExp (E.pushERel env x t') e
487 in
488 ((L'.EAbs (x, t', e'), loc),
489 (L'.TFun (t', et), loc))
490 end
491 | L.ECApp (e, c) =>
492 let
493 val (e', et) = elabExp env e
494 val (c', ck) = elabCon env c
495 in
496 raise Fail "ECApp"
497 end
498 | L.ECAbs _ => raise Fail "ECAbs"
271 499
272 datatype decl_error = 500 datatype decl_error =
273 KunifsRemainKind of ErrorMsg.span * L'.kind 501 KunifsRemainKind of ErrorMsg.span * L'.kind
274 | KunifsRemainCon of ErrorMsg.span * L'.con 502 | KunifsRemainCon of ErrorMsg.span * L'.con
503 | KunifsRemainExp of ErrorMsg.span * L'.exp
504 | CunifsRemainCon of ErrorMsg.span * L'.con
505 | CunifsRemainExp of ErrorMsg.span * L'.exp
275 506
276 fun declError env err = 507 fun declError env err =
277 case err of 508 case err of
278 KunifsRemainKind (loc, k) => 509 KunifsRemainKind (loc, k) =>
279 (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in kind"; 510 (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in kind";
280 eprefaces' [("Kind", p_kind k)]) 511 eprefaces' [("Kind", p_kind k)])
281 | KunifsRemainCon (loc, c) => 512 | KunifsRemainCon (loc, c) =>
282 (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in constructor"; 513 (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in constructor";
283 eprefaces' [("Constructor", p_con env c)]) 514 eprefaces' [("Constructor", p_con env c)])
515 | KunifsRemainExp (loc, e) =>
516 (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in expression";
517 eprefaces' [("Expression", p_exp env e)])
518 | CunifsRemainCon (loc, c) =>
519 (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in constructor";
520 eprefaces' [("Constructor", p_con env c)])
521 | CunifsRemainExp (loc, e) =>
522 (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression";
523 eprefaces' [("Expression", p_exp env e)])
284 524
285 fun elabDecl env (d, loc) = 525 fun elabDecl env (d, loc) =
286 (resetKunif (); 526 (resetKunif ();
287 case d of 527 case d of
288 L.DCon (x, ko, c) => 528 L.DCon (x, ko, c) =>
306 else 546 else
307 (); 547 ();
308 548
309 (env', 549 (env',
310 (L'.DCon (x, n, k', c'), loc)) 550 (L'.DCon (x, n, k', c'), loc))
551 end
552 | L.DVal (x, co, e) =>
553 let
554 val (c', ck) = case co of
555 NONE => (cunif ktype, ktype)
556 | SOME c => elabCon env c
557
558 val (e', et) = elabExp env e
559 val (env', n) = E.pushENamed env x c'
560 in
561 checkCon env e' et c';
562
563 if kunifsInCon c' then
564 declError env (KunifsRemainCon (loc, c'))
565 else
566 ();
567
568 if cunifsInCon c' then
569 declError env (CunifsRemainCon (loc, c'))
570 else
571 ();
572
573 if kunifsInExp e' then
574 declError env (KunifsRemainExp (loc, e'))
575 else
576 ();
577
578 if cunifsInExp e' then
579 declError env (CunifsRemainExp (loc, e'))
580 else
581 ();
582
583 (env',
584 (L'.DVal (x, n, c', e'), loc))
311 end) 585 end)
312 586
313 fun elabFile env ds = 587 fun elabFile env ds =
314 ListUtil.mapfoldl (fn (d, env) => elabDecl env d) env ds 588 ListUtil.mapfoldl (fn (d, env) => elabDecl env d) env ds
315 589