comparison doc/manual.tex @ 545:f31aa2a3a72d

DML
author Adam Chlipala <adamc@hcoop.net>
date Sun, 07 Dec 2008 10:24:23 -0500
parents 4154b4dc62c6
children 7417c4b57aeb
comparison
equal deleted inserted replaced
544:4154b4dc62c6 545:f31aa2a3a72d
979 \hspace{.2in} \mt{Limit} : \mt{sql\_limit}, \\ 979 \hspace{.2in} \mt{Limit} : \mt{sql\_limit}, \\
980 \hspace{.2in} \mt{Offset} : \mt{sql\_offset}\} \\ 980 \hspace{.2in} \mt{Offset} : \mt{sql\_offset}\} \\
981 \hspace{.1in} \to \mt{sql\_query} \; \mt{selectedFields} \; \mt{selectedExps} 981 \hspace{.1in} \to \mt{sql\_query} \; \mt{selectedFields} \; \mt{selectedExps}
982 \end{array}$$ 982 \end{array}$$
983 983
984 Queries are used by folding over their results inside transactions.
985 $$\begin{array}{l}
986 \mt{val} \; \mt{query} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \lambda [\mt{tables} \sim \mt{exps}] \Rightarrow \mt{state} ::: \mt{Type} \to \mt{sql\_query} \; \mt{tables} \; \mt{exps} \\
987 \hspace{.1in} \to (\$(\mt{exps} \rc \mt{fold} \; (\lambda \mt{nm} \; (\mt{fields} :: \{\mt{Type}\}) \; \mt{acc} \; [[\mt{nm}] \sim \mt{acc}] \Rightarrow [\mt{nm} = \$\mt{fields}] \rc \mt{acc}) \; [] \; \mt{tables}) \\
988 \hspace{.2in} \to \mt{state} \to \mt{transaction} \; \mt{state}) \\
989 \hspace{.1in} \to \mt{state} \to \mt{transaction} \; \mt{state}
990 \end{array}$$
991
984 Most of the complexity of the query encoding is in the type $\mt{sql\_query1}$, which includes simple queries and derived queries based on relational operators. Constructor arguments respectively specify the tables we select from, the subset of fields that we keep from each table for the result rows, and the extra expressions that we select. 992 Most of the complexity of the query encoding is in the type $\mt{sql\_query1}$, which includes simple queries and derived queries based on relational operators. Constructor arguments respectively specify the tables we select from, the subset of fields that we keep from each table for the result rows, and the extra expressions that we select.
985 $$\begin{array}{l} 993 $$\begin{array}{l}
986 \mt{con} \; \mt{sql\_query1} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ 994 \mt{con} \; \mt{sql\_query1} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
987 \\ 995 \\
988 \mt{type} \; \mt{sql\_relop} \\ 996 \mt{type} \; \mt{sql\_relop} \\
1149 \mt{type} \; \mt{sql\_offset} \\ 1157 \mt{type} \; \mt{sql\_offset} \\
1150 \mt{val} \; \mt{sql\_no\_offset} : \mt{sql\_offset} \\ 1158 \mt{val} \; \mt{sql\_no\_offset} : \mt{sql\_offset} \\
1151 \mt{val} \; \mt{sql\_offset} : \mt{int} \to \mt{sql\_offset} 1159 \mt{val} \; \mt{sql\_offset} : \mt{int} \to \mt{sql\_offset}
1152 \end{array}$$ 1160 \end{array}$$
1153 1161
1162
1163 \subsubsection{DML}
1164
1165 The Ur/Web library also includes an embedding of a fragment of SQL's DML, the Data Manipulation Language, for modifying database tables. Any piece of DML may be executed in a transaction.
1166
1167 $$\begin{array}{l}
1168 \mt{type} \; \mt{dml} \\
1169 \mt{val} \; \mt{dml} : \mt{dml} \to \mt{transaction} \; \mt{unit}
1170 \end{array}$$
1171
1172 Properly-typed records may be used to form $\mt{INSERT}$ commands.
1173 $$\begin{array}{l}
1174 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\
1175 \hspace{.1in} \to \$(\mt{fold} \; (\lambda \mt{nm} \; (\mt{t} :: \mt{Type}) \; \mt{acc} \; [[\mt{nm}] \sim \mt{acc}] \Rightarrow [\mt{nm} = \mt{sql\_exp} \; [] \; [] \; [] \; \mt{t}] \rc \mt{acc}) \; [] \; \mt{fields}) \to \mt{dml}
1176 \end{array}$$
1177
1178 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.
1179 $$\begin{array}{l}
1180 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to \lambda [\mt{changed} \sim \mt{unchanged}] \\
1181 \hspace{.1in} \Rightarrow \$(\mt{fold} \; (\lambda \mt{nm} \; (\mt{t} :: \mt{Type}) \; \mt{acc} \; [[\mt{nm}] \sim \mt{acc}] \Rightarrow [\mt{nm} = \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{t}] \rc \mt{acc}) \; [] \; \mt{changed}) \\
1182 \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}
1183 \end{array}$$
1184
1185 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause.
1186 $$\begin{array}{l}
1187 \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}
1188 \end{array}$$
1189
1154 \end{document} 1190 \end{document}