Mercurial > urweb

comparison doc/manual.tex @ 1573:34364e383bed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
For new IF, fix Monoize typing and add to manual
author Adam Chlipala <adam@chlipala.net>
date Sat, 15 Oct 2011 09:04:41 -0400
parents 0fab80567fa3
children 644558d9c756
comparison
equal deleted inserted replaced
1572:5530a8075b62 1573:34364e383bed
1781 $$\begin{array}{l} 1781 $$\begin{array}{l}
1782 \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} \\ 1782 \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} \\
1783 \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} 1783 \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}
1784 \end{array}$$ 1784 \end{array}$$
1785 1785
1786 There is also an \cd{IF..THEN..ELSE..} construct that is compiled into standard SQL \cd{CASE} expressions.
1787 $$\begin{array}{l}
1788 \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} \\
1789 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool} \\
1790 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
1791 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\
1792 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
1793 \end{array}$$
1794
1786 \texttt{FROM} clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause. 1795 \texttt{FROM} clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause.
1787 $$\begin{array}{l} 1796 $$\begin{array}{l}
1788 \mt{con} \; \mt{sql\_from\_items} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\ 1797 \mt{con} \; \mt{sql\_from\_items} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\
1789 \mt{val} \; \mt{sql\_from\_table} : \mt{free} ::: \{\{\mt{Type}\}\} \\ 1798 \mt{val} \; \mt{sql\_from\_table} : \mt{free} ::: \{\{\mt{Type}\}\} \\
1790 \hspace{.1in} \to \mt{t} ::: \mt{Type} \to \mt{fs} ::: \{\mt{Type}\} \to \mt{fieldsOf} \; \mt{t} \; \mt{fs} \to \mt{name} :: \mt{Name} \to \mt{t} \to \mt{sql\_from\_items} \; \mt{free} \; [\mt{name} = \mt{fs}] \\ 1799 \hspace{.1in} \to \mt{t} ::: \mt{Type} \to \mt{fs} ::: \{\mt{Type}\} \to \mt{fieldsOf} \; \mt{t} \; \mt{fs} \to \mt{name} :: \mt{Name} \to \mt{t} \to \mt{sql\_from\_items} \; \mt{free} \; [\mt{name} = \mt{fs}] \\
2131 &&& n & \textrm{nullary operators} \\ 2140 &&& n & \textrm{nullary operators} \\
2132 &&& u \; E & \textrm{unary operators} \\ 2141 &&& u \; E & \textrm{unary operators} \\
2133 &&& E \; b \; E & \textrm{binary operators} \\ 2142 &&& E \; b \; E & \textrm{binary operators} \\
2134 &&& \mt{COUNT}(\ast) & \textrm{count number of rows} \\ 2143 &&& \mt{COUNT}(\ast) & \textrm{count number of rows} \\
2135 &&& a(E) & \textrm{other aggregate function} \\ 2144 &&& a(E) & \textrm{other aggregate function} \\
2145 &&& \mt{IF} \; E \; \mt{THEN} \; E \; \mt{ELSE} \; E & \textrm{conditional} \\
2136 &&& (Q) & \textrm{subquery (must return a single expression column)} \\ 2146 &&& (Q) & \textrm{subquery (must return a single expression column)} \\
2137 &&& (E) & \textrm{explicit precedence} \\ 2147 &&& (E) & \textrm{explicit precedence} \\
2138 \textrm{Nullary operators} & n &::=& \mt{CURRENT\_TIMESTAMP} \\ 2148 \textrm{Nullary operators} & n &::=& \mt{CURRENT\_TIMESTAMP} \\
2139 \textrm{Unary operators} & u &::=& \mt{NOT} \\ 2149 \textrm{Unary operators} & u &::=& \mt{NOT} \\
2140 \textrm{Binary operators} & b &::=& \mt{AND} \mid \mt{OR} \mid \neq \mid < \mid \leq \mid > \mid \geq \\ 2150 \textrm{Binary operators} & b &::=& \mt{AND} \mid \mt{OR} \mid \neq \mid < \mid \leq \mid > \mid \geq \\