Mercurial > urweb

comparison doc/manual.tex @ 2155:7ce804ecd56b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A number of bug fixes in the manual
author Adam Chlipala <adam@chlipala.net>
date Thu, 11 Jun 2015 19:38:03 -0400
parents 752e5efe9da9
children 3acaaff30c85
comparison
equal deleted inserted replaced
2154:9ea29c93246d 2155:7ce804ecd56b
507 \textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\ 507 \textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\
508 &&& x & \textrm{variable} \\ 508 &&& x & \textrm{variable} \\
509 &&& \ell & \textrm{constant} \\ 509 &&& \ell & \textrm{constant} \\
510 &&& \hat{X} & \textrm{nullary constructor} \\ 510 &&& \hat{X} & \textrm{nullary constructor} \\
511 &&& \hat{X} \; p & \textrm{unary constructor} \\ 511 &&& \hat{X} \; p & \textrm{unary constructor} \\
512 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\ 512 &&& \{(X = p,)^*\} & \textrm{rigid record pattern} \\
513 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\ 513 &&& \{(X = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
514 &&& p : \tau & \textrm{type annotation} \\ 514 &&& p : \tau & \textrm{type annotation} \\
515 &&& (p) & \textrm{explicit precedence} \\ 515 &&& (p) & \textrm{explicit precedence} \\
516 \\ 516 \\
517 \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\ 517 \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\
518 &&& M.X & \textrm{projection from a module} \\ 518 &&& M.X & \textrm{projection from a module} \\
966 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} 966 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
967 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau 967 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
968 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau'' 968 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
969 }$$ 969 }$$
970 970
971 $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{ 971 $$\infer{\Gamma \vdash \{\overline{X = p}\} \leadsto \Gamma_n; \{\overline{X = \tau}\}}{
972 \Gamma_0 = \Gamma 972 \Gamma_0 = \Gamma
973 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i 973 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
974 } 974 }
975 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{ 975 \quad \infer{\Gamma \vdash \{\overline{X = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{X = \tau}] \rc c)}{
976 \Gamma_0 = \Gamma 976 \Gamma_0 = \Gamma
977 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i 977 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
978 }$$ 978 }$$
979 979
980 $$\infer{\Gamma \vdash p : \tau \leadsto \Gamma'; \tau}{ 980 $$\infer{\Gamma \vdash p : \tau \leadsto \Gamma'; \tau}{
1422 \\ 1422 \\
1423 \mt{val} \; \mt{fold} : \mt{K} \longrightarrow \mt{tf} :: (\{\mt{K}\} \to \mt{Type}) \\ 1423 \mt{val} \; \mt{fold} : \mt{K} \longrightarrow \mt{tf} :: (\{\mt{K}\} \to \mt{Type}) \\
1424 \hspace{.1in} \to (\mt{nm} :: \mt{Name} \to \mt{v} :: \mt{K} \to \mt{r} :: \{\mt{K}\} \to [[\mt{nm}] \sim \mt{r}] \Rightarrow \\ 1424 \hspace{.1in} \to (\mt{nm} :: \mt{Name} \to \mt{v} :: \mt{K} \to \mt{r} :: \{\mt{K}\} \to [[\mt{nm}] \sim \mt{r}] \Rightarrow \\
1425 \hspace{.2in} \mt{tf} \; \mt{r} \to \mt{tf} \; ([\mt{nm} = \mt{v}] \rc \mt{r})) \\ 1425 \hspace{.2in} \mt{tf} \; \mt{r} \to \mt{tf} \; ([\mt{nm} = \mt{v}] \rc \mt{r})) \\
1426 \hspace{.1in} \to \mt{tf} \; [] \\ 1426 \hspace{.1in} \to \mt{tf} \; [] \\
1427 \hspace{.1in} \to \mt{r} :: \{\mt{K}\} \to \mt{folder} \; \mt{r} \to \mt{tf} \; \mt{r} 1427 \hspace{.1in} \to \mt{r} ::: \{\mt{K}\} \to \mt{folder} \; \mt{r} \to \mt{tf} \; \mt{r}
1428 \end{array}$$ 1428 \end{array}$$
1429 1429
1430 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. 1430 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.
1431 1431
1432 The Ur compiler treats $\mt{folder}$ like a constructor class, using built-in rules to infer $\mt{folder}$s for records with known structure. The order in which field names are mentioned in source code is used as a hint about the permutation that the programmer would like. 1432 The Ur compiler treats $\mt{folder}$ like a constructor class, using built-in rules to infer $\mt{folder}$s for records with known structure. The order in which field names are mentioned in source code is used as a hint about the permutation that the programmer would like.
1859 1859
1860 Any SQL query that returns single columns may be turned into a subquery expression. 1860 Any SQL query that returns single columns may be turned into a subquery expression.
1861 1861
1862 $$\begin{array}{l} 1862 $$\begin{array}{l}
1863 \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} \\ 1863 \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} \\
1864 \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} 1864 \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}
1865 \end{array}$$ 1865 \end{array}$$
1866 1866
1867 There is also an \cd{IF..THEN..ELSE..} construct that is compiled into standard SQL \cd{CASE} expressions. 1867 There is also an \cd{IF..THEN..ELSE..} construct that is compiled into standard SQL \cd{CASE} expressions.
1868 $$\begin{array}{l} 1868 $$\begin{array}{l}
1869 \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} \\ 1869 \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} \\
1988 $$\begin{array}{l} 1988 $$\begin{array}{l}
1989 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\ 1989 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\
1990 \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml} 1990 \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml}
1991 \end{array}$$ 1991 \end{array}$$
1992 1992
1993 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}$. 1993 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}$.
1994 $$\begin{array}{l} 1994 $$\begin{array}{l}
1995 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to [\mt{changed} \sim \mt{unchanged}] \\ 1995 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to [\mt{changed} \sim \mt{unchanged}] \\
1996 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\ 1996 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\
1997 \hspace{.1in} \to \mt{sql\_table} \; (\mt{changed} \rc \mt{unchanged}) \to \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{bool} \to \mt{dml} 1997 \hspace{.1in} \to \mt{sql\_table} \; (\mt{changed} \rc \mt{unchanged}) \to \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{bool} \to \mt{dml}
1998 \end{array}$$ 1998 \end{array}$$
2285 \textrm{Column names} & f &::=& X & \textrm{constant column name} \\ 2285 \textrm{Column names} & f &::=& X & \textrm{constant column name} \\
2286 &&& \{c\} & \textrm{computed column name (of kind $\mt{Name}$)} \\ 2286 &&& \{c\} & \textrm{computed column name (of kind $\mt{Name}$)} \\
2287 \textrm{Tables} & T &::=& x & \textrm{table variable, named locally by its own capitalization} \\ 2287 \textrm{Tables} & T &::=& x & \textrm{table variable, named locally by its own capitalization} \\
2288 &&& x \; \mt{AS} \; X & \textrm{table variable, with local name} \\ 2288 &&& x \; \mt{AS} \; X & \textrm{table variable, with local name} \\
2289 &&& x \; \mt{AS} \; \{c\} & \textrm{table variable, with computed local name} \\ 2289 &&& x \; \mt{AS} \; \{c\} & \textrm{table variable, with computed local name} \\
2290 &&& \{\{e\}\} \; \mt{AS} \; t & \textrm{computed table expression, with local name} \\ 2290 &&& \{\{e\}\} \; \mt{AS} \; X & \textrm{computed table expression, with local name} \\
2291 &&& \{\{e\}\} \; \mt{AS} \; \{c\} & \textrm{computed table expression, with computed local name} \\ 2291 &&& \{\{e\}\} \; \mt{AS} \; \{c\} & \textrm{computed table expression, with computed local name} \\
2292 \textrm{$\mt{FROM}$ items} & F &::=& T \mid \{\{e\}\} \mid F \; J \; \mt{JOIN} \; F \; \mt{ON} \; E \\ 2292 \textrm{$\mt{FROM}$ items} & F &::=& T \mid \{\{e\}\} \mid F \; J \; \mt{JOIN} \; F \; \mt{ON} \; E \\
2293 &&& \mid F \; \mt{CROSS} \; \mt{JOIN} \ F \\ 2293 &&& \mid F \; \mt{CROSS} \; \mt{JOIN} \ F \\
2294 &&& \mid (Q) \; \mt{AS} \; t \mid (\{\{e\}\}) \; \mt{AS} \; t \\ 2294 &&& \mid (Q) \; \mt{AS} \; X \mid (Q) \; \mt{AS} \; \{c\} \\
2295 &&& \mid (\{\{e\}\}) \; \mt{AS} \; t \\
2295 \textrm{Joins} & J &::=& [\mt{INNER}] \\ 2296 \textrm{Joins} & J &::=& [\mt{INNER}] \\
2296 &&& \mid [\mt{LEFT} \mid \mt{RIGHT} \mid \mt{FULL}] \; [\mt{OUTER}] \\ 2297 &&& \mid [\mt{LEFT} \mid \mt{RIGHT} \mid \mt{FULL}] \; [\mt{OUTER}] \\
2297 \textrm{SQL expressions} & E &::=& t.f & \textrm{column references} \\ 2298 \textrm{SQL expressions} & E &::=& t.f & \textrm{column references} \\
2298 &&& X & \textrm{named expression references} \\ 2299 &&& X & \textrm{named expression references} \\
2299 &&& \{[e]\} & \textrm{injected native Ur expressions} \\ 2300 &&& \{[e]\} & \textrm{injected native Ur expressions} \\