Mercurial > urweb

comparison src/elaborate.sml @ 12:d89477f07c1e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fun with records
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 17:34:57 -0400
parents e97c6d335869
children 6049e2193bf2
comparison
equal deleted inserted replaced
11:e97c6d335869 12:d89477f07c1e
134 134
135 val dummy = ErrorMsg.dummySpan 135 val dummy = ErrorMsg.dummySpan
136 136
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 val ktype_record = (L'.KRecord ktype, dummy)
139 140
140 val cerror = (L'.CError, dummy) 141 val cerror = (L'.CError, dummy)
141 val kerror = (L'.KError, dummy) 142 val kerror = (L'.KError, dummy)
142 val eerror = (L'.EError, dummy) 143 val eerror = (L'.EError, dummy)
143 144
311 datatype cunify_error = 312 datatype cunify_error =
312 CKind of L'.kind * L'.kind * kunify_error 313 CKind of L'.kind * L'.kind * kunify_error
313 | COccursCheckFailed of L'.con * L'.con 314 | COccursCheckFailed of L'.con * L'.con
314 | CIncompatible of L'.con * L'.con 315 | CIncompatible of L'.con * L'.con
315 | CExplicitness of L'.con * L'.con 316 | CExplicitness of L'.con * L'.con
317 | CKindof of L'.con
318 | CRecordFailure
316 319
317 exception CUnify' of cunify_error 320 exception CUnify' of cunify_error
318 321
319 fun cunifyError env err = 322 fun cunifyError env err =
320 case err of 323 case err of
333 ("Con 2", p_con env c2)] 336 ("Con 2", p_con env c2)]
334 | CExplicitness (c1, c2) => 337 | CExplicitness (c1, c2) =>
335 eprefaces "Differing constructor function explicitness" 338 eprefaces "Differing constructor function explicitness"
336 [("Con 1", p_con env c1), 339 [("Con 1", p_con env c1),
337 ("Con 2", p_con env c2)] 340 ("Con 2", p_con env c2)]
338 341 | CKindof c =>
339 fun hnormCon env (cAll as (c, _)) = 342 eprefaces "Kind unification variable blocks kindof calculation"
343 [("Con", p_con env c)]
344 | CRecordFailure =>
345 eprefaces "Can't unify record constructors" []
346
347 exception SynUnif
348
349 val liftConInCon =
350 U.Con.mapB {kind = fn k => k,
351 con = fn bound => fn c =>
352 case c of
353 L'.CRel xn =>
354 if xn < bound then
355 c
356 else
357 L'.CRel (xn + 1)
358 | L'.CUnif _ => raise SynUnif
359 | _ => c,
360 bind = fn (bound, U.Con.Rel _) => bound + 1
361 | (bound, _) => bound}
362
363 val subConInCon =
364 U.Con.mapB {kind = fn k => k,
365 con = fn (xn, rep) => fn c =>
366 case c of
367 L'.CRel xn' =>
368 if xn = xn' then
369 #1 rep
370 else
371 c
372 | L'.CUnif _ => raise SynUnif
373 | _ => c,
374 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
375 | (ctx, _) => ctx}
376
377 type record_summary = {
378 fields : (L'.con * L'.con) list,
379 unifs : (L'.con * L'.con option ref) list,
380 others : L'.con list
381 }
382
383 fun summaryToCon {fields, unifs, others} =
384 let
385 val c = (L'.CRecord (ktype, []), dummy)
386 val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
387 val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
388 in
389 (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy)
390 end
391
392 fun p_summary env s = p_con env (summaryToCon s)
393
394 exception CUnify of L'.con * L'.con * cunify_error
395
396 fun hnormKind (kAll as (k, _)) =
397 case k of
398 L'.KUnif (_, ref (SOME k)) => hnormKind k
399 | _ => kAll
400
401 fun kindof env (c, loc) =
402 case c of
403 L'.TFun _ => ktype
404 | L'.TCFun _ => ktype
405 | L'.TRecord _ => ktype
406
407 | L'.CRel xn => #2 (E.lookupCRel env xn)
408 | L'.CNamed xn => #2 (E.lookupCNamed env xn)
409 | L'.CApp (c, _) =>
410 (case #1 (hnormKind (kindof env c)) of
411 L'.KArrow (_, k) => k
412 | L'.KError => kerror
413 | _ => raise CUnify' (CKindof c))
414 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
415
416 | L'.CName _ => kname
417
418 | L'.CRecord (k, _) => (L'.KRecord k, loc)
419 | L'.CConcat (c, _) => kindof env c
420
421 | L'.CError => kerror
422 | L'.CUnif (k, _, _) => k
423
424 fun unifyRecordCons env (c1, c2) =
425 let
426 val k1 = kindof env c1
427 val k2 = kindof env c2
428 in
429 unifyKinds k1 k2;
430 unifySummaries env (k1, recordSummary env c1, recordSummary env c2)
431 end
432
433 and recordSummary env c : record_summary =
434 case hnormCon env c of
435 (L'.CRecord (_, xcs), _) => {fields = xcs, unifs = [], others = []}
436 | (L'.CConcat (c1, c2), _) =>
437 let
438 val s1 = recordSummary env c1
439 val s2 = recordSummary env c2
440 in
441 {fields = #fields s1 @ #fields s2,
442 unifs = #unifs s1 @ #unifs s2,
443 others = #others s1 @ #others s2}
444 end
445 | (L'.CUnif (_, _, ref (SOME c)), _) => recordSummary env c
446 | c' as (L'.CUnif (_, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
447 | c' => {fields = [], unifs = [], others = [c']}
448
449 and consEq env (c1, c2) =
450 (unifyCons env c1 c2;
451 true)
452 handle CUnify _ => false
453
454 and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
455 let
456 val () = eprefaces "Summaries" [("#1", p_summary env s1),
457 ("#2", p_summary env s2)]
458
459 fun eatMatching p (ls1, ls2) =
460 let
461 fun em (ls1, ls2, passed1) =
462 case ls1 of
463 [] => (rev passed1, ls2)
464 | h1 :: t1 =>
465 let
466 fun search (ls2', passed2) =
467 case ls2' of
468 [] => em (t1, ls2, h1 :: passed1)
469 | h2 :: t2 =>
470 if p (h1, h2) then
471 em (t1, List.revAppend (passed2, t2), passed1)
472 else
473 search (t2, h2 :: passed2)
474 in
475 search (ls2, [])
476 end
477 in
478 em (ls1, ls2, [])
479 end
480
481 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
482 if consEq env (x1, x2) then
483 (unifyCons env c1 c2;
484 true)
485 else
486 false) (#fields s1, #fields s2)
487 val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
488 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]
489 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
490 val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2)
491
492 fun unifFields (fs, others, unifs) =
493 case (fs, others, unifs) of
494 ([], [], _) => ([], [], unifs)
495 | (_, _, []) => (fs, others, [])
496 | (_, _, (_, r) :: rest) =>
497 let
498 val r' = ref NONE
499 val cr' = (L'.CUnif (k, "recd", r'), dummy)
500
501 val prefix = case (fs, others) of
502 ([], other :: others) =>
503 List.foldl (fn (other, c) =>
504 (L'.CConcat (c, other), dummy))
505 other others
506 | (fs, []) =>
507 (L'.CRecord (k, fs), dummy)
508 | (fs, others) =>
509 List.foldl (fn (other, c) =>
510 (L'.CConcat (c, other), dummy))
511 (L'.CRecord (k, fs), dummy) others
512 in
513 r := SOME (L'.CConcat (prefix, cr'), dummy);
514 ([], [], (cr', r') :: rest)
515 end
516
517 val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
518 val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
519
520 val clear1 = case (fs1, others1) of
521 ([], []) => true
522 | _ => false
523 val clear2 = case (fs2, others2) of
524 ([], []) => true
525 | _ => false
526 val empty = (L'.CRecord (k, []), dummy)
527 fun pairOffUnifs (unifs1, unifs2) =
528 case (unifs1, unifs2) of
529 ([], _) =>
530 if clear1 then
531 List.app (fn (_, r) => r := SOME empty) unifs2
532 else
533 raise CUnify' CRecordFailure
534 | (_, []) =>
535 if clear2 then
536 List.app (fn (_, r) => r := SOME empty) unifs1
537 else
538 raise CUnify' CRecordFailure
539 | ((c1, _) :: rest1, (_, r2) :: rest2) =>
540 (r2 := SOME c1;
541 pairOffUnifs (rest1, rest2))
542 in
543 pairOffUnifs (unifs1, unifs2)
544 end
545
546 and hnormCon env (cAll as (c, _)) =
340 case c of 547 case c of
341 L'.CUnif (_, _, ref (SOME c)) => hnormCon env c 548 L'.CUnif (_, _, ref (SOME c)) => hnormCon env c
342 549
343 | L'.CNamed xn => 550 | L'.CNamed xn =>
344 (case E.lookupCNamed env xn of 551 (case E.lookupCNamed env xn of
345 (_, _, SOME c') => hnormCon env c' 552 (_, _, SOME c') => hnormCon env c'
346 | _ => cAll) 553 | _ => cAll)
347 554
555 | L'.CApp (c1, c2) =>
556 (case hnormCon env c1 of
557 (L'.CAbs (_, _, cb), _) =>
558 ((hnormCon env (subConInCon (0, c2) cb))
559 handle SynUnif => cAll)
560 | _ => cAll)
561
562 | L'.CConcat (c1, c2) =>
563 (case (hnormCon env c1, hnormCon env c2) of
564 ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) =>
565 (L'.CRecord (k, xcs1 @ xcs2), loc)
566 | _ => cAll)
567
348 | _ => cAll 568 | _ => cAll
349 569
350 fun unifyCons' env c1 c2 = 570 and unifyCons' env c1 c2 =
351 unifyCons'' env (hnormCon env c1) (hnormCon env c2) 571 unifyCons'' env (hnormCon env c1) (hnormCon env c2)
352 572
353 and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) = 573 and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =
354 let 574 let
355 fun err f = raise CUnify' (f (c1All, c2All)) 575 fun err f = raise CUnify' (f (c1All, c2All))
576
577 fun isRecord () = unifyRecordCons env (c1All, c2All)
356 in 578 in
357 case (c1, c2) of 579 case (c1, c2) of
358 (L'.TFun (d1, r1), L'.TFun (d2, r2)) => 580 (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
359 (unifyCons' env d1 d2; 581 (unifyCons' env d1 d2;
360 unifyCons' env r1 r2) 582 unifyCons' env r1 r2)
388 if n1 = n2 then 610 if n1 = n2 then
389 () 611 ()
390 else 612 else
391 err CIncompatible 613 err CIncompatible
392 614
393 | (L'.CRecord (k1, rs1), L'.CRecord (k2, rs2)) =>
394 (unifyKinds k1 k2;
395 ((ListPair.appEq (fn ((n1, v1), (n2, v2)) =>
396 (unifyCons' env n1 n2;
397 unifyCons' env v1 v2)) (rs1, rs2))
398 handle ListPair.UnequalLengths => err CIncompatible))
399 | (L'.CConcat (d1, r1), L'.CConcat (d2, r2)) =>
400 (unifyCons' env d1 d2;
401 unifyCons' env r1 r2)
402
403
404 | (L'.CError, _) => () 615 | (L'.CError, _) => ()
405 | (_, L'.CError) => () 616 | (_, L'.CError) => ()
406 617
407 | (L'.CUnif (_, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All 618 | (L'.CUnif (_, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All
408 | (_, L'.CUnif (_, _, ref (SOME c2All))) => unifyCons' env c1All c2All 619 | (_, L'.CUnif (_, _, ref (SOME c2All))) => unifyCons' env c1All c2All
423 if occursCon r c1All then 634 if occursCon r c1All then
424 err COccursCheckFailed 635 err COccursCheckFailed
425 else 636 else
426 r := SOME c1All 637 r := SOME c1All
427 638
639 | (L'.CRecord _, _) => isRecord ()
640 | (_, L'.CRecord _) => isRecord ()
641 | (L'.CConcat _, _) => isRecord ()
642 | (_, L'.CConcat _) => isRecord ()
643
428 | _ => err CIncompatible 644 | _ => err CIncompatible
429 end 645 end
430 646
431 exception CUnify of L'.con * L'.con * cunify_error 647 and unifyCons env c1 c2 =
432
433 fun unifyCons env c1 c2 =
434 unifyCons' env c1 c2 648 unifyCons' env c1 c2
435 handle CUnify' err => raise CUnify (c1, c2, err) 649 handle CUnify' err => raise CUnify (c1, c2, err)
436 | KUnify args => raise CUnify (c1, c2, CKind args) 650 | KUnify args => raise CUnify (c1, c2, CKind args)
437 651
438 datatype exp_error = 652 datatype exp_error =
462 fun checkCon env e c1 c2 = 676 fun checkCon env e c1 c2 =
463 unifyCons env c1 c2 677 unifyCons env c1 c2
464 handle CUnify (c1, c2, err) => 678 handle CUnify (c1, c2, err) =>
465 expError env (Unify (e, c1, c2, err)) 679 expError env (Unify (e, c1, c2, err))
466 680
467 exception SynUnif
468
469 val liftConInCon =
470 U.Con.mapB {kind = fn k => k,
471 con = fn bound => fn c =>
472 case c of
473 L'.CRel xn =>
474 if xn < bound then
475 c
476 else
477 L'.CRel (xn + 1)
478 | L'.CUnif _ => raise SynUnif
479 | _ => c,
480 bind = fn (bound, U.Con.Rel _) => bound + 1
481 | (bound, _) => bound}
482
483 val subConInCon =
484 U.Con.mapB {kind = fn k => k,
485 con = fn (xn, rep) => fn c =>
486 case c of
487 L'.CRel xn' =>
488 if xn = xn' then
489 #1 rep
490 else
491 c
492 | L'.CUnif _ => raise SynUnif
493 | _ => c,
494 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
495 | (ctx, _) => ctx}
496
497 fun elabExp env (e, loc) = 681 fun elabExp env (e, loc) =
498 case e of 682 case e of
499 L.EAnnot (e, t) => 683 L.EAnnot (e, t) =>
500 let 684 let
501 val (e', et) = elabExp env e 685 val (e', et) = elabExp env e
573 val (e', et) = elabExp (E.pushCRel env x k') e 757 val (e', et) = elabExp (E.pushCRel env x k') e
574 in 758 in
575 ((L'.ECAbs (expl', x, k', e'), loc), 759 ((L'.ECAbs (expl', x, k', e'), loc),
576 (L'.TCFun (expl', x, k', et), loc)) 760 (L'.TCFun (expl', x, k', et), loc))
577 end 761 end
762
763 | L.ERecord xes =>
764 let
765 val xes' = map (fn (x, e) =>
766 let
767 val (x', xk) = elabCon env x
768 val (e', et) = elabExp env e
769 in
770 checkKind env x' xk kname;
771 (x', e', et)
772 end) xes
773 in
774 ((L'.ERecord (map (fn (x', e', _) => (x', e')) xes'), loc),
775 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc))
776 end
777
778 | L.EField (e, c) =>
779 let
780 val (e', et) = elabExp env e
781 val (c', ck) = elabCon env c
782
783 val ft = cunif ktype
784 val rest = cunif ktype_record
785 in
786 checkKind env c' ck kname;
787 checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc);
788 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft)
789 end
790
578 791
579 datatype decl_error = 792 datatype decl_error =
580 KunifsRemainKind of ErrorMsg.span * L'.kind 793 KunifsRemainKind of ErrorMsg.span * L'.kind
581 | KunifsRemainCon of ErrorMsg.span * L'.con 794 | KunifsRemainCon of ErrorMsg.span * L'.con
582 | KunifsRemainExp of ErrorMsg.span * L'.exp 795 | KunifsRemainExp of ErrorMsg.span * L'.exp
601 (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression"; 814 (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression";
602 eprefaces' [("Expression", p_exp env e)]) 815 eprefaces' [("Expression", p_exp env e)])
603 816
604 fun elabDecl env (d, loc) = 817 fun elabDecl env (d, loc) =
605 (resetKunif (); 818 (resetKunif ();
819 resetCunif ();
606 case d of 820 case d of
607 L.DCon (x, ko, c) => 821 L.DCon (x, ko, c) =>
608 let 822 let
609 val k' = case ko of 823 val k' = case ko of
610 NONE => kunif () 824 NONE => kunif ()