changeset 709:0406e9cccb72

FOREIGN KEY, without ability to link NULL to NOT NULL (and with some lingering problems in row inference)
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 18:47:47 -0400
parents 1a317a707d71
children 71409a4ccb67
files demo/broadcast.ur lib/ur/basis.urs src/disjoint.sml src/elaborate.sml src/elisp/urweb-mode.el src/monoize.sml src/urweb.grm src/urweb.lex tests/cst.ur
diffstat 9 files changed, 300 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/demo/broadcast.ur	Tue Apr 07 16:22:11 2009 -0400
+++ b/demo/broadcast.ur	Tue Apr 07 18:47:47 2009 -0400
@@ -1,7 +1,7 @@
 functor Make(M : sig type t end) = struct
     sequence s
     table t : {Id : int, Client : client, Channel : channel M.t}
-      PRIMARY KEY Id
+      PRIMARY KEY (Id, Client)
 
     type topic = int
 
--- a/lib/ur/basis.urs	Tue Apr 07 16:22:11 2009 -0400
+++ b/lib/ur/basis.urs	Tue Apr 07 18:47:47 2009 -0400
@@ -161,10 +161,37 @@
     => sql_constraints fs uniques1 -> sql_constraints fs uniques2
        -> sql_constraints fs (uniques1 ++ uniques2)
 
+
 val unique : rest ::: {Type} -> t ::: Type -> unique1 :: Name -> unique :: {Type}
              -> [[unique1] ~ unique] => [[unique1 = t] ++ unique ~ rest]
     => sql_constraint ([unique1 = t] ++ unique ++ rest) ([unique1] ++ map (fn _ => ()) unique)
 
+con matching :: {Type} -> {Type} -> Type
+val mat_nil : matching [] []
+val mat_cons : t ::: Type -> rest1 ::: {Type} -> rest2 ::: {Type}
+               -> nm1 :: Name -> nm2 :: Name
+               -> [[nm1] ~ rest1] => [[nm2] ~ rest2]
+    => matching rest1 rest2
+       -> matching ([nm1 = t] ++ rest1) ([nm2 = t] ++ rest2)
+
+con propagation_mode :: {Type} -> Type
+val restrict : fs ::: {Type} -> propagation_mode fs
+val cascade : fs ::: {Type} -> propagation_mode fs
+val no_action : fs ::: {Type} -> propagation_mode fs
+val set_null : fs ::: {Type} -> propagation_mode (map option fs)
+
+
+val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused ::: {Type}
+                  -> foreign ::: {Type} -> funused ::: {Type}
+                  -> nm ::: Name -> uniques ::: {{Unit}}
+                  -> [[mine1] ~ mine] => [[mine1 = t] ++ mine ~ munused]
+    => [foreign ~ funused] => [[nm] ~ uniques]
+    => matching ([mine1 = t] ++ mine) foreign
+       -> sql_table (foreign ++ funused) ([nm = map (fn _ => ()) foreign] ++ uniques)
+       -> {OnDelete : propagation_mode ([mine1 = t] ++ mine),
+           OnUpdate : propagation_mode ([mine1 = t] ++ mine)}
+       -> sql_constraint ([mine1 = t] ++ mine ++ munused) []
+
 
 (*** Queries *)
 
--- a/src/disjoint.sml	Tue Apr 07 16:22:11 2009 -0400
+++ b/src/disjoint.sml	Tue Apr 07 18:47:47 2009 -0400
@@ -254,7 +254,8 @@
         val hasUnknown = List.exists (fn Unknown _ => true | _ => false)
         val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
     in
-        if hasUnknown ps1 orelse hasUnknown ps2 then
+        if (hasUnknown ps1 andalso not (List.null ps2))
+           orelse (hasUnknown ps2 andalso not (List.null ps1)) then
             [(loc, env, denv, c1, c2)]
         else
             let
--- a/src/elaborate.sml	Tue Apr 07 16:22:11 2009 -0400
+++ b/src/elaborate.sml	Tue Apr 07 18:47:47 2009 -0400
@@ -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
+                 if occursCon r c then
+                     failure ()
+                 else
+                     r := SOME c
              end
