Mercurial > urweb

comparison doc/manual.tex @ 528:9e2abd85529b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Declarations and modules
author Adam Chlipala <adamc@hcoop.net>
date Thu, 27 Nov 2008 15:43:10 -0500
parents 74dd4dca9e32
children 4df69124e9c5
comparison
equal deleted inserted replaced
527:74dd4dca9e32 528:9e2abd85529b
97 &&& S \; \mt{where} \; x = c & \textrm{concretizing an abstract constructor} \\ 97 &&& S \; \mt{where} \; x = c & \textrm{concretizing an abstract constructor} \\
98 &&& M.X & \textrm{projection from a module} \\ 98 &&& M.X & \textrm{projection from a module} \\
99 \\ 99 \\
100 \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\ 100 \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
101 &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\ 101 &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
102 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype declaration} \\ 102 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
103 &&& \mt{datatype} \; x = M.x & \textrm{algebraic datatype import} \\ 103 &&& \mt{datatype} \; x = M.x & \textrm{algebraic datatype import} \\
104 &&& \mt{val} \; x : \tau & \textrm{value} \\ 104 &&& \mt{val} \; x : \tau & \textrm{value} \\
105 &&& \mt{structure} \; X : S & \textrm{sub-module} \\ 105 &&& \mt{structure} \; X : S & \textrm{sub-module} \\
106 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\ 106 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
107 &&& \mt{include} \; S & \textrm{signature inclusion} \\ 107 &&& \mt{include} \; S & \textrm{signature inclusion} \\
157 \\ 157 \\
158 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\ 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} \\ 159 &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
160 \end{array}$$ 160 \end{array}$$
161 161
162 \emph{Declarations} primarily bring new symbols into context.
163 $$\begin{array}{rrcll}
164 \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
165 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
166 &&& \mt{datatype} \; x = M.x & \textrm{algebraic datatype import} \\
167 &&& \mt{val} \; x : \tau = e & \textrm{value} \\
168 &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
169 &&& \mt{structure} \; X : S = M & \textrm{module definition} \\
170 &&& \mt{signature} \; X = S & \textrm{signature definition} \\
171 &&& \mt{open} \; M & \textrm{module inclusion} \\
172 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
173 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
174 &&& \mt{table} \; x : c & \textrm{SQL table} \\
175 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
176 &&& \mt{class} \; x = c & \textrm{concrete type class} \\
177 &&& \mt{cookie} \; x : c & \textrm{HTTP cookie} \\
178 \\
179 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \mt{constant} \\
180 &&& X & \mt{variable} \\
181 &&& M.X & \mt{projection} \\
182 &&& M(M) & \mt{functor application} \\
183 &&& \mt{functor}(X : S) : S = M & \mt{functor abstraction} \\
184 \end{array}$$
185
186 There are two kinds of Ur files. A file named $M\texttt{.ur}$ is an \emph{implementation file}, and it should contain a sequence of declarations $d^*$. A file named $M\texttt{.urs}$ is an \emph{interface file}; it must always have a matching $M\texttt{.ur}$ and should contain a sequence of signature items $s^*$. When both files are present, the overall effect is the same as a monolithic declaration $\mt{structure} \; M : \mt{sig} \; s^* \; \mt{end} = \mt{struct} \; d^* \; \mt{end}$. When no interface file is included, the overall effect is similar, with a signature for module $M$ being inferred rather than just checked against an interface.
162 187
163 \end{document} 188 \end{document}