1 files changed, 411 insertions, 0 deletions
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
new file mode 100644
index 00000000..68d57226
--- /dev/null
+++ b/doc/refman/RefMan-mod.tex
@@ -0,0 +1,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: