Mercurial > urweb

comparison src/elaborate.sml @ 223:bbe5899a9585

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Queries back to working as well as before, after start of refactoring to support grouping
author Adam Chlipala <adamc@hcoop.net>
date Thu, 21 Aug 2008 12:49:29 -0400
parents 2b665e822e9a
children 19e5791923d0
comparison
equal deleted inserted replaced
222:36fef91a6bbf 223:bbe5899a9585
638 Print.PD.string (case s of 638 Print.PD.string (case s of
639 Nil => "Nil" 639 Nil => "Nil"
640 | Cons => "Cons" 640 | Cons => "Cons"
641 | Unknown => "Unknown") 641 | Unknown => "Unknown")
642 642
643 exception SummaryFailure
644
643 fun unifyRecordCons (env, denv) (c1, c2) = 645 fun unifyRecordCons (env, denv) (c1, c2) =
644 let 646 let
645 fun rkindof c = 647 fun rkindof c =
646 case hnormKind (kindof env c) of 648 case hnormKind (kindof env c) of
647 (L'.KRecord k, _) => k 649 (L'.KRecord k, _) => k
699 (L'.CName x1, L'.CName x2) => x1 <> x2 701 (L'.CName x1, L'.CName x2) => x1 <> x2
700 | _ => false 702 | _ => false
701 703
702 and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) = 704 and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
703 let 705 let
706 val loc = #2 k
704 (*val () = eprefaces "Summaries" [("#1", p_summary env s1), 707 (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
705 ("#2", p_summary env s2)]*) 708 ("#2", p_summary env s2)]*)
706 709
707 fun eatMatching p (ls1, ls2) = 710 fun eatMatching p (ls1, ls2) =
708 let 711 let
709 fun em (ls1, ls2, passed1) = 712 fun em (ls1, ls2, passed1) =
710 case ls1 of 713 case ls1 of
730 not (consNeq env (x1, x2)) 733 not (consNeq env (x1, x2))
731 andalso consEq (env, denv) (c1, c2) 734 andalso consEq (env, denv) (c1, c2)
732 andalso consEq (env, denv) (x1, x2)) 735 andalso consEq (env, denv) (x1, x2))
733 (#fields s1, #fields s2) 736 (#fields s1, #fields s2)
734 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}), 737 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
735 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*) 738 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
736 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) 739 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
737 val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2) 740 val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2)
741 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
742 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
738 743
739 fun unifFields (fs, others, unifs) = 744 fun unifFields (fs, others, unifs) =
740 case (fs, others, unifs) of 745 case (fs, others, unifs) of
741 ([], [], _) => ([], [], unifs) 746 ([], [], _) => ([], [], unifs)
742 | (_, _, []) => (fs, others, []) 747 | (_, _, []) => (fs, others, [])
763 end 768 end
764 769
765 val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2) 770 val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
766 val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1) 771 val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
767 772
773 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
774 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
775
776 fun isGuessable (other, fs) =
777 let
778 val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure)
779 in
780 List.all (fn (loc, env, denv, c1, c2) =>
781 case D.prove env denv (c1, c2, loc) of
782 [] => true
783 | _ => false) gs
784 end
785 handle SummaryFailure => false
786
787 val (fs1, fs2, others1, others2) =
788 case (fs1, fs2, others1, others2) of
789 ([], _, [other1], []) =>
790 if isGuessable (other1, fs2) then
791 ([], [], [], [])
792 else
793 (fs1, fs2, others1, others2)
794 | _ => (fs1, fs2, others1, others2)
795
796 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
797 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
798
768 val clear = case (fs1, others1, fs2, others2) of 799 val clear = case (fs1, others1, fs2, others2) of
769 ([], [], [], []) => true 800 ([], [], [], []) => true
770 | _ => false 801 | _ => false
771 val empty = (L'.CRecord (k, []), dummy) 802 val empty = (L'.CRecord (k, []), dummy)
803
772 fun pairOffUnifs (unifs1, unifs2) = 804 fun pairOffUnifs (unifs1, unifs2) =
773 case (unifs1, unifs2) of 805 case (unifs1, unifs2) of
774 ([], _) => 806 ([], _) =>
775 if clear then 807 if clear then
776 List.app (fn (_, r) => r := SOME empty) unifs2 808 List.app (fn (_, r) => r := SOME empty) unifs2
784 | ((c1, _) :: rest1, (_, r2) :: rest2) => 816 | ((c1, _) :: rest1, (_, r2) :: rest2) =>
785 (r2 := SOME c1; 817 (r2 := SOME c1;
786 pairOffUnifs (rest1, rest2)) 818 pairOffUnifs (rest1, rest2))
787 in 819 in
788 pairOffUnifs (unifs1, unifs2) 820 pairOffUnifs (unifs1, unifs2)
821 (*before eprefaces "Summaries'" [("#1", p_summary env s1),
822 ("#2", p_summary env s2)]*)
823 end
824
825 and guessFold (env, denv) (c1, c2, gs, ex) =
826 let
827 val loc = #2 c1
828
829 fun unfold (dom, ran, f, i, r, c) =
830 let
831 val nm = cunif (loc, (L'.KName, loc))
832 val v = cunif (loc, dom)
833 val rest = cunif (loc, (L'.KRecord dom, loc))
834 val acc = (L'.CFold (dom, ran), loc)
835 val acc = (L'.CApp (acc, f), loc)
836 val acc = (L'.CApp (acc, i), loc)
837 val acc = (L'.CApp (acc, rest), loc)
838
839 val (iS, gs3) = summarizeCon (env, denv) i
840
841 val app = (L'.CApp (f, nm), loc)
842 val app = (L'.CApp (app, v), loc)
843 val app = (L'.CApp (app, acc), loc)
844 val (appS, gs4) = summarizeCon (env, denv) app
845
846 val (cS, gs5) = summarizeCon (env, denv) c
847 in
848 (*prefaces "Summaries" [("iS", p_con_summary iS),
849 ("appS", p_con_summary appS),
850 ("cS", p_con_summary cS)];*)
851
852 if compatible (iS, appS) then
853 raise ex
854 else if compatible (cS, iS) then
855 let
856 (*val () = prefaces "Same?" [("i", p_con env i),
857 ("c", p_con env c)]*)
858 val gs6 = unifyCons (env, denv) i c
859 (*val () = TextIO.print "Yes!\n"*)
860
861 val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
862 in
863 gs @ gs3 @ gs5 @ gs6 @ gs7
864 end
865 else if compatible (cS, appS) then
866 let
867 (*val () = prefaces "Same?" [("app", p_con env app),
868 ("c", p_con env c),
869 ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
870 val gs6 = unifyCons (env, denv) app c
871 (*val () = TextIO.print "Yes!\n"*)
872
873 val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
874 val concat = (L'.CConcat (singleton, rest), loc)
875 (*val () = prefaces "Pre-crew" [("r", p_con env r),
876 ("concat", p_con env concat)]*)
877 val gs7 = unifyCons (env, denv) r concat
878 in
879 (*prefaces "The crew" [("nm", p_con env nm),
880 ("v", p_con env v),
881 ("rest", p_con env rest)];*)
882
883 gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
884 end
885 else
886 raise ex
887 end
888 handle _ => raise ex
889 in
890 case (#1 c1, #1 c2) of
891 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) =>
892 unfold (dom, ran, f, i, r, c2)
893 | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) =>
894 unfold (dom, ran, f, i, r, c1)
895 | _ => raise ex
789 end 896 end
790 897
791 and unifyCons' (env, denv) c1 c2 = 898 and unifyCons' (env, denv) c1 c2 =
792 let 899 let
793 val (c1, gs1) = hnormCon (env, denv) c1 900 val (c1, gs1) = hnormCon (env, denv) c1
796 let 903 let
797 val gs3 = unifyCons'' (env, denv) c1 c2 904 val gs3 = unifyCons'' (env, denv) c1 c2
798 in 905 in
799 gs1 @ gs2 @ gs3 906 gs1 @ gs2 @ gs3
800 end 907 end
801 handle ex => 908 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
802 let
803 val loc = #2 c1
804
805 fun unfold (dom, f, i, r, c) =
806 let
807 val nm = cunif (loc, (L'.KName, loc))
808 val v = cunif (loc, dom)
809 val rest = cunif (loc, (L'.KRecord dom, loc))
810
811 val (iS, gs3) = summarizeCon (env, denv) i
812
813 val app = (L'.CApp (f, nm), loc)
814 val app = (L'.CApp (app, v), loc)
815 val app = (L'.CApp (app, rest), loc)
816 val (appS, gs4) = summarizeCon (env, denv) app
817
818 val (cS, gs5) = summarizeCon (env, denv) c
819 in
820 (*prefaces "Summaries" [("iS", p_con_summary iS),
821 ("appS", p_con_summary appS),
822 ("cS", p_con_summary cS)];*)
823
824 if compatible (iS, appS) then
825 raise ex
826 else if compatible (cS, iS) then
827 let
828 (*val () = prefaces "Same?" [("i", p_con env i),
829 ("c", p_con env c)]*)
830 val gs6 = unifyCons (env, denv) i c
831 (*val () = TextIO.print "Yes!\n"*)
832
833 val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
834 in
835 gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
836 end
837 else if compatible (cS, appS) then
838 let
839 (*val () = prefaces "Same?" [("app", p_con env app),
840 ("c", p_con env c),
841 ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
842 val gs6 = unifyCons (env, denv) app c
843 (*val () = TextIO.print "Yes!\n"*)
844
845 val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
846 val concat = (L'.CConcat (singleton, rest), loc)
847 val gs7 = unifyCons (env, denv) r concat
848 in
849 gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
850 end
851 else
852 raise ex
853 end
854 handle _ => raise ex
855 in
856 case (#1 c1, #1 c2) of
857 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, _), _), f), _), i), _), r), _) =>
858 unfold (dom, f, i, r, c2)
859 | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, _), _), f), _), i), _), r)) =>
860 unfold (dom, f, i, r, c1)
861 | _ => raise ex
862 end
863 end 909 end
864 910
865 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = 911 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
866 let 912 let
867 fun err f = raise CUnify' (f (c1All, c2All)) 913 fun err f = raise CUnify' (f (c1All, c2All))