changeset 712:915ec60592d4

More flexible foreign keying
author Adam Chlipala <adamc@hcoop.net>
date Thu, 09 Apr 2009 13:59:34 -0400
parents 7292bcb7c02d
children baaae037e7f6
files lib/ur/basis.urs src/elab_err.sml src/elaborate.sml src/monoize.sml src/urweb.grm tests/cst.ur
diffstat 6 files changed, 53 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/lib/ur/basis.urs	Thu Apr 09 12:31:56 2009 -0400
+++ b/lib/ur/basis.urs	Thu Apr 09 13:59:34 2009 -0400
@@ -166,13 +166,19 @@
              -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
     => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
 
+class linkable :: Type -> Type -> Type
+val linkable_same : t ::: Type -> linkable t t
+val linkable_from_nullable : t ::: Type -> linkable (option t) t
+val linkable_to_nullable : t ::: Type -> linkable t (option t)
+
 con matching :: {Type} -> {Type} -> Type
 val mat_nil : matching [] []
-val mat_cons : t ::: Type -> rest1 ::: {Type} -> rest2 ::: {Type}
+val mat_cons : t1 ::: Type -> rest1 ::: {Type} -> t2 ::: Type -> rest2 ::: {Type}
                -> nm1 :: Name -> nm2 :: Name
                -> [[nm1] ~ rest1] => [[nm2] ~ rest2]
-    => matching rest1 rest2
-       -> matching ([nm1 = t] ++ rest1) ([nm2 = t] ++ rest2)
+    => linkable t1 t2
+       -> matching rest1 rest2
+       -> matching ([nm1 = t1] ++ rest1) ([nm2 = t2] ++ rest2)
 
 con propagation_mode :: {Type} -> Type
 val restrict : fs ::: {Type} -> propagation_mode fs
--- a/src/elab_err.sml	Thu Apr 09 12:31:56 2009 -0400
+++ b/src/elab_err.sml	Thu Apr 09 13:59:34 2009 -0400
@@ -217,7 +217,7 @@
                                               ("Type", p_con env c)]) co)
       | Unresolvable (loc, c) =>
         (ErrorMsg.errorAt loc "Can't resolve type class instance";
-         eprefaces' [("Class constraint", p_con env c),
+         eprefaces' [("Class constraint", p_con env c)(*,
                      ("Class database", p_list (fn (c, rules) =>
                                                    box [P.p_con env c,
                                                         PD.string ":",
@@ -227,7 +227,7 @@
                                                                         PD.string ":",
                                                                         space,
                                                                         P.p_con env c]) rules])
