diff options
| -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 | 90 | ||||
| -rw-r--r-- | lib/ur/basis.urs | 122 | ||||
| -rw-r--r-- | lib/ur/top.ur | 10 | ||||
| -rw-r--r-- | lib/ur/top.urs | 14 | ||||
| -rw-r--r-- | src/monoize.sml | 56 |
10 files changed, 186 insertions, 142 deletions
diff --git a/demo/batchFun.ur b/demo/batchFun.ur index d69d68af..69a68423 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 [] [] [] t.1) cols)] + [fn cols => $(map (fn t => sql_exp [] [] [] disallow_window t.1) cols)] (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] input col acc => acc ++ {nm = @sql_inject col.Inject input}) {} M.fl (r -- #Id) M.cols diff --git a/demo/crud.ur b/demo/crud.ur index 4d2753ea..0222e30f 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 [] [] [] t.1) cols)] + [fn cols => $(map (fn t => sql_exp [] [] [] disallow_window t.1) cols)] (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] => fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)}) {} M.fl inputs M.cols @@ -110,7 +110,7 @@ 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] [] [] t.1) cols)] + [fn cols => $(map (fn t => sql_exp [T = [Id = int] ++ map fst M.cols] [] [] disallow_window t.1) cols)] (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] => fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)}) diff --git a/demo/more/dbgrid.ur b/demo/more/dbgrid.ur index fc593533..13092db6 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 [] []] + @map2 [rawMeta] [ident] [sql_exp env [] [] disallow_window] (fn [t] meta v => @sql_inject meta.Inj v) wholeRow M.raw r @@ -396,12 +396,12 @@ functor Make(M : sig dml (insert M.tab (ensql row)); return row - fun selector (r : $M.key) : sql_exp [T = M.key ++ M.row] [] [] bool = + fun selector (r : $M.key) : sql_exp [T = M.key ++ M.row] [] [] disallow_window bool = @foldR2 [rawMeta] [ident] - [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool] + [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] disallow_window bool] (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key] (meta : rawMeta t) (v : t) - (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool) + (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] disallow_window bool) [rest :: {Type}] [rest ~ [nm = t] ++ key] => (WHERE T.{nm} = {@sql_inject meta.Inj v} AND {exp [[nm = t] ++ rest]})) (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE)) diff --git a/demo/more/orm.ur b/demo/more/orm.ur index 468281f7..2e1fc2e0 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 [] []) fs') = - @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1] + fun ensql [avail ::_] (r : row') : $(map (sql_exp avail [] [] disallow_window) fs') = + @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] disallow_window ts.1] (fn [ts] meta v => @sql_inject meta.Inj v) M.folder M.cols r @@ -53,11 +53,11 @@ functor Table(M : sig val list = resultsOut (SELECT * FROM t) - con col = fn t => {Exp : sql_exp [T = fs] [] [] t, + con col = fn t => {Exp : sql_exp [T = fs] [] [] disallow_window t, Inj : sql_injectable t} val idCol = {Exp = sql_field [#T] [#Id], Inj = _} con meta' = fn (fs :: {Type}) (col :: Type, parent :: Type) => - {Col : {Exp : sql_exp [T = fs] [] [] col, + {Col : {Exp : sql_exp [T = fs] [] [] disallow_window col, Inj : sql_injectable col}, Parent : $fs -> transaction (option parent)} val cols = @foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] => @@ -75,7 +75,7 @@ functor Table(M : sig M.folder M.cols [[Id = (id, row)]] ! - type filter = sql_exp [T = fs] [] [] bool + type filter = sql_exp [T = fs] [] [] disallow_window bool fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f}) fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f}) diff --git a/demo/more/versioned.ur b/demo/more/versioned.ur index d08ebcb0..5da8704c 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 [] [] []] + @map2 [sql_injectable] [ident] [sql_exp [] [] [] disallow_window] (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 [] [] [] (option t)] + [fn t => sql_exp [] [] [] disallow_window (option t)] (fn [t] x v => @sql_inject (@sql_option_prim x.Inj) (Some v)) M.dataFolder M.data (r --- M.key))) - fun keyExp (r : $M.key) : sql_exp [T = all] [] [] bool = + fun keyExp (r : $M.key) : sql_exp [T = all] [] [] disallow_window bool = @foldR2 [sql_injectable] [ident] [fn before => after :: {Type} -> [before ~ after] - => sql_exp [T = before ++ after] [] [] bool] + => sql_exp [T = before ++ after] [] [] disallow_window bool] (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before] (inj : sql_injectable t) (v : t) (e : after :: {Type} -> [before ~ after] - => sql_exp [T = before ++ after] [] [] bool) + => sql_exp [T = before ++ after] [] [] disallow_window bool) [after :: {Type}] [[nm = t] ++ before ~ after] => (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after]})) (fn [after :: {Type}] [[] ~ after] => (SQL TRUE)) @@ -113,7 +113,7 @@ functor Make(M : sig | Some cur => vr <- nextval s; let - val r' = @map3 [dmeta] [ident] [ident] [fn t => sql_exp [] [] [] (option t)] + val r' = @map3 [dmeta] [ident] [ident] [fn t => sql_exp [] [] [] disallow_window (option t)] (fn [t] (meta : dmeta t) old new => @sql_inject (@sql_option_prim meta.Inj) (if @@eq [_] meta.Eq old new then diff --git a/doc/manual.tex b/doc/manual.tex index c44089b8..62c20d44 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{bool} \to \mt{sql\_constraint} \; \mt{fs} \; [] + \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \mt{disallow\_window} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; [] \end{array}$$ Section \ref{tables} shows the expanded syntax of the $\mt{table}$ declaration and signature item that includes constraints. There is no other way to use constraints with SQL in Ur/Web. @@ -1662,11 +1662,11 @@ $$\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{bool}, \\ + \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; (\mt{free} \rc \mt{tables}) \; \mt{afree} \; [] \; \mt{disallow\_window} \; \mt{bool}, \\ \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\ - \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{bool}, \\ + \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{disallow\_window} \; \mt{bool}, \\ \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; \mt{empties} \rc \mt{selectedFields}), \\ - \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; []) \; \mt{selectedExps}) \} \\ + \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{allow\_window}) \; \mt{selectedExps}) \} \\ \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps} \end{array}$$ @@ -1680,24 +1680,26 @@ $$\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, and the type of the expression. +SQL expressions are used in several places, including $\mt{SELECT}$, $\mt{WHERE}$, $\mt{HAVING}$, and $\mt{ORDER} \; \mt{BY}$ clauses. They reify a fragment of the standard SQL expression language, while making it possible to inject ``native'' Ur values in some places. The arguments to the $\mt{sql\_exp}$ type family respectively give the unrestricted-availability table fields, the table fields that may only be used in arguments to aggregate functions, the available selected expressions, whether window functions are allowed, and the type of the expression. Two abstract constructors are declared to use to specify window function allowedness. $$\begin{array}{l} - \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type} + \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \{\mt{Unit}\} \to \mt{Type} \\ + \mt{con} \; \mt{disallow\_window} :: \{\mt{Unit}\} \\ + \mt{con} \; \mt{allow\_window} :: \{\mt{Unit}\} \end{array}$$ Any field in scope may be converted to an expression. $$\begin{array}{l} \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\ - \hspace{.1in} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\ + \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\ \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\ \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\ - \hspace{.1in} \to \mt{sql\_exp} \; ([\mt{tab} = [\mt{field} = \mt{fieldType}] \rc \mt{otherFields}] \rc \mt{otherTabs}) \; \mt{agg} \; \mt{exps} \; \mt{fieldType} + \hspace{.1in} \to \mt{sql\_exp} \; ([\mt{tab} = [\mt{field} = \mt{fieldType}] \rc \mt{otherFields}] \rc \mt{otherTabs}) \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{fieldType} \end{array}$$ There is an analogous function for referencing named expressions. $$\begin{array}{l} - \mt{val} \; \mt{sql\_exp} : \mt{tabs} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{t} ::: \mt{Type} \to \mt{rest} ::: \{\mt{Type}\} \to \mt{nm} :: \mt{Name} \\ - \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{t} + \mt{val} \; \mt{sql\_exp} : \mt{tabs} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \to \mt{rest} ::: \{\mt{Type}\} \to \mt{nm} :: \mt{Name} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{aw} \; \mt{t} \end{array}$$ Ur values of appropriate types may be injected into SQL expressions. @@ -1716,8 +1718,8 @@ $$\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{t} ::: \mt{Type} \to \mt{sql\_injectable} \; \mt{t} \\ - \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} + \mt{val} \; \mt{sql\_inject} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \to \mt{sql\_injectable} \; \mt{t} \\ + \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \end{array}$$ Additionally, most function-free types may be injected safely, via the $\mt{serialized}$ type family. @@ -1730,39 +1732,44 @@ $$\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{t} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{t}) \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool} + \mt{val} \; \mt{sql\_is\_null} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{aw} \; \mt{t}) \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{bool} \end{array}$$ As another way of dealing with null values, there is also a restricted form of the standard \cd{COALESCE} function. $$\begin{array}{l} \mt{val} \; \mt{sql\_coalesce} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ - \hspace{.1in} \to \mt{t} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{t}) \\ - \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ - \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} + \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; (\mt{option} \; \mt{t}) \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \end{array}$$ We have generic nullary, unary, and binary operators. $$\begin{array}{l} \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\ \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\ - \mt{val} \; \mt{sql\_nfunc} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\\end{array}$$ + \mt{val} \; \mt{sql\_nfunc} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} +\end{array}$$ $$\begin{array}{l} \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\ - \mt{val} \; \mt{sql\_unary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{arg} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_unary} \; \mt{arg} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{res} \\ + \mt{val} \; \mt{sql\_unary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{arg} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_unary} \; \mt{arg} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{res} \end{array}$$ $$\begin{array}{l} \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\ \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\ \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\ - \mt{val} \; \mt{sql\_binary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{arg_1} ::: \mt{Type} \to \mt{arg_2} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_binary} \; \mt{arg_1} \; \mt{arg_2} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg_1} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg_2} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{res} + \mt{val} \; \mt{sql\_binary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \\ + \hspace{.1in} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{arg_1} ::: \mt{Type} \to \mt{arg_2} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_binary} \; \mt{arg_1} \; \mt{arg_2} \; \mt{res} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg_1} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{arg_2} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{res} \end{array}$$ $$\begin{array}{l} @@ -1779,13 +1786,13 @@ $$\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}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{int} + \mt{val} \; \mt{sql\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \mt{aw} ::: \{\mt{Unit}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{int} \end{array}$$ $$\begin{array}{l} \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ - \mt{val} \; \mt{sql\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{dom} ::: \mt{Type} \to \mt{ran} ::: \mt{Type} \\ - \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{dom} \; \mt{ran} \to \mt{sql\_exp} \; \mt{agg} \; \mt{agg} \; \mt{exps} \; \mt{dom} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{ran} + \mt{val} \; \mt{sql\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Type}\} \mt{dom} ::: \mt{Type} \to \mt{ran} ::: \mt{Type} \\ + \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{dom} \; \mt{ran} \to \mt{sql\_exp} \; \mt{agg} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{dom} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{ran} \end{array}$$ $$\begin{array}{l} @@ -1815,17 +1822,18 @@ $$\begin{array}{l} Any SQL query that returns single columns may be turned into a subquery expression. $$\begin{array}{l} -\mt{val} \; \mt{sql\_subquery} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \to \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \\ -\hspace{.1in} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_query} \; \mt{tables} \; \mt{agg} \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{nt} +\mt{val} \; \mt{sql\_subquery} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \\ +\hspace{.1in} \to \mt{aw} ::: \mt{Type} \to \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \\ +\hspace{.1in} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_query} \; \mt{tables} \; \mt{agg} \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{nt} \end{array}$$ There is also an \cd{IF..THEN..ELSE..} construct that is compiled into standard SQL \cd{CASE} expressions. $$\begin{array}{l} -\mt{val} \; \mt{sql\_if\_then\_else} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ -\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool} \\ -\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ -\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ -\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} +\mt{val} \; \mt{sql\_if\_then\_else} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{aw} ::: \{\mt{Unit}\} \to \mt{t} ::: \mt{Type} \\ +\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{bool} \\ +\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\ +\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \\ +\hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{aw} \; \mt{t} \end{array}$$ \texttt{FROM} clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause. @@ -1840,7 +1848,7 @@ $$\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{bool} \\ + \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \\ \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{tabs2}) \end{array}$$ @@ -1858,7 +1866,7 @@ $$\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{bool} \\ + \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \\ \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.2)) \; \mt{tabs2}) \end{array}$$ @@ -1871,7 +1879,7 @@ $$\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{t} \to \mt{sql\_direction} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ + \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; [] \; \mt{exps} \; \mt{allow\_window} \; \mt{t} \to \mt{sql\_direction} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ \mt{val} \; \mt{sql\_order\_by\_random} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\ \\ \mt{type} \; \mt{sql\_limit} \\ @@ -1902,19 +1910,19 @@ $$\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{fields}) \to \mt{dml} + \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; [] \; \mt{disallow\_window}) \; \mt{fields}) \to \mt{dml} \end{array}$$ An $\mt{UPDATE}$ command is formed from a choice of which table fields to leave alone and which to change, along with an expression to use to compute the new value of each changed field and a $\mt{WHERE}$ clause. Note that, in the table environment applied to expressions, the table being updated is hardcoded at the name $\mt{T}$. The parsing extension for $\mt{UPDATE}$ will elaborate all table-free field references to use table variable $\mt{T}$. $$\begin{array}{l} \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to [\mt{changed} \sim \mt{unchanged}] \\ - \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\ - \hspace{.1in} \to \mt{sql\_table} \; (\mt{changed} \rc \mt{unchanged}) \to \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{bool} \to \mt{dml} + \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{disallow\_window}) \; \mt{changed}) \\ + \hspace{.1in} \to \mt{sql\_table} \; (\mt{changed} \rc \mt{unchanged}) \to \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \to \mt{dml} \end{array}$$ A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause. The above use of $\mt{T}$ is repeated. $$\begin{array}{l} - \mt{val} \; \mt{delete} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \to \mt{sql\_exp} \; [\mt{T} = \mt{fields}] \; [] \; [] \; \mt{bool} \to \mt{dml} + \mt{val} \; \mt{delete} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \to \mt{sql\_exp} \; [\mt{T} = \mt{fields}] \; [] \; [] \; \mt{disallow\_window} \; \mt{bool} \to \mt{dml} \end{array}$$ \subsubsection{Sequences} diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index 760cc4d2..27b6393b 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -305,15 +305,23 @@ val foreign_key : mine1 ::: Name -> t ::: Type -> mine ::: {Type} -> munused ::: OnUpdate : propagation_mode ([mine1 = t] ++ mine)} -> sql_constraint ([mine1 = t] ++ mine ++ munused) [] -con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type -val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type +con allow_window :: {Unit} +con disallow_window :: {Unit} + +con sql_exp :: {{Type}} (* Free tables, for normal use *) + -> {{Type}} (* Free tables, for use in arguments to aggregate functions *) + -> {Type} (* Free ad-hoc variables *) + -> {Unit} (* Allow window functions here? ([allow_window] indicates yes.) *) + -> Type (* SQL type of this expression *) + -> Type +val sql_exp_weaken : fs ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} -> t ::: Type -> fs' ::: {{Type}} -> agg' ::: {{Type}} -> exps' ::: {Type} -> [fs ~ fs'] => [agg ~ agg'] => [exps ~ exps'] => - sql_exp fs agg exps t - -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') t + sql_exp fs agg exps aw t + -> sql_exp (fs ++ fs') (agg ++ agg') (exps ++ exps') aw t val check : fs ::: {Type} - -> sql_exp [] [] fs bool + -> sql_exp [] [] fs disallow_window bool -> sql_constraint fs [] @@ -351,7 +359,7 @@ val sql_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) [] [] bool + -> sql_exp (free ++ tabs1 ++ tabs2) [] [] disallow_window bool -> sql_from_items free (tabs1 ++ tabs2) class nullify :: Type -> Type -> Type @@ -362,14 +370,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) [] [] bool + -> sql_exp (free ++ tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] disallow_window bool -> sql_from_items free (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2) val sql_right_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{Type}} -> [free ~ tabs1] => [free ~ tabs2] => [tabs1 ~ tabs2] => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs1) -> sql_from_items free (map (map (fn p :: (Type * Type) => p.1)) tabs1) -> sql_from_items free tabs2 - -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] bool + -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) tabs1 ++ tabs2) [] [] disallow_window bool -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) tabs1 ++ tabs2) val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 ::: {{(Type * Type)}} @@ -377,7 +385,7 @@ 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)) [] [] bool + -> sql_exp (free ++ map (map (fn p :: (Type * Type) => p.1)) (tabs1 ++ tabs2)) [] [] disallow_window bool -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2)) val sql_query1 : free ::: {{Type}} @@ -393,11 +401,11 @@ val sql_query1 : free ::: {{Type}} => [empties ~ selectedFields] => {Distinct : bool, From : sql_from_items free tables, - Where : sql_exp (free ++ tables) afree [] bool, + Where : sql_exp (free ++ tables) afree [] disallow_window bool, GroupBy : sql_subset tables grouped, - Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool, + Having : sql_exp (free ++ grouped) (afree ++ tables) [] disallow_window bool, SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields), - SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) []) + SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) [] allow_window) selectedExps) } -> sql_query1 free afree tables selectedFields selectedExps @@ -427,7 +435,7 @@ val sql_desc : sql_direction con sql_order_by :: {{Type}} -> {Type} -> Type val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type - -> sql_exp tables [] exps t -> sql_direction + -> sql_exp tables [] exps allow_window t -> sql_direction -> sql_order_by tables exps -> sql_order_by tables exps val sql_order_by_random : tables ::: {{Type}} -> exps ::: {Type} @@ -454,42 +462,42 @@ val sql_query : free ::: {{Type}} -> sql_query free afree selectedFields selectedExps val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} - -> fieldType ::: Type -> agg ::: {{Type}} + -> aw ::: {Unit} -> fieldType ::: Type -> agg ::: {{Type}} -> exps ::: {Type} -> tab :: Name -> field :: Name -> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) - agg exps fieldType + agg exps aw fieldType -val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} +val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> aw ::: {Unit} -> t ::: Type -> rest ::: {Type} -> nm :: Name - -> sql_exp tabs agg ([nm = t] ++ rest) t + -> sql_exp tabs agg ([nm = t] ++ rest) aw t class sql_injectable val sql_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable t val sql_option_prim : t ::: Type -> sql_injectable_prim t -> sql_injectable (option t) val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_injectable t -> t -> sql_exp tables agg exps t + -> aw ::: {Unit} -> t ::: Type + -> sql_injectable t -> t -> sql_exp tables agg exps aw t val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_exp tables agg exps (option t) - -> sql_exp tables agg exps bool + -> aw ::: {Unit} -> t ::: Type + -> sql_exp tables agg exps aw (option t) + -> sql_exp tables agg exps aw bool val sql_coalesce : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_exp tables agg exps (option t) - -> sql_exp tables agg exps t - -> sql_exp tables agg exps t + -> aw ::: {Unit} -> t ::: Type + -> sql_exp tables agg exps aw (option t) + -> sql_exp tables agg exps aw t + -> sql_exp tables agg exps aw t val sql_if_then_else : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_exp tables agg exps bool - -> sql_exp tables agg exps t - -> sql_exp tables agg exps t - -> sql_exp tables agg exps t + -> aw ::: {Unit} -> t ::: Type + -> sql_exp tables agg exps aw bool + -> sql_exp tables agg exps aw t + -> sql_exp tables agg exps aw t + -> sql_exp tables agg exps aw t class sql_arith val sql_arith_int : sql_arith int @@ -499,9 +507,9 @@ 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} - -> arg ::: Type -> res ::: Type - -> sql_unary arg res -> sql_exp tables agg exps arg - -> sql_exp tables agg exps res + -> aw ::: {Unit} -> arg ::: Type -> res ::: Type + -> sql_unary arg res -> sql_exp tables agg exps aw arg + -> sql_exp tables agg exps aw res val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t @@ -509,10 +517,10 @@ 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} - -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type - -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1 - -> sql_exp tables agg exps arg2 - -> sql_exp tables agg exps res + -> aw ::: {Unit} -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type + -> sql_binary arg1 arg2 res -> sql_exp tables agg exps aw arg1 + -> sql_exp tables agg exps aw arg2 + -> sql_exp tables agg exps aw res val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t @@ -529,14 +537,14 @@ val sql_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} - -> sql_exp tables agg exps int +val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} + -> sql_exp tables agg exps aw int con sql_aggregate :: Type -> Type -> Type val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> dom ::: Type -> ran ::: Type - -> sql_aggregate dom ran -> sql_exp agg agg exps dom - -> sql_exp tables agg exps ran + -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type + -> sql_aggregate dom ran -> sql_exp agg agg exps aw dom + -> sql_exp tables agg exps aw ran val sql_count_col : t ::: Type -> sql_aggregate (option t) int @@ -558,29 +566,29 @@ val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_ con sql_nfunc :: Type -> Type val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type - -> sql_nfunc t -> sql_exp tables agg exps t + -> aw ::: {Unit} -> t ::: Type + -> sql_nfunc t -> sql_exp tables agg exps aw t val sql_current_timestamp : sql_nfunc time con sql_ufunc :: Type -> Type -> Type val sql_ufunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> dom ::: Type -> ran ::: Type - -> sql_ufunc dom ran -> sql_exp tables agg exps dom - -> sql_exp tables agg exps ran + -> aw ::: {Unit} -> dom ::: Type -> ran ::: Type + -> sql_ufunc dom ran -> sql_exp tables agg exps aw dom + -> sql_exp tables agg exps aw ran val sql_octet_length : sql_ufunc blob int val sql_known : t ::: Type -> sql_ufunc t bool val sql_lower : sql_ufunc string string val sql_upper : sql_ufunc string string -val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type +val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> aw ::: {Unit} -> t ::: Type -> sql_injectable_prim t - -> sql_exp tables agg exps t - -> sql_exp tables agg exps (option t) + -> sql_exp tables agg exps aw t + -> sql_exp tables agg exps aw (option t) -val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type -> nt ::: Type +val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> aw ::: {Unit} -> t ::: Type -> nt ::: Type -> nullify t nt -> sql_query tables agg [] [nm = t] - -> sql_exp tables agg exps nt + -> sql_exp tables agg exps aw nt (*** Executing queries *) @@ -604,19 +612,19 @@ val tryDml : dml -> transaction (option string) val insert : fields ::: {Type} -> uniques ::: {{Unit}} -> sql_table fields uniques - -> $(map (fn t :: Type => sql_exp [] [] [] t) fields) + -> $(map (fn t :: Type => sql_exp [] [] [] disallow_window t) fields) -> dml val update : unchanged ::: {Type} -> uniques ::: {{Unit}} -> changed :: {Type} -> [changed ~ unchanged] => - $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed) + $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] disallow_window t) changed) -> sql_table (changed ++ unchanged) uniques - -> sql_exp [T = changed ++ unchanged] [] [] bool + -> sql_exp [T = changed ++ unchanged] [] [] disallow_window bool -> dml val delete : fields ::: {Type} -> uniques ::: {{Unit}} -> sql_table fields uniques - -> sql_exp [T = fields] [] [] bool + -> sql_exp [T = fields] [] [] disallow_window bool -> dml (*** Sequences *) diff --git a/lib/ur/top.ur b/lib/ur/top.ur index e504204e..60774ba5 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}] - [t ::: Type] (_ : sql_injectable (option t)) - (e1 : sql_exp tables agg exps (option t)) - (e2 : sql_exp tables agg exps (option t)) = + [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t)) + (e1 : sql_exp tables agg exps aw (option t)) + (e2 : sql_exp tables agg exps aw (option t)) = (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2}) fun eqNullable' [tables ::: {{Type}}] [agg ::: {{Type}}] [exps ::: {Type}] - [t ::: Type] (_ : sql_injectable (option t)) - (e1 : sql_exp tables agg exps (option t)) + [aw ::: {Unit}] [t ::: Type] (_ : sql_injectable (option t)) + (e1 : sql_exp tables agg exps aw (option t)) (e2 : option t) = case e2 of None => (SQL {e1} IS NULL) diff --git a/lib/ur/top.urs b/lib/ur/top.urs index 489e744d..def3bc63 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} - -> t ::: Type -> sql_injectable (option t) - -> sql_exp tables agg exps (option t) - -> sql_exp tables agg exps (option t) - -> sql_exp tables agg exps bool + -> aw ::: {Unit} -> t ::: Type -> sql_injectable (option t) + -> sql_exp tables agg exps aw (option t) + -> sql_exp tables agg exps aw (option t) + -> sql_exp tables agg exps aw bool val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> t ::: Type -> sql_injectable (option t) - -> sql_exp tables agg exps (option t) + -> aw ::: {Unit} -> t ::: Type -> sql_injectable (option t) + -> sql_exp tables agg exps aw (option t) -> option t - -> sql_exp tables agg exps bool + -> sql_exp tables agg exps aw bool val mkRead' : t ::: Type -> (string -> option t) -> string -> read t diff --git a/src/monoize.sml b/src/monoize.sml index 46feacf8..7fba8c98 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -249,7 +249,7 @@ 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.CFfi ("Basis", "sql_exp"), _), _), _), _), _), _), _), _) => + | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_exp"), _), _), _), _), _), _), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "primary_key"), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) @@ -2107,7 +2107,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_inject"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_inject"), _), + _), _), _), _), _), _), _), _), @@ -2506,8 +2508,10 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( + (L.ECApp ( (L.EFfi ("Basis", "sql_unary"), _), _), _), + _), _), _), _), _), _), _), _), @@ -2536,7 +2540,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_binary"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_binary"), _), + _), _), _), _), _), _), _), _), @@ -2569,7 +2575,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_field"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_field"), _), + _), _), _), _), _), _), _), _), @@ -2583,7 +2591,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_exp"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_exp"), _), + _), _), _), _), _), _), _), _), @@ -2687,7 +2697,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = | L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_count"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_count"), _), + _), _), _), _), _), _), _) => ((L'.EPrim (Prim.String "COUNT(*)"), loc), @@ -2698,7 +2710,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_aggregate"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_aggregate"), _), + _), _), _), _), _), _), _), _), @@ -2770,11 +2784,13 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_nfunc"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_nfunc"), _), + _), _), _), _), _), _), _), _), - _) => + _) => let val s = (L'.TFfi ("Basis", "string"), loc) fun sc s = (L'.EPrim (Prim.String s), loc) @@ -2789,7 +2805,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_ufunc"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_ufunc"), _), + _), _), _), _), _), _), _), _), @@ -2823,7 +2841,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_is_null"), _), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_is_null"), _), _), + _), _), _), _), _), _), _), _)) => @@ -2864,7 +2884,11 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_if_then_else"), _), _), + (L.ECApp ( + (L.ECApp ( + (L.EFfi ("Basis", "sql_if_then_else"), _), _), + _), _), + _), _), _), _), _), _), _), _)) => @@ -2889,7 +2913,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_nullable"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_nullable"), _), + _), _), _), _), _), _), _), _), @@ -2910,7 +2936,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_subquery"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_subquery"), _), + _), _), _), _), _), _), _), _), |