aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/RefMan-mod.tex
blob: 9f6f2abce19f9d3622570367986d5ca5e2c7a37e (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
\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}  & ::= & {\ident} \\
 & $|$ & {\modtype} \texttt{ with Definition }{\ident} := {\term} \\
 & $|$ & {\modtype} \texttt{ with Module }{\ident} := {\qualid} \\
 &&\\

{\onemodbinding}  & ::= & {\tt ( \nelist{\ident}{} : {\modtype} )}\\
 &&\\

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

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

\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}}

  Starts an interactive module satisfying {\modtype}. 

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

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

\end{Variants}

\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} :=
    {\modexpr}}

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

\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}

\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}.
\end{Variants}

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

Starts an interactive module declaration. This command is available
only in module types. 

\begin{Variants}

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

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

% Particular case of the next item
%\item{\tt Declare Module {\ident} \verb.<:. {\modtype}}
%
%  Starts an interactive declaration of a module satisfying {\modtype}.

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

  Starts an interactive declaration of a functor with parameters given
  by {\modbindings} (possibly none). The declared output module type is
  verified against the module type {\modtype}.

\end{Variants}

\subsection{\tt End {\ident}}

This command closes the interactive declaration of module {\ident}.

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

Declares a module of {\ident} of type {\modtype}. This command is available
only in module types. 

\begin{Variants}

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

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

\item{\tt Declare Module {\ident} := {\qualid}}

  Declares a module equal to the module {\qualid}.

\item{\tt Declare Module {\ident} \verb.<:. {\modtype} := {\qualid}}

  Declares a module equal to the module {\qualid}, verifying that the
  module type of the latter is a subtype of {\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}
Inside a module type the proof editing mode is not available.
Consequently commands like \texttt{Definition}\ without body,
\texttt{Lemma}, \texttt{Theorem} are not allowed.  In order to declare
constants, use \texttt{Axiom} and \texttt{Parameter}.

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.
  Declare 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 When a module declaration is started inside a module type,
  the proof editing mode is still unavailable.
\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:

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

    or

    \medskip
    {\tt Module N : SIG.\\
      \ \ \dots\\
      End N.}
    \medskip 
    
    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{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}


\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}.


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