Mercurial > urweb

comparison doc/manual.tex @ 1085:ae885ad70d83

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Updating the manual
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Dec 2009 09:56:09 -0500
parents 93315ac00394
children 99aebdf30257
comparison
equal deleted inserted replaced
1084:8e240c007442 1085:ae885ad70d83
423 &&& \mt{view} \; x : c & \textrm{SQL view} \\ 423 &&& \mt{view} \; x : c & \textrm{SQL view} \\
424 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\ 424 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
425 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\ 425 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
426 &&& \mt{style} \; x : \tau & \textrm{CSS class} \\ 426 &&& \mt{style} \; x : \tau & \textrm{CSS class} \\
427 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\ 427 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
428 &&& \mt{task} \; e = e & \textrm{recurring task} \\
428 \\ 429 \\
429 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\ 430 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
430 &&& X & \textrm{variable} \\ 431 &&& X & \textrm{variable} \\
431 &&& M.X & \textrm{projection} \\ 432 &&& M.X & \textrm{projection} \\
432 &&& M(M) & \textrm{functor application} \\ 433 &&& M(M) & \textrm{functor application} \\
891 892
892 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{ 893 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
893 \Gamma \vdash \tau :: \mt{Type} 894 \Gamma \vdash \tau :: \mt{Type}
894 } 895 }
895 \quad \infer{\Gamma \vdash \mt{style} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{css\_class}}{}$$ 896 \quad \infer{\Gamma \vdash \mt{style} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{css\_class}}{}$$
897
898 $$\infer{\Gamma \vdash \mt{task} \; e_1 = e_2 \leadsto \Gamma}{
899 \Gamma \vdash e_1 :: \mt{Basis}.\mt{task\_kind}
900 & \Gamma \vdash e_2 :: \mt{Basis}.\mt{transaction} \; \{\}
901 }$$
896 902
897 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{ 903 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
898 \Gamma \vdash c :: \kappa 904 \Gamma \vdash c :: \kappa
899 }$$ 905 }$$
900 906
1298 \mt{val} \; \mt{bless} : \mt{string} \to \mt{url} \\ 1304 \mt{val} \; \mt{bless} : \mt{string} \to \mt{url} \\
1299 \mt{val} \; \mt{checkUrl} : \mt{string} \to \mt{option} \; \mt{url} 1305 \mt{val} \; \mt{checkUrl} : \mt{string} \to \mt{option} \; \mt{url}
1300 \end{array}$$ 1306 \end{array}$$
1301 $\mt{bless}$ raises a runtime error if the string passed to it fails the URL policy. 1307 $\mt{bless}$ raises a runtime error if the string passed to it fails the URL policy.
1302 1308
1309 It is possible to grab the current page's URL or to build a URL for an arbitrary transaction that would also be an acceptable value of a \texttt{link} attribute of the \texttt{a} tag.
1310 $$\begin{array}{l}
1311 \mt{val} \; \mt{currentUrl} : \mt{transaction} \; \mt{url} \\
1312 \mt{val} \; \mt{url} : \mt{transaction} \; \mt{page} \to \mt{url}
1313 \end{array}$$
1314
1315 Page generation may be interrupted at any time with a request to redirect to a particular URL instead.
1316 $$\begin{array}{l}
1317 \mt{val} \; \mt{redirect} : \mt{t} ::: \mt{Type} \to \mt{url} \to \mt{transaction} \; \mt{t}
1318 \end{array}$$
1319
1303 It's possible for pages to return files of arbitrary MIME types. A file can be input from the user using this data type, along with the $\mt{upload}$ form tag. 1320 It's possible for pages to return files of arbitrary MIME types. A file can be input from the user using this data type, along with the $\mt{upload}$ form tag.
1304 $$\begin{array}{l} 1321 $$\begin{array}{l}
1305 \mt{type} \; \mt{file} \\ 1322 \mt{type} \; \mt{file} \\
1306 \mt{val} \; \mt{fileName} : \mt{file} \to \mt{option} \; \mt{string} \\ 1323 \mt{val} \; \mt{fileName} : \mt{file} \to \mt{option} \; \mt{string} \\
1307 \mt{val} \; \mt{fileMimeType} : \mt{file} \to \mt{string} \\ 1324 \mt{val} \; \mt{fileMimeType} : \mt{file} \to \mt{string} \\
1468 $$\begin{array}{l} 1485 $$\begin{array}{l}
1469 \mt{val} \; \mt{sql\_query1} : \mt{tables} ::: \{\{\mt{Type}\}\} \\ 1486 \mt{val} \; \mt{sql\_query1} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
1470 \hspace{.1in} \to \mt{grouped} ::: \{\{\mt{Type}\}\} \\ 1487 \hspace{.1in} \to \mt{grouped} ::: \{\{\mt{Type}\}\} \\
1471 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\ 1488 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
1472 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\ 1489 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
1473 \hspace{.1in} \to \{\mt{Distinct} : \mt{bool}, \\ 1490 \hspace{.1in} \to \mt{empties} :: \{\mt{Unit}\} \\
1491 \hspace{.1in} \to [\mt{empties} \sim \mt{selectedFields}] \\
1492 \hspace{.1in} \Rightarrow \{\mt{Distinct} : \mt{bool}, \\
1474 \hspace{.2in} \mt{From} : \mt{sql\_from\_items} \; \mt{tables}, \\ 1493 \hspace{.2in} \mt{From} : \mt{sql\_from\_items} \; \mt{tables}, \\
1475 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; \mt{tables} \; [] \; [] \; \mt{bool}, \\ 1494 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; \mt{tables} \; [] \; [] \; \mt{bool}, \\
1476 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\ 1495 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\
1477 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; [] \; \mt{bool}, \\ 1496 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; [] \; \mt{bool}, \\
1478 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; \mt{selectedFields}, \\ 1497 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; \mt{empties} \rc \mt{selectedFields}), \\
1479 \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; []) \; \mt{selectedExps}) \} \\ 1498 \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; []) \; \mt{selectedExps}) \} \\
1480 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps} 1499 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}
1481 \end{array}$$ 1500 \end{array}$$
1482 1501
1483 To encode projection of subsets of fields in $\mt{SELECT}$ clauses, and to encode $\mt{GROUP} \; \mt{BY}$ clauses, we rely on a type family $\mt{sql\_subset}$, capturing what it means for one record of table fields to be a subset of another. The main constructor $\mt{sql\_subset}$ ``proves subset facts'' by requiring a split of a record into kept and dropped parts. The extra constructor $\mt{sql\_subset\_all}$ is a convenience for keeping all fields of a record. 1502 To encode projection of subsets of fields in $\mt{SELECT}$ clauses, and to encode $\mt{GROUP} \; \mt{BY}$ clauses, we rely on a type family $\mt{sql\_subset}$, capturing what it means for one record of table fields to be a subset of another. The main constructor $\mt{sql\_subset}$ ``proves subset facts'' by requiring a split of a record into kept and dropped parts. The extra constructor $\mt{sql\_subset\_all}$ is a convenience for keeping all fields of a record.
1681 1700
1682 SQL sequences are counters with concurrency control, often used to assign unique IDs. Ur/Web supports them via a simple interface. The only way to create a sequence is with the $\mt{sequence}$ declaration form. 1701 SQL sequences are counters with concurrency control, often used to assign unique IDs. Ur/Web supports them via a simple interface. The only way to create a sequence is with the $\mt{sequence}$ declaration form.
1683 1702
1684 $$\begin{array}{l} 1703 $$\begin{array}{l}
1685 \mt{type} \; \mt{sql\_sequence} \\ 1704 \mt{type} \; \mt{sql\_sequence} \\
1686 \mt{val} \; \mt{nextval} : \mt{sql\_sequence} \to \mt{transaction} \; \mt{int} 1705 \mt{val} \; \mt{nextval} : \mt{sql\_sequence} \to \mt{transaction} \; \mt{int} \\
1706 \mt{val} \; \mt{setval} : \mt{sql\_sequence} \to \mt{int} \to \mt{transaction} \; \mt{unit}
1687 \end{array}$$ 1707 \end{array}$$
1688 1708
1689 1709
1690 \subsection{XML} 1710 \subsection{XML}
1691 1711
1855 1875
1856 Queries $Q$ are added to the rules for expressions $e$. 1876 Queries $Q$ are added to the rules for expressions $e$.
1857 1877
1858 $$\begin{array}{rrcll} 1878 $$\begin{array}{rrcll}
1859 \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; (E \; [o],)^+] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\ 1879 \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; (E \; [o],)^+] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\
1860 \textrm{Pre-queries} & q &::=& \mt{SELECT} \; [\mt{DISTINCT}] \; P \; \mt{FROM} \; T,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\ 1880 \textrm{Pre-queries} & q &::=& \mt{SELECT} \; [\mt{DISTINCT}] \; P \; \mt{FROM} \; F,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\
1861 &&& \mid q \; R \; q \\ 1881 &&& \mid q \; R \; q \mid \{\{\{e\}\}\} \\
1862 \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT} 1882 \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT}
1863 \end{array}$$ 1883 \end{array}$$
1864 1884
1865 $$\begin{array}{rrcll} 1885 $$\begin{array}{rrcll}
1866 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\ 1886 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\
1873 \textrm{Column names} & f &::=& X & \textrm{constant column name} \\ 1893 \textrm{Column names} & f &::=& X & \textrm{constant column name} \\
1874 &&& \{c\} & \textrm{computed column name (of kind $\mt{Name}$)} \\ 1894 &&& \{c\} & \textrm{computed column name (of kind $\mt{Name}$)} \\
1875 \textrm{Tables} & T &::=& x & \textrm{table variable, named locally by its own capitalization} \\ 1895 \textrm{Tables} & T &::=& x & \textrm{table variable, named locally by its own capitalization} \\
1876 &&& x \; \mt{AS} \; t & \textrm{table variable, with local name} \\ 1896 &&& x \; \mt{AS} \; t & \textrm{table variable, with local name} \\
1877 &&& \{\{e\}\} \; \mt{AS} \; t & \textrm{computed table expression, with local name} \\ 1897 &&& \{\{e\}\} \; \mt{AS} \; t & \textrm{computed table expression, with local name} \\
1898 \textrm{$\mt{FROM}$ items} & F &::=& T \mid \{\{e\}\} \mid F \; J \; \mt{JOIN} \; F \; \mt{ON} \; E \\
1899 &&& \mid F \; \mt{CROSS} \; \mt{JOIN} \ F \\
1900 \textrm{Joins} & J &::=& [\mt{INNER}] \\
1901 &&& \mid [\mt{LEFT} \mid \mt{RIGHT} \mid \mt{FULL}] \; [\mt{OUTER}] \\
1878 \textrm{SQL expressions} & E &::=& p & \textrm{column references} \\ 1902 \textrm{SQL expressions} & E &::=& p & \textrm{column references} \\
1879 &&& X & \textrm{named expression references} \\ 1903 &&& X & \textrm{named expression references} \\
1880 &&& \{\{e\}\} & \textrm{injected native Ur expressions} \\ 1904 &&& \{\{e\}\} & \textrm{injected native Ur expressions} \\
1881 &&& \{e\} & \textrm{computed expressions, probably using $\mt{sql\_exp}$ directly} \\ 1905 &&& \{e\} & \textrm{computed expressions, probably using $\mt{sql\_exp}$ directly} \\
1882 &&& \mt{TRUE} \mid \mt{FALSE} & \textrm{boolean constants} \\ 1906 &&& \mt{TRUE} \mid \mt{FALSE} & \textrm{boolean constants} \\
1895 \textrm{Aggregate functions} & a &::=& \mt{AVG} \mid \mt{SUM} \mid \mt{MIN} \mid \mt{MAX} \\ 1919 \textrm{Aggregate functions} & a &::=& \mt{AVG} \mid \mt{SUM} \mid \mt{MIN} \mid \mt{MAX} \\
1896 \textrm{Directions} & o &::=& \mt{ASC} \mid \mt{DESC} \\ 1920 \textrm{Directions} & o &::=& \mt{ASC} \mid \mt{DESC} \\
1897 \textrm{SQL integer} & N &::=& n \mid \{e\} \\ 1921 \textrm{SQL integer} & N &::=& n \mid \{e\} \\
1898 \end{array}$$ 1922 \end{array}$$
1899 1923
1900 Additionally, an SQL expression may be inserted into normal Ur code with the syntax $(\mt{SQL} \; E)$ or $(\mt{WHERE} \; E)$. 1924 Additionally, an SQL expression may be inserted into normal Ur code with the syntax $(\mt{SQL} \; E)$ or $(\mt{WHERE} \; E)$. Similar shorthands exist for other nonterminals, with the prefix $\mt{FROM}$ for $\mt{FROM}$ items and $\mt{SELECT1}$ for pre-queries.
1901 1925
1902 \subsubsection{DML} 1926 \subsubsection{DML}
1903 1927
1904 DML commands $D$ are added to the rules for expressions $e$. 1928 DML commands $D$ are added to the rules for expressions $e$.
1905 1929
2003 void uw_register_transactional(uw_context, void *data, uw_callback commit, 2027 void uw_register_transactional(uw_context, void *data, uw_callback commit,
2004 uw_callback rollback, uw_callback free); 2028 uw_callback rollback, uw_callback free);
2005 \end{verbatim} 2029 \end{verbatim}
2006 All side effects in Ur/Web programs need to be compatible with transactions, such that any set of actions can be undone at any time. Thus, you should not perform actions with non-local side effects directly; instead, register handlers to be called when the current transaction is committed or rolled back. The arguments here give an arbitary piece of data to be passed to callbacks, a function to call on commit, a function to call on rollback, and a function to call afterward in either case to clean up any allocated resources. A rollback handler may be called after the associated commit handler has already been called, if some later part of the commit process fails. 2030 All side effects in Ur/Web programs need to be compatible with transactions, such that any set of actions can be undone at any time. Thus, you should not perform actions with non-local side effects directly; instead, register handlers to be called when the current transaction is committed or rolled back. The arguments here give an arbitary piece of data to be passed to callbacks, a function to call on commit, a function to call on rollback, and a function to call afterward in either case to clean up any allocated resources. A rollback handler may be called after the associated commit handler has already been called, if some later part of the commit process fails.
2007 2031
2008 To accommodate some stubbornly non-transactional real-world actions like sending an e-mail message, Ur/Web allows the \texttt{rollback} parameter to be \texttt{NULL}. When a transaction commits, all \texttt{commit} actions that have non-\texttt{NULL} rollback actions are tried before any \texttt{commit} actions that have \texttt{NULL} rollback actions. Thus, if a single execution uses only one non-transactional action, and if that action never fails partway through its execution while still causing an observable side effect, then Ur/Web can maintain the transactional abstraction. 2032 Any of the callbacks may be \texttt{NULL}. To accommodate some stubbornly non-transactional real-world actions like sending an e-mail message, Ur/Web treats \texttt{NULL} \texttt{rollback} callbacks specially. When a transaction commits, all \texttt{commit} actions that have non-\texttt{NULL} rollback actions are tried before any \texttt{commit} actions that have \texttt{NULL} rollback actions. Thus, if a single execution uses only one non-transactional action, and if that action never fails partway through its execution while still causing an observable side effect, then Ur/Web can maintain the transactional abstraction.
2033
2034 \item \begin{verbatim}
2035 void *uw_get_global(uw_context, char *name);
2036 void uw_set_global(uw_context, char *name, void *data, uw_callback free);
2037 \end{verbatim}
2038 Different FFI-based extensions may want to associate their own pieces of data with contexts. The global interface provides a way of doing that, where each extension must come up with its own unique key. The \texttt{free} argument to \texttt{uw\_set\_global()} explains how to deallocate the saved data.
2039
2009 \end{itemize} 2040 \end{itemize}
2010
2011 2041
2012 \subsection{Writing JavaScript FFI Code} 2042 \subsection{Writing JavaScript FFI Code}
2013 2043
2014 JavaScript is dynamically typed, so Ur/Web type definitions imply no JavaScript code. The JavaScript identifier for each FFI function is set with the \texttt{jsFunc} directive. Each identifier can be defined in any JavaScript file that you ask to include with the \texttt{script} directive. 2044 JavaScript is dynamically typed, so Ur/Web type definitions imply no JavaScript code. The JavaScript identifier for each FFI function is set with the \texttt{jsFunc} directive. Each identifier can be defined in any JavaScript file that you ask to include with the \texttt{script} directive.
2015 2045