Mercurial > urweb
comparison doc/manual.tex @ 2226:e10881cd92da
Merge.
| author | Ziv Scully <ziv@mit.edu> |
|---|---|
| date | Fri, 27 Mar 2015 11:26:06 -0400 |
| parents | 15d46eb02570 |
| children | 752e5efe9da9 |
comparison
equal
deleted
inserted
replaced
| 2225:6262dabc08d6 | 2226:e10881cd92da |
|---|---|
| 4 \usepackage{ae,aecompl} | 4 \usepackage{ae,aecompl} |
| 5 \newcommand{\cd}[1]{\texttt{#1}} | 5 \newcommand{\cd}[1]{\texttt{#1}} |
| 6 \newcommand{\mt}[1]{\mathsf{#1}} | 6 \newcommand{\mt}[1]{\mathsf{#1}} |
| 7 | 7 |
| 8 \newcommand{\rc}{+ \hspace{-.075in} + \;} | 8 \newcommand{\rc}{+ \hspace{-.075in} + \;} |
| 9 \newcommand{\rcut}{\; \texttt{--} \;} | 9 \newcommand{\rcut}{\; \texttt{-{}-} \;} |
| 10 \newcommand{\rcutM}{\; \texttt{---} \;} | 10 \newcommand{\rcutM}{\; \texttt{-{}-{}-} \;} |
| 11 | 11 |
| 12 \begin{document} | 12 \begin{document} |
| 13 | 13 |
| 14 \title{The Ur/Web Manual} | 14 \title{The Ur/Web Manual} |
| 15 \author{Adam Chlipala} | 15 \author{Adam Chlipala} |
| 630 | 630 |
| 631 A signature item $\mt{table} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_table} \; c \; []$. $\mt{view} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_view} \; c$, $\mt{sequence} \; x$ is short for $\mt{val} \; x : \mt{Basis}.\mt{sql\_sequence}$. $\mt{cookie} \; x : \tau$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{http\_cookie} \; \tau$, and $\mt{style} \; x$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{css\_class}$. | 631 A signature item $\mt{table} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_table} \; c \; []$. $\mt{view} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_view} \; c$, $\mt{sequence} \; x$ is short for $\mt{val} \; x : \mt{Basis}.\mt{sql\_sequence}$. $\mt{cookie} \; x : \tau$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{http\_cookie} \; \tau$, and $\mt{style} \; x$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{css\_class}$. |
| 632 | 632 |
| 633 It is possible to write a $\mt{let}$ expression with its constituents in reverse order, along the lines of Haskell's \cd{where}. An expression $\mt{let} \; e \; \mt{where} \; ed^* \; \mt{end}$ desugars to $\mt{let} \; ed^* \; \mt{in} \; e \; \mt{end}$. | 633 It is possible to write a $\mt{let}$ expression with its constituents in reverse order, along the lines of Haskell's \cd{where}. An expression $\mt{let} \; e \; \mt{where} \; ed^* \; \mt{end}$ desugars to $\mt{let} \; ed^* \; \mt{in} \; e \; \mt{end}$. |
| 634 | 634 |
| 635 Ur/Web also includes a few more infix operators: $f \; \texttt{<|} \; x$ desugars to $f \; x$, $x \; \texttt{|>} \; f$ to $f \; x$, $f \; \texttt{<{}<{}<} \; g$ to $\mt{Top}.\mt{compose} \; f \; g$, and $g \; \texttt{>{}>{}>} \; f$ to $\mt{Top}.\mt{compose} \; f \; g$. (The latter two are doing function composition in the usual way.) Furthermore, any identifier may be changed into an infix operator by placing it between backticks, e.g. a silly way to do addition is $x \; \texttt{`}\mt{plus}\texttt{`} \; y$ instead of $x + y$. | |
| 636 | |
| 637 Hexadecimal integer literals are supported like \texttt{0xDEADBEEF}. Only capital letters are allowed. | |
| 638 | |
| 635 | 639 |
| 636 \section{Static Semantics} | 640 \section{Static Semantics} |
| 637 | 641 |
| 638 In this section, we give a declarative presentation of Ur's typing rules and related judgments. Inference is the subject of the next section; here, we assume that an oracle has filled in all wildcards with concrete values. | 642 In this section, we give a declarative presentation of Ur's typing rules and related judgments. Inference is the subject of the next section; here, we assume that an oracle has filled in all wildcards with concrete values. |
| 639 | 643 |
| 2261 $$\begin{array}{rrcll} | 2265 $$\begin{array}{rrcll} |
| 2262 \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; O] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\ | 2266 \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; O] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\ |
| 2263 \textrm{Pre-queries} & q &::=& \mt{SELECT} \; [\mt{DISTINCT}] \; P \; \mt{FROM} \; F,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\ | 2267 \textrm{Pre-queries} & q &::=& \mt{SELECT} \; [\mt{DISTINCT}] \; P \; \mt{FROM} \; F,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\ |
| 2264 &&& \mid q \; R \; q \mid \{\{\{e\}\}\} \\ | 2268 &&& \mid q \; R \; q \mid \{\{\{e\}\}\} \\ |
| 2265 \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT} \\ | 2269 \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT} \\ |
| 2266 \textrm{$\mt{ORDER \; BY}$ items} & O &::=& \mt{RANDOM} [()] \mid \hat{E} \; [o] \mid \hat{E} \; [o], O | 2270 \textrm{$\mt{ORDER \; BY}$ items} & O &::=& \mt{RANDOM} [()] \mid \hat{E} \; [o] \mid \hat{E} \; [o], O \mid \{\{\{e\}\}\} |
| 2267 \end{array}$$ | 2271 \end{array}$$ |
| 2268 | 2272 |
| 2269 $$\begin{array}{rrcll} | 2273 $$\begin{array}{rrcll} |
| 2270 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\ | 2274 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\ |
| 2271 &&& p,^+ & \textrm{particular columns} \\ | 2275 &&& p,^+ & \textrm{particular columns} \\ |