# HG changeset patch # User Adam Chlipala # Date 1338665758 14400 # Node ID 6bc2a8cb3a67cc2abdac2bc4f10d267d9ad8efad # Parent 27fdd78bd2f5605550a49eaf8a46d15adee7e21a Track whether SQL expressions may use window functions, in preparation for actual window function support diff -r 27fdd78bd2f5 -r 6bc2a8cb3a67 demo/batchFun.ur --- a/demo/batchFun.ur Sat Jun 02 10:54:49 2012 -0400 +++ b/demo/batchFun.ur Sat Jun 02 15:35:58 2012 -0400 @@ -46,7 +46,7 @@ fun add r = dml (insert t (@foldR2 [fst] [colMeta] - [fn cols => $(map (fn t => sql_exp [] [] [] t.1) cols)] + [fn cols => $(map (fn t => sql_exp [] [] [] disallow_window t.1) cols)] (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] input col acc => acc ++ {nm = @sql_inject col.Inject input}) {} M.fl (r -- #Id) M.cols diff -r 27fdd78bd2f5 -r 6bc2a8cb3a67 demo/crud.ur --- a/demo/crud.ur Sat Jun 02 10:54:49 2012 -0400 +++ b/demo/crud.ur Sat Jun 02 15:35:58 2012 -0400 @@ -93,7 +93,7 @@ id <- nextval seq; dml (insert tab (@foldR2 [snd] [colMeta] - [fn cols => $(map (fn t => sql_exp [] [] [] t.1) cols)] + [fn cols => $(map (fn t => sql_exp [] [] [] disallow_window t.1) cols)] (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] => fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)}) {} M.fl inputs M.cols @@ -110,7 +110,7 @@ fun save (inputs : $(map snd M.cols)) = dml (update [map fst M.cols] (@foldR2 [snd] [colMeta] - [fn cols => $(map (fn t => sql_exp [T = [Id = int] ++ map fst M.cols] [] [] t.1) cols)] + [fn cols => $(map (fn t => sql_exp [T = [Id = int] ++ map fst M.cols] [] [] disallow_window t.1) cols)] (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] => fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)}) diff -r 27fdd78bd2f5 -r 6bc2a8cb3a67 demo/more/dbgrid.ur --- a/demo/more/dbgrid.ur Sat Jun 02 10:54:49 2012 -0400 +++ b/demo/more/dbgrid.ur Sat Jun 02 15:35:58 2012 -0400 @@ -385,7 +385,7 @@ val wholeRow = @Folder.concat ! M.keyFolder M.rowFolder fun ensql [env] (r : $(M.key ++ M.row)) = - @map2 [rawMeta] [ident] [sql_exp env [] []] + @map2 [rawMeta] [ident] [sql_exp env [] [] disallow_window] (fn [t] meta v => @sql_inject meta.Inj v) wholeRow M.raw r @@ -396,12 +396,12 @@ dml (insert M.tab (ensql row)); return row - fun selector (r : $M.key) : sql_exp [T = M.key ++ M.row] [] [] bool = + fun selector (r : $M.key) : sql_exp [T = M.key ++ M.row] [] [] disallow_window bool = @foldR2 [rawMeta] [ident] - [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool] + [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] disallow_window bool] (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key] (meta : rawMeta t) (v : t) - (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool) + (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] disallow_window bool) [rest :: {Type}] [rest ~ [nm = t] ++ key] => (WHERE T.{nm} = {@sql_inject meta.Inj v} AND {exp [[nm = t] ++ rest]})) (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE)) diff -r 27fdd78bd2f5 -r 6bc2a8cb3a67 demo/more/orm.ur --- a/demo/more/orm.ur Sat Jun 02 10:54:49 2012 -0400 +++ b/demo/more/orm.ur Sat Jun 02 15:35:58 2012 -0400 @@ -32,8 +32,8 @@ val id = {Link = fn id => resultOut (SELECT * FROM t WHERE t.Id = {[id]}), Inj = inj} - fun ensql [avail ::_] (r : row') : $(map (sql_exp avail [] []) fs') = - @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1] + fun ensql [avail ::_] (r : row') : $(map (sql_exp avail [] [] disallow_window) fs') = + @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] disallow_window ts.1] (fn [ts] meta v => @sql_inject meta.Inj v) M.folder M.cols r @@ -53,11 +53,11 @@ val list = resultsOut (SELECT * FROM t) - con col = fn t => {Exp : sql_exp [T = fs] [] [] t, + con col = fn t => {Exp : sql_exp [T = fs] [] [] disallow_window t, Inj : sql_injectable t} val idCol = {Exp = sql_field [#T] [#Id], Inj = _} con meta' = fn (fs :: {Type}) (col :: Type, parent :: Type) => - {Col : {Exp : sql_exp [T = fs] [] [] col, + {Col : {Exp : sql_exp [T = fs] [] [] disallow_window col, Inj : sql_injectable col}, Parent : $fs -> transaction (option parent)} val cols = @foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] => @@ -75,7 +75,7 @@ M.folder M.cols [[Id = (id, row)]] ! - type filter = sql_exp [T = fs] [] [] bool + type filter = sql_exp [T = fs] [] [] disallow_window bool fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f}) fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f}) diff -r 27fdd78bd2f5 -r 6bc2a8cb3a67 demo/more/versioned.ur --- a/demo/more/versioned.ur Sat Jun 02 10:54:49 2012 -0400 +++ b/demo/more/versioned.ur Sat Jun 02 15:35:58 2012 -0400 @@ -24,7 +24,7 @@ Eq : eq t} fun keyRecd (r : $(M.key ++ M.data)) = - @map2 [sql_injectable] [ident] [sql_exp [] [] []] + @map2 [sql_injectable] [ident] [sql_exp [] [] [] disallow_window] (fn [t] => @sql_inject) M.keyFolder M.key (r --- M.data) @@ -34,18 +34,18 @@ ({Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)} ++ keyRecd r ++ @map2 [dmeta] [ident] - [fn t => sql_exp [] [] [] (option t)] + [fn t => sql_exp [] [] [] disallow_window (option t)] (fn [t] x v => @sql_inject (@sql_option_prim x.Inj) (Some v)) M.dataFolder M.data (r --- M.key))) - fun keyExp (r : $M.key) : sql_exp [T = all] [] [] bool = + fun keyExp (r : $M.key) : sql_exp [T = all] [] [] disallow_window bool = @foldR2 [sql_injectable] [ident] [fn before => after :: {Type} -> [before ~ after] - => sql_exp [T = before ++ after] [] [] bool] + => sql_exp [T = before ++ after] [] [] disallow_window bool] (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before] (inj : sql_injectable t) (v : t) (e : after :: {Type} -> [before ~ after] - => sql_exp [T = before ++ after] [] [] bool) + => sql_exp [T = before ++ after] [] [] disallow_window bool) [after :: {Type}] [[nm = t] ++ before ~ after] => (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after]})) (fn [after :: {Type}] [[] ~ after] => (SQL TRUE)) @@ -113,7 +113,7 @@ | Some cur => vr <- nextval s; let - val r' = @map3 [dmeta] [ident] [ident] [fn t => sql_exp [] [] [] (option t)] + val r' = @map3 [dmeta] [ident] [ident] [fn t => sql_exp [] [] [] disallow_window (option t)] (fn [t] (meta : dmeta t) old new => @sql_inject (@sql_option_prim meta.Inj) (if @@eq [_] meta.Eq old new then diff -r 27fdd78bd2f5 -r 6bc2a8cb3a67 doc/manual.tex --- a/doc/manual.tex Sat Jun 02 10:54:49 2012 -0400 +++ b/doc/manual.tex Sat Jun 02 15:35:58 2012 -0400 @@ -1595,7 +1595,7 @@ The last kind of constraint is a \texttt{CHECK} constraint, which attaches a boolean invariant over a row's contents. It is defined using the $\mt{sql\_exp}$ type family, which we discuss in more detail below. $$\begin{array}{l} - \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; [] + \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \mt{disallow\_window} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; [] \end{array}$$ Section \ref{tables} shows the expanded syntax of the $\mt{table}$ declaration and signature item that includes constraints. There is no other way to use constraints with SQL in Ur/Web. @@ -1662,11 +1662,11 @@ \hspace{.1in} \Rightarrow [\mt{empties} \sim \mt{selectedFields}] \\ \hspace{.1in} \Rightarrow \{\mt{Distinct} : \mt{bool}, \\ \hspace{.2in} \mt{From} : \mt{sql\_from\_items} \; \mt{free} \; \mt{tables}, \\ - \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; (\mt{free} \rc \mt{tables}) \; \mt{afree} \; [] \; \mt{bool}, \\ + \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; (\mt{free} \rc \mt{tables}) \; \mt{afree} \; [] \; \mt{disallow\_window} \; \mt{bool}, \\ \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\ - \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{bool}, \\ + \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{disallow\_window} \; \mt{bool}, \\ \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; \mt{empties} \rc \mt{selectedFields}), \\ - \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; []) \; \mt{selectedExps}) \} \\ + \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{allow\_window}) \; \mt{selectedExps}) \} \\ \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps} \end{array}$$ @@ -1680,24 +1680,26 @@ \mt{val} \; \mt{sql\_subset\_all} : \mt{tables} :: \{\{\mt{Type}\}\} \to \mt{sql\_subset} \; \mt{tables} \; \mt{tables} \end{array}$$ -SQL expressions are used in several places, including $\mt{SELECT}$, $\mt{WHERE}$, $\mt{HAVING}$, and $\mt{ORDER} \; \mt{BY}$ clauses. They reify a fragment of the standard SQL expression language, while making it possible to inject ``native'' Ur values in some places. The arguments to the $\mt{sql\_exp}$ type family respectively give the unrestricted-availability table fields, the table fields that may only be used in arguments to aggregate functions, the available selected expressions, and the type of the expression. +SQL expressions are used in several places, including $\mt{SELECT}$, $\mt{WHERE}$, $\mt{HAVING}$, and $\mt{ORDER} \; \mt{BY}$ clauses. They reify a fragment of the standard SQL expression language, while making it possible to inject ``native'' Ur values in some places. The arguments to the $\mt{sql\_exp}$ type family respectively give the unrestricted-availability table fields, the table fields that may only be used in arguments to aggregate functions, the available selected expressions, whether window functions are allowed, and the type of the expression. Two abstract constructors are declared to use to specify window function allowedness. $$\begin{array}{l} - \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type} + \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \{\mt{Unit}\} \to \mt{Type} \\ + \mt{con} \; \mt{disallow\_window} :: \{\mt{Unit}\} \\ + \mt{con} \; \mt{allow\_window} :: \{\mt{Unit}\} \end{array}$$ Any field in scope may be converted to an expression. $$\begin{array}{l} \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\ - \hspace{.1in} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\ + \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\ \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\ \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\ - \hspace{.1in} \to \mt{sql\_exp} \; ([\mt{tab} = [\mt{field} = \mt{fieldType}] \rc \mt{otherFields}] \rc \mt{otherTabs}) \; \mt{agg} \; \mt{exps} \; \mt{fieldType} + \hspace{.1in} \to \mt{sql\_exp} \; ([\mt{tab} = [\mt{field} = \mt{fieldType}] \rc \mt{otherFields}] \rc \mt{otherTabs}) \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{fieldType} \end{array}$$ There is an analogous function for referencing named expressions. $$\begin{array}{l} - \mt{val} \; \mt{sql\_exp} : \mt{tabs} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{t} ::: \mt{Type} \to \mt{rest} ::: \{\mt{Type}\} \to \mt{nm} :: \mt{Name} \\ - \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{t} + \mt{val} \; \mt{sql\_exp} : \mt{tabs} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \to \mt{rest} ::: \{\mt{Type}\} \to \mt{nm} :: \mt{Name} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{aw} \; \mt{t} \end{array}$$ Ur values of appropriate types may be injected into SQL expressions. @@ -1716,8 +1718,8 @@ \mt{val} \; \mt{sql\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; \mt{t} \\ \mt{val} \; \mt{sql\_option\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; (\mt{option} \; \mt{t}) \\ \\ - \mt{val} \; \mt{sql\_inject} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \to \mt{sql\_injectable} \; \mt{t} \\ - \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} + \mt{val} \; \mt{sql\_inject} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \to \mt{sql\_injectable} \; \mt{t} \\ + \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \end{array}$$ Additionally, most function-free types may be injected safely, via the $\mt{serialized}$ type family. @@ -1730,39 +1732,44 @@ We have the SQL nullness test, which is necessary because of the strange SQL semantics of equality in the presence of null values. $$\begin{array}{l} - \mt{val} \; \mt{sql\_is\_null} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{t}) \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool} + \mt{val} \; \mt{sql\_is\_null} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{aw} \; \mt{t}) \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{bool} \end{array}$$ As another way of dealing with null values, there is also a restricted form of the standard \cd{COALESCE} function. $$\begin{array}{l} \mt{val} \; \mt{sql\_coalesce} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ - \hspace{.1in} \to \mt{t} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{t}) \\ - \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ - \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} + \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; (\mt{option} \; \mt{t}) \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \end{array}$$ We have generic nullary, unary, and binary operators. $$\begin{array}{l} \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\ \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\ - \mt{val} \; \mt{sql\_nfunc} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\\end{array}$$ + \mt{val} \; \mt{sql\_nfunc} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} +\end{array}$$ $$\begin{array}{l} \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\ - \mt{val} \; \mt{sql\_unary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{arg} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_unary} \; \mt{arg} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{res} \\ + \mt{val} \; \mt{sql\_unary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{arg} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_unary} \; \mt{arg} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{res} \end{array}$$ $$\begin{array}{l} \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\ \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\ \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\ - \mt{val} \; \mt{sql\_binary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{arg_1} ::: \mt{Type} \to \mt{arg_2} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_binary} \; \mt{arg_1} \; \mt{arg_2} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg_1} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg_2} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{res} + \mt{val} \; \mt{sql\_binary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ + \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{arg_1} ::: \mt{Type} \to \mt{arg_2} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_binary} \; \mt{arg_1} \; \mt{arg_2} \; \mt{res} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg_1} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg_2} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{res} \end{array}$$ $$\begin{array}{l} @@ -1779,13 +1786,13 @@ Finally, we have aggregate functions. The $\mt{COUNT(\ast)}$ syntax is handled specially, since it takes no real argument. The other aggregate functions are placed into a general type family, using constructor classes to restrict usage to properly-typed arguments. The key aspect of the $\mt{sql\_aggregate}$ function's type is the shift of aggregate-function-only fields into unrestricted fields. $$\begin{array}{l} - \mt{val} \; \mt{sql\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{int} + \mt{val} \; \mt{sql\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \mt{aw} ::: \{\mt{Unit}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{int} \end{array}$$ $$\begin{array}{l} \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ - \mt{val} \; \mt{sql\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{dom} ::: \mt{Type} \to \mt{ran} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{dom} \; \mt{ran} \to \mt{sql\_exp} \; \mt{agg} \; \mt{agg} \; \mt{exps} \; \mt{dom} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{ran} + \mt{val} \; \mt{sql\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Type}\} \mt{dom} ::: \mt{Type} \to \mt{ran} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{dom} \; \mt{ran} \to \mt{sql\_exp} \; \mt{agg} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{dom} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{ran} \end{array}$$ $$\begin{array}{l} @@ -1815,17 +1822,18 @@ Any SQL query that returns single columns may be turned into a subquery expression. $$\begin{array}{l} -\mt{val} \; \mt{sql\_subquery} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \to \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \\ -\hspace{.1in} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_query} \; \mt{tables} \; \mt{agg} \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{nt} +\mt{val} \; \mt{sql\_subquery} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \\ +\hspace{.1in} \to \mt{aw} ::: \mt{Type} \to \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \\ +\hspace{.1in} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_query} \; \mt{tables} \; \mt{agg} \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{nt} \end{array}$$ There is also an \cd{IF..THEN..ELSE..} construct that is compiled into standard SQL \cd{CASE} expressions. $$\begin{array}{l} -\mt{val} \; \mt{sql\_if\_then\_else} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ -\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool} \\ -\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ -\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ -\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} +\mt{val} \; \mt{sql\_if\_then\_else} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ +\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{bool} \\ +\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\ +\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\ +\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \end{array}$$ \texttt{FROM} clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause. @@ -1840,7 +1848,7 @@ \mt{val} \; \mt{sql\_inner\_join} : \mt{free} ::: \{\{\mt{Type}\}\} \to \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \\ \hspace{.1in} \to [\mt{free} \sim \mt{tabs1}] \Rightarrow [\mt{free} \sim \mt{tabs2}] \Rightarrow [\mt{tabs1} \sim \mt{tabs2}] \\ \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs2} \\ - \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{bool} \\ + \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \\ \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{tabs2}) \end{array}$$ @@ -1858,7 +1866,7 @@ \hspace{.1in} \to [\mt{free} \sim \mt{tabs1}] \Rightarrow [\mt{free} \sim \mt{tabs2}] \Rightarrow [\mt{tabs1} \sim \mt{tabs2}] \\ \hspace{.1in} \Rightarrow \$(\mt{map} \; (\lambda \mt{r} \Rightarrow \$(\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{nullify} \; \mt{p}.1 \; \mt{p}.2) \; \mt{r})) \; \mt{tabs2}) \\ \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \\ - \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \; [] \; [] \; \mt{bool} \\ + \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \\ \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.2)) \; \mt{tabs2}) \end{array}$$ @@ -1871,7 +1879,7 @@ \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ \mt{val} \; \mt{sql\_order\_by\_Nil} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} :: \{\mt{Type}\} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; [] \; \mt{exps} \; \mt{t} \to \mt{sql\_direction} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; [] \; \mt{exps} \; \mt{allow\_window} \; \mt{t} \to \mt{sql\_direction} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ \mt{val} \; \mt{sql\_order\_by\_random} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ \\ \mt{type} \; \mt{sql\_limit} \\ @@ -1902,19 +1910,19 @@ Properly-typed records may be used to form $\mt{INSERT}$ commands. $$\begin{array}{l} \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\ - \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml} + \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; [] \; \mt{disallow\_window}) \; \mt{fields}) \to \mt{dml} \end{array}$$ An $\mt{UPDATE}$ command is formed from a choice of which table fields to leave alone and which to change, along with an expression to use to compute the new value of each changed field and a $\mt{WHERE}$ clause. Note that, in the table environment applied to expressions, the table being updated is hardcoded at the name $\mt{T}$. The parsing extension for $\mt{UPDATE}$ will elaborate all table-free field references to use table variable $\mt{T}$. $$\begin{array}{l} \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to [\mt{changed} \sim \mt{unchanged}] \\ - \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\ - \hspace{.1in} \to \mt{sql\_table} \; (\mt{changed} \rc \mt{unchanged}) \to \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{bool} \to \mt{dml} + \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{disallow\_window}) \; \mt{changed}) \\ + \hspace{.1in} \to \mt{sql\_table} \; (\mt{changed} \rc \mt{unchanged}) \to \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \to \mt{dml} \end{array}$$ A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause. The above use of $\mt{T}$ is repeated. $$\begin{array}{l} - \mt{val} \; \mt{delete} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \to \mt{sql\_exp} \; [\mt{T} = \mt{fields}] \; [] \; [] \; \mt{bool} \to \mt{dml} + \mt{val} \; \mt{delete} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \to \mt{sql\_exp} \; [\mt{T} = \mt{fields}] \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \to \mt{dml} \end{array}$$ \subsubsection{Sequences} diff -r 27fdd78bd2f5 -r 6bc2a8cb3a67 lib/ur/basis.urs --- a/lib/ur/basis.urs Sat Jun 02 10:54:49 2012 -0400 +++ b/lib/ur/basis.urs Sat Jun 02 15:35:58 2012 -0400 @@ -305,15 +305,23 @@ OnUpdate : propagation_mode ([mine1 = t] ++ mine)} -> sql_constraint ([mine1 = t] ++ mine ++ munused) [] -con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type -val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type +con allow_window :: {Unit} +con disallow_window :: {Unit} + +con sql_exp :: {{Type}} (* Free tables, for normal use *) + -> {{Type}} (* Free tables, for use in arguments to aggregate functions *) + -> {Type} (* Free ad-hoc variables *) + -> {Unit} (* Allow window functions here? ([allow_window] indicates yes.) *) + -> Type (* SQL type of this expression *) + -> Type +val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} -> t ::: Type -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type} -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] => - sql_exp fs agg exps t - -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') t + sql_exp fs agg exps aw t + -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') aw t val check : fs ::: {Type} - -> sql_exp [] [] fs bool + -> sql_exp [] [] fs disallow_window bool -> sql_constraint fs [] @@ -351,7 +359,7 @@ val sql_inner_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}} -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] => sql_from_items free tabs1 -> sql_from_items free tabs2 - -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool + -> sql_exp (free ++ tabs1 ++ tabs2) [] [] disallow_window bool -> sql_from_items free (tabs1 ++ tabs2) class nullify :: Type -> Type -> Type @@ -362,14 +370,14 @@ -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2) -> sql_from_items free tabs1 -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2) - -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool + -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] disallow_window bool -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2) val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}} -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1) -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2 - -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool + -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] disallow_window bool -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2) val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}} @@ -377,7 +385,7 @@ => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) (tabs1 ++ tabs2)) -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs2) - -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool + -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] disallow_window bool -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2)) val sql_query1 : free ::: {{Type}} @@ -393,11 +401,11 @@ => [empties ~ selectedFields] => {Distinct : bool, From : sql_from_items free tables, - Where : sql_exp (free ++ tables) afree [] bool, + Where : sql_exp (free ++ tables) afree [] disallow_window bool, GroupBy : sql_subset tables grouped, - Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool, + Having : sql_exp (free ++ grouped) (afree ++ tables) [] disallow_window bool, SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields), - SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) []) + SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [] allow_window) selectedExps) } -> sql_query1 free afree tables selectedFields selectedExps @@ -427,7 +435,7 @@ con sql_order_by :: {{Type}} -> {Type} -> Type val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type - -> sql_exp tables [] exps t -> sql_direction + -> sql_exp tables [] exps allow_window t -> sql_direction -> sql_order_by tables exps -> sql_order_by tables exps val sql_order_by_random : tables ::: {{Type}} -> exps ::: {Type} @@ -454,42 +462,42 @@ -> sql_query free afree selectedFields selectedExps val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} - -> fieldType ::: Type -> agg ::: {{Type}} + -> aw ::: {Unit} -> fieldType ::: Type -> agg ::: {{Type}} -> exps ::: {Type} -> tab :: Name -> field :: Name -> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) - agg exps fieldType + agg exps aw fieldType -val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} +val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> aw ::: {Unit} -> t ::: Type -> rest ::: {Type} -> nm :: Name - -> sql_exp tabs agg ([nm = t] ++ rest) t + -> sql_exp tabs agg ([nm = t] ++ rest) aw t 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) val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_injectable t -> t -> sql_exp tables agg exps t + -> aw ::: {Unit} -> t ::: Type + -> sql_injectable t -> t -> sql_exp tables agg exps aw t val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_exp tables agg exps (option t) - -> sql_exp tables agg exps bool + -> aw ::: {Unit} -> t ::: Type + -> sql_exp tables agg exps aw (option t) + -> sql_exp tables agg exps aw bool val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_exp tables agg exps (option t) - -> sql_exp tables agg exps t - -> sql_exp tables agg exps t + -> aw ::: {Unit} -> t ::: Type + -> sql_exp tables agg exps aw (option t) + -> sql_exp tables agg exps aw t + -> sql_exp tables agg exps aw t val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_exp tables agg exps bool - -> sql_exp tables agg exps t - -> sql_exp tables agg exps t - -> sql_exp tables agg exps t + -> aw ::: {Unit} -> t ::: Type + -> sql_exp tables agg exps aw bool + -> sql_exp tables agg exps aw t + -> sql_exp tables agg exps aw t + -> sql_exp tables agg exps aw t class sql_arith val sql_arith_int : sql_arith int @@ -499,9 +507,9 @@ con sql_unary :: Type -> Type -> Type val sql_not : sql_unary bool bool val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> arg ::: Type -> res ::: Type - -> sql_unary arg res -> sql_exp tables agg exps arg - -> sql_exp tables agg exps res + -> aw ::: {Unit} -> arg ::: Type -> res ::: Type + -> sql_unary arg res -> sql_exp tables agg exps aw arg + -> sql_exp tables agg exps aw res val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t @@ -509,10 +517,10 @@ val sql_and : sql_binary bool bool bool val sql_or : sql_binary bool bool bool val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type - -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1 - -> sql_exp tables agg exps arg2 - -> sql_exp tables agg exps res + -> aw ::: {Unit} -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type + -> sql_binary arg1 arg2 res -> sql_exp tables agg exps aw arg1 + -> sql_exp tables agg exps aw arg2 + -> sql_exp tables agg exps aw res val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t @@ -529,14 +537,14 @@ val sql_like : sql_binary string string bool -val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> sql_exp tables agg exps int +val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} + -> sql_exp tables agg exps aw int con sql_aggregate :: Type -> Type -> Type val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> dom ::: Type -> ran ::: Type - -> sql_aggregate dom ran -> sql_exp agg agg exps dom - -> sql_exp tables agg exps ran + -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type + -> sql_aggregate dom ran -> sql_exp agg agg exps aw dom + -> sql_exp tables agg exps aw ran val sql_count_col : t ::: Type -> sql_aggregate (option t) int @@ -558,29 +566,29 @@ con sql_nfunc :: Type -> Type val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_nfunc t -> sql_exp tables agg exps t + -> aw ::: {Unit} -> t ::: Type + -> sql_nfunc t -> sql_exp tables agg exps aw t val sql_current_timestamp : sql_nfunc time con sql_ufunc :: Type -> Type -> Type val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> dom ::: Type -> ran ::: Type - -> sql_ufunc dom ran -> sql_exp tables agg exps dom - -> sql_exp tables agg exps ran + -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type + -> sql_ufunc dom ran -> sql_exp tables agg exps aw dom + -> sql_exp tables agg exps aw ran val sql_octet_length : sql_ufunc blob int val sql_known : t ::: Type -> sql_ufunc t bool val sql_lower : sql_ufunc string string val sql_upper : sql_ufunc string string -val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type +val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} -> t ::: Type -> sql_injectable_prim t - -> sql_exp tables agg exps t - -> sql_exp tables agg exps (option t) + -> sql_exp tables agg exps aw t + -> sql_exp tables agg exps aw (option t) -val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type -> nt ::: Type +val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> aw ::: {Unit} -> t ::: Type -> nt ::: Type -> nullify t nt -> sql_query tables agg [] [nm = t] - -> sql_exp tables agg exps nt + -> sql_exp tables agg exps aw nt (*** Executing queries *) @@ -604,19 +612,19 @@ val insert : fields ::: {Type} -> uniques ::: {{Unit}} -> sql_table fields uniques - -> $(map (fn t :: Type => sql_exp [] [] [] t) fields) + -> $(map (fn t :: Type => sql_exp [] [] [] disallow_window t) fields) -> dml val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} -> [changed ~ unchanged] => - $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed) + $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] disallow_window t) changed) -> sql_table (changed ++ unchanged) uniques - -> sql_exp [T = changed ++ unchanged] [] [] bool + -> sql_exp [T = changed ++ unchanged] [] [] disallow_window bool -> dml val delete : fields ::: {Type} -> uniques ::: {{Unit}} -> sql_table fields uniques - -> sql_exp [T = fields] [] [] bool + -> sql_exp [T = fields] [] [] disallow_window bool -> dml (*** Sequences *) diff -r 27fdd78bd2f5 -r 6bc2a8cb3a67 lib/ur/top.ur --- a/lib/ur/top.ur Sat Jun 02 10:54:49 2012 -0400 +++ b/lib/ur/top.ur Sat Jun 02 15:35:58 2012 -0400 @@ -376,14 +376,14 @@ oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t) fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}] - [t ::: Type] (_ : sql_injectable (option t)) - (e1 : sql_exp tables agg exps (option t)) - (e2 : sql_exp tables agg exps (option t)) = + [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t)) + (e1 : sql_exp tables agg exps aw (option t)) + (e2 : sql_exp tables agg exps aw (option t)) = (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2}) fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}] - [t ::: Type] (_ : sql_injectable (option t)) - (e1 : sql_exp tables agg exps (option t)) + [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t)) + (e1 : sql_exp tables agg exps aw (option t)) (e2 : option t) = case e2 of None => (SQL {e1} IS NULL) diff -r 27fdd78bd2f5 -r 6bc2a8cb3a67 lib/ur/top.urs --- a/lib/ur/top.urs Sat Jun 02 10:54:49 2012 -0400 +++ b/lib/ur/top.urs Sat Jun 02 15:35:58 2012 -0400 @@ -269,15 +269,15 @@ -> transaction bool val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type -> sql_injectable (option t) - -> sql_exp tables agg exps (option t) - -> sql_exp tables agg exps (option t) - -> sql_exp tables agg exps bool + -> aw ::: {Unit} -> t ::: Type -> sql_injectable (option t) + -> sql_exp tables agg exps aw (option t) + -> sql_exp tables agg exps aw (option t) + -> sql_exp tables agg exps aw bool val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type -> sql_injectable (option t) - -> sql_exp tables agg exps (option t) + -> aw ::: {Unit} -> t ::: Type -> sql_injectable (option t) + -> sql_exp tables agg exps aw (option t) -> option t - -> sql_exp tables agg exps bool + -> sql_exp tables agg exps aw bool val mkRead' : t ::: Type -> (string -> option t) -> string -> read t diff -r 27fdd78bd2f5 -r 6bc2a8cb3a67 src/monoize.sml --- a/src/monoize.sml Sat Jun 02 10:54:49 2012 -0400 +++ b/src/monoize.sml Sat Jun 02 15:35:58 2012 -0400 @@ -249,7 +249,7 @@ (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_from_items"), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) - | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_exp"), _), _), _), _), _), _), _), _) => + | L.CApp ((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) @@ -2107,7 +2107,9 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_inject"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_inject"), _), + _), _), _), _), _), _), _), _), @@ -2506,8 +2508,10 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( + (L.ECApp ( (L.EFfi ("Basis", "sql_unary"), _), _), _), + _), _), _), _), _), _), _), _), @@ -2536,7 +2540,9 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_binary"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_binary"), _), + _), _), _), _), _), _), _), _), @@ -2569,7 +2575,9 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_field"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_field"), _), + _), _), _), _), _), _), _), _), @@ -2583,7 +2591,9 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_exp"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_exp"), _), + _), _), _), _), _), _), _), _), @@ -2687,7 +2697,9 @@ | L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_count"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_count"), _), + _), _), _), _), _), _), _) => ((L'.EPrim (Prim.String "COUNT(*)"), loc), @@ -2698,7 +2710,9 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_aggregate"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_aggregate"), _), + _), _), _), _), _), _), _), _), @@ -2770,11 +2784,13 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_nfunc"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_nfunc"), _), + _), _), _), _), _), _), _), _), - _) => + _) => let val s = (L'.TFfi ("Basis", "string"), loc) fun sc s = (L'.EPrim (Prim.String s), loc) @@ -2789,7 +2805,9 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_ufunc"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_ufunc"), _), + _), _), _), _), _), _), _), _), @@ -2823,7 +2841,9 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_is_null"), _), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_is_null"), _), _), + _), _), _), _), _), _), _), _)) => @@ -2864,7 +2884,11 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_if_then_else"), _), _), + (L.ECApp ( + (L.ECApp ( + (L.EFfi ("Basis", "sql_if_then_else"), _), _), + _), _), + _), _), _), _), _), _), _), _)) => @@ -2889,7 +2913,9 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_nullable"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_nullable"), _), + _), _), _), _), _), _), _), _), @@ -2910,7 +2936,9 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_subquery"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_subquery"), _), + _), _), _), _), _), _), _), _),