From 8fce558858a4a8efffc735239dacba6af6594826 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Wed, 15 Dec 2010 09:37:36 -0500
Subject: Smarter record unification

---
 src/elaborate.sml | 49 ++++++++++++++++++++++++++++++++++++++-----------
 1 file 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,
-- 
cgit v1.2.3