summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2015-06-11 19:38:03 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2015-06-11 19:38:03 -0400
commit9bc8214356403845bb44535127c46e6378fa1ba6 (patch)
treeeb0ca0fe291e6cf7d70b5cbc0d2413a6c08062e7 /doc
parent443fa1a2ad02b653c96de2fb159fbdb510a87171 (diff)
A number of bug fixes in the manual
Diffstat (limited to 'doc')
-rw-r--r--doc/manual.tex19
1 files changed, 10 insertions, 9 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 1ff3f7aa..e140fac1 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -509,8 +509,8 @@ $$\begin{array}{rrcll}
&&& \ell & \textrm{constant} \\
&&& \hat{X} & \textrm{nullary constructor} \\
&&& \hat{X} \; p & \textrm{unary constructor} \\
- &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
- &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
+ &&& \{(X = p,)^*\} & \textrm{rigid record pattern} \\
+ &&& \{(X = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
&&& p : \tau & \textrm{type annotation} \\
&&& (p) & \textrm{explicit precedence} \\
\\
@@ -968,11 +968,11 @@ $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i
& \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
}$$
-$$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
+$$\infer{\Gamma \vdash \{\overline{X = p}\} \leadsto \Gamma_n; \{\overline{X = \tau}\}}{
\Gamma_0 = \Gamma
& \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
}
-\quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
+\quad \infer{\Gamma \vdash \{\overline{X = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{X = \tau}] \rc c)}{
\Gamma_0 = \Gamma
& \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
}$$
@@ -1424,7 +1424,7 @@ $$\begin{array}{l}
\hspace{.1in} \to (\mt{nm} :: \mt{Name} \to \mt{v} :: \mt{K} \to \mt{r} :: \{\mt{K}\} \to [[\mt{nm}] \sim \mt{r}] \Rightarrow \\
\hspace{.2in} \mt{tf} \; \mt{r} \to \mt{tf} \; ([\mt{nm} = \mt{v}] \rc \mt{r})) \\
\hspace{.1in} \to \mt{tf} \; [] \\
- \hspace{.1in} \to \mt{r} :: \{\mt{K}\} \to \mt{folder} \; \mt{r} \to \mt{tf} \; \mt{r}
+ \hspace{.1in} \to \mt{r} ::: \{\mt{K}\} \to \mt{folder} \; \mt{r} \to \mt{tf} \; \mt{r}
\end{array}$$
For a type-level record $\mt{r}$, a $\mt{folder} \; \mt{r}$ encodes a permutation of $\mt{r}$'s elements. The $\mt{fold}$ function can be called on a $\mt{folder}$ to iterate over the elements of $\mt{r}$ in that order. $\mt{fold}$ is parameterized on a type-level function to be used to calculate the type of each intermediate result of folding. After processing a subset $\mt{r'}$ of $\mt{r}$'s entries, the type of the accumulator should be $\mt{tf} \; \mt{r'}$. The next two expression arguments to $\mt{fold}$ are the usual step function and initial accumulator, familiar from fold functions over lists. The final two arguments are the record to fold over and a $\mt{folder}$ for it.
@@ -1861,7 +1861,7 @@ Any SQL query that returns single columns may be turned into a subquery expressi
$$\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}
+\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}
\end{array}$$
There is also an \cd{IF..THEN..ELSE..} construct that is compiled into standard SQL \cd{CASE} expressions.
@@ -1990,7 +1990,7 @@ $$\begin{array}{l}
\hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \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}$.
+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 constant table name $\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}) \\
@@ -2287,11 +2287,12 @@ $$\begin{array}{rrcll}
\textrm{Tables} & T &::=& x & \textrm{table variable, named locally by its own capitalization} \\
&&& x \; \mt{AS} \; X & \textrm{table variable, with local name} \\
&&& x \; \mt{AS} \; \{c\} & \textrm{table variable, with computed local name} \\
- &&& \{\{e\}\} \; \mt{AS} \; t & \textrm{computed table expression, with local name} \\
+ &&& \{\{e\}\} \; \mt{AS} \; X & \textrm{computed table expression, with local name} \\
&&& \{\{e\}\} \; \mt{AS} \; \{c\} & \textrm{computed table expression, with computed local name} \\
\textrm{$\mt{FROM}$ items} & F &::=& T \mid \{\{e\}\} \mid F \; J \; \mt{JOIN} \; F \; \mt{ON} \; E \\
&&& \mid F \; \mt{CROSS} \; \mt{JOIN} \ F \\
- &&& \mid (Q) \; \mt{AS} \; t \mid (\{\{e\}\}) \; \mt{AS} \; t \\
+ &&& \mid (Q) \; \mt{AS} \; X \mid (Q) \; \mt{AS} \; \{c\} \\
+ &&& \mid (\{\{e\}\}) \; \mt{AS} \; t \\
\textrm{Joins} & J &::=& [\mt{INNER}] \\
&&& \mid [\mt{LEFT} \mid \mt{RIGHT} \mid \mt{FULL}] \; [\mt{OUTER}] \\
\textrm{SQL expressions} & E &::=& t.f & \textrm{column references} \\