comparison doc/manual.tex @ 701:f963356b53fd

Update the manual
author Adam Chlipala <adamc@hcoop.net>
date Sun, 05 Apr 2009 12:37:38 -0400
parents c90906b2f431
children ec0a0dd0ca12
comparison
equal deleted inserted replaced
700:db6ab16cd8f3 701:f963356b53fd
126 A blank line always separates the named directives from a list of modules to include in the project; if there are no named directives, a blank line must begin the file. 126 A blank line always separates the named directives from a list of modules to include in the project; if there are no named directives, a blank line must begin the file.
127 127
128 For each entry \texttt{M} in the module list, the file \texttt{M.urs} is included in the project if it exists, and the file \texttt{M.ur} must exist and is always included. 128 For each entry \texttt{M} in the module list, the file \texttt{M.urs} is included in the project if it exists, and the file \texttt{M.ur} must exist and is always included.
129 129
130 A few other named directives are supported. \texttt{prefix PREFIX} sets the prefix included before every URI within the generated application; the default is \texttt{/}. \texttt{exe FILENAME} sets the filename to which to write the output executable; the default for file \texttt{P.urp} is \texttt{P.exe}. \texttt{debug} saves some intermediate C files, which is mostly useful to help in debugging the compiler itself. \texttt{profile} generates an executable that may be used with gprof. 130 A few other named directives are supported. \texttt{prefix PREFIX} sets the prefix included before every URI within the generated application; the default is \texttt{/}. \texttt{exe FILENAME} sets the filename to which to write the output executable; the default for file \texttt{P.urp} is \texttt{P.exe}. \texttt{debug} saves some intermediate C files, which is mostly useful to help in debugging the compiler itself. \texttt{profile} generates an executable that may be used with gprof.
131
132 \texttt{timeout N} sets to \texttt{N} seconds the amount of time that the generated server will wait after the last contact from a client before determining that that client has exited the application. Clients that remain active will take the timeout setting into account in determining how often to ping the server, so it only makes sense to set a high timeout to cope with browser and network delays and failures. Higher timeouts can lead to more unnecessary client information taking up memory on the server. The timeout goes unused by any page that doesn't involve the \texttt{recv} function, since the server only needs to store per-client information for clients that receive asynchronous messages.
133
131 134
132 \subsection{Building an Application} 135 \subsection{Building an Application}
133 136
134 To compile project \texttt{P.urp}, simply run 137 To compile project \texttt{P.urp}, simply run
135 \begin{verbatim} 138 \begin{verbatim}
1451 $$\begin{array}{l} 1454 $$\begin{array}{l}
1452 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t} 1455 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t}
1453 \end{array}$$ 1456 \end{array}$$
1454 1457
1455 1458
1456 \subsection{Functional-Reactive Client-Side Programming} 1459 \subsection{Client-Side Programming}
1457 1460
1458 Ur/Web supports running code on web browsers, via automatic compilation to JavaScript. Most approaches to this kind of coding involve imperative manipulation of the DOM tree representing an HTML document's structure. Ur/Web follows the \emph{functional-reactive} approach instead. Programs may allocate mutable \emph{sources} of arbitrary types, and an HTML page is effectively a pure function over the latest values of the sources. The page is not mutated directly, but rather it changes automatically as the sources are mutated. 1461 Ur/Web supports running code on web browsers, via automatic compilation to JavaScript.
1462
1463 \subsubsection{The Basics}
1464
1465 Clients can open alert dialog boxes, in the usual annoying JavaScript way.
1466 $$\begin{array}{l}
1467 \mt{val} \; \mt{alert} : \mt{string} \to \mt{transaction} \; \mt{unit}
1468 \end{array}$$
1469
1470 Any transaction may be run in a new thread with the $\mt{spawn}$ function.
1471 $$\begin{array}{l}
1472 \mt{val} \; \mt{spawn} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit}
1473 \end{array}$$
1474
1475 The current thread can be paused for at least a specified number of milliseconds.
1476 $$\begin{array}{l}
1477 \mt{val} \; \mt{sleep} : \mt{int} \to \mt{transaction} \; \mt{unit}
1478 \end{array}$$
1479
1480 \subsubsection{Functional-Reactive Page Generation}
1481
1482 Most approaches to ``AJAX''-style coding involve imperative manipulation of the DOM tree representing an HTML document's structure. Ur/Web follows the \emph{functional-reactive} approach instead. Programs may allocate mutable \emph{sources} of arbitrary types, and an HTML page is effectively a pure function over the latest values of the sources. The page is not mutated directly, but rather it changes automatically as the sources are mutated.
1459 1483
1460 $$\begin{array}{l} 1484 $$\begin{array}{l}
1461 \mt{con} \; \mt{source} :: \mt{Type} \to \mt{Type} \\ 1485 \mt{con} \; \mt{source} :: \mt{Type} \to \mt{Type} \\
1462 \mt{val} \; \mt{source} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; (\mt{source} \; \mt{t}) \\ 1486 \mt{val} \; \mt{source} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; (\mt{source} \; \mt{t}) \\
1463 \mt{val} \; \mt{set} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\ 1487 \mt{val} \; \mt{set} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\
1473 \end{array}$$ 1497 \end{array}$$
1474 1498
1475 A reactive portion of an HTML page is injected with a $\mt{dyn}$ tag, which has a signal-valued attribute $\mt{Signal}$. 1499 A reactive portion of an HTML page is injected with a $\mt{dyn}$ tag, which has a signal-valued attribute $\mt{Signal}$.
1476 1500
1477 $$\begin{array}{l} 1501 $$\begin{array}{l}
1478 \mt{val} \; \mt{dyn} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \mt{unit} \\ 1502 \mt{val} \; \mt{dyn} : \mt{use} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \mt{unit} \\
1479 \hspace{.1in} \to \mt{tag} \; [\mt{Signal} = \mt{signal} \; (\mt{xml} \; \mt{ctx} \; \mt{use} \; \mt{bind})] \; \mt{ctx} \; [] \; \mt{use} \; \mt{bind} 1503 \hspace{.1in} \to \mt{tag} \; [\mt{Signal} = \mt{signal} \; (\mt{xml} \; \mt{body} \; \mt{use} \; \mt{bind})] \; \mt{body} \; [] \; \mt{use} \; \mt{bind}
1480 \end{array}$$ 1504 \end{array}$$
1481 1505
1482 Transactions can be run on the client by including them in attributes like the $\mt{OnClick}$ attribute of $\mt{button}$, and GUI widgets like $\mt{ctextbox}$ have $\mt{Source}$ attributes that can be used to connect them to sources, so that their values can be read by code running because of, e.g., an $\mt{OnClick}$ event. 1506 Transactions can be run on the client by including them in attributes like the $\mt{Onclick}$ attribute of $\mt{button}$, and GUI widgets like $\mt{ctextbox}$ have $\mt{Source}$ attributes that can be used to connect them to sources, so that their values can be read by code running because of, e.g., an $\mt{Onclick}$ event.
1507
1508 \subsubsection{Asynchronous Message-Passing}
1509
1510 To support asynchronous, ``server push'' delivery of messages to clients, any client that might need to receive an asynchronous message is assigned a unique ID. These IDs may be retrieved both on the client and on the server, during execution of code related to a client.
1511
1512 $$\begin{array}{l}
1513 \mt{type} \; \mt{client} \\
1514 \mt{val} \; \mt{self} : \mt{transaction} \; \mt{client}
1515 \end{array}$$
1516
1517 \emph{Channels} are the means of message-passing. Each channel is created in the context of a client and belongs to that client; no other client may receive the channel's messages. Each channel type includes the type of values that may be sent over the channel. Sending and receiving are asynchronous, in the sense that a client need not be ready to receive a message right away. Rather, sent messages may queue up, waiting to be processed.
1518
1519 $$\begin{array}{l}
1520 \mt{con} \; \mt{channel} :: \mt{Type} \to \mt{Type} \\
1521 \mt{val} \; \mt{channel} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; (\mt{channel} \; \mt{t}) \\
1522 \mt{val} \; \mt{send} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\
1523 \mt{val} \; \mt{recv} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{transaction} \; \mt{t}
1524 \end{array}$$
1525
1526 The $\mt{channel}$ and $\mt{send}$ operations may only be executed on the server, and $\mt{recv}$ may only be executed on a client. Neither clients nor channels may be passed as arguments from clients to server-side functions, so persistent channels can only be maintained by storing them in the database and looking them up using the current client ID or some application-specific value as a key.
1527
1528 Clients and channels live only as long as the web browser page views that they are associated with. When a user surfs away, his client and its channels will be garbage-collected, after that user is not heard from for the timeout period. Garbage collection deletes any database row that contains a client or channel directly. Any reference to one of these types inside an $\mt{option}$ is set to $\mt{None}$ instead. Both kinds of handling have the flavor of weak pointers, and that is a useful way to think about clients and channels in the database.
1529
1483 1530
1484 \section{Ur/Web Syntax Extensions} 1531 \section{Ur/Web Syntax Extensions}
1485 1532
1486 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. 1533 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.
1487 1534