Mercurial > urweb

comparison doc/manual.tex @ 527:74dd4dca9e32

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Expressions
author Adam Chlipala <adamc@hcoop.net>
date Thu, 27 Nov 2008 15:27:17 -0500
parents f87fd1549c33
children 9e2abd85529b
comparison
equal deleted inserted replaced
526:f87fd1549c33 527:74dd4dca9e32
3 3
4 \newcommand{\cd}[1]{\texttt{#1}} 4 \newcommand{\cd}[1]{\texttt{#1}}
5 \newcommand{\mt}[1]{\mathsf{#1}} 5 \newcommand{\mt}[1]{\mathsf{#1}}
6 6
7 \newcommand{\rc}{+ \hspace{-.075in} + \;} 7 \newcommand{\rc}{+ \hspace{-.075in} + \;}
8 \newcommand{\rcut}{\; \texttt{--} \;}
9 \newcommand{\rcutM}{\; \texttt{---} \;}
8 10
9 \begin{document} 11 \begin{document}
10 12
11 \title{The Ur/Web Manual} 13 \title{The Ur/Web Manual}
12 \author{Adam Chlipala} 14 \author{Adam Chlipala}
24 \textbf{\LaTeX} & \textbf{ASCII} \\ 26 \textbf{\LaTeX} & \textbf{ASCII} \\
25 $\to$ & \cd{->} \\ 27 $\to$ & \cd{->} \\
26 $\times$ & \cd{*} \\ 28 $\times$ & \cd{*} \\
27 $\lambda$ & \cd{fn} \\ 29 $\lambda$ & \cd{fn} \\
28 $\Rightarrow$ & \cd{=>} \\ 30 $\Rightarrow$ & \cd{=>} \\
29 $\rc$ & \cd{++} \\ 31 & \cd{---} \\
30 \\ 32 \\
31 $x$ & Normal textual identifier, not beginning with an uppercase letter \\ 33 $x$ & Normal textual identifier, not beginning with an uppercase letter \\
32 $X$ & Normal textual identifier, beginning with an uppercase letter \\ 34 $X$ & Normal textual identifier, beginning with an uppercase letter \\
33 \end{tabular} 35 \end{tabular}
34 \end{center} 36 \end{center}
35 37
36 We often write syntax like $e^*$ to indicate zero or more copies of $e$, $e^+$ to indicate one or more copies, and $e,^*$ and $e,^+$ to indicate multiple copies separated by commas. Another separator may be used in place of a comma. The $e$ term may be surrounded by parentheses to indicate grouping; those parentheses should not be included in the actual ASCII. 38 We often write syntax like $e^*$ to indicate zero or more copies of $e$, $e^+$ to indicate one or more copies, and $e,^*$ and $e,^+$ to indicate multiple copies separated by commas. Another separator may be used in place of a comma. The $e$ term may be surrounded by parentheses to indicate grouping; those parentheses should not be included in the actual ASCII.
37 39
38 We write $\ell$ for literals of the primitive types, for the most part following C conventions. There are $\mt{int}$, $\mt{float}$, and $\mt{string}$ literals. 40 We write $\ell$ for literals of the primitive types, for the most part following C conventions. There are $\mt{int}$, $\mt{float}$, and $\mt{string}$ literals.
41
42 This version of the manual doesn't include operator precedences; see \texttt{src/urweb.grm} for that.
39 43
40 \subsection{Core Syntax} 44 \subsection{Core Syntax}
41 45
42 \emph{Kinds} classify types and other compile-time-only entities. Each kind in the grammar is listed with a description of the sort of data it classifies. 46 \emph{Kinds} classify types and other compile-time-only entities. Each kind in the grammar is listed with a description of the sort of data it classifies.
43 $$\begin{array}{rrcll} 47 $$\begin{array}{rrcll}
45 &&& \mt{Unit} & \textrm{the trivial constructor} \\ 49 &&& \mt{Unit} & \textrm{the trivial constructor} \\
46 &&& \mt{Name} & \textrm{field names} \\ 50 &&& \mt{Name} & \textrm{field names} \\
47 &&& \kappa \to \kappa & \textrm{type-level functions} \\ 51 &&& \kappa \to \kappa & \textrm{type-level functions} \\
48 &&& \{\kappa\} & \textrm{type-level records} \\ 52 &&& \{\kappa\} & \textrm{type-level records} \\
49 &&& (\kappa\times^+) & \textrm{type-level tuples} \\ 53 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
54 &&& \_ & \textrm{wildcard} \\
50 &&& (\kappa) & \textrm{explicit precedence} \\ 55 &&& (\kappa) & \textrm{explicit precedence} \\
51 \end{array}$$ 56 \end{array}$$
52 57
53 Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions. 58 Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions.
54 $$\begin{array}{rrcll} 59 $$\begin{array}{rrcll}
78 &&& (c^+) & \textrm{type-level tuple} \\ 83 &&& (c^+) & \textrm{type-level tuple} \\
79 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\ 84 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
80 \\ 85 \\
81 &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\ 86 &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
82 \\ 87 \\
88 &&& \_ & \textrm{wildcard} \\
83 &&& (c) & \textrm{explicit precedence} \\ 89 &&& (c) & \textrm{explicit precedence} \\
84 \end{array}$$ 90 \end{array}$$
85 91
86 Modules of the module system are described by \emph{signatures}. 92 Modules of the module system are described by \emph{signatures}.
87 $$\begin{array}{rrcll} 93 $$\begin{array}{rrcll}
114 &&& \ell & \textrm{constant} \\ 120 &&& \ell & \textrm{constant} \\
115 &&& \hat{X} & \textrm{nullary constructor} \\ 121 &&& \hat{X} & \textrm{nullary constructor} \\
116 &&& \hat{X} \; p & \textrm{unary constructor} \\ 122 &&& \hat{X} \; p & \textrm{unary constructor} \\
117 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\ 123 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
118 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\ 124 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
125 &&& (p) & \textrm{explicit precedence} \\
119 \\ 126 \\
120 \textrm{Qualified capitalized variable} & \hat{X} &::=& X & \textrm{not from a module} \\ 127 \textrm{Qualified capitalized variable} & \hat{X} &::=& X & \textrm{not from a module} \\
121 &&& M.X & \textrm{projection from a module} \\ 128 &&& M.X & \textrm{projection from a module} \\
122 \end{array}$$ 129 \end{array}$$
123 130
131 \emph{Expressions} are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages.
132 $$\begin{array}{rrcll}
133 \textrm{Expressions} & e &::=& e : \tau & \textrm{type annotation} \\
134 &&& x & \textrm{variable} \\
135 &&& \ell & \textrm{constant} \\
136 \\
137 &&& e \; e & \textrm{function application} \\
138 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
139 &&& e [c] & \textrm{polymorphic function application} \\
140 &&& \lambda x \; ? \; \kappa \Rightarrow e & \textrm{polymorphic function abstraction} \\
141 \\
142 &&& \{(c = e,)^*\} & \textrm{known-length record} \\
143 &&& e.c & \textrm{record field projection} \\
144 &&& e \rc e & \textrm{record concatenation} \\
145 &&& e \rcut c & \textrm{removal of a single record field} \\
146 &&& e \rcutM c & \textrm{removal of multiple record fields} \\
147 &&& \mt{fold} & \textrm{fold over fields of a type-level record} \\
148 \\
149 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
150 \\
151 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\
152 \\
153 &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression} \\
154 \\
155 &&& \_ & \textrm{wildcard} \\
156 &&& (e) & \textrm{explicit precedence} \\
157 \\
158 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
159 &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
160 \end{array}$$
161
162
124 \end{document} 163 \end{document}