Mercurial > urweb
comparison doc/manual.tex @ 788:f5fea13a60b9
Constraint syntax
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 05 May 2009 14:36:16 -0400 |
| parents | c9c76aeaae64 |
| children | d18f6f0bcf60 |
comparison
equal
deleted
inserted
replaced
| 787:c9c76aeaae64 | 788:f5fea13a60b9 |
|---|---|
| 1736 Ur/Web features some syntactic shorthands for building values using the functions from the last section. This section sketches the grammar of those extensions. We write spans of syntax inside brackets to indicate that they are optional. | 1736 Ur/Web features some syntactic shorthands for building values using the functions from the last section. This section sketches the grammar of those extensions. We write spans of syntax inside brackets to indicate that they are optional. |
| 1737 | 1737 |
| 1738 \subsection{SQL} | 1738 \subsection{SQL} |
| 1739 | 1739 |
| 1740 \subsubsection{\label{tables}Table Declarations} | 1740 \subsubsection{\label{tables}Table Declarations} |
| 1741 | |
| 1742 $\mt{table}$ declarations may include constraints, via these grammar rules. | |
| 1743 $$\begin{array}{rrcll} | |
| 1744 \textrm{Declarations} & d &::=& \mt{table} \; x : c \; [pk[,]] \; cts \\ | |
| 1745 \textrm{Primary key constraints} & pk &::=& \mt{PRIMARY} \; \mt{KEY} \; K \\ | |
| 1746 \textrm{Keys} & K &::=& f \mid (f, (f,)^+) \\ | |
| 1747 \textrm{Constraint sets} & cts &::=& \mt{CONSTRAINT} f \; ct \mid cts, cts \mid \{\{e\}\} \\ | |
| 1748 \textrm{Constraints} & ct &::=& \mt{UNIQUE} \; K \mid \mt{CHECK} \; E \\ | |
| 1749 &&& \mid \mt{FOREIGN} \; \mt{KEY} \; K \; \mt{REFERENCES} \; F \; (K) \; [\mt{ON} \; \mt{DELETE} \; pr] \; [\mt{ON} \; \mt{UPDATE} \; pr] \\ | |
| 1750 \textrm{Foreign tables} & F &::=& x \mid \{\{e\}\} \\ | |
| 1751 \textrm{Propagation modes} & pr &::=& \mt{NO} \; \mt{ACTION} \mid \mt{RESTRICT} \mid \mt{CASCADE} \mid \mt{SET} \; \mt{NULL} | |
| 1752 \end{array}$$ | |
| 1753 | |
| 1754 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. | |
| 1755 | |
| 1741 | 1756 |
| 1742 \subsubsection{Queries} | 1757 \subsubsection{Queries} |
| 1743 | 1758 |
| 1744 Queries $Q$ are added to the rules for expressions $e$. | 1759 Queries $Q$ are added to the rules for expressions $e$. |
| 1745 | 1760 |