diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2012-06-03 11:29:31 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2012-06-03 11:29:31 -0400 |
| commit | 797db05343b520b16ea4f8eeab5fea6255d3284d (patch) | |
| tree | deacf0a9ebedccbc3e22fdb143c51d3dcc153a5b | |
| parent | 858481a426ea3873440c3bed30eb563f8cf3480e (diff) | |
Lighter-weight encoding of window function use
| -rw-r--r-- | demo/batchFun.ur | 2 | ||||
| -rw-r--r-- | demo/crud.ur | 4 | ||||
| -rw-r--r-- | demo/more/dbgrid.ur | 8 | ||||
| -rw-r--r-- | demo/more/orm.ur | 10 | ||||
| -rw-r--r-- | demo/more/versioned.ur | 12 | ||||
| -rw-r--r-- | doc/manual.tex | 177 | ||||
| -rw-r--r-- | lib/ur/basis.urs | 191 | ||||
| -rw-r--r-- | lib/ur/top.ur | 10 | ||||
| -rw-r--r-- | lib/ur/top.urs | 14 | ||||
| -rw-r--r-- | src/elab_err.sml | 6 | ||||
| -rw-r--r-- | src/monoize.sml | 280 | ||||
| -rw-r--r-- | src/settings.sml | 2 | ||||
| -rw-r--r-- | src/urweb.grm | 87 | ||||
| -rw-r--r-- | src/urweb.lex | 4 | ||||
| -rw-r--r-- | tests/window.ur | 4 |
15 files changed, 417 insertions, 394 deletions
diff --git a/demo/batchFun.ur b/demo/batchFun.ur index 69a68423..d69d68af 100644 --- a/demo/batchFun.ur +++ b/demo/batchFun.ur @@ -46,7 +46,7 @@ functor Make(M : sig 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 --git a/demo/crud.ur b/demo/crud.ur index 0222e30f..4d2753ea 100644 --- a/demo/crud.ur +++ b/demo/crud.ur @@ -93,7 +93,7 @@ functor Make(M : sig 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 @@ functor Make(M : sig 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 --git a/demo/more/dbgrid.ur b/demo/more/dbgrid.ur index 13092db6..fc593533 100644 --- a/demo/more/dbgrid.ur +++ b/demo/more/dbgrid.ur @@ -385,7 +385,7 @@ functor Make(M : sig 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 @@ functor Make(M : sig 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 --git a/demo/more/orm.ur b/demo/more/orm.ur index 2e1fc2e0..468281f7 100644 --- a/demo/more/orm.ur +++ b/demo/more/orm.ur @@ -32,8 +32,8 @@ functor Table(M : sig 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 @@ functor Table(M : sig 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 @@ functor Table(M : sig 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 --git a/demo/more/versioned.ur b/demo/more/versioned.ur index 5da8704c..d08ebcb0 100644 --- a/demo/more/versioned.ur +++ b/demo/more/versioned.ur @@ -24,7 +24,7 @@ functor Make(M : sig 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 @@ functor Make(M : sig ({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 @@ functor Make(M : sig | 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 --git a/doc/manual.tex b/doc/manual.tex index 7f8b01c2..589177dd 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -1595,7 +1595,7 @@ $$\begin{array}{l} 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 @@ $$\begin{array}{l} \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 @@ $$\begin{array}{l} \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 @@ $$\begin{array}{l} \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 @@ $$\begin{array}{l} 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 @@ $$\begin{array}{l} 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 @@ $$\begin{array}{l} \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: - -$$\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 @@ $$\begin{array}{l} \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 @@ $$\begin{array}{l} \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 @@ $$\begin{array}{l} \\ \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 @@ $$\begin{array}{l} \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 @@ $$\begin{array}{l} 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 @@ $$\begin{array}{rrcll} \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 @@ $$\begin{array}{rrcll} \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 @@ $$\begin{array}{rrcll} \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 @@ $$\begin{array}{rrcll} &&& 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 @@ $$\begin{array}{rrcll} \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 --git a/lib/ur/basis.urs b/lib/ur/basis.urs index 68e20fb0..bea6e105 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -305,23 +305,15 @@ val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused ::: 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_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type 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 @@ val sql_left_join : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{(Type -> [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 @@ val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 :: => $(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 @@ val sql_query1 : free ::: {{Type}} => [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 @@ type sql_direction 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 @@ val sql_query : free ::: {{Type}} -> 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 @@ val sql_arith_option : t ::: Type -> sql_arith t -> sql_arith (option t) 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 @@ con sql_binary :: Type -> Type -> Type -> Type 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_ge : t ::: Type -> sql_binary t t bool 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_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t) 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 tryDml : dml -> transaction (option string) 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 --git a/lib/ur/top.ur b/lib/ur/top.ur index 60774ba5..e504204e 100644 --- a/lib/ur/top.ur +++ b/lib/ur/top.ur @@ -376,14 +376,14 @@ fun nonempty [fs] [us] (t : sql_table fs us) = 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 --git a/lib/ur/top.urs b/lib/ur/top.urs index def3bc63..489e744d 100644 --- a/lib/ur/top.urs +++ b/lib/ur/top.urs @@ -269,15 +269,15 @@ val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us -> 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 --git a/src/elab_err.sml b/src/elab_err.sml index 0e04cf51..4754d4ce 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -242,7 +242,11 @@ fun expError env err = 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 --git a/src/monoize.sml b/src/monoize.sml index 8224b26f..4985c932 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -249,7 +249,13 @@ fun monoType env = (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 @@ fun monoType env = (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 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_inject"), _), - _), _), + (L.EFfi ("Basis", "sql_inject"), _), _), _), _), _), _), _), @@ -2426,7 +2430,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = | 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 @@ fun monoExp (env, st, fm) (all as (e, loc)) = 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 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( (L.EFfi ("Basis", "sql_unary"), _), _), _), - _), _), _), _), _), _), _), _), @@ -2544,9 +2549,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_binary"), _), - _), _), + (L.EFfi ("Basis", "sql_binary"), _), _), _), _), _), _), _), @@ -2579,9 +2582,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_field"), _), - _), _), + (L.EFfi ("Basis", "sql_field"), _), _), _), _), _), _), _), @@ -2595,9 +2596,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_exp"), _), - _), _), + (L.EFfi ("Basis", "sql_exp"), _), _), _), _), _), _), _), @@ -2701,9 +2700,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = | 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 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_aggregate"), _), - _), _), + (L.EFfi ("Basis", "sql_aggregate"), _), _), _), _), _), _), _), @@ -2732,7 +2727,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = 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,73 +2776,33 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (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.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.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_window"), _), + (L.EFfi ("Basis", "sql_nfunc"), _), _), _), _), _), _), _), - _) => + _) => 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), + ((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_aggregate"), _), + (L.EFfi ("Basis", "sql_window"), _), _), _), _), _), _), _), @@ -2855,43 +2810,13 @@ fun monoExp (env, st, fm) (all as (e, loc)) = _) => 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), + ((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.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 ( @@ -2899,9 +2824,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_ufunc"), _), - _), _), + (L.EFfi ("Basis", "sql_ufunc"), _), _), _), _), _), _), _), @@ -2935,9 +2858,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_is_null"), _), _), - _), _), + (L.EFfi ("Basis", "sql_is_null"), _), _), _), _), _), _), _), _)) => @@ -2978,11 +2899,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (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 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_nullable"), _), - _), _), + (L.EFfi ("Basis", "sql_nullable"), _), _), _), _), _), _), _), @@ -3030,9 +2945,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.ECApp ( - (L.EFfi ("Basis", "sql_subquery"), _), - _), _), + (L.EFfi ("Basis", "sql_subquery"), _), _), _), _), _), _), _), @@ -3051,6 +2964,97 @@ fun monoExp (env, st, fm) (all as (e, loc)) = 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 --git a/src/settings.sml b/src/settings.sml index 3b89ce46..28739d6a 100644 --- a/src/settings.sml +++ b/src/settings.sml @@ -538,7 +538,7 @@ type dbms = { falseString : string, onlyUnion : bool, nestedRelops : bool, - windowFunctions : bool + windowFunctions: bool } val dbmses = ref ([] : dbms list) diff --git a/src/urweb.grm b/src/urweb.grm index eec8f8c1..708e5fcd 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -309,7 +309,7 @@ fun applyWindow loc e window = (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 @@ fun applyWindow loc e window = | 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 @@ fun applyWindow loc e window = | 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 @@ query1 : SELECT dopt select FROM tables wopt gopt hopt 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 @@ sqlexp : TRUE (sql_inject (EVar (["Basis"], "True", In | 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 @@ sqlexp : TRUE (sql_inject (EVar (["Basis"], "True", In 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 --git a/src/urweb.lex b/src/urweb.lex index 272c5e65..0994ecec 100644 --- a/src/urweb.lex +++ b/src/urweb.lex @@ -463,8 +463,6 @@ xint = x[0-9a-fA-F][0-9a-fA-F]; <INITIAL> "OFFSET" => (Tokens.OFFSET (pos yypos, pos yypos + size yytext)); <INITIAL> "ALL" => (Tokens.ALL (pos yypos, pos yypos + size yytext)); <INITIAL> "SELECT1" => (Tokens.SELECT1 (pos yypos, pos yypos + size yytext)); -<INITIAL> "OVER" => (Tokens.OVER (pos yypos, pos yypos + size yytext)); -<INITIAL> "PARTITION" => (Tokens.PARTITION (pos yypos, pos yypos + size yytext)); <INITIAL> "JOIN" => (Tokens.JOIN (pos yypos, pos yypos + size yytext)); <INITIAL> "INNER" => (Tokens.INNER (pos yypos, pos yypos + size yytext)); @@ -490,6 +488,8 @@ xint = x[0-9a-fA-F][0-9a-fA-F]; <INITIAL> "MIN" => (Tokens.MIN (pos yypos, pos yypos + size yytext)); <INITIAL> "MAX" => (Tokens.MAX (pos yypos, pos yypos + size yytext)); <INITIAL> "RANK" => (Tokens.RANK (pos yypos, pos yypos + size yytext)); +<INITIAL> "PARTITION" => (Tokens.PARTITION (pos yypos, pos yypos + size yytext)); +<INITIAL> "OVER" => (Tokens.OVER (pos yypos, pos yypos + size yytext)); <INITIAL> "IF" => (Tokens.CIF (pos yypos, pos yypos + size yytext)); <INITIAL> "THEN" => (Tokens.CTHEN (pos yypos, pos yypos + size yytext)); diff --git a/tests/window.ur b/tests/window.ur index dc338a43..c0eaf6e2 100644 --- a/tests/window.ur +++ b/tests/window.ur @@ -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, |