summaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-mod.tex
blob: 68d572265a9a458b61b774e73cd4c7203266608d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
\section{Module system
\index{Modules}
\label{section:Modules}}

The module system provides a way of packaging related elements
together, as well as a mean of massive abstraction.

\begin{figure}[t]
\begin{centerframe}
\begin{tabular}{rcl}
{\modtype}  & ::= & {\qualid} \\
 & $|$ & {\modtype} \texttt{ with Definition }{\qualid} := {\term} \\
 & $|$ & {\modtype} \texttt{ with Module }{\qualid} := {\qualid} \\
 & $|$ & {\qualid} \nelist{\qualid}{}\\
 & $|$ & $!${\qualid} \nelist{\qualid}{}\\
 &&\\

{\onemodbinding}  & ::= & {\tt ( [Import|Export] \nelist{\ident}{} : {\modtype} )}\\
 &&\\

{\modbindings} & ::= & \nelist{\onemodbinding}{}\\
 &&\\

{\modexpr} & ::= & \nelist{\qualid}{} \\
           & $|$ & $!$\nelist{\qualid}{}
\end{tabular}
\end{centerframe}
\caption{Syntax of modules}
\end{figure}

In the syntax of module application, the $!$ prefix indicates that
any {\tt Inline} directive in the type of the functor arguments
will be ignored (see \ref{Inline} below).

\subsection{\tt Module {\ident}
\comindex{Module}}

This command is used to start an interactive module named {\ident}.

\begin{Variants}

\item{\tt Module {\ident} {\modbindings}}

  Starts an interactive functor with parameters given by {\modbindings}.

\item{\tt Module {\ident} \verb.:. {\modtype}}

  Starts an interactive module specifying its module type. 

\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype}}

  Starts an interactive functor with parameters given by
  {\modbindings}, and output module type {\modtype}.

\item{\tt Module {\ident} \verb.<:. {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:.{ \modtype$_n$}}

  Starts an interactive module satisfying each {\modtype$_i$}. 

\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:. {\modtype$_n$}}

  Starts an interactive functor with parameters given by
  {\modbindings}. The output module type is verified against each
  module type {\modtype$_i$}.

\item\texttt{Module [Import|Export]}

  Behaves like \texttt{Module}, but automatically imports or exports
  the module.

\end{Variants}
\subsubsection{Reserved commands inside an interactive module:
\comindex{Include}}
\begin{enumerate}
\item {\tt Include {\module}}

  Includes the content of {\module} in the current interactive
 module. Here {\module} can be a module expresssion or a module type
 expression. If {\module} is a high-order module or module type
 expression then the system tries to instanciate {\module}
 by the current interactive module.

\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} 

is a shortcut for {\tt Include {\module$_1$}}  $\ldots$ {\tt Include {\module$_n$}}
\end{enumerate}
\subsection{\tt End {\ident}
\comindex{End}}

This command closes the interactive module {\ident}. If the module type
was given the content of the module is matched against it and an error
is signaled if the matching fails. If the module is basic (is not a
functor) its components (constants, inductive types, submodules etc) are
now available through the dot notation.

\begin{ErrMsgs}
\item \errindex{No such label {\ident}}
\item \errindex{Signature components for label {\ident} do not match}
\item \errindex{This is not the last opened module}
\end{ErrMsgs}


\subsection{\tt Module {\ident} := {\modexpr}
\comindex{Module}}

This command defines the module identifier {\ident} to be equal to
{\modexpr}. 

\begin{Variants}
\item{\tt Module {\ident} {\modbindings} := {\modexpr}}

 Defines a functor with parameters given by {\modbindings} and body {\modexpr}.

% Particular cases of the next 2 items
%\item{\tt Module {\ident} \verb.:. {\modtype} := {\modexpr}}
%
%  Defines a module with body {\modexpr} and interface {\modtype}.
%\item{\tt Module {\ident} \verb.<:. {\modtype} := {\modexpr}}
%
%  Defines a module with body {\modexpr}, satisfying {\modtype}.

