summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/ur/basis.urs52
-rw-r--r--src/core.sml2
-rw-r--r--src/core_env.sml8
-rw-r--r--src/core_print.sml30
-rw-r--r--src/core_util.sml19
-rw-r--r--src/corify.sml6
-rw-r--r--src/defunc.sig32
-rw-r--r--src/defunc.sml260
-rw-r--r--src/elab.sml2
-rw-r--r--src/elab_env.sml8
-rw-r--r--src/elab_print.sml22
-rw-r--r--src/elab_util.sml21
-rw-r--r--src/elaborate.sml132
-rw-r--r--src/expl.sml2
-rw-r--r--src/expl_env.sml8
-rw-r--r--src/expl_print.sml22
-rw-r--r--src/explify.sml2
-rw-r--r--src/monoize.sml50
-rw-r--r--src/reduce.sml5
-rw-r--r--src/shake.sml4
-rw-r--r--src/sources3
-rw-r--r--src/urweb.grm19
-rw-r--r--tests/cst.ur9
23 files changed, 239 insertions, 479 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index dcf2a13d..4e926f87 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -122,20 +122,27 @@ val self : transaction client
(** SQL *)
-con sql_table :: {Type} -> Type
+con sql_table :: {Type} -> {{Unit}} -> Type
(*** Constraints *)
-con sql_constraints :: {Unit} -> {Type} -> Type
-con sql_constraint :: {Type} -> Type
+con sql_constraints :: {Type} -> {{Unit}} -> Type
+(* Arguments: column types, uniqueness implications of constraints *)
-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
+con sql_constraint :: {Type} -> {Unit} -> Type
-val unique : rest ::: {Type} -> unique :: {Type} -> [unique ~ rest] => sql_constraint (unique ++ rest)
+val no_constraint : fs ::: {Type} -> sql_constraints fs []
+val one_constraint : fs ::: {Type} -> unique ::: {Unit} -> name :: Name
+ -> sql_constraint fs unique
+ -> sql_constraints fs [name = unique]
+val join_constraints : fs ::: {Type}
+ -> uniques1 ::: {{Unit}} -> uniques2 ::: {{Unit}} -> [uniques1 ~ uniques2]
+ => 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)
(*** Queries *)
@@ -151,17 +158,18 @@ val sql_subset : keep_drop :: {({Type} * {Type})}
(map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop)
val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
-val sql_query1 : tables ::: {{Type}}
+val sql_query1 : tables ::: {({Type} * {{Unit}})}
-> grouped ::: {{Type}}
-> selectedFields ::: {{Type}}
-> selectedExps ::: {Type}
- -> {From : $(map sql_table tables),
- Where : sql_exp tables [] [] bool,
- GroupBy : sql_subset tables grouped,
- Having : sql_exp grouped tables [] bool,
+ -> {From : $(map (fn p :: ({Type} * {{Unit}}) => sql_table p.1 p.2) tables),
+ Where : sql_exp (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [] [] bool,
+ GroupBy : sql_subset (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) grouped,
+ Having : sql_exp grouped (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [] bool,
SelectFields : sql_subset grouped selectedFields,
- SelectExps : $(map (sql_exp grouped tables []) selectedExps) }
- -> sql_query1 tables selectedFields selectedExps
+ SelectExps : $(map (sql_exp grouped (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) [])
+ selectedExps) }
+ -> sql_query1 (map (fn p :: ({Type} * {{Unit}}) => p.1) tables) selectedFields selectedExps
type sql_relop
val sql_union : sql_relop
@@ -321,20 +329,20 @@ val query : tables ::: {{Type}} -> exps ::: {Type}
type dml
val dml : dml -> transaction unit
-val insert : fields ::: {Type}
- -> sql_table fields
+val insert : fields ::: {Type} -> uniques ::: {{Unit}}
+ -> sql_table fields uniques
-> $(map (fn t :: Type => sql_exp [] [] [] t) fields)
-> dml
-val update : unchanged ::: {Type} -> changed :: {Type} ->
+val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} ->
[changed ~ unchanged] =>
$(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed)
- -> sql_table (changed ++ unchanged)
+ -> sql_table (changed ++ unchanged) uniques
-> sql_exp [T = changed ++ unchanged] [] [] bool
-> dml
-val delete : fields ::: {Type}
- -> sql_table fields
+val delete : fields ::: {Type} -> uniques ::: {{Unit}}
+ -> sql_table fields uniques
-> sql_exp [T = fields] [] [] bool
-> dml
diff --git a/src/core.sml b/src/core.sml
index 74ef138c..687b913f 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 * exp
+ | DTable of string * int * con * string * exp * con
| 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 d1e956d8..4c4cc68f 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -313,11 +313,13 @@ 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, _, cc) =>
let
- val t = (CApp ((CFfi ("Basis", "sql_table"), loc), c), loc)
+ val ct = (CFfi ("Basis", "sql_table"), loc)
+ val ct = (CApp (ct, c), loc)
+ val ct = (CApp (ct, cc), loc)
in
- pushENamed env x n t NONE s
+ pushENamed env x n ct NONE s
end
| DSequence (x, n, s) =>
let
diff --git a/src/core_print.sml b/src/core_print.sml
index d68ba288..216cc8ac 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -546,21 +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, 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, 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 b342f2f7..df8bb271 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -933,12 +933,14 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
(DValRec vis', loc))
end
| DExport _ => S.return2 dAll
- | DTable (x, n, c, s, e) =>
+ | DTable (x, n, c, s, e, cc) =>
S.bind2 (mfc ctx c,
fn c' =>
- S.map2 (mfe ctx e,
+ S.bind2 (mfe ctx e,
fn e' =>
- (DTable (x, n, c', s, e'), loc)))
+ S.map2 (mfc ctx cc,
+ fn cc' =>
+ (DTable (x, n, c', s, e', cc'), loc))))
| DSequence _ => S.return2 dAll
| DDatabase _ => S.return2 dAll
| DCookie (x, n, c, s) =>
@@ -1060,11 +1062,14 @@ 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, _, cc) =>
let
- val t = (CApp ((CFfi ("Basis", "sql_table"), #2 d'), c), #2 d')
+ val loc = #2 d'
+ val ct = (CFfi ("Basis", "sql_table"), loc)
+ val ct = (CApp (ct, c), loc)
+ val ct = (CApp (ct, cc), loc)
in
- bind (ctx, NamedE (x, n, t, NONE, s))
+ bind (ctx, NamedE (x, n, ct, NONE, s))
end
| DSequence (x, n, s) =>
let
@@ -1136,7 +1141,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 fc8bb1de..3387e73a 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, e) =>
+ | L.DTable (_, x, n, c, e, 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), loc)], st)
+ ([(L'.DTable (x, n, corifyCon st c, s, corifyExp st e, corifyCon st cc), 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/defunc.sig b/src/defunc.sig
deleted file mode 100644
index 6e8f2136..00000000
--- a/src/defunc.sig
+++ /dev/null
@@ -1,32 +0,0 @@
-(* Copyright (c) 2008, Adam Chlipala
- * All rights reserved.
- *
- * Redistribution and use in source and binary forms, with or without
- * modification, are permitted provided that the following conditions are met:
- *
- * - Redistributions of source code must retain the above copyright notice,
- * this list of conditions and the following disclaimer.
- * - Redistributions in binary form must reproduce the above copyright notice,
- * this list of conditions and the following disclaimer in the documentation
- * and/or other materials provided with the distribution.
- * - The names of contributors may not be used to endorse or promote products
- * derived from this software without specific prior written permission.
- *
- * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
- * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
- * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
- * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
- * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
- * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
- * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
- * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
- * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
- * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
- * POSSIBILITY OF SUCH DAMAGE.
- *)
-
-signature DEFUNC = sig
-
- val defunc : Core.file -> Core.file
-
-end
diff --git a/src/defunc.sml b/src/defunc.sml
deleted file mode 100644
index 7a17d1dc..00000000
--- a/src/defunc.sml
+++ /dev/null
@@ -1,260 +0,0 @@
-(* Copyright (c) 2008, Adam Chlipala
- * All rights reserved.
- *
- * Redistribution and use in source and binary forms, with or without
- * modification, are permitted provided that the following conditions are met:
- *
- * - Redistributions of source code must retain the above copyright notice,
- * this list of conditions and the following disclaimer.
- * - Redistributions in binary form must reproduce the above copyright notice,
- * this list of conditions and the following disclaimer in the documentation
- * and/or other materials provided with the distribution.
- * - The names of contributors may not be used to endorse or promote products
- * derived from this software without specific prior written permission.
- *
- * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
- * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
- * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
- * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
- * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
- * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
- * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
- * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
- * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
- * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
- * POSSIBILITY OF SUCH DAMAGE.
- *)
-
-structure Defunc :> DEFUNC = struct
-
-open Core
-
-structure E = CoreEnv
-structure U = CoreUtil
-
-structure IS = IntBinarySet
-
-val functionInside = U.Con.exists {kind = fn _ => false,
- con = fn TFun _ => true
- | CFfi ("Basis", "transaction") => true
- | _ => false}
-
-val freeVars = U.Exp.foldB {kind = fn (_, _, xs) => xs,
- con = fn (_, _, xs) => xs,
- exp = fn (bound, e, xs) =>
- case e of
- ERel x =>
- if x >= bound then
- IS.add (xs, x - bound)
- else
- xs
- | _ => xs,
- bind = fn (bound, b) =>
- case b of
- U.Exp.RelE _ => bound + 1
- | _ => bound}
- 0 IS.empty
-
-fun positionOf (v : int, ls) =
- let
- fun pof (pos, ls) =
- case ls of
- [] => raise Fail "Defunc.positionOf"
- | v' :: ls' =>
- if v = v' then
- pos
- else
- pof (pos + 1, ls')
- in
- pof (0, ls)
- end
-
-fun squish fvs =
- U.Exp.mapB {kind = fn _ => fn k => k,
- con = fn _ => fn c => c,
- exp = fn bound => fn e =>
- case e of
- ERel x =>
- if x >= bound then
- ERel (positionOf (x - bound, fvs) + bound)
- else
- e
- | _ => e,
- bind = fn (bound, b) =>
- case b of
- U.Exp.RelE _ => bound + 1
- | _ => bound}
- 0
-
-fun default (_, x, st) = (x, st)
-
-datatype 'a search =
- Yes
- | No
- | Maybe of 'a
-
-structure EK = struct
-type ord_key = exp
-val compare = U.Exp.compare
-end
-
-structure EM = BinaryMapFn(EK)
-
-type state = {
- maxName : int,
- funcs : int EM.map,
- vis : (string * int * con * exp * string) list
-}
-
-fun exp (env, e, st) =
- case e of
- ERecord xes =>
- let
- val (xes, st) =
- ListUtil.foldlMap
- (fn (tup as (fnam as (CName x, loc), e, xt), st) =>
- if (x <> "Link" andalso x <> "Action")
- orelse case #1 e of
- ENamed _ => true
- | _ => false then
- (tup, st)
- else
- let
- fun needsAttention (e, _) =
- case e of
- ENamed f => Maybe (#2 (E.lookupENamed env f))
- | EApp (f, _) =>
- (case needsAttention f of
- No => No
- | Yes => Yes
- | Maybe t =>
- case t of
- (TFun (dom, _), _) =>
- if functionInside dom then
- Yes
- else
- No
- | _ => No)
- | _ => No
-
- fun headSymbol (e, _) =
- case e of
- ENamed f => f
- | EApp (e, _) => headSymbol e
- | _ => raise Fail "Defunc: headSymbol"
-
- fun rtype (e, _) =
- case e of
- ENamed f => #2 (E.lookupENamed env f)
- | EApp (f, _) =>
- (case rtype f of
- (TFun (_, ran), _) => ran
- | _ => raise Fail "Defunc: rtype [1]")
- | _ => raise Fail "Defunc: rtype [2]"
- in
- (*Print.prefaces "Found one!"
- [("e", CorePrint.p_exp env e)];*)
- case needsAttention e of
- Yes =>
- let
- (*val () = print "Yes\n"*)
- val f = headSymbol e
-
- val fvs = IS.listItems (freeVars e)
-
- val e = squish fvs e
- val (e, t) = foldl (fn (n, (e, t)) =>
- let
- val (x, xt) = E.lookupERel env n
- in
- ((EAbs (x, xt, t, e), loc),
- (TFun (xt, t), loc))
- end)
- (e, rtype e) fvs
-
- val (f', st) =
- case EM.find (#funcs st, e) of
- SOME f' => (f', st)
- | NONE =>
- let
- val (fx, _, _, tag) = E.lookupENamed env f
- val f' = #maxName st
-
- val vi = (fx, f', t, e, tag)
- in
- (f', {maxName = f' + 1,
- funcs = EM.insert (#funcs st, e, f'),
- vis = vi :: #vis st})
- end
-
- val e = foldr (fn (n, e) =>
- (EApp (e, (ERel n, loc)), loc))
- (ENamed f', loc) fvs
- in
- (*app (fn n => Print.prefaces
- "Free"
- [("n", CorePrint.p_exp env (ERel n, ErrorMsg.dummySpan))])
- fvs;
- Print.prefaces "Squished"
- [("e", CorePrint.p_exp CoreEnv.empty e)];*)
-
- ((fnam, e, xt), st)
- end
- | _ => (tup, st)
- end
- | (tup, st) => (tup, st))
- st xes
- in
- (ERecord xes, st)
- end
- | _ => (e, st)
-
-fun bind (env, b) =
- case b of
- U.Decl.RelK x => E.pushKRel env x
- | U.Decl.RelC (x, k) => E.pushCRel env x k
- | U.Decl.NamedC (x, n, k, co) => E.pushCNamed env x n k co
- | U.Decl.RelE (x, t) => E.pushERel env x t
- | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s
-
-fun doDecl env = U.Decl.foldMapB {kind = default,
- con = default,
- exp = exp,
- decl = default,
- bind = bind}
- env
-
-fun defunc file =
- let
- fun doDecl' (d, (env, st)) =
- let
- val env = E.declBinds env d
-
- val (d, st) = doDecl env st d
-
- val ds =
- case #vis st of
- [] => [d]
- | vis =>
- case d of
- (DValRec vis', loc) => [(DValRec (vis' @ vis), loc)]
- | _ => [(DValRec vis, #2 d), d]
- in
- (ds,
- (env,
- {maxName = #maxName st,
- funcs = #funcs st,
- vis = []}))
- end
-
- val (file, _) = ListUtil.foldlMapConcat doDecl'
- (E.empty,
- {maxName = U.File.maxName file + 1,
- funcs = EM.empty,
- vis = []})
- file
- in
- file
- end
-
-end
diff --git a/src/elab.sml b/src/elab.sml
index dd2952d2..c31483ec 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 * exp
+ | DTable of int * string * int * con * exp * con
| 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 7adc8dd9..8bb769c1 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1532,11 +1532,13 @@ 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, _, cc) =>
let
- val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc)
+ val ct = (CModProj (tn, [], "sql_table"), loc)
+ val ct = (CApp (ct, c), loc)
+ val ct = (CApp (ct, cc), loc)
in
- pushENamedAs env x n t
+ pushENamedAs env x n ct
end
| DSequence (tn, x, n) =>
let
diff --git a/src/elab_print.sml b/src/elab_print.sml
index f98592cc..b65e1bd6 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -740,17 +740,17 @@ fun p_decl env (dAll as (d, _) : decl) =
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, 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 6700686d..32f399dc 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -766,9 +766,14 @@ 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, _) =>
- bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "sql_table"), loc),
- c), loc)))
+ | DTable (tn, x, n, c, _, cc) =>
+ let
+ val ct = (CModProj (n, [], "sql_table"), loc)
+ val ct = (CApp (ct, c), loc)
+ val ct = (CApp (ct, cc), loc)
+ in
+ bind (ctx, NamedE (x, ct))
+ end
| DSequence (tn, x, n) =>
bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
| DClass (x, n, k, _) =>
@@ -864,12 +869,14 @@ 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, e) =>
+ | DTable (tn, x, n, c, e, cc) =>
S.bind2 (mfc ctx c,
fn c' =>
- S.map2 (mfe ctx e,
+ S.bind2 (mfe ctx e,
fn e' =>
- (DTable (tn, x, n, c', e'), loc)))
+ S.map2 (mfc ctx cc,
+ fn cc' =>
+ (DTable (tn, x, n, c', e', cc'), loc))))
| DSequence _ => S.return2 dAll
| DClass (x, n, k, c) =>
@@ -1020,7 +1027,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 0beab9e7..224c3e50 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -880,6 +880,64 @@
(L'.CError, _) => ()
| (_, L'.CError) => ()
+ | (L'.CProj (c1, n1), _) =>
+ let
+ fun trySnd () =
+ case #1 (hnormCon env c2All) of
+ L'.CProj (c2, n2) =>
+ let
+ fun tryNormal () =
+ if n1 = n2 then
+ unifyCons' env c1 c2
+ else
+ err CIncompatible
+ in
+ case #1 (hnormCon env c2) of
+ L'.CUnif (_, k, _, r) =>
+ (case #1 (hnormKind k) of
+ L'.KTuple ks =>
+ let
+ val loc = #2 c2
+ val us = map (fn k => cunif (loc, k)) ks
+ in
+ r := SOME (L'.CTuple us, loc);
+ unifyCons' env c1All (List.nth (us, n2 - 1))
+ end
+ | _ => tryNormal ())
+ | _ => tryNormal ()
+ end
+ | _ => err CIncompatible
+ in
+ case #1 (hnormCon env c1) of
+ L'.CUnif (_, k, _, r) =>
+ (case #1 (hnormKind k) of
+ L'.KTuple ks =>
+ let
+ val loc = #2 c1
+ val us = map (fn k => cunif (loc, k)) ks
+ in
+ r := SOME (L'.CTuple us, loc);
+ unifyCons' env (List.nth (us, n1 - 1)) c2All
+ end
+ | _ => trySnd ())
+ | _ => trySnd ()
+ end
+
+ | (_, L'.CProj (c2, n2)) =>
+ (case #1 (hnormCon env c2) of
+ L'.CUnif (_, k, _, r) =>
+ (case #1 (hnormKind k) of
+ L'.KTuple ks =>
+ let
+ val loc = #2 c2
+ val us = map (fn k => cunif (loc, k)) ks
+ in
+ r := SOME (L'.CTuple us, loc);
+ unifyCons' env c1All (List.nth (us, n2 - 1))
+ end
+ | _ => err CIncompatible)
+ | _ => err CIncompatible)
+
| (L'.CRecord _, _) => isRecord ()
| (_, L'.CRecord _) => isRecord ()
| (L'.CConcat _, _) => isRecord ()
@@ -962,64 +1020,6 @@
((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2))
handle ListPair.UnequalLengths => err CIncompatible)
- | (L'.CProj (c1, n1), _) =>
- let
- fun trySnd () =
- case #1 (hnormCon env c2All) of
- L'.CProj (c2, n2) =>
- let
- fun tryNormal () =
- if n1 = n2 then
- unifyCons' env c1 c2
- else
- err CIncompatible
- in
- case #1 (hnormCon env c2) of
- L'.CUnif (_, k, _, r) =>
- (case #1 (hnormKind k) of
- L'.KTuple ks =>
- let
- val loc = #2 c2
- val us = map (fn k => cunif (loc, k)) ks
- in
- r := SOME (L'.CTuple us, loc);
- unifyCons' env c1All (List.nth (us, n2 - 1))
- end
- | _ => tryNormal ())
- | _ => tryNormal ()
- end
- | _ => err CIncompatible
- in
- case #1 (hnormCon env c1) of
- L'.CUnif (_, k, _, r) =>
- (case #1 (hnormKind k) of
- L'.KTuple ks =>
- let
- val loc = #2 c1
- val us = map (fn k => cunif (loc, k)) ks
- in
- r := SOME (L'.CTuple us, loc);
- unifyCons' env (List.nth (us, n1 - 1)) c2All
- end
- | _ => trySnd ())
- | _ => trySnd ()
- end
-
- | (_, L'.CProj (c2, n2)) =>
- (case #1 (hnormCon env c2) of
- L'.CUnif (_, k, _, r) =>
- (case #1 (hnormKind k) of
- L'.KTuple ks =>
- let
- val loc = #2 c2
- val us = map (fn k => cunif (loc, k)) ks
- in
- r := SOME (L'.CTuple us, loc);
- unifyCons' env c1All (List.nth (us, n2 - 1))
- end
- | _ => err CIncompatible)
- | _ => err CIncompatible)
-
| (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
(unifyKinds env dom1 dom2;
unifyKinds env ran1 ran2)
@@ -2319,7 +2319,8 @@ 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, _, cc) =>
+ [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), cc), 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 _ => []
@@ -3268,17 +3269,22 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs)) =
| 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 uniques = cunif (loc, (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc))
+
+ val ct = tableOf ()
+ val ct = (L'.CApp (ct, c'), loc)
+ val ct = (L'.CApp (ct, uniques), loc)
+
+ val (env, n) = E.pushENamed env x ct
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)
+ 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'), loc)], (env, denv, gs'' @ enD gs' @ gs))
+ ([(L'.DTable (!basis_r, x, n, c', e', uniques), loc)], (env, denv, gs'' @ enD gs' @ gs))
end
| L.DSequence x =>
let
diff --git a/src/expl.sml b/src/expl.sml
index a347a8e8..6cd9b7a8 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 * exp
+ | DTable of int * string * int * con * exp * con
| 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 f4e16cb5..31b1c0a3 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -298,11 +298,13 @@ 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, _, cc) =>
let
- val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc)
+ val ct = (CModProj (tn, [], "sql_table"), loc)
+ val ct = (CApp (ct, c), loc)
+ val ct = (CApp (ct, cc), loc)
in
- pushENamed env x n t
+ pushENamed env x n ct
end
| DSequence (tn, x, n) =>
let
diff --git a/src/expl_print.sml b/src/expl_print.sml
index c7a506b1..05d68941 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -663,17 +663,17 @@ fun p_decl env (dAll as (d, _) : decl) =
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, 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 d567bde3..fa35bd0d 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, e) => SOME (L'.DTable (nt, x, n, explifyCon c, explifyExp e), loc)
+ | L.DTable (nt, x, n, c, e, cc) => SOME (L'.DTable (nt, x, n, explifyCon c, explifyExp e, 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)
diff --git a/src/monoize.sml b/src/monoize.sml
index af414c08..057a9222 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -139,7 +139,7 @@ fun monoType env =
(L'.TSignal (mt env dtmap t), loc)
| L.CApp ((L.CFfi ("Basis", "http_cookie"), _), _) =>
(L'.TFfi ("Basis", "string"), loc)
- | L.CApp ((L.CFfi ("Basis", "sql_table"), _), _) =>
+ | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_table"), _), _), _), _) =>
(L'.TFfi ("Basis", "string"), loc)
| L.CFfi ("Basis", "sql_sequence") =>
(L'.TFfi ("Basis", "string"), loc)
@@ -151,7 +151,7 @@ fun monoType env =
(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.CApp ((L.CApp ((L.CFfi ("Basis", "sql_constraint"), _), _), _), _) =>
(L'.TFfi ("Basis", "string"), loc)
| L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_subset"), _), _), _), _) =>
@@ -1162,13 +1162,19 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
| L.ECApp ((L.EFfi ("Basis", "no_constraint"), _), _) =>
((L'.ERecord [], loc),
fm)
- | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "one_constraint"), _), _), _), (L.CName name, _)) =>
+ | L.ECApp ((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"), _), _), _), _), _), _) =>
+ | L.ECApp (
+ (L.ECApp (
+ (L.ECApp (
+ (L.EFfi ("Basis", "join_constraints"), _),
+ _), _),
+ _), _),
+ _) =>
let
val constraints = (L'.TFfi ("Basis", "sql_constraints"), loc)
in
@@ -1178,12 +1184,18 @@ fun monoExp (env, st, fm) (all as (e, 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.ECApp (
+ (L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "unique"), _), _), _), t), _),
+ nm), _),
+ (L.CRecord (_, unique), _)) =>
+ let
+ val unique = (nm, t) :: unique
+ in
+ ((L'.EPrim (Prim.String ("UNIQUE ("
+ ^ String.concatWith ", " (map (fn (x, _) => "uw_" ^ monoName env x) unique)
+ ^ ")")), loc),
+ fm)
+ end
| L.EFfiApp ("Basis", "dml", [e]) =>
let
@@ -1193,7 +1205,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
fm)
end
- | L.ECApp ((L.EFfi ("Basis", "insert"), _), fields) =>
+ | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "insert"), _), fields), _), _) =>
(case monoType env (L.TRecord fields, loc) of
(L'.TRecord fields, _) =>
let
@@ -1217,7 +1229,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
end
| _ => poly ())
- | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "update"), _), _), _), changed) =>
+ | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "update"), _), _), _), _), _), changed) =>
(case monoType env (L.TRecord changed, loc) of
(L'.TRecord changed, _) =>
let
@@ -1246,7 +1258,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
end
| _ => poly ())
- | L.ECApp ((L.EFfi ("Basis", "delete"), _), _) =>
+ | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "delete"), _), _), _), _) =>
let
val s = (L'.TFfi ("Basis", "string"), loc)
fun sc s = (L'.EPrim (Prim.String s), loc)
@@ -1348,6 +1360,12 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
val un = (L'.TRecord [], loc)
fun gf s = (L'.EField ((L'.ERel 0, loc), s), loc)
+ val tables = List.mapPartial
+ (fn (x, (L.CTuple [y, _], _)) => SOME (x, y)
+ | _ => (E.errorAt loc "Bad sql_query1 tables pair";
+ NONE))
+ tables
+
fun doTables tables =
let
val tables = map (fn ((L.CName x, _), xts) =>
@@ -2481,7 +2499,7 @@ 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, e) =>
+ | L.DTable (x, n, (L.CRecord (_, xts), _), s, e, _) =>
let
val t = (L.CFfi ("Basis", "string"), loc)
val t' = (L'.TFfi ("Basis", "string"), loc)
@@ -2615,7 +2633,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
@@ -2660,7 +2678,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/reduce.sml b/src/reduce.sml
index 6754d708..d6357f1b 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -461,8 +461,9 @@ 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', e) => ((DTable (s, n, con namedC [] c, s',
- exp (namedC, namedE) [] e), loc), st)
+ | DTable (s, n, c, s', e, cc) => ((DTable (s, n, con namedC [] c, s',
+ exp (namedC, namedE) [] e,
+ 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)
diff --git a/src/shake.sml b/src/shake.sml
index 2f873e94..19204ebb 100644
--- a/src/shake.sml
+++ b/src/shake.sml
@@ -59,7 +59,7 @@ fun shake file =
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, _, e, _), _), (usedE, usedC, table_cs)) =>
let
val (usedE, usedC) = usedVars (usedE, usedC) e
in
@@ -79,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)))
diff --git a/src/sources b/src/sources
index b2d7b855..27b6673b 100644
--- a/src/sources
+++ b/src/sources
@@ -105,9 +105,6 @@ core_untangle.sml
especialize.sig
especialize.sml
-defunc.sig
-defunc.sml
-
rpcify.sig
rpcify.sml
diff --git a/src/urweb.grm b/src/urweb.grm
index 784c62ee..ad92ff11 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -294,9 +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
+ | tnameW of con * con
+ | tnames of (con * con) * (con * con) list
+ | tnames' of (con * con) * (con * con) list
| table of con * exp
| tident of con
| fident of con
@@ -493,7 +493,9 @@ cst : UNIQUE tnames (let
val loc = s (UNIQUEleft, tnamesright)
val e = (EVar (["Basis"], "unique", Infer), loc)
- val e = (ECApp (e, tnames), loc)
+ val e = (ECApp (e, #1 (#1 tnames)), loc)
+ val e = (ECApp (e, (CRecord (#2 tnames), loc)), loc)
+ val e = (EDisjointApp e, loc)
in
(EDisjointApp e, loc)
end)
@@ -505,12 +507,11 @@ tnameW : tname (let
(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, [])
+ | LPAREN tnames' RPAREN (tnames')
-tnames': tnameW ([tnameW])
- | tnameW COMMA tnames' (tnameW :: tnames')
+tnames': tnameW (tnameW, [])
+ | tnameW COMMA tnames' (#1 tnames', tnameW :: #2 tnames')
valis : vali ([vali])
| vali AND valis (vali :: valis)
diff --git a/tests/cst.ur b/tests/cst.ur
index 104a9f34..0ebcc977 100644
--- a/tests/cst.ur
+++ b/tests/cst.ur
@@ -4,9 +4,12 @@ table t : {A : int, B : int}
CONSTRAINT UniBoth UNIQUE (A, B),
CONSTRAINT UniAm UNIQUE {#A},
- CONSTRAINT UniAm2 UNIQUE {{[A = _]}},
- CONSTRAINT UniAm3 {unique [[A = _]] !},
- {{one_constraint [#UniAm4] (unique [[A = _]] !)}}
+ CONSTRAINT UniAm2 {unique [#A] [[]] ! !},
+ {{one_constraint [#UniAm3] (unique [#A] [[]] ! !)}},
+
+ CONSTRAINT UniBothm UNIQUE ({#A}, {#B}),
+ CONSTRAINT UniBothm2 {unique [#A] [[B = _]] ! !},
+ {{one_constraint [#UniBothm3] (unique [#A] [[B = _]] ! !)}}
fun main () : transaction page =
queryI (SELECT * FROM t) (fn _ => return ());
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-21 13:39:35 +0000