Mercurial > urweb
comparison doc/manual.tex @ 1578:7d2aa0ddc531
Some notes on 'T' for update/delete combinators
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 20 Oct 2011 09:27:37 -0400 |
parents | 644558d9c756 |
children | e1f4ac9ca34b |
comparison
equal
deleted
inserted
replaced
1577:911ebbd23919 | 1578:7d2aa0ddc531 |
---|---|
1868 $$\begin{array}{l} | 1868 $$\begin{array}{l} |
1869 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\ | 1869 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\ |
1870 \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml} | 1870 \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml} |
1871 \end{array}$$ | 1871 \end{array}$$ |
1872 | 1872 |
1873 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. | 1873 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}$. |
1874 $$\begin{array}{l} | 1874 $$\begin{array}{l} |
1875 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to [\mt{changed} \sim \mt{unchanged}] \\ | 1875 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to [\mt{changed} \sim \mt{unchanged}] \\ |
1876 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\ | 1876 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\ |
1877 \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} | 1877 \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} |
1878 \end{array}$$ | 1878 \end{array}$$ |
1879 | 1879 |
1880 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause. | 1880 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause. The above use of $\mt{T}$ is repeated. |
1881 $$\begin{array}{l} | 1881 $$\begin{array}{l} |
1882 \mt{val} \; \mt{delete} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \to \mt{sql\_exp} \; [\mt{T} = \mt{fields}] \; [] \; [] \; \mt{bool} \to \mt{dml} | 1882 \mt{val} \; \mt{delete} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \to \mt{sql\_exp} \; [\mt{T} = \mt{fields}] \; [] \; [] \; \mt{bool} \to \mt{dml} |
1883 \end{array}$$ | 1883 \end{array}$$ |
1884 | 1884 |
1885 \subsubsection{Sequences} | 1885 \subsubsection{Sequences} |