# HG changeset patch # User Adam Chlipala # Date 1338737371 14400 # Node ID 818d4097e2ed5ef255ded1a2c122ff3811a30608 # Parent 59b07fdae1ff3848dfac04b0eddfedbeb3bd9ad8 Lighter-weight encoding of window function use diff -r 59b07fdae1ff -r 818d4097e2ed demo/batchFun.ur --- a/demo/batchFun.ur Sat Jun 02 16:47:09 2012 -0400 +++ b/demo/batchFun.ur Sun Jun 03 11:29:31 2012 -0400 @@ -46,7 +46,7 @@ fun add r = dml (insert t (@foldR2 [fst] [colMeta] - [fn cols => $(map (fn t => sql_exp [] [] [] disallow_window t.1) cols)] + [fn cols => $(map (fn t => sql_exp [] [] [] 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 59b07fdae1ff -r 818d4097e2ed demo/crud.ur --- a/demo/crud.ur Sat Jun 02 16:47:09 2012 -0400 +++ b/demo/crud.ur Sun Jun 03 11:29:31 2012 -0400 @@ -93,7 +93,7 @@ id <- nextval seq; dml (insert tab (@foldR2 [snd] [colMeta] - [fn cols => $(map (fn t => sql_exp [] [] [] disallow_window t.1) cols)] + [fn cols => $(map (fn t => sql_exp [] [] [] 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] [] [] disallow_window t.1) cols)] + [fn cols => $(map (fn t => sql_exp [T = [Id = int] ++ map fst M.cols] [] [] 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 59b07fdae1ff -r 818d4097e2ed demo/more/dbgrid.ur --- a/demo/more/dbgrid.ur Sat Jun 02 16:47:09 2012 -0400 +++ b/demo/more/dbgrid.ur Sun Jun 03 11:29:31 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 [] [] disallow_window] + @map2 [rawMeta] [ident] [sql_exp env [] []] (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] [] [] disallow_window bool = + fun selector (r : $M.key) : sql_exp [T = M.key ++ M.row] [] [] bool = @foldR2 [rawMeta] [ident] - [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] disallow_window bool] + [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] 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] [] [] disallow_window bool) + (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] 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 59b07fdae1ff -r 818d4097e2ed demo/more/orm.ur --- a/demo/more/orm.ur Sat Jun 02 16:47:09 2012 -0400 +++ b/demo/more/orm.ur Sun Jun 03 11:29:31 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 [] [] disallow_window) fs') = - @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] disallow_window ts.1] + fun ensql [avail ::_] (r : row') : $(map (sql_exp avail [] []) fs') = + @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] 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] [] [] disallow_window t, + con col = fn t => {Exp : sql_exp [T = fs] [] [] 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] [] [] disallow_window col, + {Col : {Exp : sql_exp [T = fs] [] [] 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] [] [] disallow_window bool + type filter = sql_exp [T = fs] [] [] bool fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f}) fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f}) diff -r 59b07fdae1ff -r 818d4097e2ed demo/more/versioned.ur --- a/demo/more/versioned.ur Sat Jun 02 16:47:09 2012 -0400 +++ b/demo/more/versioned.ur Sun Jun 03 11:29:31 2012 -0400 @@ -24,7 +24,7 @@ Eq : eq t} fun keyRecd (r : $(M.key ++ M.data)) = - @map2 [sql_injectable] [ident] [sql_exp [] [] [] disallow_window] + @map2 [sql_injectable] [ident] [sql_exp [] [] []] (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 [] [] [] disallow_window (option t)] + [fn t => sql_exp [] [] [] (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] [] [] disallow_window bool = + fun keyExp (r : $M.key) : sql_exp [T = all] [] [] bool = @foldR2 [sql_injectable] [ident] [fn before => after :: {Type} -> [before ~ after] - => sql_exp [T = before ++ after] [] [] disallow_window bool] + => sql_exp [T = before ++ after] [] [] 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] [] [] disallow_window bool) + => sql_exp [T = before ++ after] [] [] 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 [] [] [] disallow_window (option t)] + val r' = @map3 [dmeta] [ident] [ident] [fn t => sql_exp [] [] [] (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 59b07fdae1ff -r 818d4097e2ed doc/manual.tex --- a/doc/manual.tex Sat Jun 02 16:47:09 2012 -0400 +++ b/doc/manual.tex Sun Jun 03 11:29:31 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{disallow\_window} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; [] + \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \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{disallow\_window} \; \mt{bool}, \\ + \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; (\mt{free} \rc \mt{tables}) \; \mt{afree} \; [] \; \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{disallow\_window} \; \mt{bool}, \\ + \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \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{allow\_window}) \; \mt{selectedExps}) \} \\ + \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_expw} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; []) \; \mt{selectedExps}) \} \\ \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps} \end{array}$$ @@ -1680,26 +1680,24 @@ \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, whether window functions are allowed, and the type of the expression. Two abstract constructors are declared to use to specify window function allowedness. +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. $$\begin{array}{l} - \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}\} + \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type} \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{aw} ::: \{\mt{Unit}\} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\ + \hspace{.1in} \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{aw} \; \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{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{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} + \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} \end{array}$$ Ur values of appropriate types may be injected into SQL expressions. @@ -1718,8 +1716,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{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} + \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} \end{array}$$ Additionally, most function-free types may be injected safely, via the $\mt{serialized}$ type family. @@ -1732,44 +1730,39 @@ 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{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} + \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} \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{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} + \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} \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{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}$$ + \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}$$ $$\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{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} + \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} \\ \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}\} \\ - \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} + \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} \end{array}$$ $$\begin{array}{l} @@ -1786,13 +1779,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}\} \mt{aw} ::: \{\mt{Unit}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{int} + \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} \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{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} + \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} \end{array}$$ $$\begin{array}{l} @@ -1819,43 +1812,20 @@ \mt{val} \; \mt{sql\_min} : \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt} \end{array}$$ -There is a fancier class of aggregates called \emph{window functions}, defined in the SQL standard but currently only supported by Postgres, among the DBMSes that Ur/Web supports. Here are the type family and associated combinator for creating a window function expression: +Any SQL query that returns single columns may be turned into a subquery expression. $$\begin{array}{l} -\mt{con} \; \mt{sql\_window} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type} \\ -\mt{val} \; \mt{sql\_window} : \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\_window} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ -\hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps} \\ -\hspace{.1in} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ -\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{allow\_window} \; \mt{t} -\end{array}$$ - -The function argument for an SQL \cd{PARTITION BY} clause uses the following type family and combinators: -$$\begin{array}{l} -\mt{con} \; \mt{sql\_partition} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ -\mt{val} \; \mt{sql\_no\_partition} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ -\hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps} \\ -\mt{val} \; \mt{sql\_partition} : \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{disallow\_window} \; \mt{t} \\ -\hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps} -\end{array}$$ - -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} \\ -\hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \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} +\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} \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{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} +\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} \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. @@ -1870,7 +1840,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{disallow\_window} \; \mt{bool} \\ + \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{bool} \\ \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{tabs2}) \end{array}$$ @@ -1888,7 +1858,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{disallow\_window} \; \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{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}$$ @@ -1900,8 +1870,9 @@ \\ \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{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\_Cons} : \mt{tf} ::: (\{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}) \\ + \hspace{.1in} \to \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_window} \; \mt{tf} \to \mt{tf} \; \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} \\ \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} \\ @@ -1913,6 +1884,45 @@ \mt{val} \; \mt{sql\_offset} : \mt{int} \to \mt{sql\_offset} \end{array}$$ +When using Postgres, \cd{SELECT} and \cd{ORDER BY} are allowed to contain top-level uses of \emph{window functions}. A separate type family \cd{sql\_expw} is provided for such cases, with some type class convenience for overloading between normal and window expressions. +$$\begin{array}{l} + \mt{con} \; \mt{sql\_expw} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type} \\ + \\ + \mt{class} \; \mt{sql\_window} :: (\{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}) \to \mt{Type} \\ + \mt{val} \; \mt{sql\_window\_normal} : \mt{sql\_window} \; \mt{sql\_exp} \\ + \mt{val} \; \mt{sql\_window\_fancy} : \mt{sql\_window} \; \mt{sql\_expw} \\ + \mt{val} \; \mt{sql\_window} : \mt{tf} ::: (\{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}) \\ + \hspace{.1in} \to \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_window} \; \mt{tf} \\ + \hspace{.1in} \to \mt{tf} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ + \hspace{.1in} \to \mt{sql\_expw} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ + \\ + \mt{con} \; \mt{sql\_partition} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ + \mt{val} \; \mt{sql\_no\_partition} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ + \hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps} \\ + \mt{val} \; \mt{sql\_partition} : \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{t} \\ + \hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps} \\ + \\ + \mt{con} \; \mt{sql\_window\_function} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type} \\ + \mt{val} \; \mt{sql\_window\_function} : \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\_window\_function} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ + \hspace{.1in} \to \mt{sql\_partition} \; \mt{tables} \; \mt{agg} \; \mt{exps} \\ + \hspace{.1in} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ + \hspace{.1in} \to \mt{sql\_expw} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ + \\ + \mt{val} \; \mt{sql\_window\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ + \hspace{.1in} \to \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ + \hspace{.1in} \to \mt{sql\_window\_function} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{nt} \\ + \mt{val} \; \mt{sql\_window\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ + \hspace{.1in} \to \mt{sql\_window\_function} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{int} \\ + \mt{val} \; \mt{sql\_rank} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ + \hspace{.1in} \to \mt{sql\_window\_function} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{int} +\end{array}$$ + \subsubsection{DML} @@ -1932,19 +1942,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{disallow\_window}) \; \mt{fields}) \to \mt{dml} + \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \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{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} + \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} \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{disallow\_window} \; \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{bool} \to \mt{dml} \end{array}$$ \subsubsection{Sequences} @@ -2188,7 +2198,7 @@ \textrm{Pre-queries} & q &::=& \mt{SELECT} \; [\mt{DISTINCT}] \; P \; \mt{FROM} \; F,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\ &&& \mid q \; R \; q \mid \{\{\{e\}\}\} \\ \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT} \\ - \textrm{$\mt{ORDER \; BY}$ items} & O &::=& \mt{RANDOM} [()] \mid E \; [o] \mid E \; [o], O + \textrm{$\mt{ORDER \; BY}$ items} & O &::=& \mt{RANDOM} [()] \mid \hat{E} \; [o] \mid \hat{E} \; [o], O \end{array}$$ $$\begin{array}{rrcll} @@ -2197,7 +2207,7 @@ \textrm{Pre-projections} & p &::=& t.f & \textrm{one column from a table} \\ &&& t.\{\{c\}\} & \textrm{a record of columns from a table (of kind $\{\mt{Type}\}$)} \\ &&& t.* & \textrm{all columns from a table} \\ - &&& E \; [\mt{AS} \; f] & \textrm{expression column} \\ + &&& \hat{E} \; [\mt{AS} \; f] & \textrm{expression column} \\ \textrm{Table names} & t &::=& x & \textrm{constant table name (automatically capitalized)} \\ &&& X & \textrm{constant table name} \\ &&& \{\{c\}\} & \textrm{computed table name (of kind $\mt{Name}$)} \\ @@ -2216,8 +2226,7 @@ \textrm{SQL expressions} & E &::=& t.f & \textrm{column references} \\ &&& X & \textrm{named expression references} \\ &&& \{[e]\} & \textrm{injected native Ur expressions} \\ - &&& \{e\} & \textrm{computed expressions, probably using} \\ - &&&& \hspace{.1in} \textrm{$\mt{sql\_exp}$ directly} \\ + &&& \{e\} & \textrm{computed expressions, probably using $\mt{sql\_exp}$ directly} \\ &&& \mt{TRUE} \mid \mt{FALSE} & \textrm{boolean constants} \\ &&& \ell & \textrm{primitive type literals} \\ &&& \mt{NULL} & \textrm{null value (injection of $\mt{None}$)} \\ @@ -2226,12 +2235,10 @@ &&& n & \textrm{nullary operators} \\ &&& u \; E & \textrm{unary operators} \\ &&& E \; b \; E & \textrm{binary operators} \\ - &&& \mt{COUNT}(\ast) \; [w] & \textrm{count number of rows} \\ - &&& \mt{RANK}() \; [w] & \textrm{rank in sequence (Postgres only)} \\ - &&& a(E) \; [w] & \textrm{other aggregate function} \\ + &&& \mt{COUNT}(\ast) & \textrm{count number of rows} \\ + &&& a(E) & \textrm{other aggregate function} \\ &&& \mt{IF} \; E \; \mt{THEN} \; E \; \mt{ELSE} \; E & \textrm{conditional} \\ - &&& (Q) & \textrm{subquery (must return a single} \\ - &&&& \hspace{.1in} \textrm{expression column)} \\ + &&& (Q) & \textrm{subquery (must return a single expression column)} \\ &&& (E) & \textrm{explicit precedence} \\ \textrm{Nullary operators} & n &::=& \mt{CURRENT\_TIMESTAMP} \\ \textrm{Unary operators} & u &::=& \mt{NOT} \\ @@ -2239,7 +2246,13 @@ \textrm{Aggregate functions} & a &::=& \mt{COUNT} \mid \mt{AVG} \mid \mt{SUM} \mid \mt{MIN} \mid \mt{MAX} \\ \textrm{Directions} & o &::=& \mt{ASC} \mid \mt{DESC} \mid \{e\} \\ \textrm{SQL integer} & N &::=& n \mid \{e\} \\ - \textrm{Window} & w &::=& \mt{OVER} \; ([\mt{PARTITION} \; \mt{BY} \; E] \; [\mt{ORDER} \; \mt{BY} \; O]) & \textrm{(Postgres only)} + \textrm{Windowable expressions} & \hat{E} &::=& E \\ + &&& w \; [\mt{OVER} \; ( & \textrm{(Postgres only)} \\ + &&& \hspace{.1in} [\mt{PARTITION} \; \mt{BY} \; E] \\ + &&& \hspace{.1in} [\mt{ORDER} \; \mt{BY} \; O])] \\ + \textrm{Window function} & w &::=& \mt{RANK}() \\ + &&& \mt{COUNT}(*) \\ + &&& a(E) \end{array}$$ Additionally, an SQL expression may be inserted into normal Ur code with the syntax $(\mt{SQL} \; E)$ or $(\mt{WHERE} \; E)$. Similar shorthands exist for other nonterminals, with the prefix $\mt{FROM}$ for $\mt{FROM}$ items and $\mt{SELECT1}$ for pre-queries. diff -r 59b07fdae1ff -r 818d4097e2ed lib/ur/basis.urs --- a/lib/ur/basis.urs Sat Jun 02 16:47:09 2012 -0400 +++ b/lib/ur/basis.urs Sun Jun 03 11:29:31 2012 -0400 @@ -305,23 +305,15 @@ OnUpdate : propagation_mode ([mine1 = t] ++ mine)} -> sql_constraint ([mine1 = t] ++ mine ++ munused) [] -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 +con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type +val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type} -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] => - sql_exp fs agg exps aw t - -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') aw t + sql_exp fs agg exps t + -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') t val check : fs ::: {Type} - -> sql_exp [] [] fs disallow_window bool + -> sql_exp [] [] fs bool -> sql_constraint fs [] @@ -359,7 +351,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) [] [] disallow_window bool + -> sql_exp (free ++ tabs1 ++ tabs2) [] [] bool -> sql_from_items free (tabs1 ++ tabs2) class nullify :: Type -> Type -> Type @@ -370,14 +362,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) [] [] disallow_window bool + -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] 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) [] [] disallow_window bool + -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] 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)}} @@ -385,9 +377,12 @@ => $(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)) [] [] disallow_window bool + -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] bool -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2)) +(** [ORDER BY] and [SELECT] expressions may use window functions, so we introduce a type family for such expressions. *) +con sql_expw :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type + val sql_query1 : free ::: {{Type}} -> afree ::: {{Type}} -> tables ::: {{Type}} @@ -401,11 +396,11 @@ => [empties ~ selectedFields] => {Distinct : bool, From : sql_from_items free tables, - Where : sql_exp (free ++ tables) afree [] disallow_window bool, + Where : sql_exp (free ++ tables) afree [] bool, GroupBy : sql_subset tables grouped, - Having : sql_exp (free ++ grouped) (afree ++ tables) [] disallow_window bool, + Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool, SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields), - SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [] allow_window) + SelectExps : $(map (sql_expw (free ++ grouped) (afree ++ tables) []) selectedExps) } -> sql_query1 free afree tables selectedFields selectedExps @@ -432,10 +427,21 @@ val sql_asc : sql_direction val sql_desc : sql_direction +(** This type class supports automatic injection of either regular or window expressions into [sql_expw]. *) +class sql_window :: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type) -> Type +val sql_window_normal : sql_window sql_exp +val sql_window_fancy : sql_window sql_expw +val sql_window : tf ::: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type) + -> tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type + -> sql_window tf + -> tf tables agg exps t + -> sql_expw tables agg exps t + 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 allow_window t -> sql_direction +val sql_order_by_Cons : tf ::: ({{Type}} -> {{Type}} -> {Type} -> Type -> Type) -> tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type + -> sql_window tf + -> tf tables [] exps t -> sql_direction -> sql_order_by tables exps -> sql_order_by tables exps val sql_order_by_random : tables ::: {{Type}} -> exps ::: {Type} @@ -462,42 +468,42 @@ -> sql_query free afree selectedFields selectedExps val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} - -> aw ::: {Unit} -> fieldType ::: Type -> agg ::: {{Type}} + -> fieldType ::: Type -> agg ::: {{Type}} -> exps ::: {Type} -> tab :: Name -> field :: Name -> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) - agg exps aw fieldType + agg exps fieldType -val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> aw ::: {Unit} -> t ::: Type -> rest ::: {Type} +val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} -> nm :: Name - -> sql_exp tabs agg ([nm = t] ++ rest) aw t + -> sql_exp tabs agg ([nm = t] ++ rest) 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} - -> aw ::: {Unit} -> t ::: Type - -> sql_injectable t -> t -> sql_exp tables agg exps aw t + -> t ::: Type + -> sql_injectable t -> t -> sql_exp tables agg exps t val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> aw ::: {Unit} -> t ::: Type - -> sql_exp tables agg exps aw (option t) - -> sql_exp tables agg exps aw bool + -> t ::: Type + -> sql_exp tables agg exps (option t) + -> sql_exp tables agg exps bool val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> 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 + -> t ::: Type + -> sql_exp tables agg exps (option t) + -> sql_exp tables agg exps t + -> sql_exp tables agg exps t val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> 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 + -> 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 class sql_arith val sql_arith_int : sql_arith int @@ -507,9 +513,9 @@ con sql_unary :: Type -> Type -> Type val sql_not : sql_unary bool bool val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> aw ::: {Unit} -> arg ::: Type -> res ::: Type - -> sql_unary arg res -> sql_exp tables agg exps aw arg - -> sql_exp tables agg exps aw res + -> arg ::: Type -> res ::: Type + -> sql_unary arg res -> sql_exp tables agg exps arg + -> sql_exp tables agg exps res val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t @@ -517,10 +523,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} - -> 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 + -> 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 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 @@ -537,14 +543,14 @@ val sql_like : sql_binary string string bool -val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} - -> sql_exp tables agg exps aw int +val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> sql_exp tables agg exps int con sql_aggregate :: Type -> Type -> Type val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type - -> sql_aggregate dom ran -> sql_exp agg agg exps aw dom - -> sql_exp tables agg exps aw ran + -> dom ::: Type -> ran ::: Type + -> sql_aggregate dom ran -> sql_exp agg agg exps dom + -> sql_exp tables agg exps ran val sql_count_col : t ::: Type -> sql_aggregate (option t) int @@ -564,56 +570,59 @@ val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt -con sql_partition :: {{Type}} -> {{Type}} -> {Type} -> Type -val sql_no_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> sql_partition tables agg exps -val sql_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type - -> sql_exp tables agg exps disallow_window t - -> sql_partition tables agg exps - -con sql_window :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type -val sql_window : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_window tables agg exps t - -> sql_partition tables agg exps - -> sql_order_by tables exps - -> sql_exp tables agg exps allow_window t - -val sql_window_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type -> nt ::: Type - -> sql_aggregate t nt - -> sql_exp tables agg exps disallow_window t - -> sql_window tables agg exps nt -val sql_window_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> sql_window tables agg exps int -val sql_window_rank : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> sql_window tables agg exps int - con sql_nfunc :: Type -> Type val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> aw ::: {Unit} -> t ::: Type - -> sql_nfunc t -> sql_exp tables agg exps aw t + -> t ::: Type + -> sql_nfunc t -> sql_exp tables agg exps t val sql_current_timestamp : sql_nfunc time con sql_ufunc :: Type -> Type -> Type val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type - -> sql_ufunc dom ran -> sql_exp tables agg exps aw dom - -> sql_exp tables agg exps aw ran + -> dom ::: Type -> ran ::: Type + -> sql_ufunc dom ran -> sql_exp tables agg exps dom + -> sql_exp tables agg exps 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} -> aw ::: {Unit} -> t ::: Type +val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type -> sql_injectable_prim t - -> sql_exp tables agg exps aw t - -> sql_exp tables agg exps aw (option t) + -> sql_exp tables agg exps t + -> sql_exp tables agg exps (option t) -val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> aw ::: {Unit} -> t ::: Type -> nt ::: Type +val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type -> nt ::: Type -> nullify t nt -> sql_query tables agg [] [nm = t] - -> sql_exp tables agg exps aw nt + -> sql_exp tables agg exps nt + +(** Window function expressions *) + +con sql_partition :: {{Type}} -> {{Type}} -> {Type} -> Type +val sql_no_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> sql_partition tables agg exps +val sql_partition : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type + -> sql_exp tables agg exps t + -> sql_partition tables agg exps + +con sql_window_function :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type +val sql_window_function : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> t ::: Type + -> sql_window_function tables agg exps t + -> sql_partition tables agg exps + -> sql_order_by tables exps + -> sql_expw tables agg exps t + +val sql_window_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> t ::: Type -> nt ::: Type + -> sql_aggregate t nt + -> sql_exp tables agg exps t + -> sql_window_function tables agg exps nt +val sql_window_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> sql_window_function tables agg exps int +val sql_rank : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> sql_window_function tables agg exps int + (*** Executing queries *) @@ -637,19 +646,19 @@ val insert : fields ::: {Type} -> uniques ::: {{Unit}} -> sql_table fields uniques - -> $(map (fn t :: Type => sql_exp [] [] [] disallow_window t) fields) + -> $(map (fn t :: Type => sql_exp [] [] [] t) fields) -> dml val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} -> [changed ~ unchanged] => - $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] disallow_window t) changed) + $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed) -> sql_table (changed ++ unchanged) uniques - -> sql_exp [T = changed ++ unchanged] [] [] disallow_window bool + -> sql_exp [T = changed ++ unchanged] [] [] bool -> dml val delete : fields ::: {Type} -> uniques ::: {{Unit}} -> sql_table fields uniques - -> sql_exp [T = fields] [] [] disallow_window bool + -> sql_exp [T = fields] [] [] bool -> dml (*** Sequences *) diff -r 59b07fdae1ff -r 818d4097e2ed lib/ur/top.ur --- a/lib/ur/top.ur Sat Jun 02 16:47:09 2012 -0400 +++ b/lib/ur/top.ur Sun Jun 03 11:29:31 2012 -0400 @@ -376,14 +376,14 @@ oneRowE1 (SELECT COUNT( * ) > 0 AS B FROM t) fun eqNullable [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}] - [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)) = + [t ::: Type] (_ : sql_injectable (option t)) + (e1 : sql_exp tables agg exps (option t)) + (e2 : sql_exp tables agg exps (option t)) = (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2}) fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}] - [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t)) - (e1 : sql_exp tables agg exps aw (option t)) + [t ::: Type] (_ : sql_injectable (option t)) + (e1 : sql_exp tables agg exps (option t)) (e2 : option t) = case e2 of None => (SQL {e1} IS NULL) diff -r 59b07fdae1ff -r 818d4097e2ed lib/ur/top.urs --- a/lib/ur/top.urs Sat Jun 02 16:47:09 2012 -0400 +++ b/lib/ur/top.urs Sun Jun 03 11:29:31 2012 -0400 @@ -269,15 +269,15 @@ -> transaction bool val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> 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 + -> 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 val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> aw ::: {Unit} -> t ::: Type -> sql_injectable (option t) - -> sql_exp tables agg exps aw (option t) + -> t ::: Type -> sql_injectable (option t) + -> sql_exp tables agg exps (option t) -> option t - -> sql_exp tables agg exps aw bool + -> sql_exp tables agg exps bool val mkRead' : t ::: Type -> (string -> option t) -> string -> read t diff -r 59b07fdae1ff -r 818d4097e2ed src/elab_err.sml --- a/src/elab_err.sml Sat Jun 02 16:47:09 2012 -0400 +++ b/src/elab_err.sml Sun Jun 03 11:29:31 2012 -0400 @@ -242,7 +242,11 @@ eprefaces' ([("Class constraint", p_con env c)] @ (case E.resolveFailureCause () of NONE => [] - | SOME c' => [("Reduced to unresolvable", p_con env c')]))) + | SOME c' => [("Reduced to unresolvable", p_con env c')]))(*; + app (fn (c, rs) => (eprefaces' [("CLASS", p_con env c)]; + app (fn (c, e) => eprefaces' [("RULE", p_con env c), + ("IMPL", p_exp env e)]) rs)) + (E.listClasses env)*)) | IllegalRec (x, e) => (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)"; eprefaces' [("Variable", PD.string x), diff -r 59b07fdae1ff -r 818d4097e2ed src/monoize.sml --- a/src/monoize.sml Sat Jun 02 16:47:09 2012 -0400 +++ b/src/monoize.sml Sun Jun 03 11:29:31 2012 -0400 @@ -249,7 +249,13 @@ (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.CApp ((L.CFfi ("Basis", "sql_exp"), _), _), _), _), _), _), _), _), _), _) => + | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_exp"), _), _), _), _), _), _), _), _) => + (L'.TFfi ("Basis", "string"), loc) + | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_expw"), _), _), _), _), _), _), _), _) => + (L'.TFfi ("Basis", "string"), loc) + | L.CApp ((L.CFfi ("Basis", "sql_window"), _), _) => + (L'.TRecord [], loc) + | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_window_function"), _), _), _), _), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "primary_key"), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) @@ -299,16 +305,16 @@ (L'.TRecord [], loc) | L.CApp ((L.CFfi ("Basis", "sql_maxable"), _), _) => (L'.TRecord [], loc) - | L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_partition"), _), _), _), _), _), _) => - (L'.TFfi ("Basis", "string"), loc) - | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_window"), _), _), _), _), _), _), _), _) => - (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CFfi ("Basis", "sql_arith"), _), _) => (L'.TRecord [], loc) | L.CApp ((L.CFfi ("Basis", "sql_nfunc"), _), _) => (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_ufunc"), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) + | L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_partition"), _), _), _), _), _), _) => + (L'.TFfi ("Basis", "string"), loc) + | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_window"), _), _), _), _), _), _), _), _) => + (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CFfi ("Basis", "channel"), _), _) => (L'.TFfi ("Basis", "channel"), loc) @@ -2111,9 +2117,7 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_inject"), _), - _), _), + (L.EFfi ("Basis", "sql_inject"), _), _), _), _), _), _), _), @@ -2426,7 +2430,9 @@ | L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_order_by_Cons"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_order_by_Cons"), _), + _), _), _), _), _), _), _) => @@ -2434,19 +2440,20 @@ val s = (L'.TFfi ("Basis", "string"), loc) fun sc s = (L'.EPrim (Prim.String s), loc) in - ((L'.EAbs ("e1", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc), - (L'.EAbs ("d", s, (L'.TFun (s, s), loc), - (L'.EAbs ("e2", s, s, - (L'.ECase ((L'.ERel 0, loc), - [((L'.PPrim (Prim.String ""), loc), - strcat [(L'.ERel 2, loc), - (L'.ERel 1, loc)]), - ((L'.PWild, loc), - strcat [(L'.ERel 2, loc), - (L'.ERel 1, loc), - sc ", ", - (L'.ERel 0, loc)])], - {disc = s, result = s}), loc)), loc)), loc)), loc), + ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun (s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc)), loc), + (L'.EAbs ("e1", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc), + (L'.EAbs ("d", s, (L'.TFun (s, s), loc), + (L'.EAbs ("e2", s, s, + (L'.ECase ((L'.ERel 0, loc), + [((L'.PPrim (Prim.String ""), loc), + strcat [(L'.ERel 2, loc), + (L'.ERel 1, loc)]), + ((L'.PWild, loc), + strcat [(L'.ERel 2, loc), + (L'.ERel 1, loc), + sc ", ", + (L'.ERel 0, loc)])], + {disc = s, result = s}), loc)), loc)), loc)), loc)), loc), fm) end @@ -2512,10 +2519,8 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( (L.EFfi ("Basis", "sql_unary"), _), _), _), - _), _), _), _), _), _), _), _), @@ -2544,9 +2549,7 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_binary"), _), - _), _), + (L.EFfi ("Basis", "sql_binary"), _), _), _), _), _), _), _), @@ -2579,9 +2582,7 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_field"), _), - _), _), + (L.EFfi ("Basis", "sql_field"), _), _), _), _), _), _), _), @@ -2595,9 +2596,7 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_exp"), _), - _), _), + (L.EFfi ("Basis", "sql_exp"), _), _), _), _), _), _), _), @@ -2701,9 +2700,7 @@ | L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_count"), _), - _), _), + (L.EFfi ("Basis", "sql_count"), _), _), _), _), _), _) => ((L'.EPrim (Prim.String "COUNT(*)"), loc), @@ -2714,9 +2711,7 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_aggregate"), _), - _), _), + (L.EFfi ("Basis", "sql_aggregate"), _), _), _), _), _), _), _), @@ -2732,7 +2727,7 @@ sc ")"] in ((L'.EAbs ("c", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc), - (L'.EAbs ("e1", s, s, main), loc)), loc), + (L'.EAbs ("e1", s, (L'.TFun (s, s), loc), main), loc)), loc), fm) end @@ -2781,18 +2776,34 @@ (L'.EPrim (Prim.String "MIN"), loc)), loc)), loc), fm) - | L.ECApp ( - (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_no_partition"), _), - _), _), - _), _), - _) => ((L'.EPrim (Prim.String ""), loc), fm) + | L.EFfi ("Basis", "sql_asc") => ((L'.EPrim (Prim.String ""), loc), fm) + | L.EFfi ("Basis", "sql_desc") => ((L'.EPrim (Prim.String " DESC"), loc), fm) | L.ECApp ( (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_partition"), _), + (L.EFfi ("Basis", "sql_nfunc"), _), + _), _), + _), _), + _), _), + _) => + let + val s = (L'.TFfi ("Basis", "string"), loc) + fun sc s = (L'.EPrim (Prim.String s), loc) + in + ((L'.EAbs ("s", s, s, (L'.ERel 0, loc)), loc), + fm) + end + + | L.EFfi ("Basis", "sql_window_normal") => ((L'.ERecord [], loc), fm) + | L.EFfi ("Basis", "sql_window_fancy") => ((L'.ERecord [], loc), fm) + | L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.EFfi ("Basis", "sql_window"), _), + _), _), _), _), _), _), _), _), @@ -2800,108 +2811,20 @@ let val s = (L'.TFfi ("Basis", "string"), loc) in - ((L'.EAbs ("e", s, s, strcat [(L'.EPrim (Prim.String "PARTITION BY "), loc), (L'.ERel 0, loc)]), loc), + ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun (s, s), loc), + (L'.EAbs ("e", s, s, + (L'.ERel 0, loc)), loc)), loc), fm) end - | L.ECApp ( - (L.ECApp ( - (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_window"), _), - _), _), - _), _), - _), _), - _) => - let - val () = if #windowFunctions (Settings.currentDbms ()) then - () - else - ErrorMsg.errorAt loc "The DBMS you've selected doesn't support window functions." - - val s = (L'.TFfi ("Basis", "string"), loc) - fun sc s = (L'.EPrim (Prim.String s), loc) - - val main = strcat [(L'.ERel 2, loc), - sc " OVER (", - (L'.ERel 1, loc), - (L'.ECase ((L'.ERel 0, loc), - [((L'.PPrim (Prim.String ""), loc), - sc ""), - ((L'.PWild, loc), - strcat [sc " ORDER BY ", - (L'.ERel 0, loc)])], - {disc = s, - result = s}), loc), - sc ")"] - in - ((L'.EAbs ("w", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc), - (L'.EAbs ("p", s, (L'.TFun (s, s), loc), - (L'.EAbs ("o", s, s, - main), loc)), loc)), loc), - fm) - end + | L.EFfi ("Basis", "sql_current_timestamp") => ((L'.EPrim (Prim.String "CURRENT_TIMESTAMP"), loc), fm) | L.ECApp ( (L.ECApp ( (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_window_aggregate"), _), - _), _), - _), _), - _), _), - _), _), - _) => - let - val s = (L'.TFfi ("Basis", "string"), loc) - fun sc s = (L'.EPrim (Prim.String s), loc) - - val main = strcat [(L'.ERel 1, loc), - sc "(", - (L'.ERel 0, loc), - sc ")"] - in - ((L'.EAbs ("c", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc), - (L'.EAbs ("e1", s, s, main), loc)), loc), - fm) - end - - | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_window_count"), _), _), _), _), _), _) => - ((L'.EPrim (Prim.String "COUNT(*)"), loc), fm) - | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_window_rank"), _), _), _), _), _), _) => - ((L'.EPrim (Prim.String "RANK()"), loc), fm) - - | L.EFfi ("Basis", "sql_asc") => ((L'.EPrim (Prim.String ""), loc), fm) - | L.EFfi ("Basis", "sql_desc") => ((L'.EPrim (Prim.String " DESC"), loc), fm) - | L.ECApp ( - (L.ECApp ( - (L.ECApp ( - (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_nfunc"), _), - _), _), - _), _), - _), _), - _), _), - _) => - let - val s = (L'.TFfi ("Basis", "string"), loc) - fun sc s = (L'.EPrim (Prim.String s), loc) - in - ((L'.EAbs ("s", s, s, (L'.ERel 0, loc)), loc), - fm) - end - | L.EFfi ("Basis", "sql_current_timestamp") => ((L'.EPrim (Prim.String "CURRENT_TIMESTAMP"), loc), fm) - - | L.ECApp ( - (L.ECApp ( - (L.ECApp ( - (L.ECApp ( - (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_ufunc"), _), - _), _), + (L.EFfi ("Basis", "sql_ufunc"), _), _), _), _), _), _), _), @@ -2935,9 +2858,7 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_is_null"), _), _), - _), _), + (L.EFfi ("Basis", "sql_is_null"), _), _), _), _), _), _), _), _)) => @@ -2978,11 +2899,7 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_if_then_else"), _), _), - _), _), - _), _), + (L.EFfi ("Basis", "sql_if_then_else"), _), _), _), _), _), _), _), _)) => @@ -3007,9 +2924,7 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_nullable"), _), - _), _), + (L.EFfi ("Basis", "sql_nullable"), _), _), _), _), _), _), _), @@ -3030,9 +2945,7 @@ (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_subquery"), _), - _), _), + (L.EFfi ("Basis", "sql_subquery"), _), _), _), _), _), _), _), @@ -3051,6 +2964,97 @@ fm) end + | L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.EFfi ("Basis", "sql_no_partition"), _), + _), _), + _), _), + _) => ((L'.EPrim (Prim.String ""), loc), fm) + | L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.EFfi ("Basis", "sql_partition"), _), + _), _), + _), _), + _), _), + _) => + let + val s = (L'.TFfi ("Basis", "string"), loc) + in + ((L'.EAbs ("e", s, s, strcat [(L'.EPrim (Prim.String "PARTITION BY "), loc), (L'.ERel 0, loc)]), loc), + fm) + end + + | L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.EFfi ("Basis", "sql_window_function"), _), + _), _), + _), _), + _), _), + _) => + let + val () = if #windowFunctions (Settings.currentDbms ()) then + () + else + ErrorMsg.errorAt loc "The DBMS you've selected doesn't support window functions." + + val s = (L'.TFfi ("Basis", "string"), loc) + fun sc s = (L'.EPrim (Prim.String s), loc) + + val main = strcat [(L'.ERel 2, loc), + sc " OVER (", + (L'.ERel 1, loc), + (L'.ECase ((L'.ERel 0, loc), + [((L'.PPrim (Prim.String ""), loc), + sc ""), + ((L'.PWild, loc), + strcat [sc " ORDER BY ", + (L'.ERel 0, loc)])], + {disc = s, + result = s}), loc), + sc ")"] + in + ((L'.EAbs ("w", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc), + (L'.EAbs ("p", s, (L'.TFun (s, s), loc), + (L'.EAbs ("o", s, s, + main), loc)), loc)), loc), + fm) + end + + | L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.EFfi ("Basis", "sql_window_aggregate"), _), + _), _), + _), _), + _), _), + _), _), + _) => + let + val s = (L'.TFfi ("Basis", "string"), loc) + fun sc s = (L'.EPrim (Prim.String s), loc) + + val main = strcat [(L'.ERel 1, loc), + sc "(", + (L'.ERel 0, loc), + sc ")"] + in + ((L'.EAbs ("c", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc), + (L'.EAbs ("e1", s, s, main), loc)), loc), + fm) + end + + | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_window_count"), _), _), _), _), _), _) => + ((L'.EPrim (Prim.String "COUNT(*)"), loc), fm) + | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_rank"), _), _), _), _), _), _) => + ((L'.EPrim (Prim.String "RANK()"), loc), fm) + | L.EFfiApp ("Basis", "nextval", [(e, _)]) => let val (e, fm) = monoExp (env, st, fm) e diff -r 59b07fdae1ff -r 818d4097e2ed src/settings.sml --- a/src/settings.sml Sat Jun 02 16:47:09 2012 -0400 +++ b/src/settings.sml Sun Jun 03 11:29:31 2012 -0400 @@ -538,7 +538,7 @@ falseString : string, onlyUnion : bool, nestedRelops : bool, - windowFunctions : bool + windowFunctions: bool } val dbmses = ref ([] : dbms list) diff -r 59b07fdae1ff -r 818d4097e2ed src/urweb.grm --- a/src/urweb.grm Sat Jun 02 16:47:09 2012 -0400 +++ b/src/urweb.grm Sun Jun 03 11:29:31 2012 -0400 @@ -309,7 +309,7 @@ (ECApp ((EVar (["Basis"], "sql_order_by_Nil", Infer), dummy), (CWild (KRecord (KType, dummy), dummy), dummy)), dummy))) - val e' = (EVar (["Basis"], "sql_window", Infer), loc) + val e' = (EVar (["Basis"], "sql_window_function", Infer), loc) val e' = (EApp (e', e), loc) val e' = (EApp (e', pb), loc) in @@ -345,7 +345,7 @@ | UNION | INTERSECT | EXCEPT | LIMIT | OFFSET | ALL | TRUE | FALSE | CAND | OR | NOT - | COUNT | AVG | SUM | MIN | MAX | RANK + | COUNT | AVG | SUM | MIN | MAX | RANK | PARTITION | OVER | ASC | DESC | RANDOM | INSERT | INTO | VALUES | UPDATE | SET | DELETE | NULL | IS | COALESCE | LIKE | CURRENT_TIMESTAMP @@ -353,7 +353,6 @@ | CCONSTRAINT | UNIQUE | CHECK | PRIMARY | FOREIGN | KEY | ON | NO | ACTION | RESTRICT | CASCADE | REFERENCES | JOIN | INNER | CROSS | OUTER | LEFT | RIGHT | FULL | CIF | CTHEN | CELSE - | OVER | PARTITION %nonterm file of decl list @@ -1755,6 +1754,8 @@ exps) end + val exps = map (fn (c, e) => (c, (EApp ((EVar (["Basis"], "sql_window", Infer), loc), e), loc))) exps + val sel = (CRecord sel, loc) val grp = case gopt of @@ -2041,49 +2042,37 @@ | NULL (sql_inject ((EVar (["Basis"], "None", Infer), s (NULLleft, NULLright)))) - | COUNT LPAREN STAR RPAREN window (let - val loc = s (COUNTleft, windowright) - in - case window of - NONE => (EVar (["Basis"], "sql_count", Infer), loc) - | SOME _ => - let - val e = (EVar (["Basis"], "sql_window_count", Infer), loc) - in - applyWindow loc e window - end - end) - | RANK UNIT window (let - val loc = s (RANKleft, windowright) - val e = (EVar (["Basis"], "sql_window_rank", Infer), loc) - in - applyWindow loc e window - end) - | COUNT LPAREN sqlexp RPAREN window (let - val loc = s (COUNTleft, windowright) - - val e = (EVar (["Basis"], "sql_count_col", Infer), loc) - in - case window of - NONE => - let - val e = (EApp ((EVar (["Basis"], "sql_aggregate", Infer), loc), - e), loc) - in - (EApp (e, sqlexp), loc) - end - | SOME _ => - let - val e = (EApp ((EVar (["Basis"], "sql_window_aggregate", Infer), loc), - e), loc) - val e = (EApp (e, sqlexp), loc) - in - applyWindow loc e window - end - end) + | COUNT LPAREN STAR RPAREN window(let + val loc = s (COUNTleft, windowright) + in + case window of + NONE => (EVar (["Basis"], "sql_count", Infer), loc) + | SOME _ => applyWindow loc (EVar (["Basis"], "sql_window_count", Infer), loc) window + end) + | COUNT LPAREN sqlexp RPAREN window(let + val loc = s (COUNTleft, RPARENright) + val e = (EVar (["Basis"], "sql_count_col", Infer), loc) + in + case window of + NONE => + let + val e = (EApp ((EVar (["Basis"], "sql_aggregate", Infer), loc), + e), loc) + in + (EApp (e, sqlexp), loc) + end + | SOME _ => + let + val e = (EVar (["Basis"], "sql_count_col", Infer), loc) + val e = (EApp ((EVar (["Basis"], "sql_window_aggregate", Infer), loc), + e), loc) + in + applyWindow loc (EApp (e, sqlexp), loc) window + end + end) | sqlagg LPAREN sqlexp RPAREN window (let - val loc = s (sqlaggleft, windowright) - + val loc = s (sqlaggleft, RPARENright) + val e = (EVar (["Basis"], "sql_" ^ sqlagg, Infer), loc) in case window of @@ -2098,11 +2087,15 @@ let val e = (EApp ((EVar (["Basis"], "sql_window_aggregate", Infer), loc), e), loc) - val e = (EApp (e, sqlexp), loc) in - applyWindow loc e window + applyWindow loc (EApp (e, sqlexp), loc) window end end) + | RANK UNIT window (let + val loc = s (RANKleft, windowright) + in + applyWindow loc (EVar (["Basis"], "sql_rank", Infer), loc) window + end) | COALESCE LPAREN sqlexp COMMA sqlexp RPAREN (let val loc = s (COALESCEright, sqlexp2right) diff -r 59b07fdae1ff -r 818d4097e2ed src/urweb.lex --- a/src/urweb.lex Sat Jun 02 16:47:09 2012 -0400 +++ b/src/urweb.lex Sun Jun 03 11:29:31 2012 -0400 @@ -463,8 +463,6 @@ "OFFSET" => (Tokens.OFFSET (pos yypos, pos yypos + size yytext)); "ALL" => (Tokens.ALL (pos yypos, pos yypos + size yytext)); "SELECT1" => (Tokens.SELECT1 (pos yypos, pos yypos + size yytext)); - "OVER" => (Tokens.OVER (pos yypos, pos yypos + size yytext)); - "PARTITION" => (Tokens.PARTITION (pos yypos, pos yypos + size yytext)); "JOIN" => (Tokens.JOIN (pos yypos, pos yypos + size yytext)); "INNER" => (Tokens.INNER (pos yypos, pos yypos + size yytext)); @@ -490,6 +488,8 @@ "MIN" => (Tokens.MIN (pos yypos, pos yypos + size yytext)); "MAX" => (Tokens.MAX (pos yypos, pos yypos + size yytext)); "RANK" => (Tokens.RANK (pos yypos, pos yypos + size yytext)); + "PARTITION" => (Tokens.PARTITION (pos yypos, pos yypos + size yytext)); + "OVER" => (Tokens.OVER (pos yypos, pos yypos + size yytext)); "IF" => (Tokens.CIF (pos yypos, pos yypos + size yytext)); "THEN" => (Tokens.CTHEN (pos yypos, pos yypos + size yytext)); diff -r 59b07fdae1ff -r 818d4097e2ed tests/window.ur --- a/tests/window.ur Sat Jun 02 16:47:09 2012 -0400 +++ b/tests/window.ur Sun Jun 03 11:29:31 2012 -0400 @@ -1,6 +1,6 @@ table empsalary : { Depname : string, - Empno : int, - Salary : int } + Empno : int, + Salary : int } fun main () : transaction page = x <- queryX (SELECT empsalary.Depname, empsalary.Empno, empsalary.Salary,