Mercurial > urweb

comparison src/elaborate.sml @ 777:87a7702d681d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
outer demo
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 May 2009 14:57:33 -0400
parents 8688e01ae469
children d20d6afc1206
comparison
equal deleted inserted replaced
776:9f2555f06901 777:87a7702d681d
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
518 fun summaryToCon {fields, unifs, others} = 500 fun summaryToCon {fields, unifs, others} =
519 let 501 let
520 val c = (L'.CRecord (ktype, []), dummy) 502 val c = (L'.CRecord (ktype, []), dummy)
521 val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others 503 val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
522 val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs 504 val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
637 | L'.TKFun _ => false 619 | L'.TKFun _ => false
638 620
639 val recdCounter = ref 0 621 val recdCounter = ref 0
640 622
641 val mayDelay = ref false 623 val mayDelay = ref false
642 val delayedUnifs = ref ([] : (E.env * L'.kind * record_summary * record_summary) list) 624 val delayedUnifs = ref ([] : (ErrorMsg.span * E.env * L'.kind * record_summary * record_summary) list)
643 625
644 fun unifyRecordCons env (c1, c2) = 626 fun unifyRecordCons env (loc, c1, c2) =
645 let 627 let
646 fun rkindof c = 628 fun rkindof c =
647 case hnormKind (kindof env c) of 629 case hnormKind (kindof env c) of
648 (L'.KRecord k, _) => k 630 (L'.KRecord k, _) => k
649 | (L'.KError, _) => kerror 631 | (L'.KError, _) => kerror
661 643
662 val r1 = recordSummary env c1 644 val r1 = recordSummary env c1
663 val r2 = recordSummary env c2 645 val r2 = recordSummary env c2
664 in 646 in
665 unifyKinds env k1 k2; 647 unifyKinds env k1 k2;
666 unifySummaries env (k1, r1, r2) 648 unifySummaries env (loc, k1, r1, r2)
667 end 649 end
650
651 and normalizeRecordSummary env (r : record_summary) =
652 recordSummary env (summaryToCon r)
668 653
669 and recordSummary env c = 654 and recordSummary env c =
670 let 655 let
671 val c = hnormCon env c 656 val c = hnormCon env c
672 657
688 in 673 in
689 sum 674 sum
690 end 675 end
691 676
692 and consEq env (c1, c2) = 677 and consEq env (c1, c2) =
693 (unifyCons env c1 c2; 678 let
694 true) 679 val mayDelay' = !mayDelay
695 handle CUnify _ => false 680 in
681 (mayDelay := false;
682 unifyCons env c1 c2;
683 mayDelay := mayDelay';
684 true)
685 handle CUnify _ => (mayDelay := mayDelay'; false)
686 end
696 687
697 and consNeq env (c1, c2) = 688 and consNeq env (c1, c2) =
698 case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of 689 case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of
699 (L'.CName x1, L'.CName x2) => x1 <> x2 690 (L'.CName x1, L'.CName x2) => x1 <> x2
700 | _ => false 691 | _ => false
701 692
702 and unifySummaries env (k, s1 : record_summary, s2 : record_summary) = 693 and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) =
703 let 694 let
704 val loc = #2 k 695 val loc = #2 k
696 val pdescs = [("#1", p_summary env s1),
697 ("#2", p_summary env s2)]
705 (*val () = eprefaces "Summaries" [("#1", p_summary env s1), 698 (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
706 ("#2", p_summary env s2)]*) 699 ("#2", p_summary env s2)]*)
707 700
708 fun eatMatching p (ls1, ls2) = 701 fun eatMatching p (ls1, ls2) =
709 let 702 let
789 else 782 else
790 orig 783 orig
791 | orig => orig 784 | orig => orig
792 785
793 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 786 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
794 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 787 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
795 788
796 fun isGuessable (other, fs, unifs) = 789 fun isGuessable (other, fs, unifs) =
797 let 790 let
798 val c = (L'.CRecord (k, fs), loc) 791 val c = (L'.CRecord (k, fs), loc)
799 val c = foldl (fn ((c', _), c) => (L'.CConcat (c', c), loc)) c unifs 792 val c = foldl (fn ((c', _), c) => (L'.CConcat (c', c), loc)) c unifs
809 if isGuessable (other1, fs2, unifs2) then 802 if isGuessable (other1, fs2, unifs2) then
810 ([], [], [], [], [], []) 803 ([], [], [], [], [], [])
811 else 804 else
812 (fs1, fs2, others1, others2, unifs1, unifs2) 805 (fs1, fs2, others1, others2, unifs1, unifs2)
813 | (_, [], [], [other2], _, []) => 806 | (_, [], [], [other2], _, []) =>
814 if isGuessable (other2, fs1, unifs1) then 807 if isGuessable (other2, fs1, unifs1) then
815 ([], [], [], [], [], []) 808 ([], [], [], [], [], [])
816 else 809 else
817 (prefaces "Not guessable" [("other2", p_con env other2), 810 (fs1, fs2, others1, others2, unifs1, unifs2)
818 ("fs1", p_con env (L'.CRecord (k, fs1), loc)),
819 ("#unifs1", PD.string (Int.toString (length unifs1)))];
820 (fs1, fs2, others1, others2, unifs1, unifs2))
821 | _ => (fs1, fs2, others1, others2, unifs1, unifs2) 811 | _ => (fs1, fs2, others1, others2, unifs1, unifs2)
822 812
823 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 813 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
824 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 814 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
825 815
826 val empty = (L'.CRecord (k, []), dummy) 816 val empty = (L'.CRecord (k, []), dummy)
827 fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) 817 fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
828 in 818 in
829 case (unifs1, fs1, others1, unifs2, fs2, others2) of 819 (case (unifs1, fs1, others1, unifs2, fs2, others2) of
830 (_, [], [], [], [], []) => 820 (_, [], [], [], [], []) =>
831 app (fn (_, r) => r := SOME empty) unifs1 821 app (fn (_, r) => r := SOME empty) unifs1
832 | ([], [], [], _, [], []) => 822 | ([], [], [], _, [], []) =>
833 app (fn (_, r) => r := SOME empty) unifs2 823 app (fn (_, r) => r := SOME empty) unifs2
834 | ([], _, _, _, _ :: _, _) => failure () 824 | _ =>
835 | ([], _, _, _, _, _ :: _) => failure () 825 if !mayDelay then
836 | (_, _ :: _, _, [], _, _) => failure () 826 delayedUnifs := (loc, env, k, s1, s2) :: !delayedUnifs
837 | (_, _, _ :: _, [], _, _) => failure () 827 else
838 | _ => 828 failure ())
839 if !mayDelay then 829
840 delayedUnifs := (env, k, s1, s2) :: !delayedUnifs 830 (*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)),
841 else 831 ("#2", p_summary env (normalizeRecordSummary env s2))]*)
842 failure ()
843
844 (*before eprefaces "Summaries'" [("#1", p_summary env s1),
845 ("#2", p_summary env s2)]*)
846 end 832 end
847 833
848 and guessMap env (c1, c2, ex) = 834 and guessMap env (c1, c2, ex) =
849 let 835 let
850 val loc = #2 c1 836 val loc = #2 c1
880 unfold (r1, c1'); 866 unfold (r1, c1');
881 unfold (r2, c2'); 867 unfold (r2, c2');
882 unifyCons env r (L'.CConcat (r1, r2), loc) 868 unifyCons env r (L'.CConcat (r1, r2), loc)
883 end 869 end
884 | L'.CUnif (_, _, _, ur) => 870 | L'.CUnif (_, _, _, ur) =>
885 let 871 ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc)
886 val ur' = cunif (loc, (L'.KRecord dom, loc))
887 in
888 ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), ur'), loc)
889 end
890 | _ => raise ex 872 | _ => raise ex
891 in 873 in
892 unfold (r, c) 874 unfold (r, c)
893 end 875 end
894 handle _ => raise ex 876 handle _ => raise ex
976 unifyCons' env c1All (List.nth (us, n2 - 1)) 958 unifyCons' env c1All (List.nth (us, n2 - 1))
977 end 959 end
978 | _ => onFail ()) 960 | _ => onFail ())
979 | _ => onFail () 961 | _ => onFail ()
980 962
981 fun isRecord' () = unifyRecordCons env (c1All, c2All) 963 fun isRecord' () = unifyRecordCons env (loc, c1All, c2All)
982 964
983 fun isRecord () = 965 fun isRecord () =
984 case (c1, c2) of 966 case (c1, c2) of
985 (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord') 967 (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord')
986 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord') 968 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord')
3735 (ds, (env, gs)) 3717 (ds, (env, gs))
3736 end 3718 end
3737 3719
3738 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file 3720 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
3739 3721
3740 val delayed = !delayedUnifs 3722 fun oneSummaryRound () =
3723 if ErrorMsg.anyErrors () then
3724 ()
3725 else
3726 let
3727 val delayed = !delayedUnifs
3728 in
3729 delayedUnifs := [];
3730 app (fn (loc, env, k, s1, s2) =>
3731 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2))
3732 delayed
3733 end
3741 in 3734 in
3742 delayedUnifs := []; 3735 oneSummaryRound ();
3743 app (fn (env, k, s1, s2) =>
3744 unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2))
3745 delayed;
3746 3736
3747 if ErrorMsg.anyErrors () then 3737 if ErrorMsg.anyErrors () then
3748 () 3738 ()
3749 else 3739 else
3750 let 3740 let
3806 end) 3796 end)
3807 false gs 3797 false gs
3808 in 3798 in
3809 case (gs, solved) of 3799 case (gs, solved) of
3810 ([], _) => () 3800 ([], _) => ()
3811 | (_, true) => solver gs 3801 | (_, true) => (oneSummaryRound (); solver gs)
3812 | _ => 3802 | _ =>
3813 app (fn Disjoint (loc, env, denv, c1, c2) => 3803 app (fn Disjoint (loc, env, denv, c1, c2) =>
3814 ((ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; 3804 ((ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
3815 eprefaces' [("Con 1", p_con env c1), 3805 eprefaces' [("Con 1", p_con env c1),
3816 ("Con 2", p_con env c2), 3806 ("Con 2", p_con env c2),
3824 solver gs 3814 solver gs
3825 end; 3815 end;
3826 3816
3827 mayDelay := false; 3817 mayDelay := false;
3828 3818
3829 app (fn (env, k, s1, s2) => 3819 if ErrorMsg.anyErrors () then
3830 unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) 3820 ()
3831 handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in final record unification"; 3821 else
3832 cunifyError env err)) 3822 (app (fn (loc, env, k, s1, s2) =>
3833 (!delayedUnifs); 3823 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
3834 delayedUnifs := []; 3824 handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification";
3825 cunifyError env err))
3826 (!delayedUnifs);
3827 delayedUnifs := []);
3835 3828
3836 if ErrorMsg.anyErrors () then 3829 if ErrorMsg.anyErrors () then
3837 () 3830 ()
3838 else 3831 else
3839 app (fn f => f ()) (!checks); 3832 app (fn f => f ()) (!checks);