Mercurial > urweb
comparison doc/manual.tex @ 1573:34364e383bed
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 \\ |