From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- doc/refman/RefMan-mod.tex | 411 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 411 insertions(+) create mode 100644 doc/refman/RefMan-mod.tex (limited to 'doc/refman/RefMan-mod.tex') 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: -- cgit v1.2.3