Mercurial > urweb
changeset 1341:91eaa1542c5a
Smarter record unification
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 15 Dec 2010 09:37:36 -0500 |
parents | caff0a4d5fc1 |
children | 78fe9841c39d |
files | src/elaborate.sml |
diffstat | 1 files changed, 38 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Tue Dec 14 10:59:17 2010 -0500 +++ b/src/elaborate.sml Wed Dec 15 09:37:36 2010 -0500 @@ -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 @@ ("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,