comparison doc/manual.tex @ 1684:9dd8d47c3e58

Extend and document RANDOM
author Adam Chlipala <adam@chlipala.net>
date Sat, 04 Feb 2012 10:42:18 -0500
parents be1ed46d73e2
children 0930c92a608e
comparison
equal deleted inserted replaced
1683:be1ed46d73e2 1684:9dd8d47c3e58
1846 \\ 1846 \\
1847 \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ 1847 \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
1848 \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} \\ 1848 \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} \\
1849 \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ 1849 \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
1850 \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} \\ 1850 \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} \\
1851 \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} \\
1851 \\ 1852 \\
1852 \mt{type} \; \mt{sql\_limit} \\ 1853 \mt{type} \; \mt{sql\_limit} \\
1853 \mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\ 1854 \mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\
1854 \mt{val} \; \mt{sql\_limit} : \mt{int} \to \mt{sql\_limit} \\ 1855 \mt{val} \; \mt{sql\_limit} : \mt{int} \to \mt{sql\_limit} \\
1855 \\ 1856 \\
2123 \subsubsection{Queries} 2124 \subsubsection{Queries}
2124 2125
2125 Queries $Q$ are added to the rules for expressions $e$. 2126 Queries $Q$ are added to the rules for expressions $e$.
2126 2127
2127 $$\begin{array}{rrcll} 2128 $$\begin{array}{rrcll}
2128 \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; (E \; [o],)^+] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\ 2129 \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; O] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\
2129 \textrm{Pre-queries} & q &::=& \mt{SELECT} \; [\mt{DISTINCT}] \; P \; \mt{FROM} \; F,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\ 2130 \textrm{Pre-queries} & q &::=& \mt{SELECT} \; [\mt{DISTINCT}] \; P \; \mt{FROM} \; F,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\
2130 &&& \mid q \; R \; q \mid \{\{\{e\}\}\} \\ 2131 &&& \mid q \; R \; q \mid \{\{\{e\}\}\} \\
2131 \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT} 2132 \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT} \\
2133 \textrm{$\mt{ORDER \; BY}$ items} & O &::=& \mt{RANDOM} [()] \mid E \; [o] \mid E \; [o], O
2132 \end{array}$$ 2134 \end{array}$$
2133 2135
2134 $$\begin{array}{rrcll} 2136 $$\begin{array}{rrcll}
2135 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\ 2137 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\
2136 &&& p,^+ & \textrm{particular columns} \\ 2138 &&& p,^+ & \textrm{particular columns} \\