Mercurial > urweb
changeset 707:d8217b4cb617
PRIMARY KEY
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 07 Apr 2009 16:14:31 -0400 |
| parents | 1fb318c17546 |
| children | 1a317a707d71 |
| files | lib/ur/basis.urs src/cjr.sml src/cjr_print.sml src/cjrize.sml src/core.sml src/core_env.sml src/core_print.sml src/core_util.sml src/corify.sml src/elab.sml src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/expl.sml src/expl_env.sml src/expl_print.sml src/explify.sml src/mono.sml src/mono_print.sml src/mono_util.sml src/monoize.sml src/pathcheck.sml src/reduce.sml src/shake.sml src/source.sml src/source_print.sml src/urweb.grm src/urweb.lex tests/cst.ur tests/pkey.ur tests/pkey.urp |
| diffstat | 32 files changed, 356 insertions(+), 181 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Tue Apr 07 15:04:07 2009 -0400 +++ b/lib/ur/basis.urs Tue Apr 07 16:14:31 2009 -0400 @@ -126,6 +126,27 @@ (*** Constraints *) +(**** Primary keys *) + +class sql_injectable_prim +val sql_bool : sql_injectable_prim bool +val sql_int : sql_injectable_prim int +val sql_float : sql_injectable_prim float +val sql_string : sql_injectable_prim string +val sql_time : sql_injectable_prim time +val sql_channel : t ::: Type -> sql_injectable_prim (channel t) +val sql_client : sql_injectable_prim client + +con primary_key :: {Type} -> {{Unit}} -> Type +val no_primary_key : fs ::: {Type} -> primary_key fs [] +val primary_key : rest ::: {Type} -> t ::: Type -> key1 :: Name -> keys :: {Type} + -> [[key1] ~ keys] => [[key1 = t] ++ keys ~ rest] + => $([key1 = sql_injectable_prim t] ++ map sql_injectable_prim keys) + -> primary_key ([key1 = t] ++ keys ++ rest) + [Pkey = [key1] ++ map (fn _ => ()) keys] + +(**** Other constraints *) + con sql_constraints :: {Type} -> {{Unit}} -> Type (* Arguments: column types, uniqueness implications of constraints *) @@ -224,15 +245,6 @@ -> nm :: Name -> sql_exp tabs agg ([nm = t] ++ rest) t -class sql_injectable_prim -val sql_bool : sql_injectable_prim bool -val sql_int : sql_injectable_prim int -val sql_float : sql_injectable_prim float -val sql_string : sql_injectable_prim string -val sql_time : sql_injectable_prim time -val sql_channel : t ::: Type -> sql_injectable_prim (channel t) -val sql_client : sql_injectable_prim client - class sql_injectable val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t)
--- a/src/cjr.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/cjr.sml Tue Apr 07 16:14:31 2009 -0400 @@ -104,7 +104,7 @@ | DFun of string * int * (string * typ) list * typ * exp | DFunRec of (string * int * (string * typ) list * typ * exp) list - | DTable of string * (string * typ) list * (string * string) list + | DTable of string * (string * typ) list * string * (string * string) list | DSequence of string | DDatabase of {name : string, expunge : int, initialize : int} | DPreparedStatements of (string * int) list
--- a/src/cjr_print.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/cjr_print.sml Tue Apr 07 16:14:31 2009 -0400 @@ -1941,19 +1941,25 @@ p_list_sep newline (p_fun env) vis, newline] end - | DTable (x, _, csts) => box [string "/* SQL table ", - string x, - space, - string "constraints", - space, - p_list (fn (x, v) => box [string x, - space, - string ":", - space, - string v]) csts, - space, - string " */", - newline] + | DTable (x, _, pk, csts) => box [string "/* SQL table ", + string x, + space, + case pk of + "" => box [] + | _ => box [string "keys", + space, + string pk, + space], + string "constraints", + space, + p_list (fn (x, v) => box [string x, + space, + string ":", + space, + string v]) csts, + space, + string " */", + newline] | DSequence x => box [string "/* SQL sequence ", string x, string " */", @@ -2467,7 +2473,7 @@ val pds' = map p_page ps - val tables = List.mapPartial (fn (DTable (s, xts, _), _) => SOME (s, xts) + val tables = List.mapPartial (fn (DTable (s, xts, _, _), _) => SOME (s, xts) | _ => NONE) ds val sequences = List.mapPartial (fn (DSequence s, _) => SOME s | _ => NONE) ds @@ -2811,7 +2817,7 @@ (fn (dAll as (d, _), env) => let val pp = case d of - DTable (s, xts, csts) => + DTable (s, xts, pk, csts) => box [string "CREATE TABLE ", string s, string "(", @@ -2820,10 +2826,23 @@ string (CharVector.map Char.toLower x), space, p_sqltype env (t, ErrorMsg.dummySpan)]) xts, - case csts of - [] => box [] - | _ => box [string ","], + case (pk, csts) of + ("", []) => box [] + | _ => string ",", cut, + case pk of + "" => box [] + | _ => box [string "PRIMARY", + space, + string "KEY", + space, + string "(", + string pk, + string ")", + case csts of + [] => box [] + | _ => string ",", + newline], p_list_sep (box [string ",", newline]) (fn (x, c) => box [string "CONSTRAINT",
--- a/src/cjrize.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/cjrize.sml Tue Apr 07 16:14:31 2009 -0400 @@ -524,7 +524,7 @@ (NONE, SOME (ek, "/" ^ s, n, ts, t, L'.ServerAndPullAndPush), sm) end - | L.DTable (s, xts, e) => + | L.DTable (s, xts, pe, ce) => let val (xts, sm) = ListUtil.foldlMap (fn ((x, t), sm) => let @@ -540,10 +540,17 @@ | L.EStrcat (e1, e2) => flatten e1 @ flatten e2 | _ => (ErrorMsg.errorAt loc "Constraint has not been fully determined"; Print.prefaces "Undetermined constraint" - [("e", MonoPrint.p_exp MonoEnv.empty e)]; + [("e", MonoPrint.p_exp MonoEnv.empty e)]; []) + + val pe = case #1 pe of + L.EPrim (Prim.String s) => s + | _ => (ErrorMsg.errorAt loc "Primary key has not been fully determined"; + Print.prefaces "Undetermined constraint" + [("e", MonoPrint.p_exp MonoEnv.empty pe)]; + "") in - (SOME (L'.DTable (s, xts, flatten e), loc), NONE, sm) + (SOME (L'.DTable (s, xts, pe, flatten ce), loc), NONE, sm) end | L.DSequence s => (SOME (L'.DSequence s, loc), NONE, sm)
--- a/src/core.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/core.sml Tue Apr 07 16:14:31 2009 -0400 @@ -130,7 +130,7 @@ | DVal of string * int * con * exp * string | DValRec of (string * int * con * exp * string) list | DExport of export_kind * int - | DTable of string * int * con * string * exp * con + | DTable of string * int * con * string * exp * con * exp * con | DSequence of string * int * string | DDatabase of string | DCookie of string * int * con * string
--- a/src/core_env.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/core_env.sml Tue Apr 07 16:14:31 2009 -0400 @@ -313,11 +313,11 @@ | DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s | DValRec vis => foldl (fn ((x, n, t, e, s), env) => pushENamed env x n t NONE s) env vis | DExport _ => env - | DTable (x, n, c, s, _, cc) => + | DTable (x, n, c, s, _, pc, _, cc) => let val ct = (CFfi ("Basis", "sql_table"), loc) val ct = (CApp (ct, c), loc) - val ct = (CApp (ct, cc), loc) + val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc) in pushENamed env x n ct NONE s end
--- a/src/core_print.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/core_print.sml Tue Apr 07 16:14:31 2009 -0400 @@ -546,21 +546,25 @@ space, (p_con env (#2 (E.lookupENamed env n)) handle E.UnboundNamed _ => string "UNBOUND")] - | DTable (x, n, c, s, e, _) => box [string "table", - space, - p_named x n, - space, - string "as", - space, - string s, - space, - string ":", - space, - p_con env c, - space, - string "constraints", - space, - p_exp env e] + | DTable (x, n, c, s, pe, _, ce, _) => box [string "table", + space, + p_named x n, + space, + string "as", + space, + string s, + space, + string ":", + space, + p_con env c, + space, + string "keys", + space, + p_exp env pe, + space, + string "constraints", + space, + p_exp env ce] | DSequence (x, n, s) => box [string "sequence", space, p_named x n,
--- a/src/core_util.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/core_util.sml Tue Apr 07 16:14:31 2009 -0400 @@ -933,14 +933,18 @@ (DValRec vis', loc)) end | DExport _ => S.return2 dAll - | DTable (x, n, c, s, e, cc) => + | DTable (x, n, c, s, pe, pc, ce, cc) => S.bind2 (mfc ctx c, fn c' => - S.bind2 (mfe ctx e, - fn e' => - S.map2 (mfc ctx cc, - fn cc' => - (DTable (x, n, c', s, e', cc'), loc)))) + S.bind2 (mfe ctx pe, + fn pe' => + S.bind2 (mfc ctx pc, + fn pc' => + S.bind2 (mfe ctx ce, + fn ce' => + S.map2 (mfc ctx cc, + fn cc' => + (DTable (x, n, c', s, pe', pc', ce', cc'), loc)))))) | DSequence _ => S.return2 dAll | DDatabase _ => S.return2 dAll | DCookie (x, n, c, s) => @@ -1062,11 +1066,11 @@ foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s))) ctx vis | DExport _ => ctx - | DTable (x, n, c, s, _, cc) => + | DTable (x, n, c, s, _, pc, _, cc) => let val loc = #2 d' val ct = (CFfi ("Basis", "sql_table"), loc) - val ct = (CApp (ct, c), loc) + val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc) val ct = (CApp (ct, cc), loc) in bind (ctx, NamedE (x, n, ct, NONE, s)) @@ -1141,7 +1145,7 @@ | DVal (_, n, _, _, _) => Int.max (n, count) | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis | DExport _ => count - | DTable (_, n, _, _, _, _) => Int.max (n, count) + | DTable (_, n, _, _, _, _, _, _) => Int.max (n, count) | DSequence (_, n, _) => Int.max (n, count) | DDatabase _ => count | DCookie (_, n, _, _) => Int.max (n, count)) 0
--- a/src/corify.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/corify.sml Tue Apr 07 16:14:31 2009 -0400 @@ -976,12 +976,14 @@ end | _ => raise Fail "Non-const signature for 'export'") - | L.DTable (_, x, n, c, e, cc) => + | L.DTable (_, x, n, c, pe, pc, ce, cc) => let val (st, n) = St.bindVal st x n val s = relify (doRestify (mods, x)) in - ([(L'.DTable (x, n, corifyCon st c, s, corifyExp st e, corifyCon st cc), loc)], st) + ([(L'.DTable (x, n, corifyCon st c, s, + corifyExp st pe, corifyCon st pc, + corifyExp st ce, corifyCon st cc), loc)], st) end | L.DSequence (_, x, n) => let @@ -1052,7 +1054,7 @@ | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str)) | L.DFfiStr (_, n', _) => Int.max (n, n') | L.DExport _ => n - | L.DTable (_, _, n', _, _, _) => Int.max (n, n') + | L.DTable (_, _, n', _, _, _, _, _) => Int.max (n, n') | L.DSequence (_, _, n') => Int.max (n, n') | L.DDatabase _ => n | L.DCookie (_, _, n', _) => Int.max (n, n'))
--- a/src/elab.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/elab.sml Tue Apr 07 16:14:31 2009 -0400 @@ -166,7 +166,7 @@ | DFfiStr of string * int * sgn | DConstraint of con * con | DExport of int * sgn * str - | DTable of int * string * int * con * exp * con + | DTable of int * string * int * con * exp * con * exp * con | DSequence of int * string * int | DClass of string * int * kind * con | DDatabase of string
--- a/src/elab_env.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/elab_env.sml Tue Apr 07 16:14:31 2009 -0400 @@ -1532,11 +1532,11 @@ | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn | DConstraint _ => env | DExport _ => env - | DTable (tn, x, n, c, _, cc) => + | DTable (tn, x, n, c, _, pc, _, cc) => let val ct = (CModProj (tn, [], "sql_table"), loc) val ct = (CApp (ct, c), loc) - val ct = (CApp (ct, cc), loc) + val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc) in pushENamedAs env x n ct end
--- a/src/elab_print.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/elab_print.sml Tue Apr 07 16:14:31 2009 -0400 @@ -740,17 +740,21 @@ string ":", space, p_sgn env sgn] - | DTable (_, x, n, c, e, _) => box [string "table", - space, - p_named x n, - space, - string ":", - space, - p_con env c, - space, - string "constraints", - space, - p_exp env e] + | DTable (_, x, n, c, pe, _, ce, _) => box [string "table", + space, + p_named x n, + space, + string ":", + space, + p_con env c, + space, + string "keys", + space, + p_exp env pe, + space, + string "constraints", + space, + p_exp env ce] | DSequence (_, x, n) => box [string "sequence", space, p_named x n]
--- a/src/elab_util.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/elab_util.sml Tue Apr 07 16:14:31 2009 -0400 @@ -766,11 +766,11 @@ bind (ctx, Str (x, sgn)) | DConstraint _ => ctx | DExport _ => ctx - | DTable (tn, x, n, c, _, cc) => + | DTable (tn, x, n, c, _, pc, _, cc) => let val ct = (CModProj (n, [], "sql_table"), loc) val ct = (CApp (ct, c), loc) - val ct = (CApp (ct, cc), loc) + val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc) in bind (ctx, NamedE (x, ct)) end @@ -869,14 +869,18 @@ fn str' => (DExport (en, sgn', str'), loc))) - | DTable (tn, x, n, c, e, cc) => + | DTable (tn, x, n, c, pe, pc, ce, cc) => S.bind2 (mfc ctx c, fn c' => - S.bind2 (mfe ctx e, - fn e' => - S.map2 (mfc ctx cc, - fn cc' => - (DTable (tn, x, n, c', e', cc'), loc)))) + S.bind2 (mfe ctx pe, + fn pe' => + S.bind2 (mfc ctx pc, + fn pc' => + S.bind2 (mfe ctx ce, + fn ce' => + S.map2 (mfc ctx cc, + fn cc' => + (DTable (tn, x, n, c', pe', pc', ce', cc'), loc)))))) | DSequence _ => S.return2 dAll | DClass (x, n, k, c) => @@ -1027,7 +1031,7 @@ | DConstraint _ => 0 | DClass (_, n, _, _) => n | DExport _ => 0 - | DTable (n1, _, n2, _, _, _) => Int.max (n1, n2) + | DTable (n1, _, n2, _, _, _, _, _) => Int.max (n1, n2) | DSequence (n1, _, n2) => Int.max (n1, n2) | DDatabase _ => 0 | DCookie (n1, _, n2, _) => Int.max (n1, n2)
--- a/src/elaborate.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/elaborate.sml Tue Apr 07 16:14:31 2009 -0400 @@ -2027,7 +2027,7 @@ ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) end - | L.SgiTable (x, c, e) => + | L.SgiTable (x, c, pe, ce) => let val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) val x' = x ^ "_hidden_constraints" @@ -2035,28 +2035,38 @@ val hidden = (L'.CNamed hidden_n, loc) val (c', ck, gs') = elabCon (env, denv) c + val pkey = cunif (loc, cstK) val visible = cunif (loc, cstK) val uniques = (L'.CConcat (visible, hidden), loc) val ct = tableOf () val ct = (L'.CApp (ct, c'), loc) - val ct = (L'.CApp (ct, uniques), loc) + val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc) + + val (pe', pet, gs'') = elabExp (env', denv) pe + val gs'' = List.mapPartial (fn Disjoint x => SOME x + | _ => NONE) gs'' + + val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc) + val pst = (L'.CApp (pst, c'), loc) + val pst = (L'.CApp (pst, pkey), loc) val (env', n) = E.pushENamed env' x ct - val (e', et, gs'') = elabExp (env, denv) e - val gs'' = List.mapPartial (fn Disjoint x => SOME x - | _ => NONE) gs'' + val (ce', cet, gs''') = elabExp (env', denv) ce + val gs''' = List.mapPartial (fn Disjoint x => SOME x + | _ => NONE) gs''' val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) val cst = (L'.CApp (cst, c'), loc) val cst = (L'.CApp (cst, visible), loc) in checkKind env c' ck (L'.KRecord (L'.KType, loc), loc); - checkCon env' e' et cst; + checkCon env' pe' pet pst; + checkCon env' ce' cet cst; ([(L'.SgiConAbs (x', hidden_n, cstK), loc), - (L'.SgiVal (x, n, ct), loc)], (env', denv, gs'' @ gs' @ gs)) + (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs)) end | L.SgiStr (x, sgn) => @@ -2360,8 +2370,9 @@ | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] | L'.DExport _ => [] - | L'.DTable (tn, x, n, c, _, cc) => - [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), cc), loc)), loc)] + | L'.DTable (tn, x, n, c, _, pc, _, cc) => + [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), + (L'.CConcat (pc, cc), loc)), loc)), loc)] | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] | L'.DDatabase _ => [] @@ -3307,25 +3318,35 @@ ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs)) end - | L.DTable (x, c, e) => + | L.DTable (x, c, pe, ce) => let + val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) + val (c', k, gs') = elabCon (env, denv) c - val uniques = cunif (loc, (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)) + val pkey = cunif (loc, cstK) + val uniques = cunif (loc, cstK) val ct = tableOf () val ct = (L'.CApp (ct, c'), loc) - val ct = (L'.CApp (ct, uniques), loc) + val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc) val (env, n) = E.pushENamed env x ct - val (e', et, gs'') = elabExp (env, denv) e + val (pe', pet, gs'') = elabExp (env, denv) pe + val (ce', cet, gs''') = elabExp (env, denv) ce + + val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc) + val pst = (L'.CApp (pst, c'), loc) + val pst = (L'.CApp (pst, pkey), loc) val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) val cst = (L'.CApp (cst, c'), loc) val cst = (L'.CApp (cst, uniques), loc) in checkKind env c' k (L'.KRecord (L'.KType, loc), loc); - checkCon env e' et cst; - ([(L'.DTable (!basis_r, x, n, c', e', uniques), loc)], (env, denv, gs'' @ enD gs' @ gs)) + checkCon env pe' pet pst; + checkCon env ce' cet cst; + ([(L'.DTable (!basis_r, x, n, c', pe', pkey, ce', uniques), loc)], + (env, denv, gs''' @ gs'' @ enD gs' @ gs)) end | L.DSequence x => let
--- a/src/expl.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/expl.sml Tue Apr 07 16:14:31 2009 -0400 @@ -141,7 +141,7 @@ | DStr of string * int * sgn * str | DFfiStr of string * int * sgn | DExport of int * sgn * str - | DTable of int * string * int * con * exp * con + | DTable of int * string * int * con * exp * con * exp * con | DSequence of int * string * int | DDatabase of string | DCookie of int * string * int * con
--- a/src/expl_env.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/expl_env.sml Tue Apr 07 16:14:31 2009 -0400 @@ -298,11 +298,11 @@ | DStr (x, n, sgn, _) => pushStrNamed env x n sgn | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn | DExport _ => env - | DTable (tn, x, n, c, _, cc) => + | DTable (tn, x, n, c, _, pc, _, cc) => let val ct = (CModProj (tn, [], "sql_table"), loc) val ct = (CApp (ct, c), loc) - val ct = (CApp (ct, cc), loc) + val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc) in pushENamed env x n ct end
--- a/src/expl_print.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/expl_print.sml Tue Apr 07 16:14:31 2009 -0400 @@ -663,17 +663,21 @@ string ":", space, p_sgn env sgn] - | DTable (_, x, n, c, e, _) => box [string "table", - space, - p_named x n, - space, - string ":", - space, - p_con env c, - space, - string "constraints", - space, - p_exp env e] + | DTable (_, x, n, c, pe, _, ce, _) => box [string "table", + space, + p_named x n, + space, + string ":", + space, + p_con env c, + space, + string "keys", + space, + p_exp env pe, + space, + string "constraints", + space, + p_exp env ce] | DSequence (_, x, n) => box [string "sequence", space, p_named x n]
--- a/src/explify.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/explify.sml Tue Apr 07 16:14:31 2009 -0400 @@ -178,7 +178,10 @@ | L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc) | L.DConstraint (c1, c2) => NONE | L.DExport (en, sgn, str) => SOME (L'.DExport (en, explifySgn sgn, explifyStr str), loc) - | L.DTable (nt, x, n, c, e, cc) => SOME (L'.DTable (nt, x, n, explifyCon c, explifyExp e, explifyCon cc), loc) + | L.DTable (nt, x, n, c, pe, pc, ce, cc) => + SOME (L'.DTable (nt, x, n, explifyCon c, + explifyExp pe, explifyCon pc, + explifyExp ce, explifyCon cc), loc) | L.DSequence (nt, x, n) => SOME (L'.DSequence (nt, x, n), loc) | L.DClass (x, n, k, c) => SOME (L'.DCon (x, n, (L'.KArrow (explifyKind k, (L'.KType, loc)), loc), explifyCon c), loc)
--- a/src/mono.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/mono.sml Tue Apr 07 16:14:31 2009 -0400 @@ -121,7 +121,7 @@ | DValRec of (string * int * typ * exp * string) list | DExport of Core.export_kind * string * int * typ list * typ - | DTable of string * (string * typ) list * exp + | DTable of string * (string * typ) list * exp * exp | DSequence of string | DDatabase of {name : string, expunge : int, initialize : int}
--- a/src/mono_print.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/mono_print.sml Tue Apr 07 16:14:31 2009 -0400 @@ -403,22 +403,26 @@ space, p_typ env t] - | DTable (s, xts, e) => box [string "(* SQL table ", - string s, - space, - string ":", - space, - p_list (fn (x, t) => box [string x, - space, - string ":", - space, - p_typ env t]) xts, - space, - string "constraints", - space, - p_exp env e, - space, - string "*)"] + | DTable (s, xts, pe, ce) => box [string "(* SQL table ", + string s, + space, + string ":", + space, + p_list (fn (x, t) => box [string x, + space, + string ":", + space, + p_typ env t]) xts, + space, + string "keys", + space, + p_exp env pe, + space, + string "constraints", + space, + p_exp env ce, + space, + string "*)"] | DSequence s => box [string "(* SQL sequence ", string s, string "*)"]
--- a/src/mono_util.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/mono_util.sml Tue Apr 07 16:14:31 2009 -0400 @@ -465,10 +465,12 @@ S.map2 (mft t, fn t' => (DExport (ek, s, n, ts', t'), loc))) - | DTable (s, xts, e) => - S.map2 (mfe ctx e, - fn e' => - (DTable (s, xts, e'), loc)) + | DTable (s, xts, pe, ce) => + S.bind2 (mfe ctx pe, + fn pe' => + S.map2 (mfe ctx ce, + fn ce' => + (DTable (s, xts, pe', ce'), loc))) | DSequence _ => S.return2 dAll | DDatabase _ => S.return2 dAll | DJavaScript _ => S.return2 dAll
--- a/src/monoize.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/monoize.sml Tue Apr 07 16:14:31 2009 -0400 @@ -149,6 +149,8 @@ (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_exp"), _), _), _), _), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) + | L.CApp ((L.CApp ((L.CFfi ("Basis", "primary_key"), _), _), _), _) => + (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_constraints"), _), _), _), _) => (L'.TFfi ("Basis", "sql_constraints"), loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_constraint"), _), _), _), _) => @@ -1159,6 +1161,25 @@ fm) end + | L.ECApp ((L.EFfi ("Basis", "no_primary_key"), _), _) => + ((L'.EPrim (Prim.String ""), loc), + fm) + | L.ECApp ( + (L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "primary_key"), _), _), _), t), _), + nm), _), + (L.CRecord (_, unique), _)) => + let + val unique = (nm, t) :: unique + val witnesses = (L'.TRecord (map (fn (nm, _) => (monoName env nm, (L'.TRecord [], loc))) unique), loc) + in + ((L'.EAbs ("_", witnesses, (L'.TFfi ("Basis", "string"), loc), + (L'.EPrim (Prim.String + (String.concatWith ", " + (map (fn (x, _) => "uw_" ^ monoName env x) unique))), + loc)), loc), + fm) + end + | L.ECApp ((L.EFfi ("Basis", "no_constraint"), _), _) => ((L'.ERecord [], loc), fm) @@ -2499,7 +2520,7 @@ in SOME (env, fm, [(L'.DExport (ek, s, n, ts, ran), loc)]) end - | L.DTable (x, n, (L.CRecord (_, xts), _), s, e, _) => + | L.DTable (x, n, (L.CRecord (_, xts), _), s, pe, _, ce, _) => let val t = (L.CFfi ("Basis", "string"), loc) val t' = (L'.TFfi ("Basis", "string"), loc) @@ -2508,11 +2529,12 @@ val xts = map (fn (x, t) => (monoName env x, monoType env t)) xts - val (e, fm) = monoExp (env, St.empty, fm) e + val (pe, fm) = monoExp (env, St.empty, fm) pe + val (ce, fm) = monoExp (env, St.empty, fm) ce in SOME (Env.pushENamed env x n t NONE s, fm, - [(L'.DTable (s, xts, e), loc), + [(L'.DTable (s, xts, pe, ce), loc), (L'.DVal (x, n, t', e_name, s), loc)]) end | L.DTable _ => poly () @@ -2633,7 +2655,7 @@ in foldl (fn ((d, _), e) => case d of - L.DTable (_, _, xts, tab, _, _) => doTable (tab, #1 xts, e) + L.DTable (_, _, xts, tab, _, _, _, _) => doTable (tab, #1 xts, e) | _ => e) e file end @@ -2678,7 +2700,7 @@ in foldl (fn ((d, _), e) => case d of - L.DTable (_, _, xts, tab, _, _) => doTable (tab, #1 xts, e) + L.DTable (_, _, xts, tab, _, _, _, _) => doTable (tab, #1 xts, e) | _ => e) e file end
--- a/src/pathcheck.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/pathcheck.sml Tue Apr 07 16:14:31 2009 -0400 @@ -55,7 +55,7 @@ case d of DExport (_, s, _, _, _) => doFunc s - | DTable (s, _, e) => + | DTable (s, _, pe, ce) => let fun constraints (e, rels) = case #1 e of @@ -71,8 +71,22 @@ end | EStrcat (e1, e2) => constraints (e2, constraints (e1, rels)) | _ => rels + + val rels = #2 (doRel s) + val rels = case #1 pe of + EPrim (Prim.String "") => rels + | _ => + let + val s' = s ^ "_Pkey" + in + if SS.member (rels, s') then + E.errorAt loc ("Duplicate primary key constraint path " ^ s') + else + (); + SS.add (rels, s') + end in - (funcs, constraints (e, #2 (doRel s))) + (funcs, constraints (ce, rels)) end | DSequence s => doRel s
--- a/src/reduce.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/reduce.sml Tue Apr 07 16:14:31 2009 -0400 @@ -461,9 +461,11 @@ ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t, exp (namedC, namedE) [] e, s)) vis), loc), st) | DExport _ => (d, st) - | DTable (s, n, c, s', e, cc) => ((DTable (s, n, con namedC [] c, s', - exp (namedC, namedE) [] e, - con namedC [] cc), loc), st) + | DTable (s, n, c, s', pe, pc, ce, cc) => ((DTable (s, n, con namedC [] c, s', + exp (namedC, namedE) [] pe, + con namedC [] pc, + exp (namedC, namedE) [] ce, + con namedC [] cc), loc), st) | DSequence _ => (d, st) | DDatabase _ => (d, st) | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st)
--- a/src/shake.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/shake.sml Tue Apr 07 16:14:31 2009 -0400 @@ -59,9 +59,10 @@ val (usedE, usedC, table_cs) = List.foldl (fn ((DExport (_, n), _), (usedE, usedC, table_cs)) => (IS.add (usedE, n), usedE, table_cs) - | ((DTable (_, _, c, _, e, _), _), (usedE, usedC, table_cs)) => + | ((DTable (_, _, c, _, pe, _, ce, _), _), (usedE, usedC, table_cs)) => let - val (usedE, usedC) = usedVars (usedE, usedC) e + val (usedE, usedC) = usedVars (usedE, usedC) pe + val (usedE, usedC) = usedVars (usedE, usedC) ce in (usedE, usedC, c :: table_cs) end @@ -79,7 +80,7 @@ IM.insert (edef, n, (all_ns, t, e))) edef vis) end | ((DExport _, _), acc) => acc - | ((DTable (_, n, c, _, _, _), _), (cdef, edef)) => + | ((DTable (_, n, c, _, _, _, _, _), _), (cdef, edef)) => (cdef, IM.insert (edef, n, ([], c, dummye))) | ((DSequence (_, n, _), _), (cdef, edef)) => (cdef, IM.insert (edef, n, ([], dummyt, dummye)))
--- a/src/source.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/source.sml Tue Apr 07 16:14:31 2009 -0400 @@ -88,7 +88,7 @@ | SgiDatatype of string * string list * (string * con option) list | SgiDatatypeImp of string * string list * string | SgiVal of string * con - | SgiTable of string * con * exp + | SgiTable of string * con * exp * exp | SgiStr of string * sgn | SgiSgn of string * sgn | SgiInclude of sgn @@ -146,8 +146,6 @@ and exp = exp' located and edecl = edecl' located - - datatype decl' = DCon of string * kind option * con | DDatatype of string * string list * (string * con option) list @@ -161,7 +159,7 @@ | DConstraint of con * con | DOpenConstraints of string * string list | DExport of str - | DTable of string * con * exp + | DTable of string * con * exp * exp | DSequence of string | DClass of string * kind * con | DDatabase of string
--- a/src/source_print.sml Tue Apr 07 15:04:07 2009 -0400 +++ b/src/source_print.sml Tue Apr 07 16:14:31 2009 -0400 @@ -417,17 +417,21 @@ string ":", space, p_con c] - | SgiTable (x, c, e) => box [string "table", - space, - string x, - space, - string ":", - space, - p_con c, - space, - string "constraints", - space, - p_exp e] + | SgiTable (x, c, pe, ce) => box [string "table", + space, + string x, + space, + string ":", + space, + p_con c, + space, + string "keys", + space, + p_exp pe, + space, + string "constraints", + space, + p_exp ce] | SgiStr (x, sgn) => box [string "structure", space, string x, @@ -599,17 +603,21 @@ | DExport str => box [string "export", space, p_str str] - | DTable (x, c, e) => box [string "table", - space, - string x, - space, - string ":", - space, - p_con c, - space, - string "constraints", - space, - p_exp e] + | DTable (x, c, pe, ce) => box [string "table", + space, + string x, + space, + string ":", + space, + p_con c, + space, + string "keys", + space, + p_exp pe, + space, + string "constraints", + space, + p_exp ce] | DSequence x => box [string "sequence", space, string x]
--- a/src/urweb.grm Tue Apr 07 15:04:07 2009 -0400 +++ b/src/urweb.grm Tue Apr 07 16:14:31 2009 -0400 @@ -208,7 +208,7 @@ | INSERT | INTO | VALUES | UPDATE | SET | DELETE | NULL | IS | CURRENT_TIMESTAMP | NE | LT | LE | GT | GE - | CCONSTRAINT | UNIQUE + | CCONSTRAINT | UNIQUE | PRIMARY | KEY %nonterm file of decl list @@ -223,6 +223,9 @@ | dcons of (string * con option) list | dcon of string * con option + | pkopt of exp + | commaOpt of unit + | cst of exp | csts of exp | cstopt of exp @@ -418,7 +421,8 @@ | m :: ms => [(DOpenConstraints (m, ms), s (OPENleft, mpathright))]) | CONSTRAINT cterm TWIDDLE cterm ([(DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))]) | EXPORT spath ([(DExport spath, s (EXPORTleft, spathright))]) - | TABLE SYMBOL COLON cterm cstopt([(DTable (SYMBOL, entable cterm, cstopt), s (TABLEleft, cstoptright))]) + | TABLE SYMBOL COLON cterm pkopt commaOpt cstopt([(DTable (SYMBOL, entable cterm, pkopt, cstopt), + s (TABLEleft, cstoptright))]) | SEQUENCE SYMBOL ([(DSequence SYMBOL, s (SEQUENCEleft, SYMBOLright))]) | CLASS SYMBOL EQ cexp (let val loc = s (CLASSleft, cexpright) @@ -513,6 +517,27 @@ tnames': tnameW (tnameW, []) | tnameW COMMA tnames' (#1 tnames', tnameW :: #2 tnames') +commaOpt: () + | COMMA () + +pkopt : (EVar (["Basis"], "no_primary_key", Infer), ErrorMsg.dummySpan) + | PRIMARY KEY tnames (let + val loc = s (PRIMARYleft, tnamesright) + + val e = (EVar (["Basis"], "primary_key", Infer), loc) + val e = (ECApp (e, #1 (#1 tnames)), loc) + val e = (ECApp (e, (CRecord (#2 tnames), loc)), loc) + val e = (EDisjointApp e, loc) + val e = (EDisjointApp e, loc) + + val witness = map (fn (c, _) => + (c, (EWild, loc))) + (#1 tnames :: #2 tnames) + val witness = (ERecord witness, loc) + in + (EApp (e, witness), loc) + end) + valis : vali ([vali]) | vali AND valis (vali :: valis) @@ -554,11 +579,11 @@ s (FUNCTORleft, sgn2right))) | INCLUDE sgn ((SgiInclude sgn, s (INCLUDEleft, sgnright))) | CONSTRAINT cterm TWIDDLE cterm ((SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))) - | TABLE SYMBOL COLON cterm cstopt(let - val loc = s (TABLEleft, ctermright) - in - (SgiTable (SYMBOL, entable cterm, cstopt), loc) - end) + | TABLE SYMBOL COLON cterm pkopt commaOpt cstopt (let + val loc = s (TABLEleft, ctermright) + in + (SgiTable (SYMBOL, entable cterm, pkopt, cstopt), loc) + end) | SEQUENCE SYMBOL (let val loc = s (SEQUENCEleft, SYMBOLright) val t = (CVar (["Basis"], "sql_sequence"), loc)
--- a/src/urweb.lex Tue Apr 07 15:04:07 2009 -0400 +++ b/src/urweb.lex Tue Apr 07 16:14:31 2009 -0400 @@ -367,6 +367,8 @@ <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> "KEY" => (Tokens.KEY (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 15:04:07 2009 -0400 +++ b/tests/cst.ur Tue Apr 07 16:14:31 2009 -0400 @@ -1,4 +1,6 @@ table t : {A : int, B : int} + PRIMARY KEY B, + CONSTRAINT UniA UNIQUE A, CONSTRAINT UniB UNIQUE B, CONSTRAINT UniBoth UNIQUE (A, B),