summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-12-15 09:37:36 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2010-12-15 09:37:36 -0500
commite98bdae0deba734c2bd2f8ee04922098386ce5d1 (patch)
tree547496dbb5817dc3952fc7c16a2b577d900804b0 /src
parent8b95e4da5cc8932be6d1f1b57d432be1b6a0b56b (diff)
Smarter record unification
Diffstat (limited to 'src')
-rw-r--r--src/elaborate.sml49
1 files changed, 38 insertions, 11 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index a28d3bf4..3134c3d4 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -910,18 +910,39 @@
in
raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1)))
end
+
+ fun default () = if !mayDelay then
+ delayedUnifs := (loc, env, k, s1, s2) :: !delayedUnifs
+ else
+ failure ()
in
(case (unifs1, fs1, others1, unifs2, fs2, others2) of
(_, [], [], [], [], []) =>
app (fn (_, r) => r := SOME empty) unifs1
| ([], [], [], _, [], []) =>
app (fn (_, r) => r := SOME empty) unifs2
- | _ =>
- if !mayDelay then
- delayedUnifs := (loc, env, k, s1, s2) :: !delayedUnifs
- else
- failure ())
-
+ | (_, _, _, [], [], [cr as (L'.CUnif (nl, _, _, _, r), _)]) =>
+ let
+ val c = summaryToCon {fields = fs1, unifs = unifs1, others = others1}
+ in
+ if occursCon r c then
+ raise CUnify' (COccursCheckFailed (cr, c))
+ else
+ (r := SOME (squish nl c))
+ handle CantSquish => default ()
+ end
+ | ([], [], [cr as (L'.CUnif (nl, _, _, _, r), _)], _, _, _) =>
+ let
+ val c = summaryToCon {fields = fs2, unifs = unifs2, others = others2}
+ in
+ if occursCon r c then
+ raise CUnify' (COccursCheckFailed (cr, c))
+ else
+ (r := SOME (squish nl c))
+ handle CantSquish => default ()
+ end
+ | _ => default ())
+
(*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)),
("#2", p_summary env (normalizeRecordSummary env s2))]*)
end
@@ -1068,11 +1089,6 @@
(L'.CError, _) => ()
| (_, L'.CError) => ()
- | (L'.CRecord _, _) => isRecord ()
- | (_, L'.CRecord _) => isRecord ()
- | (L'.CConcat _, _) => isRecord ()
- | (_, L'.CConcat _) => isRecord ()
-
| (L'.CUnif (nl1, loc1, k1, _, r1), L'.CUnif (nl2, loc2, k2, _, r2)) =>
if r1 = r2 andalso nl1 = nl2 then
()
@@ -1109,6 +1125,12 @@
(r := SOME (squish nl c1All)
handle CantSquish => err (fn _ => TooDeep))
+ | (L'.CRecord _, _) => isRecord ()
+ | (_, L'.CRecord _) => isRecord ()
+ | (L'.CConcat _, _) => isRecord ()
+ | (_, L'.CConcat _) => isRecord ()
+
+
| (L'.CUnit, L'.CUnit) => ()
| (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
@@ -4368,6 +4390,11 @@ fun elabFile basis topStr topSgn env file =
("Hnormed 1", p_con env c1'),
("Hnormed 2", p_con env c2')];
+ app (fn (loc, env, k, s1, s2) =>
+ eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)),
+ ("s2", p_summary env (normalizeRecordSummary env s2))])
+ (!delayedUnifs);
+
if (isUnif c1' andalso maybeAttr c2')
orelse (isUnif c2' andalso maybeAttr c1') then
TextIO.output (TextIO.stdErr,