aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-02-04 10:42:18 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2012-02-04 10:42:18 -0500
commit36603eae600143253959ad94cdc5bb75a766b91c (patch)
tree4ee8d2bcef09c2e67f5dfdb69c50c84e4636ad25 /doc
parent044e51a1d8d21daec245acad05560716b18e352c (diff)
Extend and document RANDOM
Diffstat (limited to 'doc')
-rw-r--r--doc/manual.tex6
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 2097f71a..b1052c36 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -1848,6 +1848,7 @@ $$\begin{array}{l}
\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} \\
+ \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} \\
\mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\
@@ -2125,10 +2126,11 @@ A signature item $\mt{table} \; \mt{x} : \mt{c}$ is actually elaborated into two
Queries $Q$ are added to the rules for expressions $e$.
$$\begin{array}{rrcll}
- \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; (E \; [o],)^+] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\
+ \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; O] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\
\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{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
\end{array}$$
$$\begin{array}{rrcll}