\chapter[The Module System]{The Module System\label{chapter:Modules}}

The module system extends the Calculus of Inductive Constructions
providing a convenient way to structure large developments as well as
a mean of massive abstraction.
%It is described in details in Judicael's thesis and Jacek's thesis

\section{Modules and module types}

\paragraph{Access path.} It is denoted by $p$, it can be either a module 
variable $X$ or, if $p'$ is an access path and $id$ an identifier, then
$p'.id$ is an access path.

\paragraph{Structure element.} It is denoted by \elem\ and is either a
definition of a constant, an assumption, a definition of an inductive,
 a definition of a module, an alias of module or a module type abbreviation.

\paragraph{Structure expression.} It is denoted by $S$ and can be:
\begin{itemize}
\item an access path $p$
\item a plain structure $\struct{\nelist{\elem}{;}}$
\item a functor $\functor{X}{S}{S'}$, where $X$ is a module variable,
  $S$ and $S'$ are structure expression
\item an application $S\,p$, where $S$ is a structure expression and $p$ 
an access path 
\item a refined structure $\with{S}{p}{p'}$ or $\with{S}{p}{t:T}$ where $S$
is a structure expression, $p$ and $p'$ are access paths, $t$ is a term 
and $T$ is the type of $t$.
\end{itemize}

\paragraph{Module definition,} is written $\Mod{X}{S}{S'}$ and
 consists of a module variable $X$, a module type
$S$ which can be any structure expression and optionally a module implementation $S'$ 
 which can be any structure expression except a refined structure.

\paragraph{Module alias,} is written $\ModA{X}{p}$ and
 consists of a module variable $X$ and a module path $p$. 

\paragraph{Module type abbreviation,} is written $\ModType{Y}{S}$, where
$Y$ is an identifier and $S$ is any structure expression .


\section{Typing Modules}

In order to introduce the typing system we first slightly extend
the syntactic class of terms and environments given in
section~\ref{Terms}. The environments, apart from definitions of
constants and inductive types now also hold any other structure elements.
Terms, apart from variables, constants and complex terms, 
include also access paths.

We also need additional typing judgments: 
\begin{itemize}
\item \WFT{E}{S}, denoting that a structure $S$ is well-formed, 

\item \WTM{E}{p}{S}, denoting that the module pointed by $p$ has type $S$ in
environment $E$.

\item \WEV{E}{S}{\overline{S}}, denoting that a structure $S$ is evaluated to 
a structure $\overline{S}$ in weak head normal form.

\item \WS{E}{S_1}{S_2}, denoting that a structure $S_1$ is a subtype of a
structure $S_2$.

\item \WS{E}{\elem_1}{\elem_2}, denoting that a structure element
  $\elem_1$ is more precise that a structure element $\elem_2$.
\end{itemize}
The rules for forming structures are the following:
\begin{description}
\item[WF-STR]
\inference{%
  \frac{
    \WF{E;E'}{}
  }{%%%%%%%%%%%%%%%%%%%%%
    \WFT{E}{\struct{E'}}
  }
}
\item[WF-FUN]
\inference{%
  \frac{
    \WFT{E;\ModS{X}{S}}{\overline{S'}}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WFT{E}{\functor{X}{S}{S'}}
  }
}
\end{description}
Evaluation of structures to weak head normal form:
\begin{description}
\item[WEVAL-APP]
\inference{%
  \frac{
    \begin{array}{c}
    \WEV{E}{S}{\functor{X}{S_1}{S_2}}~~~~~\WEV{E}{S_1}{\overline{S_1}}\\
    \WTM{E}{p}{S_3}\qquad \WS{E}{S_3}{\overline{S_1}}
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WEV{E}{S\,p}{S_2\{p/X,t_1/p_1.c_1,\ldots,t_n/p_n.c_n\}}
  }
}
\end{description}
In the last rule, $\{t_1/p_1.c_1,\ldots,t_n/p_n.c_n\}$ is the resulting
 substitution from the inlining mechanism. We substitute in $S$ the
 inlined fields $p_i.c_i$ form $\ModS{X}{S_1}$ by the corresponding delta-reduced term $t_i$ in $p$.
\begin{description}
\item[WEVAL-WITH-MOD]
\inference{%
  \frac{
    \begin{array}{c}
    \WEV{E}{S}{\structe{\ModS{X}{S_1}}}~~~~~\WEV{E;\elem_1;\ldots;\elem_i}{S_1}{\overline{S_1}}\\
    \WTM{E}{p}{S_2}\qquad \WS{E;\elem_1;\ldots;\elem_i}{S_2}{\overline{S_1}}
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \begin{array}{c}
    \WEVT{E}{\with{S}{x}{p}}{\structes{\ModA{X}{p}}{p/X}}
    \end{array}
  }
}
\item[WEVAL-WITH-MOD-REC]
\inference{%
  \frac{
    \begin{array}{c}
    \WEV{E}{S}{\structe{\ModS{X_1}{S_1}}}\\
    \WEV{E;\elem_1;\ldots;\elem_i}{\with{S_1}{p}{p_1}}{\overline{S_2}}
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \begin{array}{c}
    \WEVT{E}{\with{S}{X_1.p}{p_1}}{\structes{\ModS{X}{\overline{S_2}}}{p_1/X_1.p}}
    \end{array}
  }
}
\item[WEVAL-WITH-DEF]
\inference{%
  \frac{
    \begin{array}{c}
    \WEV{E}{S}{\structe{\Assum{}{c}{T_1}}}\\
    \WS{E;\elem_1;\ldots;\elem_i}{\Def{}{c}{t}{T}}{\Assum{}{c}{T_1}}
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \begin{array}{c}
    \WEVT{E}{\with{S}{c}{t:T}}{\structe{\Def{}{c}{t}{T}}}
    \end{array}
  }
}
\item[WEVAL-WITH-DEF-REC]
\inference{%
  \frac{
    \begin{array}{c}
    \WEV{E}{S}{\structe{\ModS{X_1}{S_1}}}\\
    \WEV{E;\elem_1;\ldots;\elem_i}{\with{S_1}{p}{p_1}}{\overline{S_2}}
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \begin{array}{c}
    \WEVT{E}{\with{S}{X_1.p}{t:T}}{\structe{\ModS{X}{\overline{S_2}}}}
    \end{array}
  }
}

\item[WEVAL-PATH-MOD]
\inference{%
  \frac{
    \begin{array}{c}
    \WEV{E}{p}{\structe{ \Mod{X}{S}{S_1}}}\\
    \WEV{E;\elem_1;\ldots;\elem_i}{S}{\overline{S}}
   \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WEV{E}{p.X}{\overline{S}}
  }
}
\inference{%
  \frac{
    \begin{array}{c}
    \WF{E}{}~~~~~~\Mod{X}{S}{S_1}\in E\\
    \WEV{E}{S}{\overline{S}}
   \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WEV{E}{X}{\overline{S}}
  }
}
\item[WEVAL-PATH-ALIAS]
\inference{%
  \frac{
    \begin{array}{c}
    \WEV{E}{p}{\structe{\ModA{X}{p_1}}}\\
    \WEV{E;\elem_1;\ldots;\elem_i}{p_1}{\overline{S}}
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WEV{E}{p.X}{\overline{S}}
  }
}
\inference{%
  \frac{
    \begin{array}{c}
      \WF{E}{}~~~~~~~\ModA{X}{p_1}\in E\\
      \WEV{E}{p_1}{\overline{S}}
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WEV{E}{X}{\overline{S}}
  }
}
\item[WEVAL-PATH-TYPE]
\inference{%
  \frac{
    \begin{array}{c}
    \WEV{E}{p}{\structe{\ModType{Y}{S}}}\\
    \WEV{E;\elem_1;\ldots;\elem_i}{S}{\overline{S}}
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WEV{E}{p.Y}{\overline{S}}
  }
}
\item[WEVAL-PATH-TYPE]
\inference{%
  \frac{
    \begin{array}{c}
    \WF{E}{}~~~~~~~\ModType{Y}{S}\in E\\
    \WEV{E}{S}{\overline{S}}
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WEV{E}{Y}{\overline{S}}
  }
}
\end{description}
 Rules for typing module:
\begin{description}
\item[MT-EVAL]
\inference{%
  \frac{
 \WEV{E}{p}{\overline{S}}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WTM{E}{p}{\overline{S}}
  }
}
\item[MT-STR]
\inference{%
  \frac{
    \WTM{E}{p}{S}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WTM{E}{p}{S/p}
  }
}
\end{description}
The last rule, called strengthening is used to make all module fields
manifestly equal to themselves. The notation $S/p$ has the following
meaning:
\begin{itemize}
\item if $S\lra\struct{\elem_1;\dots;\elem_n}$ then
  $S/p=\struct{\elem_1/p;\dots;\elem_n/p}$ where $\elem/p$ is defined as
  follows:
  \begin{itemize}
  \item $\Def{}{c}{t}{T}/p\footnote{Opaque definitions are processed as assumptions.} ~=~ \Def{}{c}{t}{T}$
  \item $\Assum{}{c}{U}/p ~=~ \Def{}{c}{p.c}{U}$
  \item $\ModS{X}{S}/p ~=~ \ModA{X}{p.X}$
  \item $\ModA{X}{p'}/p ~=~ \ModA{X}{p'}$
  \item $\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}/p ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$
  \item $\Indpstr{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}{p} ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}$
  \end{itemize}
\item if $S\lra\functor{X}{S'}{S''}$ then $S/p=S$
\end{itemize}
The notation $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$ denotes an
inductive definition that is definitionally equal to the inductive
definition in the module denoted by the path $p$. All rules which have
$\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}$ as premises are also valid for 
$\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$. We give the formation rule
for $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$ below as well as
the equality rules on inductive types and constructors. \\

The module subtyping rules:
\begin{description}
\item[MSUB-STR]
\inference{%
  \frac{
    \begin{array}{c}
      \WS{E;\elem_1;\dots;\elem_n}{\elem_{\sigma(i)}}{\elem'_i}
                                  \textrm{ \ for } i=1..m \\
      \sigma : \{1\dots m\} \ra \{1\dots n\} \textrm{ \ injective}
    \end{array}
  }{
    \WS{E}{\struct{\elem_1;\dots;\elem_n}}{\struct{\elem'_1;\dots;\elem'_m}}
  }
}
\item[MSUB-FUN]
\inference{%       T_1 -> T_2 <: T_1' -> T_2'
  \frac{
    \WS{E}{\overline{S_1'}}{\overline{S_1}}~~~~~~~~~~\WS{E;\ModS{X}{S_1'}}{\overline{S_2}}{\overline{S_2'}}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WS{E}{\functor{X}{S_1}{S_2}}{\functor{X}{S_1'}{S_2'}}
  }
}
% these are derived rules
% \item[MSUB-EQ]
% \inference{%
%   \frac{
%     \WS{E}{T_1}{T_2}~~~~~~~~~~\WTERED{}{T_1}{=}{T_1'}~~~~~~~~~~\WTERED{}{T_2}{=}{T_2'}
%   }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%     \WS{E}{T_1'}{T_2'}
%   }
% }
% \item[MSUB-REFL]
% \inference{%
%   \frac{
%     \WFT{E}{T}
%   }{
%     \WS{E}{T}{T}
%   }
% }
\end{description}
Structure element subtyping rules:
\begin{description}
\item[ASSUM-ASSUM]
\inference{%
  \frac{
    \WTELECONV{}{T_1}{T_2}
  }{
    \WSE{\Assum{}{c}{T_1}}{\Assum{}{c}{T_2}}
  }
}
\item[DEF-ASSUM]
\inference{%
  \frac{
    \WTELECONV{}{T_1}{T_2}
  }{
    \WSE{\Def{}{c}{t}{T_1}}{\Assum{}{c}{T_2}}
  }
}
\item[ASSUM-DEF]
\inference{%
  \frac{
    \WTELECONV{}{T_1}{T_2}~~~~~~~~\WTECONV{}{c}{t_2}
  }{
    \WSE{\Assum{}{c}{T_1}}{\Def{}{c}{t_2}{T_2}}
  }
}
\item[DEF-DEF]
\inference{%
  \frac{
    \WTELECONV{}{T_1}{T_2}~~~~~~~~\WTECONV{}{t_1}{t_2}
  }{
    \WSE{\Def{}{c}{t_1}{T_1}}{\Def{}{c}{t_2}{T_2}}
  }
}
\item[IND-IND]
\inference{%
  \frac{
    \WTECONV{}{\Gamma_P}{\Gamma_P'}%
    ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
    ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
  }{
    \WSE{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}%
        {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
  }
}
\item[INDP-IND]
\inference{%
  \frac{
    \WTECONV{}{\Gamma_P}{\Gamma_P'}%
    ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
    ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
  }{
    \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}%
        {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
  }
}
\item[INDP-INDP]
\inference{%
  \frac{
    \WTECONV{}{\Gamma_P}{\Gamma_P'}%
    ~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
    ~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
    ~~~~~~\WTECONV{}{p}{p'}
  }{
    \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}%
        {\Indp{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}{p'}}
  }
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\item[MOD-MOD]
\inference{%
  \frac{
    \WSE{S_1}{S_2}
  }{
    \WSE{\ModS{X}{S_1}}{\ModS{X}{S_2}}
  }
}
\item[ALIAS-MOD]
\inference{%
  \frac{
    \WTM{E}{p}{S_1}~~~~~~~~\WSE{S_1}{S_2}
  }{
    \WSE{\ModA{X}{p}}{\ModS{X}{S_2}}
  }
}
\item[MOD-ALIAS]
\inference{%
  \frac{
      \WTM{E}{p}{S_2}~~~~~~~~
      \WSE{S_1}{S_2}~~~~~~~~\WTECONV{}{X}{p}
  }{
    \WSE{\ModS{X}{S_1}}{\ModA{X}{p}}
  }
}
\item[ALIAS-ALIAS]
\inference{%
  \frac{
    \WTECONV{}{p_1}{p_2}
  }{
    \WSE{\ModA{X}{p_1}}{\ModA{X}{p_2}}
  }
}
\item[MODTYPE-MODTYPE]
\inference{%
  \frac{
    \WSE{S_1}{S_2}~~~~~~~~\WSE{S_2}{S_1}
  }{
    \WSE{\ModType{Y}{S_1}}{\ModType{Y}{S_2}}
  }
}
\end{description}
New environment formation rules
\begin{description}
\item[WF-MOD]
\inference{%
  \frac{
    \WF{E}{}~~~~~~~~\WFT{E}{S}
  }{
    \WF{E;\ModS{X}{S}}{}
  }
}
\item[WF-MOD]
\inference{%
  \frac{
\begin{array}{c}
  \WS{E}{S_2}{S_1}\\
  \WF{E}{}~~~~~\WFT{E}{S_1}~~~~~\WFT{E}{S_2}
\end{array}
  }{
    \WF{E;\Mod{X}{S_1}{S_2}}{}
  }
}

\item[WF-ALIAS]
\inference{%
  \frac{
    \WF{E}{}~~~~~~~~~~~\WTE{}{p}{S}
  }{
    \WF{E,\ModA{X}{p}}{}
  }
}
\item[WF-MODTYPE]
\inference{%
  \frac{
    \WF{E}{}~~~~~~~~~~~\WFT{E}{S}
  }{
    \WF{E,\ModType{Y}{S}}{}
  }
}
\item[WF-IND]
\inference{%
  \frac{
    \begin{array}{c}
      \WF{E;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}{}\\
      \WT{E}{}{p:\struct{\elem_1;\dots;\elem_n;\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'};\dots}}\\
      \WS{E}{\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
  }
}
\end{description}
Component access rules
\begin{description}
\item[ACC-TYPE]
\inference{%
  \frac{
    \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Assum{}{c}{T};\dots}}
  }{
    \WTEG{p.c}{T}
  }
}
\\
\inference{%
  \frac{
    \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Def{}{c}{t}{T};\dots}}
  }{
    \WTEG{p.c}{T}
  }
}
\item[ACC-DELTA]
Notice that the following rule extends the delta rule defined in
section~\ref{delta}
\inference{%
  \frac{
    \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Def{}{c}{t}{U};\dots}}
  }{
    \WTEGRED{p.c}{\triangleright_\delta}{t}
  }
}
\\
In the rules below we assume $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$,
  $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
  $[c_1:C_1;\ldots;c_n:C_n]$
\item[ACC-IND]
\inference{%
  \frac{
    \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
  }{
    \WTEG{p.I_j}{(p_1:P_1)\ldots(p_r:P_r)A_j}
  }
}
\inference{%
  \frac{
    \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
  }{
    \WTEG{p.c_m}{(p_1:P_1)\ldots(p_r:P_r){C_m}{I_j}{(I_j~p_1\ldots
       p_r)}_{j=1\ldots k}}
  }
}
\item[ACC-INDP]
\inference{%
  \frac{
    \WT{E}{}{p}{\struct{\elem_1;\dots;\elem_i;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
  }{
    \WTRED{E}{}{p.I_i}{\triangleright_\delta}{p'.I_i}
  }
}
\inference{%
  \frac{
    \WT{E}{}{p}{\struct{\elem_1;\dots;\elem_i;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
  }{
    \WTRED{E}{}{p.c_i}{\triangleright_\delta}{p'.c_i}
  }
}

\end{description}

% %%% replaced by \triangle_\delta
% Module path equality is a transitive and reflexive closure of the
% relation generated by ACC-MODEQ and ENV-MODEQ.
% \begin{itemize}
% \item []MP-EQ-REFL
% \inference{%
%   \frac{
%     \WTEG{p}{T}
%   }{
%     \WTEG{p}{p}
%   }
% }
% \item []MP-EQ-TRANS
% \inference{%
%   \frac{
%     \WTEGRED{p}{=}{p'}~~~~~~\WTEGRED{p'}{=}{p''}
%   }{
%     \WTEGRED{p'}{=}{p''}
%   }
% }

% \end{itemize}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: