Mercurial > urweb

comparison src/elaborate.sml @ 709:0406e9cccb72

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FOREIGN KEY, without ability to link NULL to NOT NULL (and with some lingering problems in row inference)
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 18:47:47 -0400
parents d8217b4cb617
children 71409a4ccb67
comparison
equal deleted inserted replaced
708:1a317a707d71 709:0406e9cccb72
461 case k of 461 case k of
462 L'.KUnif (_, _, ref NONE) => true 462 L'.KUnif (_, _, ref NONE) => true
463 | _ => false 463 | _ => false
464 fun cunifsRemain c = 464 fun cunifsRemain c =
465 case c of 465 case c of
466 L'.CUnif (loc, _, _, ref NONE) => SOME loc 466 L'.CUnif (loc, (L'.KRecord k, _), _, r as ref NONE) =>
467 (r := SOME (L'.CRecord (k, []), loc);
468 NONE)
469 | L'.CUnif (loc, _, _, ref NONE) => SOME loc
467 | _ => NONE 470 | _ => NONE
468 471
469 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain, 472 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
470 con = fn _ => false, 473 con = fn _ => false,
471 exp = fn _ => false, 474 exp = fn _ => false,
615 | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit 618 | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit
616 619
617 | L'.CKAbs _ => false 620 | L'.CKAbs _ => false
618 | L'.CKApp _ => false 621 | L'.CKApp _ => false
619 | L'.TKFun _ => false 622 | L'.TKFun _ => false
623
624 val recdCounter = ref 0
620 625
621 fun unifyRecordCons env (c1, c2) = 626 fun unifyRecordCons env (c1, c2) =
622 let 627 let
623 fun rkindof c = 628 fun rkindof c =
624 case hnormKind (kindof env c) of 629 case hnormKind (kindof env c) of
709 714
710 val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2) 715 val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2)
711 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 716 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
712 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 717 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
713 718
719 fun unsummarize {fields, unifs, others} =
720 let
721 val c = (L'.CRecord (k, fields), loc)
722
723 val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
724 c unifs
725 in
726 foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
727 c others
728 end
729
730 val (unifs1, fs1, others1, unifs2, fs2, others2) =
731 case (unifs1, fs1, others1, unifs2, fs2, others2) of
732 orig as ([(_, r)], [], [], _, _, _) =>
733 let
734 val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
735 in
736 if occursCon r c then
737 orig
738 else
739 (r := SOME c;
740 ([], [], [], [], [], []))
741 end
742 | orig as (_, _, _, [(_, r)], [], []) =>
743 let
744 val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
745 in
746 if occursCon r c then
747 orig
748 else
749 (r := SOME c;
750 ([], [], [], [], [], []))
751 end
752 | orig => orig
753
714 fun unifFields (fs, others, unifs) = 754 fun unifFields (fs, others, unifs) =
715 case (fs, others, unifs) of 755 case (fs, others, unifs) of
716 ([], [], _) => ([], [], unifs) 756 ([], [], _) => ([], [], unifs)
717 | (_, _, []) => (fs, others, []) 757 | (_, _, []) => (fs, others, [])
718 | (_, _, (_, r) :: rest) => 758 | (_, _, (_, r) :: rest) =>
719 let 759 let
720 val r' = ref NONE 760 val r' = ref NONE
721 val kr = (L'.KRecord k, dummy) 761 val kr = (L'.KRecord k, dummy)
722 val cr' = (L'.CUnif (dummy, kr, "recd", r'), dummy) 762 val cr' = (L'.CUnif (dummy, kr, ("recd" ^ Int.toString (!recdCounter)), r'), dummy)
763 val () = recdCounter := 1 + !recdCounter
723 764
724 val prefix = case (fs, others) of 765 val prefix = case (fs, others) of
725 ([], other :: others) => 766 ([], other :: others) =>
726 List.foldl (fn (other, c) => 767 List.foldl (fn (other, c) =>
727 (L'.CConcat (c, other), dummy)) 768 (L'.CConcat (c, other), dummy))
760 ([], [], [], []) 801 ([], [], [], [])
761 else 802 else
762 (fs1, fs2, others1, others2) 803 (fs1, fs2, others1, others2)
763 | _ => (fs1, fs2, others1, others2) 804 | _ => (fs1, fs2, others1, others2)
764 805
806 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (unifs1, unifs2)
807
765 (*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}),
766 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 809 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
767 810
768 val clear = case (fs1, others1, fs2, others2) of 811 val clear = case (fs1, others1, fs2, others2) of
769 ([], [], [], []) => true 812 ([], [], [], []) => true
770 | _ => false 813 | _ => false
771 val empty = (L'.CRecord (k, []), dummy) 814 val empty = (L'.CRecord (k, []), dummy)
772 815
773 fun unsummarize {fields, unifs, others} = 816 fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
817 in
818 case (unifs1, fs1, others1, unifs2, fs2, others2) of
819 ([(_, r)], [], [], _, _, _) =>
774 let 820 let
775 val c = (L'.CRecord (k, fields), loc) 821 val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
776
777 val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
778 c unifs
779 in 822 in
780 foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc)) 823 if occursCon r c then
781 c others 824 failure ()
825 else
826 r := SOME c
782 end 827 end
783 828 | (_, _, _, [(_, r)], [], []) =>
784 fun pairOffUnifs (unifs1, unifs2) = 829 let
785 case (unifs1, unifs2) of 830 val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
786 ([], _) => 831 in
787 if clear then 832 if occursCon r c then
788 List.app (fn (_, r) => r := SOME empty) unifs2 833 failure ()
789 else 834 else
790 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) 835 r := SOME c
791 | (_, []) => 836 end
792 if clear then 837 | _ => if clear then
793 List.app (fn (_, r) => r := SOME empty) unifs1 838 ()
794 else 839 else
795 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) 840 failure ()
796 | ((c1, _) :: rest1, (_, r2) :: rest2) =>
797 (r2 := SOME c1;
798 pairOffUnifs (rest1, rest2))
799 in
800 pairOffUnifs (unifs1, unifs2)
801 (*before eprefaces "Summaries'" [("#1", p_summary env s1), 841 (*before eprefaces "Summaries'" [("#1", p_summary env s1),
802 ("#2", p_summary env s2)]*) 842 ("#2", p_summary env s2)]*)
803 end 843 end
804 844
805 and guessMap env (c1, c2, ex) = 845 and guessMap env (c1, c2, ex) =