-
-         fun pairOffUnifs (unifs1, unifs2) =
-             case (unifs1, unifs2) of
-                 ([], _) =>
-                 if clear then
-                     List.app (fn (_, r) => r := SOME empty) unifs2
+           | (_, _, _, [(_, 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))
-               | (_, []) =>
-                 if clear then
-                     List.app (fn (_, r) => r := SOME empty) unifs1
-                 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
--- a/src/elisp/urweb-mode.el	Tue Apr 07 16:22:11 2009 -0400
+++ b/src/elisp/urweb-mode.el	Tue Apr 07 18:47:47 2009 -0400
@@ -148,7 +148,8 @@
                  "HAVING" "LIMIT" "OFFSET" "ALL" "UNION" "INTERSECT" "EXCEPT"
                  "TRUE" "FALSE" "AND" "OR" "NOT" "COUNT" "AVG" "SUM" "MIN" "MAX"
                  "ASC" "DESC" "INSERT" "INTO" "VALUES" "UPDATE" "SET" "DELETE"
-                 "PRIMARY" "KEY" "CONSTRAINT" "UNIQUE")
+                 "PRIMARY" "KEY" "CONSTRAINT" "UNIQUE"
+                 "FOREIGN" "REFERENCES" "ON" "NO" "ACTION" "CASCADE" "RESTRICT" "NULL")
   "A regexp that matches SQL keywords.")
 
 (defconst urweb-lident-regexp "\\<[a-z_][A-Za-z0-9_']*\\>"
--- a/src/monoize.sml	Tue Apr 07 16:22:11 2009 -0400
+++ b/src/monoize.sml	Tue Apr 07 18:47:47 2009 -0400
@@ -155,6 +155,14 @@
                     (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", "matching"), _), _), _), _) =>
+                    let
+                        val string = (L'.TFfi ("Basis", "string"), loc)
+                    in
+                        (L'.TRecord [("1", string), ("2", string)], loc)
+                    end
+                  | L.CApp ((L.CFfi ("Basis", "propagation_mode"), _), _) =>
+                    (L'.TFfi ("Basis", "string"), loc)
 
                   | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_subset"), _), _), _), _) =>
                     (L'.TRecord [], loc)
@@ -1218,6 +1226,105 @@
                  fm)
             end
 
+          | L.EFfi ("Basis", "mat_nil") =>
+            let
+                val string = (L'.TFfi ("Basis", "string"), loc)
+                val stringE = (L'.EPrim (Prim.String ""), loc)
+            in
+                ((L'.ERecord [("1", stringE, string),
+                              ("2", stringE, string)], loc), fm)
+            end
+          | L.ECApp (
+            (L.ECApp (
+             (L.ECApp (
+              (L.ECApp (
+               (L.ECApp (
+                (L.EFfi ("Basis", "mat_cons"), _),
+                _), _),
+               _), _),
+              _), _),
+             (L.CName nm1, _)), _),
+            (L.CName nm2, _)) =>
+            let
+                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),
+                 fm)
+            end
+
+          | L.ECApp ((L.EFfi ("Basis", "restrict"), _), _) => ((L'.EPrim (Prim.String "RESTRICT"), loc), fm)
+          | L.ECApp ((L.EFfi ("Basis", "cascade"), _), _) => ((L'.EPrim (Prim.String "CASCADE"), loc), fm)
+          | L.ECApp ((L.EFfi ("Basis", "no_action"), _), _) => ((L'.EPrim (Prim.String "NO ACTION"), loc), fm)
+          | L.ECApp ((L.EFfi ("Basis", "set_null"), _), _) => ((L'.EPrim (Prim.String "SET NULL"), loc), fm)
+
+          | L.ECApp (
+            (L.ECApp (
+             (L.ECApp (
+              (L.ECApp (
+               (L.ECApp (
+                (L.ECApp (
+                 (L.ECApp (
+                  (L.ECApp (
+                   (L.EFfi ("Basis", "foreign_key"), _),
+                   _), _),
+                  _), _),
+                 _), _),
+                _), _),
+               _), _),
+              _), _),
+             _), _),
+            _) =>
+            let
+                val unit = (L'.TRecord [], loc)
+                val string = (L'.TFfi ("Basis", "string"), loc)
+                val mat = (L'.TRecord [("1", string), ("2", string)], loc)
+                val recd = (L'.TRecord [("OnDelete", string),
+                                        ("OnUpdate", string)], loc)
+
+                fun strcat [] = raise Fail "Monoize.strcat"
+                  | strcat [e] = e
+                  | strcat (e1 :: es) = (L'.EStrcat (e1, strcat es), loc)
+
+                fun prop (fd, kw) =
+                    (L'.ECase ((L'.EField ((L'.ERel 0, loc), fd), loc),
+                               [((L'.PPrim (Prim.String "NO ACTION"), loc),
+                                 (L'.EPrim (Prim.String ""), loc)),
+                                ((L'.PWild, loc),
+                                 strcat [(L'.EPrim (Prim.String (" ON " ^ kw ^ " ")), loc),
+                                         (L'.EField ((L'.ERel 0, loc), fd), loc)])],
+                               {disc = string,
+                                result = string}), loc)
+            in
+                ((L'.EAbs ("m", mat, (L'.TFun (string, (L'.TFun (recd, string), loc)), loc),
+                           (L'.EAbs ("tab", string, (L'.TFun (recd, string), loc),
+                                     (L'.EAbs ("pr", recd, string,
+                                               strcat [(L'.EPrim (Prim.String "FOREIGN KEY ("), loc),
+                                                       (L'.EField ((L'.ERel 2, loc), "1"), loc),
+                                                       (L'.EPrim (Prim.String ") REFERENCES "), loc),
+                                                       (L'.ERel 1, loc),
+                                                       (L'.EPrim (Prim.String " ("), loc),
+                                                       (L'.EField ((L'.ERel 2, loc), "2"), loc),
+                                                       (L'.EPrim (Prim.String ")"), loc),
+                                                       prop ("OnDelete", "DELETE"),
+                                                       prop ("OnUpdate", "UPDATE")]), loc)), loc)), loc),
+                 fm)
+            end
+
           | L.EFfiApp ("Basis", "dml", [e]) =>
             let
                 val (e, fm) = monoExp (env, st, fm) e
--- a/src/urweb.grm	Tue Apr 07 16:22:11 2009 -0400
+++ b/src/urweb.grm	Tue Apr 07 18:47:47 2009 -0400
@@ -174,6 +174,8 @@
         "table" => "tabl"
       | _ => bt
 
+datatype prop_kind = Delete | Update
+
 %%
 %header (functor UrwebLrValsFn(structure Token : TOKEN))
 
@@ -208,7 +210,7 @@
  | INSERT | INTO | VALUES | UPDATE | SET | DELETE | NULL | IS
  | CURRENT_TIMESTAMP
  | NE | LT | LE | GT | GE
- | CCONSTRAINT | UNIQUE | PRIMARY | KEY
+ | CCONSTRAINT | UNIQUE | PRIMARY | FOREIGN | KEY | ON | NO | ACTION | RESTRICT | CASCADE | REFERENCES
 
 %nonterm
    file of decl list
@@ -230,6 +232,11 @@
  | csts of exp
  | cstopt of exp
 
+ | pmode of prop_kind * exp
+ | pkind of prop_kind
+ | prule of exp
+ | pmodes of (prop_kind * exp) list
+
  | sgn of sgn
  | sgntm of sgn
  | sgi of sgn_item
@@ -503,6 +510,54 @@
                                          in
                                              (EDisjointApp e, loc)
                                          end)
+
+       | FOREIGN KEY tnames REFERENCES texp LPAREN tnames' RPAREN pmodes
+                                        (let
+                                             val loc = s (FOREIGNleft, pmodesright)
+
+                                             val mat = ListPair.foldrEq
+                                                       (fn ((nm1, _), (nm2, _), mat) =>
+                                                           let
+                                                               val e = (EVar (["Basis"], "mat_cons", Infer), loc)
+                                                               val e = (ECApp (e, nm1), loc)
+                                                               val e = (ECApp (e, nm2), loc)
+                                                               val e = (EDisjointApp e, loc)
+                                                               val e = (EDisjointApp e, loc)
+                                                           in
+                                                               (EApp (e, mat), loc)
+                                                           end)
+                                                       (EVar (["Basis"], "mat_nil", Infer), loc)
+                                                       (#1 tnames :: #2 tnames, #1 tnames' :: #2 tnames')
+
+                                             fun findMode mode =
+                                                 let
+                                                     fun findMode' pmodes =
+                                                         case pmodes of
+                                                             [] => (EVar (["Basis"], "no_action", Infer), loc)
+                                                           | (mode', rule) :: pmodes' =>
+                                                             if mode' = mode then
+                                                                 (if List.exists (fn (mode', _) => mode' = mode)
+                                                                                 pmodes' then
+                                                                      ErrorMsg.errorAt loc "Duplicate propagation rule"
+                                                                  else
+                                                                      ();
+                                                                  rule)
+                                                             else
+                                                                 findMode' pmodes'
+                                                 in
+                                                     findMode' pmodes
+                                                 end
+
+                                             val e = (EVar (["Basis"], "foreign_key", Infer), loc)
+                                             val e = (EApp (e, mat), loc)
+                                             val e = (EApp (e, texp), loc)
+                                         in
+                                             (EApp (e, (ERecord [((CName "OnDelete", loc),
+                                                                  findMode Delete),
+                                                                 ((CName "OnUpdate", loc),
+                                                                  findMode Update)], loc)), loc)
+                                         end)
+
        | LBRACE eexp RBRACE             (eexp)
 
 tnameW : tname                          (let
@@ -517,6 +572,19 @@
 tnames': tnameW                         (tnameW, [])
        | tnameW COMMA tnames'           (#1 tnames', tnameW :: #2 tnames')
 
+pmode  : ON pkind prule                 (pkind, prule)
+
+pkind  : DELETE                         (Delete)
+       | UPDATE                         (Update)
+
+prule  : NO ACTION                      (EVar (["Basis"], "no_action", Infer), s (NOleft, ACTIONright))
+       | RESTRICT                       (EVar (["Basis"], "restrict", Infer), s (RESTRICTleft, RESTRICTright))
+       | CASCADE                        (EVar (["Basis"], "cascade", Infer), s (CASCADEleft, CASCADEright))
+       | SET NULL                       (EVar (["Basis"], "set_null", Infer), s (SETleft, NULLright))
+
+pmodes :                                ([])
+       | pmode pmodes                   (pmode :: pmodes)
+
 commaOpt:                               ()
         | COMMA                         ()
 
--- a/src/urweb.lex	Tue Apr 07 16:22:11 2009 -0400
+++ b/src/urweb.lex	Tue Apr 07 18:47:47 2009 -0400
@@ -368,7 +368,16 @@
 <INITIAL> "CONSTRAINT"=> (Tokens.CCONSTRAINT (pos yypos, pos yypos + size yytext));
 <INITIAL> "UNIQUE"    => (Tokens.UNIQUE (pos yypos, pos yypos + size yytext));
 <INITIAL> "PRIMARY"   => (Tokens.PRIMARY (pos yypos, pos yypos + size yytext));
+<INITIAL> "FOREIGN"   => (Tokens.FOREIGN (pos yypos, pos yypos + size yytext));
 <INITIAL> "KEY"       => (Tokens.KEY (pos yypos, pos yypos + size yytext));
+<INITIAL> "ON"        => (Tokens.ON (pos yypos, pos yypos + size yytext));
+<INITIAL> "NO"        => (Tokens.NO (pos yypos, pos yypos + size yytext));
+<INITIAL> "ACTION"    => (Tokens.ACTION (pos yypos, pos yypos + size yytext));
+<INITIAL> "RESTRICT"  => (Tokens.RESTRICT (pos yypos, pos yypos + size yytext));
+<INITIAL> "CASCADE"   => (Tokens.CASCADE (pos yypos, pos yypos + size yytext));
+<INITIAL> "REFERENCES"=> (Tokens.REFERENCES (pos yypos, pos yypos + size yytext));
+
+<INITIAL> "CURRENT_TIMESTAMP" => (Tokens.CURRENT_TIMESTAMP (pos yypos, pos yypos + size yytext));
 
 <INITIAL> "CURRENT_TIMESTAMP" => (Tokens.CURRENT_TIMESTAMP (pos yypos, pos yypos + size yytext));
 
--- a/tests/cst.ur	Tue Apr 07 16:22:11 2009 -0400
+++ b/tests/cst.ur	Tue Apr 07 18:47:47 2009 -0400
@@ -1,3 +1,7 @@
+table u : {C : int, D : int, E : int}
+  PRIMARY KEY C,
+  CONSTRAINT U UNIQUE (C, D)
+
 table t : {A : int, B : int}
   PRIMARY KEY B,
 
@@ -11,7 +15,19 @@
 
   CONSTRAINT UniBothm UNIQUE ({#A}, {#B}),
   CONSTRAINT UniBothm2 {unique [#A] [[B = _]] ! !},
-  {{one_constraint [#UniBothm3] (unique [#A] [[B = _]] ! !)}}
+  {{one_constraint [#UniBothm3] (unique [#A] [[B = _]] ! !)}},
+
+  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 Self FOREIGN KEY B REFERENCES t (B)
+
+table s : {B : option int}
+  CONSTRAINT UniB UNIQUE B
+
+table s2 : {B : option int}
+  CONSTRAINT ForB FOREIGN KEY B REFERENCES s (B) ON DELETE SET NULL
 
 fun main () : transaction page =
     queryI (SELECT * FROM t) (fn _ => return ());