From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- doc/refman/RefMan-mod.tex | 396 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 396 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..9f6f2abc --- /dev/null +++ b/doc/refman/RefMan-mod.tex @@ -0,0 +1,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: -- cgit v1.2.3