\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype} :=
    {\modexpr}}

  Defines a functor with parameters given by {\modbindings} (possibly none),
  and output module type {\modtype}, with body {\modexpr}. 

\item{\tt Module {\ident} {\modbindings} \verb.<:.  {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:. {\modtype$_n$}:=
    {\modexpr}}

  Defines a functor with parameters given by {\modbindings} (possibly none) 
  with body {\modexpr}. The body is checked against each {\modtype$_i$}.

\item{\tt Module {\ident} {\modbindings} := {\modexpr$_1$} \verb.<+. $\ldots$ \verb.<+. {\modexpr$_n$}}

  is equivalent to an interactive module where each {\modexpr$_i$} are included.

\end{Variants}

\subsection{\tt Module Type {\ident}
\comindex{Module Type}}

This command is used to start an interactive module type {\ident}.

\begin{Variants}

\item{\tt Module Type {\ident} {\modbindings}}

  Starts an interactive functor type with parameters given by {\modbindings}.

\end{Variants}
\subsubsection{Reserved commands inside an interactive module type:
\comindex{Include}\comindex{Inline}}
\label{Inline}
\begin{enumerate}
\item {\tt Include {\module}}

 Same as {\tt Include} inside a module.

\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} 

is a shortcut for {\tt Include {\module$_1$}}  $\ldots$ {\tt Include {\module$_n$}}

\item {\tt {\assumptionkeyword} Inline {\assums} }

 The instance of this assumption will be automatically expanded at functor
 application, except when this functor application is prefixed by a $!$ annotation.
\end{enumerate}
\subsection{\tt End {\ident}
\comindex{End}}

This command closes the interactive module type {\ident}.

\begin{ErrMsgs}
\item \errindex{This is not the last opened module type}
\end{ErrMsgs}

\subsection{\tt Module Type {\ident} := {\modtype}}

Defines a module type {\ident} equal to {\modtype}.

\begin{Variants}
\item {\tt Module Type {\ident} {\modbindings} := {\modtype}}

  Defines a functor type {\ident} specifying functors taking arguments
  {\modbindings} and returning {\modtype}.

\item{\tt Module Type {\ident} {\modbindings} := {\modtype$_1$} \verb.<+. $\ldots$ \verb.<+. {\modtype$_n$}}

  is equivalent to an interactive module type were each {\modtype$_i$} are included.

\end{Variants}

\subsection{\tt Declare Module {\ident} : {\modtype}}

Declares a module {\ident} of type {\modtype}.

\begin{Variants}

\item{\tt Declare Module {\ident} {\modbindings} \verb.:. {\modtype}}

  Declares a functor with parameters {\modbindings} and output module
  type {\modtype}.


\end{Variants}


\subsubsection{Example}

Let us define a simple module.
\begin{coq_example}
Module M.
  Definition T := nat.
  Definition x := 0.
  Definition y : bool.
    exact true.
  Defined.
End M.
\end{coq_example}
Inside a module one can define constants, prove theorems and do any
other things that can be done in the toplevel. Components of a closed
module can be accessed using the dot notation:
\begin{coq_example}
Print M.x.
\end{coq_example}
A simple module type:
\begin{coq_example}
Module Type SIG.
  Parameter T : Set.
  Parameter x : T.
End SIG.
\end{coq_example}

Now we can create a new module from \texttt{M}, giving it a less
precise specification: the \texttt{y} component is dropped as well
as the body of \texttt{x}.

\begin{coq_eval}
Set Printing Depth 50.
(********** The following is not correct and should produce **********)
(***************** Error: N.y not a defined object *******************)
\end{coq_eval}
\begin{coq_example}
Module N  :  SIG with Definition T := nat  :=  M.
Print N.T.
Print N.x.
Print N.y.
\end{coq_example}
\begin{coq_eval}
Reset N.
\end{coq_eval}

\noindent
The definition of \texttt{N} using the module type expression
\texttt{SIG with Definition T:=nat} is equivalent to the following
one:

