<commit_before>\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*}<commit_msg>Definition -> Parameter dans module types<commit_after>\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 Type \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}

\noindent
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.
  Parameter T:Set.
  Parameter x:T.
End SIG.
\end{coq_example}

\noindent
Inside a module type \texttt{Definition}\ without body,
\texttt{Lemma}, \texttt{Theorem} do not start the proof mode.
In fact, inside a module type all three are equivalent and they are
moreover equivalent to \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*}
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*}
{'fraction_non_alphanumeric': 0.13998332291015217, 'fraction_numerical': 0.0, 'mean_word_length': 3.9637868598034145, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 4, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2925645', 'n_tokens_mistral': 3131, 'n_tokens_neox': 3066, 'n_words': 1131}