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
|
\section{Module system}
The module system provides a way of packaging related elements
together, as well as a mean of massive abstraction.
\begin{figure}[t]
\begin{tabular}{|rcl|}
\hline
{\modtype} & ::= & {\ident} \\
& $|$ & \modtype \texttt{ with Definition }{\ident} \verb.:=. {\term} \\
& $|$ & \modtype \texttt{ with Module }{\ident} \verb.:=. {\qualid} \\
&&\\
{\onemodbinding} & ::= & \nelist{\ident}{\texttt{,}} \verb.:. {\modtype} \\
&&\\
{\modbindings} & ::= & \nelist{\onemodbinding}{\texttt{;}}\\
&&\\
{\modexpr} & ::= & \nelist{\qualid}{} \\
\hline
\end{tabular}
\caption{Syntax of modules.}
\label{ecases-grammar}
\end{figure}
\subsection{\tt Module {\ident}}\comindex{Module}
This command is used to start an interactif module named {\ident}.
\begin{Variants}
\item{\tt Module \ident [\modbindings]}\\
Starts an interactif functor with parameters given by {\modbindings}.
\item{\tt Module {\ident} \verb.:. \modtype}\\
Starts an interactif module specifying its the module type.
\item{\tt Module {\ident} [\modbindings] \verb.:. \modtype}\\
Starts an interactif functor with parameters given by
{\modbindings}, and output module type \modtype.
\end{Variants}
\subsection{\tt End {\ident}}\comindex{End}
This command closes the interactif 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, inductives, 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.
\item{\tt Module {\ident} \verb.:. {\modtype} := {\modexpr}}\\
Defines a module specifying its module type.
\item{\tt Module {\ident} [\modbindings] \verb.:. {\modtype} := {\modexpr}}\\
Defines a functor with parameters given by {\modbindings}, and
output module type \modtype, with body {\modexpr}.
\end{Variants}
\subsection{\tt Module Type {\ident}}\comindex{Module Type}
This command is used to start an interactif module type {\ident}.
\begin{Variants}
\item{\tt Module \ident [\modbindings]}\\
Starts an interactif functor type with parameters given by {\modbindings}.
\end{Variants}
\subsection{\tt End {\ident}}\comindex{End}
This command closes the interactif module type {\ident}.
\begin{ErrMsgs}
\item \errindex{This is not the last opened module type}
\end{ErrMsgs}
\subsection{\tt Module Type {\ident} := {\modtype}}
Define a module type \ident equal to \modtype.
\begin{Variants}
\item {\tt Module Type {\ident} {\modbindings} := {\modtype}} \\
Define a functor type {\ident} specifying functors taking arguments
{\modbindings} and returning {\modtype}.
\end{Variants}
\subsubsection{Example}
Let us define a simple module.
\begin{coq_example}
Module M.
Definition T:=nat.
Definition x:=O.
Definition y:bool.
Exact true.
Defined.
End M.
\end{coq_example}
Inside a module one can define constants, prove thorems 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.
Definition T:Set.
Definition x:T.
End SIG.
\end{coq_example}
Notice that \texttt{Definition}\ without body did not start the proof
mode. Also \texttt{Lemma} or \texttt{Theorem} do not start one.
Inside a module type \texttt{Definition}\ withount body,
\texttt{Lemma}, \texttt{Theorem}, \texttt{Axiom}, \texttt{Parameter} are
equivalent.
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_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}
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.
Definition x:T.
End SIG'.
Module N : SIG' := M.
\end{coq_example*}
Now let us create a functor
\begin{coq_example}
Module Two[X,Y:SIG].
\end{coq_example}
\begin{coq_example*}
Definition T:=X.T * Y.T.
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 P:=Two M N.
Eval Compute in (plus (Fst P.x) (Snd P.x)).
\end{coq_example}
\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 is started inside a module type,
\texttt{Definition} without body, \texttt{Lemma}, and
\texttt{Theorem} still do not start the proof mode. This is still a
specification (of a sub-module component) and not a real definition.
\item The only way of using a proof mode in a module type is using the
\texttt{Goal} command.
\item One can have sections inside a module or a module type, but
not a module or a module type inside a section.
\item Other commands like \texttt{Hint} or \texttt{Syntactic
Definition} can also appear inside modules and module types. 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
the commands valid for \texttt{N} are not those from
\texttt{M} (or the module body) but the ones from \texttt{SIG}.
\end{Remarks}
\subsection{\tt Print Module {\ident}}\comindex{Print Module}
Prints the module type and the body of the module {\ident}.
\subsection{\tt Print Module Type {\ident}}\comindex{Print Module Type}
Prints the module type correspondint to {\ident}.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
