Mercurial > urweb

comparison src/elaborate.sml @ 348:b88f4297167f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Improved inference of records of tuples
author Adam Chlipala <adamc@hcoop.net>
date Sat, 04 Oct 2008 19:56:59 -0400
parents b85e6ba56618
children beb72f8a7218
comparison
equal deleted inserted replaced
347:58eeeb3cbf40 348:b88f4297167f
687 ([], _, [other1], []) => 687 ([], _, [other1], []) =>
688 if isGuessable (other1, fs2) then 688 if isGuessable (other1, fs2) then
689 ([], [], [], []) 689 ([], [], [], [])
690 else 690 else
691 (fs1, fs2, others1, others2) 691 (fs1, fs2, others1, others2)
692 | (_, [], [], [other2]) =>
693 if isGuessable (other2, fs1) then
694 ([], [], [], [])
695 else
696 (fs1, fs2, others1, others2)
692 | _ => (fs1, fs2, others1, others2) 697 | _ => (fs1, fs2, others1, others2)
693 698
694 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 699 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
695 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 700 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
696 701
697 val clear = case (fs1, others1, fs2, others2) of 702 val clear = case (fs1, others1, fs2, others2) of
698 ([], [], [], []) => true 703 ([], [], [], []) => true
699 | _ => false 704 | _ => false
700 val empty = (L'.CRecord (k, []), dummy) 705 val empty = (L'.CRecord (k, []), dummy)
887 val gs' = unifyCons' (env, denv) c1 c2 892 val gs' = unifyCons' (env, denv) c1 c2
888 in 893 in
889 gs' @ gs 894 gs' @ gs
890 end) [] (cs1, cs2)) 895 end) [] (cs1, cs2))
891 handle ListPair.UnequalLengths => err CIncompatible) 896 handle ListPair.UnequalLengths => err CIncompatible)
897
898 | (L'.CProj ((L'.CUnif (_, _, _, ref (SOME c1)), loc), n1), _) =>
899 unifyCons' (env, denv) (L'.CProj (c1, n1), loc) c2All
900 | (_, L'.CProj ((L'.CUnif (_, _, _, ref (SOME c2)), loc), n2)) =>
901 unifyCons' (env, denv) c1All (L'.CProj (c2, n2), loc)
902 | (L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n), _) =>
903 let
904 val us = map (fn k => cunif (loc, k)) ks
905 in
906 r := SOME (L'.CTuple us, loc);
907 unifyCons' (env, denv) (List.nth (us, n - 1)) c2All
908 end
909 | (_, L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n)) =>
910 let
911 val us = map (fn k => cunif (loc, k)) ks
912 in
913 r := SOME (L'.CTuple us, loc);
914 unifyCons' (env, denv) c1All (List.nth (us, n - 1))
915 end
892 | (L'.CProj (c1, n1), L'.CProj (c2, n2)) => 916 | (L'.CProj (c1, n1), L'.CProj (c2, n2)) =>
893 if n1 = n2 then 917 if n1 = n2 then
894 unifyCons' (env, denv) c1 c2 918 unifyCons' (env, denv) c1 c2
895 else 919 else
896 err CIncompatible 920 err CIncompatible