Mercurial > urweb

comparison doc/manual.tex @ 852:4d4c62d95b9c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New release
author Adam Chlipala <adamc@hcoop.net>
date Tue, 23 Jun 2009 12:53:47 -0400
parents d18f6f0bcf60
children 19fdeef40ada
comparison
equal deleted inserted replaced
851:20a364c4a6dc 852:4d4c62d95b9c
138 \item \texttt{exe FILENAME} sets the filename to which to write the output executable. The default for file \texttt{P.urp} is \texttt{P.exe}. 138 \item \texttt{exe FILENAME} sets the filename to which to write the output executable. The default for file \texttt{P.urp} is \texttt{P.exe}.
139 \item \texttt{ffi FILENAME} reads the file \texttt{FILENAME.urs} to determine the interface to a new FFI module. The name of the module is calculated from \texttt{FILENAME} in the same way as for normal source files. See the files \texttt{include/urweb.h} and \texttt{src/c/urweb.c} for examples of C headers and implementations for FFI modules. In general, every type or value \texttt{Module.ident} becomes \texttt{uw\_Module\_ident} in C. 139 \item \texttt{ffi FILENAME} reads the file \texttt{FILENAME.urs} to determine the interface to a new FFI module. The name of the module is calculated from \texttt{FILENAME} in the same way as for normal source files. See the files \texttt{include/urweb.h} and \texttt{src/c/urweb.c} for examples of C headers and implementations for FFI modules. In general, every type or value \texttt{Module.ident} becomes \texttt{uw\_Module\_ident} in C.
140 \item \texttt{jsFunc Module.ident=name} gives the JavaScript name of an FFI value. 140 \item \texttt{jsFunc Module.ident=name} gives the JavaScript name of an FFI value.
141 \item \texttt{library FILENAME} parses \texttt{FILENAME.urp} and merges its contents with the rest of the current file's contents. 141 \item \texttt{library FILENAME} parses \texttt{FILENAME.urp} and merges its contents with the rest of the current file's contents.
142 \item \texttt{link FILENAME} adds \texttt{FILENAME} to the list of files to be passed to the GCC linker at the end of compilation. This is most useful for importing extra libraries needed by new FFI modules. 142 \item \texttt{link FILENAME} adds \texttt{FILENAME} to the list of files to be passed to the GCC linker at the end of compilation. This is most useful for importing extra libraries needed by new FFI modules.
143 \item \texttt{path NAME=VALUE} creates a mapping from \texttt{NAME} to \texttt{VALUE}. This mapping may be used at the beginnings of filesystem paths given to various other configuration directives. A path like \texttt{\$NAME/rest} is expanded to \texttt{VALUE/rest}. There is an initial mapping from the empty name (for paths like \texttt{\$/list}) to the directory where the Ur/Web standard library is installed. If you accept the default \texttt{configure} options, this directory is \texttt{/usr/local/lib/urweb/ur}.
143 \item \texttt{prefix PREFIX} sets the prefix included before every URI within the generated application. The default is \texttt{/}. 144 \item \texttt{prefix PREFIX} sets the prefix included before every URI within the generated application. The default is \texttt{/}.
144 \item \texttt{profile} generates an executable that may be used with gprof. 145 \item \texttt{profile} generates an executable that may be used with gprof.
145 \item \texttt{rewrite KIND FROM TO} gives a rule for rewriting canonical module paths. For instance, the canonical path of a page may be \texttt{Mod1.Mod2.mypage}, while you would rather the page were accessed via a URL containing only \texttt{page}. The directive \texttt{rewrite url Mod1/Mod2/mypage page} would accomplish that. The possible values of \texttt{KIND} determine which kinds of objects are affected. The kind \texttt{all} matches any object, and \texttt{url} matches page URLs. The kinds \texttt{table}, \texttt{sequence}, and \texttt{view} match those sorts of SQL entities, and \texttt{relation} matches any of those three. \texttt{cookie} matches HTTP cookies, and \texttt{style} matches CSS class names. If \texttt{FROM} ends in \texttt{/*}, it is interpreted as a prefix matching rule, and rewriting occurs by replacing only the appropriate prefix of a path with \texttt{TO}. While the actual external names of relations and styles have parts separated by underscores instead of slashes, all rewrite rules must be written in terms of slashes. 146 \item \texttt{rewrite KIND FROM TO} gives a rule for rewriting canonical module paths. For instance, the canonical path of a page may be \texttt{Mod1.Mod2.mypage}, while you would rather the page were accessed via a URL containing only \texttt{page}. The directive \texttt{rewrite url Mod1/Mod2/mypage page} would accomplish that. The possible values of \texttt{KIND} determine which kinds of objects are affected. The kind \texttt{all} matches any object, and \texttt{url} matches page URLs. The kinds \texttt{table}, \texttt{sequence}, and \texttt{view} match those sorts of SQL entities, and \texttt{relation} matches any of those three. \texttt{cookie} matches HTTP cookies, and \texttt{style} matches CSS class names. If \texttt{FROM} ends in \texttt{/*}, it is interpreted as a prefix matching rule, and rewriting occurs by replacing only the appropriate prefix of a path with \texttt{TO}. While the actual external names of relations and styles have parts separated by underscores instead of slashes, all rewrite rules must be written in terms of slashes.
146 \item \texttt{script URL} adds \texttt{URL} to the list of extra JavaScript files to be included at the beginning of any page that uses JavaScript. This is most useful for importing JavaScript versions of functions found in new FFI modules. 147 \item \texttt{script URL} adds \texttt{URL} to the list of extra JavaScript files to be included at the beginning of any page that uses JavaScript. This is most useful for importing JavaScript versions of functions found in new FFI modules.
147 \item \texttt{serverOnly Module.ident} registers an FFI function or transaction that may only be run on the server. 148 \item \texttt{serverOnly Module.ident} registers an FFI function or transaction that may only be run on the server.
286 &&& \ell & \textrm{constant} \\ 287 &&& \ell & \textrm{constant} \\
287 &&& \hat{X} & \textrm{nullary constructor} \\ 288 &&& \hat{X} & \textrm{nullary constructor} \\
288 &&& \hat{X} \; p & \textrm{unary constructor} \\ 289 &&& \hat{X} \; p & \textrm{unary constructor} \\
289 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\ 290 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
290 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\ 291 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
292 &&& p : \tau & \textrm{type annotation} \\
291 &&& (p) & \textrm{explicit precedence} \\ 293 &&& (p) & \textrm{explicit precedence} \\
292 \\ 294 \\
293 \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\ 295 \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\
294 &&& M.X & \textrm{projection from a module} \\ 296 &&& M.X & \textrm{projection from a module} \\
295 \end{array}$$ 297 \end{array}$$
302 &&& \ell & \textrm{constant} \\ 304 &&& \ell & \textrm{constant} \\
303 \\ 305 \\
304 &&& e \; e & \textrm{function application} \\ 306 &&& e \; e & \textrm{function application} \\
305 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\ 307 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
306 &&& e [c] & \textrm{polymorphic function application} \\ 308 &&& e [c] & \textrm{polymorphic function application} \\
307 &&& \lambda x \; ? \; \kappa \Rightarrow e & \textrm{polymorphic function abstraction} \\ 309 &&& \lambda [x \; ? \; \kappa] \Rightarrow e & \textrm{polymorphic function abstraction} \\
308 &&& e [\kappa] & \textrm{kind-polymorphic function application} \\ 310 &&& e [\kappa] & \textrm{kind-polymorphic function application} \\
309 &&& X \Longrightarrow e & \textrm{kind-polymorphic function abstraction} \\ 311 &&& X \Longrightarrow e & \textrm{kind-polymorphic function abstraction} \\
310 \\ 312 \\
311 &&& \{(c = e,)^*\} & \textrm{known-length record} \\ 313 &&& \{(c = e,)^*\} & \textrm{known-length record} \\
312 &&& e.c & \textrm{record field projection} \\ 314 &&& e.c & \textrm{record field projection} \\
370 372
371 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$. 373 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
372 374
373 A tuple type $(\tau_1, \ldots, \tau_n)$ expands to a record type $\{1 = \tau_1, \ldots, n = \tau_n\}$, with natural numbers as field names. A tuple pattern $(p_1, \ldots, p_n)$ expands to a rigid record pattern $\{1 = p_1, \ldots, n = p_n\}$. Positive natural numbers may be used in most places where field names would be allowed. 375 A tuple type $(\tau_1, \ldots, \tau_n)$ expands to a record type $\{1 = \tau_1, \ldots, n = \tau_n\}$, with natural numbers as field names. A tuple pattern $(p_1, \ldots, p_n)$ expands to a rigid record pattern $\{1 = p_1, \ldots, n = p_n\}$. Positive natural numbers may be used in most places where field names would be allowed.
374 376
375 In general, several adjacent $\lambda$ forms may be combined into one, and kind and type annotations may be omitted, in which case they are implicitly included as wildcards. More formally, for constructor-level abstractions, we can define a new non-terminal $b ::= x \mid (x :: \kappa) \mid X$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$. 377 In general, several adjacent $\lambda$ forms may be combined into one, and kind and type annotations may be omitted, in which case they are implicitly included as wildcards. More formally, for constructor-level abstractions, we can define a new non-terminal $b ::= x \mid (x :: \kappa) \mid X$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$.
376 378
377 For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mt{val} \; x : B = A$), $B$ and the preceding colon (or similar punctuation) may be omitted, in which case it is filled in as a wildcard. 379 For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mt{val} \; x : B = A$), $B$ and the preceding colon (or similar punctuation) may be omitted, in which case it is filled in as a wildcard.
378 380
379 A signature item or declaration $\mt{type} \; x$ or $\mt{type} \; x = \tau$ is elaborated into $\mt{con} \; x :: \mt{Type}$ or $\mt{con} \; x :: \mt{Type} = \tau$, respectively. 381 A signature item or declaration $\mt{type} \; x$ or $\mt{type} \; x = \tau$ is elaborated into $\mt{con} \; x :: \mt{Type}$ or $\mt{con} \; x :: \mt{Type} = \tau$, respectively.
380 382
381 A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$. 383 A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
382 384
383 Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all implicit constructor arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally halting automatic resolution of type class instances and automatic proving of disjointness constraints. The default is that any prefix of a variable's type consisting only of implicit polymorphism, type class instances, and disjointness obligations is resolved automatically, with the variable treated as having the type that starts after the last implicit element, with suitable unification variables substituted. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors). 385 Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all implicit constructor arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally halting automatic resolution of type class instances and automatic proving of disjointness constraints. The default is that any prefix of a variable's type consisting only of implicit polymorphism, type class instances, and disjointness obligations is resolved automatically, with the variable treated as having the type that starts after the last implicit element, with suitable unification variables substituted. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors).
384 386
385 At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= x \mid (x : \tau) \mid (x \; ? \; \kappa) \mid X \mid [c \sim c]$. A lone variable $x$ as a binder stands for an expression variable of unspecified type. 387 At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= p \mid [x] \mid [x \; ? \; \kappa] \mid X \mid [c \sim c]$. A lone variable $[x]$ stands for an implicit constructor variable of unspecified kind. The standard value-level function binder is recovered as the type-annotated pattern form $x : \tau$. It is a compile-time error to include a pattern $p$ that does not match every value of the appropriate type.
386 388
387 A $\mt{val}$ or $\mt{val} \; \mt{rec}$ declaration may include expression binders before the equal sign, following the binder grammar from the last paragraph. Such declarations are elaborated into versions that add additional $\lambda$s to the fronts of the righthand sides, as appropriate. The keyword $\mt{fun}$ is a synonym for $\mt{val} \; \mt{rec}$. 389 A local $\mt{val}$ declaration may bind a pattern instead of just a plain variable. As for function arguments, only irrefutable patterns are legal.
390
391 The keyword $\mt{fun}$ is a shorthand for $\mt{val} \; \mt{rec}$ that allows arguments to be specified before the equal sign in the definition of each mutually-recursive function, as in SML. Each curried argument must follow the grammar of the $b$ non-terminal introduced two paragraphs ago. A $\mt{fun}$ declaration is elaborated into a version that adds additional $\lambda$s to the fronts of the righthand sides, as appropriate.
388 392
389 A signature item $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2$. A declaration $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2 = M$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2 = \mt{functor}(X_2 : S_1) : S_2 = M$. 393 A signature item $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2$. A declaration $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2 = M$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2 = \mt{functor}(X_2 : S_1) : S_2 = M$.
394
395 An $\mt{open} \; \mt{constraints}$ declaration is implicitly inserted for the argument of every functor at the beginning of the functor body. For every declaration of the form $\mt{structure} \; X : S = \mt{struct} \ldots \mt{end}$, an $\mt{open} \; \mt{constraints} \; X$ declaration is implicitly inserted immediately afterward.
390 396
391 A declaration $\mt{table} \; x : \{(c = c,)^*\}$ is elaborated into $\mt{table} \; x : [(c = c,)^*]$ 397 A declaration $\mt{table} \; x : \{(c = c,)^*\}$ is elaborated into $\mt{table} \; x : [(c = c,)^*]$
392 398
393 The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$. 399 The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$.
394 400
642 648
643 $$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{ 649 $$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{
644 \Gamma \vdash e : x :: \kappa \to \tau 650 \Gamma \vdash e : x :: \kappa \to \tau
645 & \Gamma \vdash c :: \kappa 651 & \Gamma \vdash c :: \kappa
646 } 652 }
647 \quad \infer{\Gamma \vdash \lambda x \; ? \; \kappa \Rightarrow e : x \; ? \; \kappa \to \tau}{ 653 \quad \infer{\Gamma \vdash \lambda [x \; ? \; \kappa] \Rightarrow e : x \; ? \; \kappa \to \tau}{
648 \Gamma, x :: \kappa \vdash e : \tau 654 \Gamma, x :: \kappa \vdash e : \tau
649 }$$ 655 }$$
650 656
651 $$\infer{\Gamma \vdash e [\kappa] : [X \mapsto \kappa]\tau}{ 657 $$\infer{\Gamma \vdash e [\kappa] : [X \mapsto \kappa]\tau}{
652 \Gamma \vdash e : X \longrightarrow \tau 658 \Gamma \vdash e : X \longrightarrow \tau
728 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i 734 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
729 } 735 }
730 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{ 736 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
731 \Gamma_0 = \Gamma 737 \Gamma_0 = \Gamma
732 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i 738 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
739 }$$
740
741 $$\infer{\Gamma \vdash p : \tau \leadsto \Gamma'; \tau}{
742 \Gamma \vdash p \leadsto \Gamma'; \tau'
743 & \Gamma \vdash \tau' \equiv \tau
733 }$$ 744 }$$
734 745
735 \subsection{Declaration Typing} 746 \subsection{Declaration Typing}
736 747
737 We use an auxiliary judgment $\overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'$, expressing the enrichment of $\Gamma$ with the types of the datatype constructors $\overline{dc}$, when they are known to belong to datatype $x$ with type parameters $\overline{y}$. 748 We use an auxiliary judgment $\overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'$, expressing the enrichment of $\Gamma$ with the types of the datatype constructors $\overline{dc}$, when they are known to belong to datatype $x$ with type parameters $\overline{y}$.