Mercurial > urweb
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 ());