-                                        (E.listClasses env))])
+                                        (E.listClasses env))*)])
       | IllegalRec (x, e) =>
         (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
          eprefaces' [("Variable", PD.string x),
--- a/src/elaborate.sml	Thu Apr 09 12:31:56 2009 -0400
+++ b/src/elaborate.sml	Thu Apr 09 13:59:34 2009 -0400
@@ -170,7 +170,7 @@
  fun cunif (loc, k) =
      let
          val n = !count
-         val s = if n <= 26 then
+         val s = if n < 26 then
                      str (chr (ord #"A" + n))
                  else
                      "U" ^ Int.toString (n - 26)
--- a/src/monoize.sml	Thu Apr 09 12:31:56 2009 -0400
+++ b/src/monoize.sml	Thu Apr 09 13:59:34 2009 -0400
@@ -155,6 +155,8 @@
                     (L'.TFfi ("Basis", "sql_constraints"), loc)
                   | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_constraint"), _), _), _), _) =>
                     (L'.TFfi ("Basis", "string"), loc)
+                  | L.CApp ((L.CApp ((L.CFfi ("Basis", "linkable"), _), _), _), _) =>
+                    (L'.TRecord [], loc)
                   | L.CApp ((L.CApp ((L.CFfi ("Basis", "matching"), _), _), _), _) =>
                     let
                         val string = (L'.TFfi ("Basis", "string"), loc)
@@ -1226,6 +1228,13 @@
                  fm)
             end
 
+          | L.ECApp ((L.EFfi ("Basis", "linkable_same"), loc), _) =>
+            ((L'.ERecord [], loc), fm)
+          | L.ECApp ((L.EFfi ("Basis", "linkable_from_nullable"), loc), _) =>
+            ((L'.ERecord [], loc), fm)
+          | L.ECApp ((L.EFfi ("Basis", "linkable_to_nullable"), loc), _) =>
+            ((L'.ERecord [], loc), fm)
+
           | L.EFfi ("Basis", "mat_nil") =>
             let
                 val string = (L'.TFfi ("Basis", "string"), loc)
@@ -1239,7 +1248,9 @@
              (L.ECApp (
               (L.ECApp (
                (L.ECApp (
-                (L.EFfi ("Basis", "mat_cons"), _),
+                (L.ECApp (
+                 (L.EFfi ("Basis", "mat_cons"), _),
+                 _), _),
                 _), _),
                _), _),
               _), _),
@@ -1249,21 +1260,27 @@
                 val string = (L'.TFfi ("Basis", "string"), loc)
                 val mat = (L'.TRecord [("1", string), ("2", string)], loc)
             in
-                ((L'.EAbs ("m", mat, mat,
-                           (L'.ECase ((L'.EField ((L'.ERel 0, loc), "1"), loc),
-                                      [((L'.PPrim (Prim.String ""), loc),
-                                        (L'.ERecord [("1", (L'.EPrim (Prim.String ("uw_" ^ nm1)), loc), string),
-                                                     ("2", (L'.EPrim (Prim.String ("uw_" ^ nm2)), loc), string)], loc)),
-                                       ((L'.PWild, loc),
-                                        (L'.ERecord [("1", (L'.EStrcat (
-                                                            (L'.EPrim (Prim.String ("uw_" ^ nm1 ^ ", ")), loc),
-                                                            (L'.EField ((L'.ERel 0, loc), "1"), loc)), loc), string),
-                                                     ("2", (L'.EStrcat (
-                                                            (L'.EPrim (Prim.String ("uw_" ^ nm2 ^ ", ")), loc),
-                                                            (L'.EField ((L'.ERel 0, loc), "2"), loc)), loc), string)],
-                                         loc))],
-                                      {disc = string,
-                                       result = mat}), loc)), loc),
+                ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun (mat, mat), loc),
+                           (L'.EAbs ("m", mat, mat,
+                                     (L'.ECase ((L'.EField ((L'.ERel 0, loc), "1"), loc),
+                                                [((L'.PPrim (Prim.String ""), loc),
+                                                  (L'.ERecord [("1", (L'.EPrim (Prim.String ("uw_" ^ nm1)),
+                                                                      loc), string),
+                                                               ("2", (L'.EPrim (Prim.String ("uw_" ^ nm2)),
+                                                                      loc), string)], loc)),
+                                                 ((L'.PWild, loc),
+                                                  (L'.ERecord [("1", (L'.EStrcat (
+                                                                      (L'.EPrim (Prim.String ("uw_" ^ nm1 ^ ", ")),
+                                                                       loc),
+                                                                      (L'.EField ((L'.ERel 0, loc), "1"), loc)),
+                                                                      loc), string),
+                                                               ("2", (L'.EStrcat (
+                                                                      (L'.EPrim (Prim.String ("uw_" ^ nm2 ^ ", ")), loc),
+                                                                      (L'.EField ((L'.ERel 0, loc), "2"), loc)),
+                                                                      loc), string)],
+                                                   loc))],
+                                                {disc = string,
+                                                 result = mat}), loc)), loc)), loc),
                  fm)
             end
 
--- a/src/urweb.grm	Thu Apr 09 12:31:56 2009 -0400
+++ b/src/urweb.grm	Thu Apr 09 13:59:34 2009 -0400
@@ -523,6 +523,7 @@
                                                                val e = (ECApp (e, nm2), loc)
                                                                val e = (EDisjointApp e, loc)
                                                                val e = (EDisjointApp e, loc)
+                                                               val e = (EApp (e, (EWild, loc)), loc)
                                                            in
                                                                (EApp (e, mat), loc)
                                                            end)
--- a/tests/cst.ur	Thu Apr 09 12:31:56 2009 -0400
+++ b/tests/cst.ur	Thu Apr 09 13:59:34 2009 -0400
@@ -1,8 +1,9 @@
-table u : {C : int, D : int, E : int}
+table u : {C : int, D : int, E : option int}
   PRIMARY KEY C,
-  CONSTRAINT U UNIQUE (C, D)
+  CONSTRAINT U UNIQUE (C, D),
+  CONSTRAINT U2 UNIQUE E
 
-table t : {A : int, B : int}
+table t : {A : int, B : int, C : option int}
   PRIMARY KEY B,
 
   CONSTRAINT UniA UNIQUE A,
@@ -20,8 +21,10 @@
   CONSTRAINT ForA FOREIGN KEY A REFERENCES u (C),
   CONSTRAINT ForAB FOREIGN KEY (A, B) REFERENCES u (D, C) ON DELETE CASCADE ON UPDATE RESTRICT,
   CONSTRAINT ForBA FOREIGN KEY (A, B) REFERENCES u (C, D) ON UPDATE NO ACTION,
+  CONSTRAINT ForB FOREIGN KEY B REFERENCES u (E),
+  CONSTRAINT ForC FOREIGN KEY C REFERENCES u (C)
 
-  CONSTRAINT Self FOREIGN KEY B REFERENCES t (B)
+  (*CONSTRAINT Self FOREIGN KEY B REFERENCES t (B)*)
 
 table s : {B : option int}
   CONSTRAINT UniB UNIQUE B