From ab0bbbf29220a995f6fa83ae43e0a4a88c9b5159 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 7 Apr 2009 18:47:47 -0400
Subject: FOREIGN KEY, without ability to link NULL to NOT NULL (and with some
 lingering problems in row inference)

---
 src/elaborate.sml | 92 +++++++++++++++++++++++++++++++++++++++----------------
 1 file changed, 66 insertions(+), 26 deletions(-)

(limited to 'src/elaborate.sml')

diff --git a/src/elaborate.sml b/src/elaborate.sml
index c2ac31a4..4971ec4c 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -463,7 +463,10 @@
        | _ => false
  fun cunifsRemain c =
      case c of
-         L'.CUnif (loc, _, _, ref NONE) => SOME loc
+         L'.CUnif (loc, (L'.KRecord k, _), _, r as ref NONE) =>
+         (r := SOME (L'.CRecord (k, []), loc);
+          NONE)
+       | L'.CUnif (loc, _, _, ref NONE) => SOME loc
        | _ => NONE
 
  val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
@@ -618,6 +621,8 @@
        | L'.CKApp _ => false
        | L'.TKFun _ => false
 
+ val recdCounter = ref 0
+
  fun unifyRecordCons env (c1, c2) =
      let
          fun rkindof c =
@@ -711,6 +716,41 @@
          (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
                                           ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
 
+         fun unsummarize {fields, unifs, others} =
+             let
+                 val c = (L'.CRecord (k, fields), loc)
+
+                 val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
+                               c unifs
+             in
+                 foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
+                       c others
+             end
+
+         val (unifs1, fs1, others1, unifs2, fs2, others2) =
+             case (unifs1, fs1, others1, unifs2, fs2, others2) of
+                 orig as ([(_, r)], [], [], _, _, _) =>
+                 let
+                     val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
+                 in
+                     if occursCon r c then
+                         orig
+                     else
+                         (r := SOME c;
+                          ([], [], [], [], [], []))
+                 end
+               | orig as (_, _, _, [(_, r)], [], []) =>
+                 let
+                     val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
+                 in
+                     if occursCon r c then
+                         orig
+                     else
+                         (r := SOME c;
+                          ([], [], [], [], [], []))
+                 end
+               | orig => orig
+
          fun unifFields (fs, others, unifs) =
              case (fs, others, unifs) of
                  ([], [], _) => ([], [], unifs)
@@ -719,7 +759,8 @@
                  let
                      val r' = ref NONE
                      val kr = (L'.KRecord k, dummy)
-                     val cr' = (L'.CUnif (dummy, kr, "recd", r'), dummy)
+                     val cr' = (L'.CUnif (dummy, kr, ("recd" ^ Int.toString (!recdCounter)), r'), dummy)
+                     val () = recdCounter := 1 + !recdCounter
 
                      val prefix = case (fs, others) of
                                       ([], other :: others) =>
@@ -762,6 +803,8 @@
                      (fs1, fs2, others1, others2)
                | _ => (fs1, fs2, others1, others2)
 
+         val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (unifs1, unifs2)
+
          (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
                                           ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
 
@@ -770,34 +813,31 @@
                         | _ => false
          val empty = (L'.CRecord (k, []), dummy)
 
-         fun unsummarize {fields, unifs, others} =
+         fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
+     in
+         case (unifs1, fs1, others1, unifs2, fs2, others2) of
+             ([(_, r)], [], [], _, _, _) =>
              let
-                 val c = (L'.CRecord (k, fields), loc)
-
-                 val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
-                               c unifs
+                 val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
              in
-                 foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
-                       c others
-             end
-
-         fun pairOffUnifs (unifs1, unifs2) =
-             case (unifs1, unifs2) of
-                 ([], _) =>
-                 if clear then
-                     List.app (fn (_, r) => r := SOME empty) unifs2
+                 if occursCon r c then
+                     failure ()
                  else
-                     raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
-               | (_, []) =>
-                 if clear then
-                     List.app (fn (_, r) => r := SOME empty) unifs1
+                     r := SOME c
+             end
+           | (_, _, _, [(_, r)], [], []) =>
+             let
+                 val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
+             in
+                 if occursCon r c then
+                     failure ()
                  else
-                     raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
-               | ((c1, _) :: rest1, (_, r2) :: rest2) =>
-                 (r2 := SOME c1;
-                  pairOffUnifs (rest1, rest2))
-     in
-         pairOffUnifs (unifs1, unifs2)
+                     r := SOME c
+             end
+           | _ => if clear then
+                      ()
+                  else
+                      failure ()
          (*before eprefaces "Summaries'" [("#1", p_summary env s1),
                                        ("#2", p_summary env s2)]*)
      end
-- 
cgit v1.2.3