Mercurial > urweb

comparison src/elaborate.sml @ 1341:91eaa1542c5a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Smarter record unification
author Adam Chlipala <adam@chlipala.net>
date Wed, 15 Dec 2010 09:37:36 -0500
parents d91f84599693
children 9e0fa4f6ac93
comparison
equal deleted inserted replaced
1340:caff0a4d5fc1 1341:91eaa1542c5a
908 else 908 else
909 SOME (nm1, c1, c2) 909 SOME (nm1, c1, c2)
910 in 910 in
911 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1))) 911 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1)))
912 end 912 end
913
914 fun default () = if !mayDelay then
915 delayedUnifs := (loc, env, k, s1, s2) :: !delayedUnifs
916 else
917 failure ()
913 in 918 in
914 (case (unifs1, fs1, others1, unifs2, fs2, others2) of 919 (case (unifs1, fs1, others1, unifs2, fs2, others2) of
915 (_, [], [], [], [], []) => 920 (_, [], [], [], [], []) =>
916 app (fn (_, r) => r := SOME empty) unifs1 921 app (fn (_, r) => r := SOME empty) unifs1
917 | ([], [], [], _, [], []) => 922 | ([], [], [], _, [], []) =>
918 app (fn (_, r) => r := SOME empty) unifs2 923 app (fn (_, r) => r := SOME empty) unifs2
919 | _ => 924 | (_, _, _, [], [], [cr as (L'.CUnif (nl, _, _, _, r), _)]) =>
920 if !mayDelay then 925 let
921 delayedUnifs := (loc, env, k, s1, s2) :: !delayedUnifs 926 val c = summaryToCon {fields = fs1, unifs = unifs1, others = others1}
922 else 927 in
923 failure ()) 928 if occursCon r c then
924 929 raise CUnify' (COccursCheckFailed (cr, c))
930 else
931 (r := SOME (squish nl c))
932 handle CantSquish => default ()
933 end
934 | ([], [], [cr as (L'.CUnif (nl, _, _, _, r), _)], _, _, _) =>
935 let
936 val c = summaryToCon {fields = fs2, unifs = unifs2, others = others2}
937 in
938 if occursCon r c then
939 raise CUnify' (COccursCheckFailed (cr, c))
940 else
941 (r := SOME (squish nl c))
942 handle CantSquish => default ()
943 end
944 | _ => default ())
945
925 (*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)), 946 (*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)),
926 ("#2", p_summary env (normalizeRecordSummary env s2))]*) 947 ("#2", p_summary env (normalizeRecordSummary env s2))]*)
927 end 948 end
928 949
929 and guessMap env loc (c1, c2, ex) = 950 and guessMap env loc (c1, c2, ex) =
1066 1087
1067 case (c1, c2) of 1088 case (c1, c2) of
1068 (L'.CError, _) => () 1089 (L'.CError, _) => ()
1069 | (_, L'.CError) => () 1090 | (_, L'.CError) => ()
1070 1091
1071 | (L'.CRecord _, _) => isRecord ()
1072 | (_, L'.CRecord _) => isRecord ()
1073 | (L'.CConcat _, _) => isRecord ()
1074 | (_, L'.CConcat _) => isRecord ()
1075
1076 | (L'.CUnif (nl1, loc1, k1, _, r1), L'.CUnif (nl2, loc2, k2, _, r2)) => 1092 | (L'.CUnif (nl1, loc1, k1, _, r1), L'.CUnif (nl2, loc2, k2, _, r2)) =>
1077 if r1 = r2 andalso nl1 = nl2 then 1093 if r1 = r2 andalso nl1 = nl2 then
1078 () 1094 ()
1079 else if nl1 = 0 then 1095 else if nl1 = 0 then
1080 (unifyKinds env k1 k2; 1096 (unifyKinds env k1 k2;
1106 if occursCon r c1All then 1122 if occursCon r c1All then
1107 err COccursCheckFailed 1123 err COccursCheckFailed
1108 else 1124 else
1109 (r := SOME (squish nl c1All) 1125 (r := SOME (squish nl c1All)
1110 handle CantSquish => err (fn _ => TooDeep)) 1126 handle CantSquish => err (fn _ => TooDeep))
1127
1128 | (L'.CRecord _, _) => isRecord ()
1129 | (_, L'.CRecord _) => isRecord ()
1130 | (L'.CConcat _, _) => isRecord ()
1131 | (_, L'.CConcat _) => isRecord ()
1132
1111 1133
1112 | (L'.CUnit, L'.CUnit) => () 1134 | (L'.CUnit, L'.CUnit) => ()
1113 1135
1114 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => 1136 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
1115 (unifyCons' env loc d1 d2; 1137 (unifyCons' env loc d1 d2;
4366 eprefaces' [("Con 1", p_con env c1), 4388 eprefaces' [("Con 1", p_con env c1),
4367 ("Con 2", p_con env c2), 4389 ("Con 2", p_con env c2),
4368 ("Hnormed 1", p_con env c1'), 4390 ("Hnormed 1", p_con env c1'),
4369 ("Hnormed 2", p_con env c2')]; 4391 ("Hnormed 2", p_con env c2')];
4370 4392
4393 app (fn (loc, env, k, s1, s2) =>
4394 eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)),
4395 ("s2", p_summary env (normalizeRecordSummary env s2))])
4396 (!delayedUnifs);
4397
4371 if (isUnif c1' andalso maybeAttr c2') 4398 if (isUnif c1' andalso maybeAttr c2')
4372 orelse (isUnif c2' andalso maybeAttr c1') then 4399 orelse (isUnif c2' andalso maybeAttr c1') then
4373 TextIO.output (TextIO.stdErr, 4400 TextIO.output (TextIO.stdErr,
4374 "You may be using a disallowed attribute with an HTML tag.\n") 4401 "You may be using a disallowed attribute with an HTML tag.\n")
4375 else 4402 else