Mercurial > urweb

comparison src/elaborate.sml @ 713:baaae037e7f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Retry failed record summary unifications at the end, in hopes that more has been learned
author Adam Chlipala <adamc@hcoop.net>
date Thu, 09 Apr 2009 14:59:29 -0400
parents 915ec60592d4
children f152f215a02c
comparison
equal deleted inserted replaced
712:915ec60592d4 713:baaae037e7f6
495 fields : (L'.con * L'.con) list, 495 fields : (L'.con * L'.con) list,
496 unifs : (L'.con * L'.con option ref) list, 496 unifs : (L'.con * L'.con option ref) list,
497 others : L'.con list 497 others : L'.con list
498 } 498 }
499 499
500 fun normalizeRecordSummary env (r : record_summary) =
501 let
502 val (fields, unifs, others) =
503 foldl (fn (u as (uc, _), (fields, unifs, others)) =>
504 let
505 val uc' = hnormCon env uc
506 in
507 case #1 uc' of
508 L'.CUnif _ => (fields, u :: unifs, others)
509 | L'.CRecord (_, fs) => (fs @ fields, unifs, others)
510 | L'.CConcat ((L'.CRecord (_, fs), _), rest) => (fs @ fields, unifs, rest :: others)
511 | _ => (fields, unifs, uc' :: others)
512 end)
513 (#fields r, [], #others r) (#unifs r)
514 in
515 {fields = fields, unifs = unifs, others = others}
516 end
517
500 fun summaryToCon {fields, unifs, others} = 518 fun summaryToCon {fields, unifs, others} =
501 let 519 let
502 val c = (L'.CRecord (ktype, []), dummy) 520 val c = (L'.CRecord (ktype, []), dummy)
503 val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others 521 val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
504 val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs 522 val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
617 | L'.CKAbs _ => false 635 | L'.CKAbs _ => false
618 | L'.CKApp _ => false 636 | L'.CKApp _ => false
619 | L'.TKFun _ => false 637 | L'.TKFun _ => false
620 638
621 val recdCounter = ref 0 639 val recdCounter = ref 0
640
641 val mayDelay = ref false
642 val delayedUnifs = ref ([] : (E.env * L'.kind * record_summary * record_summary) list)
622 643
623 fun unifyRecordCons env (c1, c2) = 644 fun unifyRecordCons env (c1, c2) =
624 let 645 let
625 fun rkindof c = 646 fun rkindof c =
626 case hnormKind (kindof env c) of 647 case hnormKind (kindof env c) of
785 | _ => (fs1, fs2, others1, others2) 806 | _ => (fs1, fs2, others1, others2)
786 807
787 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 808 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
788 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 809 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
789 810
790 val clear = case (fs1, others1, fs2, others2) of
791 ([], [], [], []) => true
792 | _ => false
793 val empty = (L'.CRecord (k, []), dummy) 811 val empty = (L'.CRecord (k, []), dummy)
812 fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
794 in 813 in
795 case (unifs1, fs1, others1, unifs2, fs2, others2) of 814 case (unifs1, fs1, others1, unifs2, fs2, others2) of
796 (_, [], [], [], [], []) => 815 (_, [], [], [], [], []) =>
797 app (fn (_, r) => r := SOME empty) unifs1 816 app (fn (_, r) => r := SOME empty) unifs1
798 | ([], [], [], _, [], []) => 817 | ([], [], [], _, [], []) =>
799 app (fn (_, r) => r := SOME empty) unifs2 818 app (fn (_, r) => r := SOME empty) unifs2
800 | _ => if clear then 819 | ([], _, _, _, _ :: _, _) => failure ()
801 () 820 | ([], _, _, _, _, _ :: _) => failure ()
802 else 821 | (_, _ :: _, _, [], _, _) => failure ()
803 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) 822 | (_, _, _ :: _, [], _, _) => failure ()
823 | _ =>
824 if !mayDelay then
825 delayedUnifs := (env, k, s1, s2) :: !delayedUnifs
826 else
827 failure ()
828
804 (*before eprefaces "Summaries'" [("#1", p_summary env s1), 829 (*before eprefaces "Summaries'" [("#1", p_summary env s1),
805 ("#2", p_summary env s2)]*) 830 ("#2", p_summary env s2)]*)
806 end 831 end
807 832
808 and guessMap env (c1, c2, ex) = 833 and guessMap env (c1, c2, ex) =
3552 (strerror, sgnerror, [])) 3577 (strerror, sgnerror, []))
3553 end 3578 end
3554 3579
3555 fun elabFile basis topStr topSgn env file = 3580 fun elabFile basis topStr topSgn env file =
3556 let 3581 let
3582 val () = mayDelay := true
3583 val () = delayedUnifs := []
3584
3557 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) 3585 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan)
3558 val () = case gs of 3586 val () = case gs of
3559 [] => () 3587 [] => ()
3560 | _ => (app (fn (_, env, _, c1, c2) => 3588 | _ => (app (fn (_, env, _, c1, c2) =>
3561 prefaces "Unresolved" 3589 prefaces "Unresolved"
3609 val (env', top_n) = E.pushStrNamed env' "Top" topSgn 3637 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
3610 val () = top_r := top_n 3638 val () = top_r := top_n
3611 3639
3612 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} 3640 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
3613 3641
3642 val checks = ref ([] : (unit -> unit) list)
3643
3614 fun elabDecl' (d, (env, gs)) = 3644 fun elabDecl' (d, (env, gs)) =
3615 let 3645 let
3616 val () = resetKunif () 3646 val () = resetKunif ()
3617 val () = resetCunif () 3647 val () = resetCunif ()
3618 val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs)) 3648 val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs))
3619 in 3649 in
3620 if ErrorMsg.anyErrors () then 3650 checks :=
3621 () 3651 (fn () =>
3622 else ( 3652 (if List.exists kunifsInDecl ds then
3623 if List.exists kunifsInDecl ds then 3653 declError env (KunifsRemain ds)
3624 declError env (KunifsRemain ds) 3654 else
3625 else 3655 ();
3626 (); 3656
3627 3657 case ListUtil.search cunifsInDecl ds of
3628 case ListUtil.search cunifsInDecl ds of 3658 NONE => ()
3629 NONE => () 3659 | SOME loc =>
3630 | SOME loc => 3660 declError env (CunifsRemain ds)))
3631 declError env (CunifsRemain ds) 3661 :: !checks;
3632 );
3633 3662
3634 (ds, (env, gs)) 3663 (ds, (env, gs))
3635 end 3664 end
3636 3665
3637 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file 3666 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
3638 in 3667 in
3668 mayDelay := false;
3669
3670 app (fn (env, k, s1, s2) =>
3671 unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
3672 handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in final record unification";
3673 cunifyError env err))
3674 (!delayedUnifs);
3675 delayedUnifs := [];
3676
3677 if ErrorMsg.anyErrors () then
3678 ()
3679 else
3680 app (fn f => f ()) (!checks);
3681
3639 if ErrorMsg.anyErrors () then 3682 if ErrorMsg.anyErrors () then
3640 () 3683 ()
3641 else 3684 else
3642 app (fn Disjoint (loc, env, denv, c1, c2) => 3685 app (fn Disjoint (loc, env, denv, c1, c2) =>
3643 (case D.prove env denv (c1, c2, loc) of 3686 (case D.prove env denv (c1, c2, loc) of