Mercurial > urweb

comparison src/elaborate.sml @ 647:ae374df5ccbd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prose for ListEdit
author Adam Chlipala <adamc@hcoop.net>
date Tue, 10 Mar 2009 13:46:45 -0400
parents fb2a0e76dcef
children fab5998b840e
comparison
equal deleted inserted replaced
646:fb2a0e76dcef 647:ae374df5ccbd
704 (#fields s1, #fields s2) 704 (#fields s1, #fields s2)
705 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}), 705 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
706 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*) 706 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
707 707
708 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) 708 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
709 fun eatMost unifs =
710 case unifs of
711 (_, r) :: (rest as _ :: _) => (r := SOME (L'.CRecord (k, []), loc);
712 eatMost rest)
713 | _ => unifs
714 val unifs1 = eatMost unifs1
715 val unifs2 = eatMost unifs2
716 709
717 val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2) 710 val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2)
718 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), 711 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
719 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) 712 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
720 713
885 878
886 case (c1, c2) of 879 case (c1, c2) of
887 (L'.CError, _) => () 880 (L'.CError, _) => ()
888 | (_, L'.CError) => () 881 | (_, L'.CError) => ()
889 882
883 | (L'.CRecord _, _) => isRecord ()
884 | (_, L'.CRecord _) => isRecord ()
885 | (L'.CConcat _, _) => isRecord ()
886 | (_, L'.CConcat _) => isRecord ()
887
890 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => 888 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
891 if r1 = r2 then 889 if r1 = r2 then
892 () 890 ()
893 else 891 else
894 (unifyKinds env k1 k2; 892 (unifyKinds env k1 k2;
1031 | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) => 1029 | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) =>
1032 (unifyKinds env k1 k2; 1030 (unifyKinds env k1 k2;
1033 unifyCons' env c1 c2) 1031 unifyCons' env c1 c2)
1034 | (L'.TKFun (x, c1), L'.TKFun (_, c2)) => 1032 | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
1035 unifyCons' (E.pushKRel env x) c1 c2 1033 unifyCons' (E.pushKRel env x) c1 c2
1036
1037 | (L'.CRecord _, _) => isRecord ()
1038 | (_, L'.CRecord _) => isRecord ()
1039 | (L'.CConcat _, _) => isRecord ()
1040 | (_, L'.CConcat _) => isRecord ()
1041 1034
1042 | _ => err CIncompatible 1035 | _ => err CIncompatible
1043 end 1036 end
1044 1037
1045 and unifyCons env c1 c2 = 1038 and unifyCons env c1 c2 =