summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--demo/broadcast.ur2
-rw-r--r--lib/ur/basis.urs27
-rw-r--r--src/disjoint.sml3
-rw-r--r--src/elaborate.sml92
-rw-r--r--src/elisp/urweb-mode.el3
-rw-r--r--src/monoize.sml107
-rw-r--r--src/urweb.grm70
-rw-r--r--src/urweb.lex9
-rw-r--r--tests/cst.ur18
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 ());