\begin{coq_example*}
Module Type SIG'.
  Definition T : Set := nat.
  Parameter x : T.
End SIG'.
Module N : SIG' := M.
\end{coq_example*}
If we just want to be sure that the our implementation satisfies a
given module type without restricting the interface, we can use a
transparent constraint
\begin{coq_example}
Module P <: SIG := M.
Print P.y.
\end{coq_example}
Now let us create a functor, i.e. a parametric module
\begin{coq_example}
Module Two (X Y: SIG).
\end{coq_example}
\begin{coq_example*}
  Definition T := (X.T * Y.T)%type.
  Definition x := (X.x, Y.x).
\end{coq_example*}
\begin{coq_example}
End Two.
\end{coq_example}
and apply it to our modules and do some computations
\begin{coq_example}
Module Q := Two M N.
Eval compute in (fst Q.x + snd Q.x).
\end{coq_example}
In the end, let us define a module type with two sub-modules, sharing
some of the fields and give one of its possible implementations:
\begin{coq_example}
Module Type SIG2.
  Declare Module M1 : SIG.
  Module M2 <: SIG.
    Definition T := M1.T.
    Parameter x : T.
  End M2.
End SIG2.
\end{coq_example}
\begin{coq_example*}
Module Mod <: SIG2.
  Module M1.
    Definition T := nat.
    Definition x := 1.
  End M1.
  Module M2 := M.
\end{coq_example*}
\begin{coq_example}
End Mod.
\end{coq_example}
Notice that \texttt{M} is a correct body for the component \texttt{M2}
since its \texttt{T} component is equal \texttt{nat} and hence
\texttt{M1.T} as specified.
\begin{coq_eval}
Reset Initial.
\end{coq_eval}

\begin{Remarks}
\item Modules and module types can be nested components of each other.
\item One can have sections inside a module or a module type, but
  not a module or a module type inside a section.
\item Commands like \texttt{Hint} or \texttt{Notation} can
  also appear inside modules and module types. Note that in case of a
  module definition like:

    \smallskip
    \noindent
    {\tt Module N : SIG := M.} 
    \smallskip

    or

    \smallskip
    {\tt Module N : SIG.\\
      \ \ \dots\\
      End N.}
    \smallskip 
    
    hints and the like valid for \texttt{N} are not those defined in
    \texttt{M} (or the module body) but the ones defined in
    \texttt{SIG}.

\end{Remarks}

\subsection{\tt Import {\qualid}
\comindex{Import}
\label{Import}}

If {\qualid} denotes a valid basic module (i.e. its module type is a
signature), makes its components available by their short names.

Example:

\begin{coq_example}
Module Mod.
\end{coq_example}
\begin{coq_example}
  Definition T:=nat.
  Check T.
\end{coq_example}
\begin{coq_example}
End Mod.
Check Mod.T.
Check T. (* Incorrect ! *)
Import Mod.
Check T. (* Now correct *)
\end{coq_example}
\begin{coq_eval}
Reset Mod.
\end{coq_eval}

Some features defined in modules are activated only when a module is
imported. This is for instance the case of notations (see
Section~\ref{Notation}).

\begin{Variants}
\item{\tt Export {\qualid}}\comindex{Export}

  When the module containing the command {\tt Export {\qualid}} is
  imported, {\qualid} is imported as well.
\end{Variants}

\begin{ErrMsgs}
  \item \errindexbis{{\qualid} is not a module}{is not a module}
% this error is impossible in the import command
%  \item \errindex{Cannot mask the absolute name {\qualid} !}
\end{ErrMsgs}

\begin{Warnings}
  \item Warning: Trying to mask the absolute name {\qualid} !
\end{Warnings}

\subsection{\tt Print Module {\ident}
\comindex{Print Module}}

Prints the module type and (optionally) the body of the module {\ident}.

\subsection{\tt Print Module Type {\ident}
\comindex{Print Module Type}}

Prints the module type corresponding to {\ident}.

\subsection{\tt Locate Module {\qualid}
\comindex{Locate Module}}

Prints the full name of the module {\qualid}.


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: