Mercurial > urweb

comparison doc/manual.tex @ 1594:d9de8b3f8167

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix completely broken manual description of 'view'
author Adam Chlipala <adam@chlipala.net>
date Mon, 14 Nov 2011 09:02:00 -0500
parents 257421857680
children e44be6ece475
comparison
equal deleted inserted replaced
1593:7e2655b25ea1 1594:d9de8b3f8167
515 &&& \mt{signature} \; X = S & \textrm{signature definition} \\ 515 &&& \mt{signature} \; X = S & \textrm{signature definition} \\
516 &&& \mt{open} \; M & \textrm{module inclusion} \\ 516 &&& \mt{open} \; M & \textrm{module inclusion} \\
517 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\ 517 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
518 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\ 518 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
519 &&& \mt{table} \; x : c & \textrm{SQL table} \\ 519 &&& \mt{table} \; x : c & \textrm{SQL table} \\
520 &&& \mt{view} \; x : c & \textrm{SQL view} \\ 520 &&& \mt{view} \; x = e & \textrm{SQL view} \\
521 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\ 521 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
522 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\ 522 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
523 &&& \mt{style} \; x : \tau & \textrm{CSS class} \\ 523 &&& \mt{style} \; x : \tau & \textrm{CSS class} \\
524 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\ 524 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
525 &&& \mt{task} \; e = e & \textrm{recurring task} \\ 525 &&& \mt{task} \; e = e & \textrm{recurring task} \\
531 &&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\ 531 &&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\
532 \end{array}$$ 532 \end{array}$$
533 533
534 There are two kinds of Ur files. A file named $M\texttt{.ur}$ is an \emph{implementation file}, and it should contain a sequence of declarations $d^*$. A file named $M\texttt{.urs}$ is an \emph{interface file}; it must always have a matching $M\texttt{.ur}$ and should contain a sequence of signature items $s^*$. When both files are present, the overall effect is the same as a monolithic declaration $\mt{structure} \; M : \mt{sig} \; s^* \; \mt{end} = \mt{struct} \; d^* \; \mt{end}$. When no interface file is included, the overall effect is similar, with a signature for module $M$ being inferred rather than just checked against an interface. 534 There are two kinds of Ur files. A file named $M\texttt{.ur}$ is an \emph{implementation file}, and it should contain a sequence of declarations $d^*$. A file named $M\texttt{.urs}$ is an \emph{interface file}; it must always have a matching $M\texttt{.ur}$ and should contain a sequence of signature items $s^*$. When both files are present, the overall effect is the same as a monolithic declaration $\mt{structure} \; M : \mt{sig} \; s^* \; \mt{end} = \mt{struct} \; d^* \; \mt{end}$. When no interface file is included, the overall effect is similar, with a signature for module $M$ being inferred rather than just checked against an interface.
535 535
536 We omit some extra possibilities in $\mt{table}$ syntax, deferring them to Section \ref{tables}. 536 We omit some extra possibilities in $\mt{table}$ syntax, deferring them to Section \ref{tables}. The concrete syntax of $\mt{view}$ declarations is also more complex than shown in the table above, with details deferred to Section \ref{tables}.
537 537
538 \subsection{Shorthands} 538 \subsection{Shorthands}
539 539
540 There are a variety of derived syntactic forms that elaborate into the core syntax from the last subsection. We will present the additional forms roughly following the order in which we presented the constructs that they elaborate into. 540 There are a variety of derived syntactic forms that elaborate into the core syntax from the last subsection. We will present the additional forms roughly following the order in which we presented the constructs that they elaborate into.
541 541
983 }$$ 983 }$$
984 984
985 $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c \; []}{ 985 $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c \; []}{
986 \Gamma \vdash c :: \{\mt{Type}\} 986 \Gamma \vdash c :: \{\mt{Type}\}
987 } 987 }
988 \quad \infer{\Gamma \vdash \mt{view} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_view} \; c}{ 988 \quad \infer{\Gamma \vdash \mt{view} \; x = e \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_view} \; c}{
989 \Gamma \vdash c :: \{\mt{Type}\} 989 \Gamma \vdash e :: \mt{Basis}.\mt{sql\_query} \; [] \; [] \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; c') \; c
990 }$$ 990 }$$
991 991
992 $$\infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$ 992 $$\infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
993 993
994 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{ 994 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
1219 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\ 1219 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
1220 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\ 1220 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\
1221 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\ 1221 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
1222 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\ 1222 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
1223 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\ 1223 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
1224 \mt{sigOf}(\mt{view} \; x : c) &=& \mt{view} \; x : c \\ 1224 \mt{sigOf}(\mt{view} \; x = e) &=& \mt{view} \; x : c \textrm{ (where $\Gamma \vdash e : \mt{Basis}.\mt{sql\_query} \; [] \; [] \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; c') \; c$)} \\
1225 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\ 1225 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
1226 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\ 1226 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
1227 \mt{sigOf}(\mt{style} \; x) &=& \mt{style} \; x \\ 1227 \mt{sigOf}(\mt{style} \; x) &=& \mt{style} \; x \\
1228 \mt{sigOf}(\mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\ 1228 \mt{sigOf}(\mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
1229 \end{eqnarray*} 1229 \end{eqnarray*}
2086 2086
2087 \subsubsection{\label{tables}Table Declarations} 2087 \subsubsection{\label{tables}Table Declarations}
2088 2088
2089 $\mt{table}$ declarations may include constraints, via these grammar rules. 2089 $\mt{table}$ declarations may include constraints, via these grammar rules.
2090 $$\begin{array}{rrcll} 2090 $$\begin{array}{rrcll}
2091 \textrm{Declarations} & d &::=& \mt{table} \; x : c \; [pk[,]] \; cts \\ 2091 \textrm{Declarations} & d &::=& \mt{table} \; x : c \; [pk[,]] \; cts \mid \mt{view} \; x = V \\
2092 \textrm{Primary key constraints} & pk &::=& \mt{PRIMARY} \; \mt{KEY} \; K \\ 2092 \textrm{Primary key constraints} & pk &::=& \mt{PRIMARY} \; \mt{KEY} \; K \\
2093 \textrm{Keys} & K &::=& f \mid (f, (f,)^+) \\ 2093 \textrm{Keys} & K &::=& f \mid (f, (f,)^+) \\
2094 \textrm{Constraint sets} & cts &::=& \mt{CONSTRAINT} f \; ct \mid cts, cts \mid \{\{e\}\} \\ 2094 \textrm{Constraint sets} & cts &::=& \mt{CONSTRAINT} f \; ct \mid cts, cts \mid \{\{e\}\} \\
2095 \textrm{Constraints} & ct &::=& \mt{UNIQUE} \; K \mid \mt{CHECK} \; E \\ 2095 \textrm{Constraints} & ct &::=& \mt{UNIQUE} \; K \mid \mt{CHECK} \; E \\
2096 &&& \mid \mt{FOREIGN} \; \mt{KEY} \; K \; \mt{REFERENCES} \; F \; (K) \; [\mt{ON} \; \mt{DELETE} \; pr] \; [\mt{ON} \; \mt{UPDATE} \; pr] \\ 2096 &&& \mid \mt{FOREIGN} \; \mt{KEY} \; K \; \mt{REFERENCES} \; F \; (K) \; [\mt{ON} \; \mt{DELETE} \; pr] \; [\mt{ON} \; \mt{UPDATE} \; pr] \\
2097 \textrm{Foreign tables} & F &::=& x \mid \{\{e\}\} \\ 2097 \textrm{Foreign tables} & F &::=& x \mid \{\{e\}\} \\
2098 \textrm{Propagation modes} & pr &::=& \mt{NO} \; \mt{ACTION} \mid \mt{RESTRICT} \mid \mt{CASCADE} \mid \mt{SET} \; \mt{NULL} 2098 \textrm{Propagation modes} & pr &::=& \mt{NO} \; \mt{ACTION} \mid \mt{RESTRICT} \mid \mt{CASCADE} \mid \mt{SET} \; \mt{NULL} \\
2099 \textrm{View expressions} & V &::=& Q \mid \{e\}
2099 \end{array}$$ 2100 \end{array}$$
2100 2101
2101 A signature item $\mt{table} \; \mt{x} : \mt{c}$ is actually elaborated into two signature items: $\mt{con} \; \mt{x\_hidden\_constraints} :: \{\{\mt{Unit}\}\}$ and $\mt{val} \; \mt{x} : \mt{sql\_table} \; \mt{c} \; \mt{x\_hidden\_constraints}$. This is appropriate for common cases where client code doesn't care which keys a table has. It's also possible to include constraints after a $\mt{table}$ signature item, with the same syntax as for $\mt{table}$ declarations. This may look like dependent typing, but it's just a convenience. The constraints are type-checked to determine a constructor $u$ to include in $\mt{val} \; \mt{x} : \mt{sql\_table} \; \mt{c} \; (u \rc \mt{x\_hidden\_constraints})$, and then the expressions are thrown away. Nonetheless, it can be useful for documentation purposes to include table constraint details in signatures. Note that the automatic generation of $\mt{x\_hidden\_constraints}$ leads to a kind of free subtyping with respect to which constraints are defined. 2102 A signature item $\mt{table} \; \mt{x} : \mt{c}$ is actually elaborated into two signature items: $\mt{con} \; \mt{x\_hidden\_constraints} :: \{\{\mt{Unit}\}\}$ and $\mt{val} \; \mt{x} : \mt{sql\_table} \; \mt{c} \; \mt{x\_hidden\_constraints}$. This is appropriate for common cases where client code doesn't care which keys a table has. It's also possible to include constraints after a $\mt{table}$ signature item, with the same syntax as for $\mt{table}$ declarations. This may look like dependent typing, but it's just a convenience. The constraints are type-checked to determine a constructor $u$ to include in $\mt{val} \; \mt{x} : \mt{sql\_table} \; \mt{c} \; (u \rc \mt{x\_hidden\_constraints})$, and then the expressions are thrown away. Nonetheless, it can be useful for documentation purposes to include table constraint details in signatures. Note that the automatic generation of $\mt{x\_hidden\_constraints}$ leads to a kind of free subtyping with respect to which constraints are defined.
2102 2103
2103 2104