diff options
| -rw-r--r-- | demo/broadcast.ur | 2 | ||||
| -rw-r--r-- | lib/ur/basis.urs | 27 | ||||
| -rw-r--r-- | src/disjoint.sml | 3 | ||||
| -rw-r--r-- | src/elaborate.sml | 92 | ||||
| -rw-r--r-- | src/elisp/urweb-mode.el | 3 | ||||
| -rw-r--r-- | src/monoize.sml | 107 | ||||
| -rw-r--r-- | src/urweb.grm | 70 | ||||
| -rw-r--r-- | src/urweb.lex | 9 | ||||
| -rw-r--r-- | tests/cst.ur | 18 |
9 files changed, 300 insertions, 31 deletions
diff --git a/demo/broadcast.ur b/demo/broadcast.ur index 29d8d8fb..0b04b136 100644 --- a/demo/broadcast.ur +++ b/demo/broadcast.ur @@ -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 diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index 997495b1..d69ddfcb 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -161,10 +161,37 @@ val join_constraints : fs ::: {Type} => 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 *) diff --git a/src/disjoint.sml b/src/disjoint.sml index 503544af..5cc9d1fb 100644 --- a/src/disjoint.sml +++ b/src/disjoint.sml @@ -254,7 +254,8 @@ and prove env denv (c1, c2, loc) = 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 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 diff --git a/src/elisp/urweb-mode.el b/src/elisp/urweb-mode.el index 65cd8abf..545902ac 100644 --- a/src/elisp/urweb-mode.el +++ b/src/elisp/urweb-mode.el @@ -148,7 +148,8 @@ See doc for the variable `urweb-mode-info'." "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_']*\\>" diff --git a/src/monoize.sml b/src/monoize.sml index 2e514b4e..84707b6e 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -155,6 +155,14 @@ fun monoType env = (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 @@ fun monoExp (env, st, fm) (all as (e, loc)) = 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 diff --git a/src/urweb.grm b/src/urweb.grm index a507e52e..5539feff 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -174,6 +174,8 @@ fun tagIn bt = "table" => "tabl" | _ => bt +datatype prop_kind = Delete | Update + %% %header (functor UrwebLrValsFn(structure Token : TOKEN)) @@ -208,7 +210,7 @@ fun tagIn bt = | 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 @@ fun tagIn bt = | 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 @@ cst : UNIQUE tnames (let 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, []) 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 () diff --git a/src/urweb.lex b/src/urweb.lex index 31c0a362..c01f018b 100644 --- a/src/urweb.lex +++ b/src/urweb.lex @@ -368,7 +368,16 @@ notags = [^<{\n]+; <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)); diff --git a/tests/cst.ur b/tests/cst.ur index fc3b0816..548862be 100644 --- a/tests/cst.ur +++ b/tests/cst.ur @@ -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 @@ table t : {A : int, B : int} 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 ()); |