path: root/doc/RefMan-mod.tex

\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.}
\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, 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 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}, and
  output module type {\modtype}, with body {\modexpr}. 
\item{\tt Module {\ident} [\modbindings] \verb.<:. {\modtype} := {\modexpr}}\\
  Defines a functor with parameters given by {\modbindings} 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}}
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}

\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}.
\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}. 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:=O.
  Definition y:bool.
    Exact true.
  Defined.
End M.
\end{coq_example}

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

\noindent
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_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.
  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 (plus (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}
\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{Syntactic Definition} 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{\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: