summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-07 12:24:31 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-07 12:24:31 -0400
commite52d6c0bc6e2e911515d21c6acc1e311a8e30db9 (patch)
treeb422a6ade536f96b318a9d9547f2f2c95562691a
parent69400f0524e8bcaa264eed203b8581992a4d1f7d (diff)
UNIQUE constraints
-rw-r--r--lib/ur/basis.urs14
-rw-r--r--src/cjr.sml2
-rw-r--r--src/cjr_print.sml43
-rw-r--r--src/cjrize.sml14
-rw-r--r--src/core.sml2
-rw-r--r--src/core_env.sml2
-rw-r--r--src/core_print.sml26
-rw-r--r--src/core_util.sml12
-rw-r--r--src/corify.sml6
-rw-r--r--src/elab.sml2
-rw-r--r--src/elab_env.sml2
-rw-r--r--src/elab_print.sml18
-rw-r--r--src/elab_util.sml12
-rw-r--r--src/elaborate.sml23
-rw-r--r--src/expl.sml2
-rw-r--r--src/expl_env.sml2
-rw-r--r--src/expl_print.sml18
-rw-r--r--src/explify.sml2
-rw-r--r--src/mono.sml2
-rw-r--r--src/mono_print.sml28
-rw-r--r--src/mono_util.sml5
-rw-r--r--src/monoize.sml44
-rw-r--r--src/pathcheck.sml34
-rw-r--r--src/reduce.sml3
-rw-r--r--src/shake.sml47
-rw-r--r--src/source.sml2
-rw-r--r--src/source_print.sml18
-rw-r--r--src/urweb.grm54
-rw-r--r--src/urweb.lex3
-rw-r--r--tests/cst.ur13
-rw-r--r--tests/cst.urp5
31 files changed, 343 insertions, 117 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 1cbca61d..dcf2a13d 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -124,6 +124,20 @@ val self : transaction client
con sql_table :: {Type} -> Type
+(*** Constraints *)
+
+con sql_constraints :: {Unit} -> {Type} -> Type
+con sql_constraint :: {Type} -> Type
+
+val no_constraint : fs ::: {Type} -> sql_constraints [] fs
+val one_constraint : fs ::: {Type} -> name :: Name -> sql_constraint fs -> sql_constraints [name] fs
+val join_constraints : names1 ::: {Unit} -> names2 ::: {Unit} -> fs ::: {Type} -> [names1 ~ names2]
+ => sql_constraints names1 fs -> sql_constraints names2 fs
+ -> sql_constraints (names1 ++ names2) fs
+
+val unique : rest ::: {Type} -> unique :: {Type} -> [unique ~ rest] => sql_constraint (unique ++ rest)
+
+
(*** Queries *)
con sql_query :: {{Type}} -> {Type} -> Type
diff --git a/src/cjr.sml b/src/cjr.sml
index 78c2e63b..7f8b2434 100644
--- a/src/cjr.sml
+++ b/src/cjr.sml
@@ -104,7 +104,7 @@ datatype decl' =
| 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
+ | DTable of string * (string * typ) list * (string * string) list
| DSequence of string
| DDatabase of {name : string, expunge : int, initialize : int}
| DPreparedStatements of (string * int) list
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index 54ec3cbf..9fc1511f 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -1435,7 +1435,7 @@ fun p_exp' par env (e, loc) =
val wontLeakAnything = notLeaky env false state
in
box [if wontLeakAnything then
- string "uw_begin_region(ctx), "
+ string "(uw_begin_region(ctx), "
else
box [],
string "({",
@@ -1585,7 +1585,11 @@ fun p_exp' par env (e, loc) =
box [],
string "acc;",
newline,
- string "})"]
+ string "})",
+ if wontLeakAnything then
+ string ")"
+ else
+ box []]
end
| EDml {dml, prepared} =>
@@ -1937,10 +1941,19 @@ fun p_decl env (dAll as (d, _) : decl) =
p_list_sep newline (p_fun env) vis,
newline]
end
- | DTable (x, _) => box [string "/* SQL table ",
- string x,
- string " */",
- newline]
+ | 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]
| DSequence x => box [string "/* SQL sequence ",
string x,
string " */",
@@ -2454,7 +2467,7 @@ fun p_file env (ds, ps) =
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
@@ -2798,7 +2811,7 @@ fun p_sql env (ds, _) =
(fn (dAll as (d, _), env) =>
let
val pp = case d of
- DTable (s, xts) =>
+ DTable (s, xts, csts) =>
box [string "CREATE TABLE ",
string s,
string "(",
@@ -2807,6 +2820,20 @@ fun p_sql env (ds, _) =
string (CharVector.map Char.toLower x),
space,
p_sqltype env (t, ErrorMsg.dummySpan)]) xts,
+ case csts of
+ [] => box []
+ | _ => box [string ","],
+ cut,
+ p_list_sep (box [string ",", newline])
+ (fn (x, c) =>
+ box [string "CONSTRAINT",
+ space,
+ string s,
+ string "_",
+ string x,
+ space,
+ string c]) csts,
+ newline,
string ");",
newline,
newline]
diff --git a/src/cjrize.sml b/src/cjrize.sml
index 5e4b647a..839c0c57 100644
--- a/src/cjrize.sml
+++ b/src/cjrize.sml
@@ -524,7 +524,7 @@ fun cifyDecl ((d, loc), sm) =
(NONE, SOME (ek, "/" ^ s, n, ts, t, L'.ServerAndPullAndPush), sm)
end
- | L.DTable (s, xts) =>
+ | L.DTable (s, xts, e) =>
let
val (xts, sm) = ListUtil.foldlMap (fn ((x, t), sm) =>
let
@@ -532,8 +532,18 @@ fun cifyDecl ((d, loc), sm) =
in
((x, t), sm)
end) sm xts
+
+ fun flatten e =
+ case #1 e of
+ L.ERecord [] => []
+ | L.ERecord [(x, (L.EPrim (Prim.String v), _), _)] => [(x, v)]
+ | 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)];
+ [])
in
- (SOME (L'.DTable (s, xts), loc), NONE, sm)
+ (SOME (L'.DTable (s, xts, flatten e), loc), NONE, sm)
end
| L.DSequence s =>
(SOME (L'.DSequence s, loc), NONE, sm)
diff --git a/src/core.sml b/src/core.sml
index b384c576..74ef138c 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -130,7 +130,7 @@ datatype decl' =
| 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
+ | DTable of string * int * con * string * exp
| DSequence of string * int * string
| DDatabase of string
| DCookie of string * int * con * string
diff --git a/src/core_env.sml b/src/core_env.sml
index dd77e3fb..d1e956d8 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -313,7 +313,7 @@ fun declBinds env (d, loc) =
| 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) =>
+ | DTable (x, n, c, s, _) =>
let
val t = (CApp ((CFfi ("Basis", "sql_table"), loc), c), loc)
in
diff --git a/src/core_print.sml b/src/core_print.sml
index cc6e5428..d68ba288 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -546,17 +546,21 @@ fun p_decl env (dAll as (d, _) : decl) =
space,
(p_con env (#2 (E.lookupENamed env n))
handle E.UnboundNamed _ => string "UNBOUND")]
- | DTable (x, n, c, s) => box [string "table",
- space,
- p_named x n,
- space,
- string "as",
- space,
- string s,
- space,
- string ":",
- space,
- p_con env c]
+ | 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]
| DSequence (x, n, s) => box [string "sequence",
space,
p_named x n,
diff --git a/src/core_util.sml b/src/core_util.sml
index b1d07b79..b342f2f7 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -933,10 +933,12 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
(DValRec vis', loc))
end
| DExport _ => S.return2 dAll
- | DTable (x, n, c, s) =>
- S.map2 (mfc ctx c,
+ | DTable (x, n, c, s, e) =>
+ S.bind2 (mfc ctx c,
fn c' =>
- (DTable (x, n, c', s), loc))
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (DTable (x, n, c', s, e'), loc)))
| DSequence _ => S.return2 dAll
| DDatabase _ => S.return2 dAll
| DCookie (x, n, c, s) =>
@@ -1058,7 +1060,7 @@ fun mapfoldB (all as {bind, ...}) =
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) =>
+ | DTable (x, n, c, s, _) =>
let
val t = (CApp ((CFfi ("Basis", "sql_table"), #2 d'), c), #2 d')
in
@@ -1134,7 +1136,7 @@ val maxName = foldl (fn ((d, _) : decl, count) =>
| 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
diff --git a/src/corify.sml b/src/corify.sml
index 9ca6c915..fc8bb1de 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -976,12 +976,12 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
end
| _ => raise Fail "Non-const signature for 'export'")
- | L.DTable (_, x, n, c) =>
+ | L.DTable (_, x, n, c, e) =>
let
val (st, n) = St.bindVal st x n
val s = relify (doRestify (mods, x))
in
- ([(L'.DTable (x, n, corifyCon st c, s), loc)], st)
+ ([(L'.DTable (x, n, corifyCon st c, s, corifyExp st e), loc)], st)
end
| L.DSequence (_, x, n) =>
let
@@ -1052,7 +1052,7 @@ fun maxName ds = foldl (fn ((d, _), n) =>
| 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'))
diff --git a/src/elab.sml b/src/elab.sml
index 3fed1918..dd2952d2 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -166,7 +166,7 @@ datatype decl' =
| DFfiStr of string * int * sgn
| DConstraint of con * con
| DExport of int * sgn * str
- | DTable of int * string * int * con
+ | DTable of int * string * int * con * exp
| DSequence of int * string * int
| DClass of string * int * kind * con
| DDatabase of string
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 370e504f..7adc8dd9 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1532,7 +1532,7 @@ fun declBinds env (d, loc) =
| DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
| DConstraint _ => env
| DExport _ => env
- | DTable (tn, x, n, c) =>
+ | DTable (tn, x, n, c, _) =>
let
val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc)
in
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 64d8cfab..f98592cc 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -740,13 +740,17 @@ fun p_decl env (dAll as (d, _) : decl) =
string ":",
space,
p_sgn env sgn]
- | DTable (_, x, n, c) => box [string "table",
- space,
- p_named x n,
- space,
- string ":",
- space,
- p_con env c]
+ | 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]
| DSequence (_, x, n) => box [string "sequence",
space,
p_named x n]
diff --git a/src/elab_util.sml b/src/elab_util.sml
index e2dd0ce6..6700686d 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -766,7 +766,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
bind (ctx, Str (x, sgn))
| DConstraint _ => ctx
| DExport _ => ctx
- | DTable (tn, x, n, c) =>
+ | DTable (tn, x, n, c, _) =>
bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "sql_table"), loc),
c), loc)))
| DSequence (tn, x, n) =>
@@ -864,10 +864,12 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
fn str' =>
(DExport (en, sgn', str'), loc)))
- | DTable (tn, x, n, c) =>
- S.map2 (mfc ctx c,
+ | DTable (tn, x, n, c, e) =>
+ S.bind2 (mfc ctx c,
fn c' =>
- (DTable (tn, x, n, c'), loc))
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (DTable (tn, x, n, c', e'), loc)))
| DSequence _ => S.return2 dAll
| DClass (x, n, k, c) =>
@@ -1018,7 +1020,7 @@ and maxNameDecl (d, _) =
| 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)
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 81af6a79..0beab9e7 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1126,11 +1126,11 @@
else
(e, t, [])
| t => (e, t, [])
- in
- case infer of
- L.DontInfer => (e, t, [])
- | _ => unravel (t, e)
- end
+ in
+ case infer of
+ L.DontInfer => (e, t, [])
+ | _ => unravel (t, e)
+ end
fun elabPat (pAll as (p, loc), (env, bound)) =
let
@@ -2319,7 +2319,7 @@ fun sgiOfDecl (d, loc) =
| 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) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)]
+ | L'.DTable (tn, x, n, c, _) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), 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 _ => []
@@ -3265,13 +3265,20 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs)) =
([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
end
- | L.DTable (x, c) =>
+ | L.DTable (x, c, e) =>
let
val (c', k, gs') = elabCon (env, denv) c
val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
+ val (e', et, gs'') = elabExp (env, denv) e
+
+ val names = cunif (loc, (L'.KRecord (L'.KUnit, loc), loc))
+ val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
+ val cst = (L'.CApp (cst, names), loc)
+ val cst = (L'.CApp (cst, c'), loc)
in
checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
- ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
+ checkCon env e' et cst;
+ ([(L'.DTable (!basis_r, x, n, c', e'), loc)], (env, denv, gs'' @ enD gs' @ gs))
end
| L.DSequence x =>
let
diff --git a/src/expl.sml b/src/expl.sml
index d7138620..a347a8e8 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -141,7 +141,7 @@ datatype decl' =
| DStr of string * int * sgn * str
| DFfiStr of string * int * sgn
| DExport of int * sgn * str
- | DTable of int * string * int * con
+ | DTable of int * string * int * con * exp
| DSequence of int * string * int
| DDatabase of string
| DCookie of int * string * int * con
diff --git a/src/expl_env.sml b/src/expl_env.sml
index 403a826a..f4e16cb5 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -298,7 +298,7 @@ fun declBinds env (d, loc) =
| 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) =>
+ | DTable (tn, x, n, c, _) =>
let
val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc)
in
diff --git a/src/expl_print.sml b/src/expl_print.sml
index e7fb51f6..c7a506b1 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -663,13 +663,17 @@ fun p_decl env (dAll as (d, _) : decl) =
string ":",
space,
p_sgn env sgn]
- | DTable (_, x, n, c) => box [string "table",
- space,
- p_named x n,
- space,
- string ":",
- space,
- p_con env c]
+ | 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]
| DSequence (_, x, n) => box [string "sequence",
space,
p_named x n]
diff --git a/src/explify.sml b/src/explify.sml
index f9f58c65..d567bde3 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -178,7 +178,7 @@ fun explifyDecl (d, loc : EM.span) =
| 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) => SOME (L'.DTable (nt, x, n, explifyCon c), loc)
+ | L.DTable (nt, x, n, c, e) => SOME (L'.DTable (nt, x, n, explifyCon c, explifyExp e), 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)
diff --git a/src/mono.sml b/src/mono.sml
index 02afb2c0..5a65a9f9 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -121,7 +121,7 @@ datatype decl' =
| DValRec of (string * int * typ * exp * string) list
| DExport of Core.export_kind * string * int * typ list * typ
- | DTable of string * (string * typ) list
+ | DTable of string * (string * typ) list * exp
| DSequence of string
| DDatabase of {name : string, expunge : int, initialize : int}
diff --git a/src/mono_print.sml b/src/mono_print.sml
index a8ece085..935f8368 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -403,18 +403,22 @@ fun p_decl env (dAll as (d, _) : decl) =
space,
p_typ env t]
- | DTable (s, xts) => 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 "*)"]
+ | 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 "*)"]
| DSequence s => box [string "(* SQL sequence ",
string s,
string "*)"]
diff --git a/src/mono_util.sml b/src/mono_util.sml
index 9455435c..ca5cf5cb 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -465,7 +465,10 @@ fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} =
S.map2 (mft t,
fn t' =>
(DExport (ek, s, n, ts', t'), loc)))
- | DTable _ => S.return2 dAll
+ | DTable (s, xts, e) =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (DTable (s, xts, e'), loc))
| DSequence _ => S.return2 dAll
| DDatabase _ => S.return2 dAll
| DJavaScript _ => S.return2 dAll
diff --git a/src/monoize.sml b/src/monoize.sml
index 620e43a5..af414c08 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -149,6 +149,10 @@ fun monoType env =
(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", "sql_constraints"), _), _), _), _) =>
+ (L'.TFfi ("Basis", "sql_constraints"), loc)
+ | L.CApp ((L.CFfi ("Basis", "sql_constraint"), _), _) =>
+ (L'.TFfi ("Basis", "string"), loc)
| L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_subset"), _), _), _), _) =>
(L'.TRecord [], loc)
@@ -1155,6 +1159,32 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
fm)
end
+ | L.ECApp ((L.EFfi ("Basis", "no_constraint"), _), _) =>
+ ((L'.ERecord [], loc),
+ fm)
+ | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "one_constraint"), _), _), _), (L.CName name, _)) =>
+ ((L'.EAbs ("c",
+ (L'.TFfi ("Basis", "string"), loc),
+ (L'.TFfi ("Basis", "sql_constraints"), loc),
+ (L'.ERecord [(name, (L'.ERel 0, loc), (L'.TFfi ("Basis", "string"), loc))], loc)), loc),
+ fm)
+ | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "join_constraints"), _), _), _), _), _), _) =>
+ let
+ val constraints = (L'.TFfi ("Basis", "sql_constraints"), loc)
+ in
+ ((L'.EAbs ("cs1", constraints, (L'.TFun (constraints, constraints), loc),
+ (L'.EAbs ("cs2", constraints, constraints,
+ (L'.EStrcat ((L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc),
+ fm)
+ end
+
+ | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "unique"), _), _), _),
+ (L.CRecord (_, unique), _)) =>
+ ((L'.EPrim (Prim.String ("UNIQUE ("
+ ^ String.concatWith ", " (map (fn (x, _) => "uw_" ^ monoName env x) unique)
+ ^ ")")), loc),
+ fm)
+
| L.EFfiApp ("Basis", "dml", [e]) =>
let
val (e, fm) = monoExp (env, st, fm) e
@@ -2451,19 +2481,21 @@ fun monoDecl (env, fm) (all as (d, loc)) =
in
SOME (env, fm, [(L'.DExport (ek, s, n, ts, ran), loc)])
end
- | L.DTable (x, n, (L.CRecord (_, xts), _), s) =>
+ | L.DTable (x, n, (L.CRecord (_, xts), _), s, e) =>
let
val t = (L.CFfi ("Basis", "string"), loc)
val t' = (L'.TFfi ("Basis", "string"), loc)
val s = "uw_" ^ s
- val e = (L'.EPrim (Prim.String s), loc)
+ val e_name = (L'.EPrim (Prim.String s), loc)
val xts = map (fn (x, t) => (monoName env x, monoType env t)) xts
+
+ val (e, fm) = monoExp (env, St.empty, fm) e
in
SOME (Env.pushENamed env x n t NONE s,
fm,
- [(L'.DTable (s, xts), loc),
- (L'.DVal (x, n, t', e, s), loc)])
+ [(L'.DTable (s, xts, e), loc),
+ (L'.DVal (x, n, t', e_name, s), loc)])
end
| L.DTable _ => poly ()
| L.DSequence (x, n, s) =>
@@ -2583,7 +2615,7 @@ fun monoize env file =
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
@@ -2628,7 +2660,7 @@ fun monoize env file =
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
diff --git a/src/pathcheck.sml b/src/pathcheck.sml
index 036d286f..6771e628 100644
--- a/src/pathcheck.sml
+++ b/src/pathcheck.sml
@@ -38,6 +38,13 @@ structure SS = BinarySetFn(struct
fun checkDecl ((d, loc), (funcs, rels)) =
let
+ fun doFunc s =
+ (if SS.member (funcs, s) then
+ E.errorAt loc ("Duplicate function path " ^ s)
+ else
+ ();
+ (SS.add (funcs, s), rels))
+
fun doRel s =
(if SS.member (rels, s) then
E.errorAt loc ("Duplicate table/sequence path " ^ s)
@@ -46,14 +53,27 @@ fun checkDecl ((d, loc), (funcs, rels)) =
(funcs, SS.add (rels, s)))
in
case d of
- DExport (_, s, _, _, _) =>
- (if SS.member (funcs, s) then
- E.errorAt loc ("Duplicate function path " ^ s)
- else
- ();
- (SS.add (funcs, s), rels))
+ DExport (_, s, _, _, _) => doFunc s
- | DTable (s, _) => doRel s
+ | DTable (s, _, e) =>
+ let
+ fun constraints (e, rels) =
+ case #1 e of
+ ERecord [(s', _, _)] =>
+ let
+ val s' = s ^ "_" ^ s'
+ in
+ if SS.member (rels, s') then
+ E.errorAt loc ("Duplicate constraint path " ^ s')
+ else
+ ();
+ SS.add (rels, s')
+ end
+ | EStrcat (e1, e2) => constraints (e2, constraints (e1, rels))
+ | _ => rels
+ in
+ (funcs, constraints (e, #2 (doRel s)))
+ end
| DSequence s => doRel s
| _ => (funcs, rels)
diff --git a/src/reduce.sml b/src/reduce.sml
index 8664d38d..6754d708 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -461,7 +461,8 @@ fun reduce file =
((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') => ((DTable (s, n, con namedC [] c, s'), loc), st)
+ | DTable (s, n, c, s', e) => ((DTable (s, n, con namedC [] c, s',
+ exp (namedC, namedE) [] e), loc), st)
| DSequence _ => (d, st)
| DDatabase _ => (d, st)
| DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st)
diff --git a/src/shake.sml b/src/shake.sml
index 4df64efa..2f873e94 100644
--- a/src/shake.sml
+++ b/src/shake.sml
@@ -46,11 +46,26 @@ val dummye = (EPrim (Prim.String ""), ErrorMsg.dummySpan)
fun shake file =
let
- val (page_es, table_cs) =
+ val usedVars = U.Exp.fold {kind = fn (_, st) => st,
+ con = fn (c, st as (es, cs)) =>
+ case c of
+ CNamed n => (es, IS.add (cs, n))
+ | _ => st,
+ exp = fn (e, st as (es, cs)) =>
+ case e of
+ ENamed n => (IS.add (es, n), cs)
+ | _ => st}
+
+ val (usedE, usedC, table_cs) =
List.foldl
- (fn ((DExport (_, n), _), (page_es, table_cs)) => (n :: page_es, table_cs)
- | ((DTable (_, _, c, _), _), (page_es, table_cs)) => (page_es, c :: table_cs)
- | (_, acc) => acc) ([], []) file
+ (fn ((DExport (_, n), _), (usedE, usedC, table_cs)) => (IS.add (usedE, n), usedE, table_cs)
+ | ((DTable (_, _, c, _, e), _), (usedE, usedC, table_cs)) =>
+ let
+ val (usedE, usedC) = usedVars (usedE, usedC) e
+ in
+ (usedE, usedC, c :: table_cs)
+ end
+ | (_, acc) => acc) (IS.empty, IS.empty, []) file
val (cdef, edef) = foldl (fn ((DCon (_, n, _, c), _), (cdef, edef)) => (IM.insert (cdef, n, [c]), edef)
| ((DDatatype (_, n, _, xncs), _), (cdef, edef)) =>
@@ -64,7 +79,7 @@ fun shake file =
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)))
@@ -122,17 +137,17 @@ fun shake file =
and shakeExp s = U.Exp.fold {kind = kind, con = con, exp = exp} s
- val s = {con = IS.empty, exp = IS.addList (IS.empty, page_es)}
-
- val s = foldl (fn (n, s) =>
- case IM.find (edef, n) of
- NONE => raise Fail "Shake: Couldn't find 'val'"
- | SOME (ns, t, e) =>
- let
- val s = shakeExp (shakeCon s t) e
- in
- foldl (fn (n, s) => exp (ENamed n, s)) s ns
- end) s page_es
+ val s = {con = usedC, exp = usedE}
+
+ val s = IS.foldl (fn (n, s) =>
+ case IM.find (edef, n) of
+ NONE => raise Fail "Shake: Couldn't find 'val'"
+ | SOME (ns, t, e) =>
+ let
+ val s = shakeExp (shakeCon s t) e
+ in
+ foldl (fn (n, s) => exp (ENamed n, s)) s ns
+ end) s usedE
val s = foldl (fn (c, s) => shakeCon s c) s table_cs
in
diff --git a/src/source.sml b/src/source.sml
index 9ef14fd9..42927ef3 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -160,7 +160,7 @@ datatype decl' =
| DConstraint of con * con
| DOpenConstraints of string * string list
| DExport of str
- | DTable of string * con
+ | DTable of string * con * exp
| DSequence of string
| DClass of string * kind * con
| DDatabase of string
diff --git a/src/source_print.sml b/src/source_print.sml
index 8d8b28c3..d1c9b6df 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -588,13 +588,17 @@ fun p_decl ((d, _) : decl) =
| DExport str => box [string "export",
space,
p_str str]
- | DTable (x, c) => box [string "table",
- space,
- string x,
- space,
- string ":",
- space,
- p_con c]
+ | DTable (x, c, e) => box [string "table",
+ space,
+ string x,
+ space,
+ string ":",
+ space,
+ p_con c,
+ space,
+ string "constraints",
+ space,
+ p_exp e]
| DSequence x => box [string "sequence",
space,
string x]
diff --git a/src/urweb.grm b/src/urweb.grm
index 98ba295a..784c62ee 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -208,6 +208,7 @@ fun tagIn bt =
| INSERT | INTO | VALUES | UPDATE | SET | DELETE | NULL | IS
| CURRENT_TIMESTAMP
| NE | LT | LE | GT | GE
+ | CCONSTRAINT | UNIQUE
%nonterm
file of decl list
@@ -222,6 +223,10 @@ fun tagIn bt =
| dcons of (string * con option) list
| dcon of string * con option
+ | cst of exp
+ | csts of exp
+ | cstopt of exp
+
| sgn of sgn
| sgntm of sgn
| sgi of sgn_item
@@ -289,6 +294,9 @@ fun tagIn bt =
| query1 of exp
| tables of (con * exp) list
| tname of con
+ | tnameW of (con * con)
+ | tnames of con
+ | tnames' of (con * con) list
| table of con * exp
| tident of con
| fident of con
@@ -410,7 +418,7 @@ decl : CON SYMBOL cargl2 kopt EQ cexp (let
| 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 cexp ([(DTable (SYMBOL, entable cexp), s (TABLEleft, cexpright))])
+ | TABLE SYMBOL COLON cterm cstopt([(DTable (SYMBOL, entable cterm, cstopt), s (TABLEleft, cstoptright))])
| SEQUENCE SYMBOL ([(DSequence SYMBOL, s (SEQUENCEleft, SYMBOLright))])
| CLASS SYMBOL EQ cexp (let
val loc = s (CLASSleft, cexpright)
@@ -460,6 +468,50 @@ vali : SYMBOL eargl2 copt EQ eexp (let
copt : (NONE)
| COLON cexp (SOME cexp)
+cstopt : (EVar (["Basis"], "no_constraint", Infer), dummy)
+ | csts (csts)
+
+csts : CCONSTRAINT tname cst (let
+ val loc = s (CCONSTRAINTleft, cstright)
+
+ val e = (EVar (["Basis"], "one_constraint", Infer), loc)
+ val e = (ECApp (e, tname), loc)
+ in
+ (EApp (e, cst), loc)
+ end)
+ | csts COMMA csts (let
+ val loc = s (csts1left, csts2right)
+
+ val e = (EVar (["Basis"], "join_constraints", Infer), loc)
+ val e = (EApp (e, csts1), loc)
+ in
+ (EApp (e, csts2), loc)
+ end)
+ | LBRACE LBRACE eexp RBRACE RBRACE (eexp)
+
+cst : UNIQUE tnames (let
+ val loc = s (UNIQUEleft, tnamesright)
+
+ val e = (EVar (["Basis"], "unique", Infer), loc)
+ val e = (ECApp (e, tnames), loc)
+ in
+ (EDisjointApp e, loc)
+ end)
+ | LBRACE eexp RBRACE (eexp)
+
+tnameW : tname (let
+ val loc = s (tnameleft, tnameright)
+ in
+ (tname, (CWild (KType, loc), loc))
+ end)
+
+tnames : tnameW (CRecord [tnameW], s (tnameWleft, tnameWright))
+ | LPAREN tnames' RPAREN (CRecord tnames', s (LPARENleft, RPARENright))
+ | LBRACE LBRACE cexp RBRACE RBRACE (cexp)
+
+tnames': tnameW ([tnameW])
+ | tnameW COMMA tnames' (tnameW :: tnames')
+
valis : vali ([vali])
| vali AND valis (vali :: valis)
diff --git a/src/urweb.lex b/src/urweb.lex
index 4a7ceaeb..735d230d 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -365,6 +365,9 @@ notags = [^<{\n]+;
<INITIAL> "NULL" => (Tokens.NULL (pos yypos, pos yypos + size yytext));
<INITIAL> "IS" => (Tokens.IS (pos yypos, pos yypos + size yytext));
+<INITIAL> "CONSTRAINT"=> (Tokens.CCONSTRAINT (pos yypos, pos yypos + size yytext));
+<INITIAL> "UNIQUE" => (Tokens.UNIQUE (pos yypos, pos yypos + size yytext));
+
<INITIAL> "CURRENT_TIMESTAMP" => (Tokens.CURRENT_TIMESTAMP (pos yypos, pos yypos + size yytext));
<INITIAL> {id} => (Tokens.SYMBOL (yytext, pos yypos, pos yypos + size yytext));
diff --git a/tests/cst.ur b/tests/cst.ur
new file mode 100644
index 00000000..104a9f34
--- /dev/null
+++ b/tests/cst.ur
@@ -0,0 +1,13 @@
+table t : {A : int, B : int}
+ CONSTRAINT UniA UNIQUE A,
+ CONSTRAINT UniB UNIQUE B,
+ CONSTRAINT UniBoth UNIQUE (A, B),
+
+ CONSTRAINT UniAm UNIQUE {#A},
+ CONSTRAINT UniAm2 UNIQUE {{[A = _]}},
+ CONSTRAINT UniAm3 {unique [[A = _]] !},
+ {{one_constraint [#UniAm4] (unique [[A = _]] !)}}
+
+fun main () : transaction page =
+ queryI (SELECT * FROM t) (fn _ => return ());
+ return <xml/>
diff --git a/tests/cst.urp b/tests/cst.urp
new file mode 100644
index 00000000..b9deaa44
--- /dev/null
+++ b/tests/cst.urp
@@ -0,0 +1,5 @@
+debug
+database dbname=cst
+sql cst.sql
+
+cst