Mercurial > urweb

comparison src/elaborate.sml @ 710:71409a4ccb67

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Get demo type-inferring again
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 20:38:01 -0400
parents 0406e9cccb72
children 7292bcb7c02d
comparison
equal deleted inserted replaced
709:0406e9cccb72 710:71409a4ccb67
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, (L'.KRecord k, _), _, r as ref NONE) => 466 L'.CUnif (loc, _, _, ref NONE) => SOME loc
467 (r := SOME (L'.CRecord (k, []), loc);
468 NONE)
469 | L'.CUnif (loc, _, _, ref NONE) => SOME loc
470 | _ => NONE 467 | _ => NONE
471 468
472 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain, 469 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
473 con = fn _ => false, 470 con = fn _ => false,
474 exp = fn _ => false, 471 exp = fn _ => false,
725 in 722 in
726 foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc)) 723 foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
727 c others 724 c others
728 end 725 end
729 726
727 val empties = ([], [], [], [], [], [])
728
730 val (unifs1, fs1, others1, unifs2, fs2, others2) = 729 val (unifs1, fs1, others1, unifs2, fs2, others2) =
731 case (unifs1, fs1, others1, unifs2, fs2, others2) of 730 case (unifs1, fs1, others1, unifs2, fs2, others2) of
732 orig as ([(_, r)], [], [], _, _, _) => 731 orig as ([(_, r)], [], [], _, _, _) =>
733 let 732 let
734 val c = unsummarize {fields = fs2, others = others2, unifs = unifs2} 733 val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
735 in 734 in
736 if occursCon r c then 735 if occursCon r c then
737 orig 736 orig
738 else 737 else
739 (r := SOME c; 738 (r := SOME c;
740 ([], [], [], [], [], [])) 739 empties)
741 end 740 end
742 | orig as (_, _, _, [(_, r)], [], []) => 741 | orig as (_, _, _, [(_, r)], [], []) =>
743 let 742 let
744 val c = unsummarize {fields = fs1, others = others1, unifs = unifs1} 743 val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
745 in 744 in
746 if occursCon r c then 745 if occursCon r c then
747 orig 746 orig
748 else 747 else
749 (r := SOME c; 748 (r := SOME c;
750 ([], [], [], [], [], [])) 749 empties)
751 end 750 end
751 | orig as ([(_, r1 as ref NONE)], _, [], [(_, r2 as ref NONE)], _, []) =>
752 if List.all (fn (x1, _) => List.all (fn (x2, _) => consNeq env (x1, x2)) fs2) fs1 then
753 let
754 val kr = (L'.KRecord k, dummy)
755 val u = cunif (loc, kr)
756 in
757 r1 := SOME (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc);
758 r2 := SOME (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc);
759 empties
760 end
761 else
762 orig
752 | orig => orig 763 | orig => orig
753 764
754 fun unifFields (fs, others, unifs) =
755 case (fs, others, unifs) of
756 ([], [], _) => ([], [], unifs)
757 | (_, _, []) => (fs, others, [])
758 | (_, _, (_, r) :: rest) =>
759 let
760 val r' = ref NONE
761 val kr = (L'.KRecord k, dummy)
762 val cr' = (L'.CUnif (dummy, kr, ("recd" ^ Int.toString (!recdCounter)), r'), dummy)
763 val () = recdCounter := 1 + !recdCounter
764
765 val prefix = case (fs, others) of
766 ([], other :: others) =>
767 List.foldl (fn (other, c) =>
768 (L'.CConcat (c, other), dummy))
769 other others
770 | (fs, []) =>
771 (L'.CRecord (k, fs), dummy)
772 | (fs, others) =>
773 List.foldl (fn (other, c) =>
774 (L'.CConcat (c, other), dummy))
775 (L'.CRecord (k, fs), dummy) others
776 in
777 r := SOME (L'.CConcat (prefix, cr'), dummy);
778 ([], [], (cr', r') :: rest)
779 end
780
781 val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
782 val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
783
784 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 765 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
785 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 766 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
786 767
787 fun isGuessable (other, fs) = 768 fun isGuessable (other, fs) =
788 (guessMap env (other, (L'.CRecord (k, fs), loc), GuessFailure); 769 (guessMap env (other, (L'.CRecord (k, fs), loc), GuessFailure);
789 true) 770 true)
790 handle GuessFailure => false 771 handle GuessFailure => false
801 ([], [], [], []) 782 ([], [], [], [])
802 else 783 else
803 (fs1, fs2, others1, others2) 784 (fs1, fs2, others1, others2)
804 | _ => (fs1, fs2, others1, others2) 785 | _ => (fs1, fs2, others1, others2)
805 786
806 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (unifs1, unifs2)
807
808 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 787 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
809 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 788 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
810 789
811 val clear = case (fs1, others1, fs2, others2) of 790 val clear = case (fs1, others1, fs2, others2) of
812 ([], [], [], []) => true 791 ([], [], [], []) => true
813 | _ => false 792 | _ => false
814 val empty = (L'.CRecord (k, []), dummy) 793 val empty = (L'.CRecord (k, []), dummy)
815
816 fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
817 in 794 in
818 case (unifs1, fs1, others1, unifs2, fs2, others2) of 795 case (unifs1, fs1, others1, unifs2, fs2, others2) of
819 ([(_, r)], [], [], _, _, _) => 796 (_, [], [], [], [], []) =>
820 let 797 app (fn (_, r) => r := SOME empty) unifs1
821 val c = unsummarize {fields = fs2, others = others2, unifs = unifs2} 798 | ([], [], [], _, [], []) =>
822 in 799 app (fn (_, r) => r := SOME empty) unifs2
823 if occursCon r c then
824 failure ()
825 else
826 r := SOME c
827 end
828 | (_, _, _, [(_, r)], [], []) =>
829 let
830 val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
831 in
832 if occursCon r c then
833 failure ()
834 else
835 r := SOME c
836 end
837 | _ => if clear then 800 | _ => if clear then
838 () 801 ()
839 else 802 else
840 failure () 803 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
841 (*before eprefaces "Summaries'" [("#1", p_summary env s1), 804 (*before eprefaces "Summaries'" [("#1", p_summary env s1),
842 ("#2", p_summary env s2)]*) 805 ("#2", p_summary env s2)]*)
843 end 806 end
844 807
845 and guessMap env (c1, c2, ex) = 808 and guessMap env (c1, c2, ex) =