\chapter{The Module System}
\label{Mod}

The module system extends the Calculus of Inductive Constructions
providing a convinient way to structure large developments as well as
a mean of massive abstraction.

\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 \Impl\ and is either a
definition of a constant, an assumption, a definition of an inductive
or a definition of a module or a module type abbreviation.

\paragraph{Module expression.} It is denoted by $M$ and can be:
\begin{itemize}
\item an access path $p$
\item a structure $\struct{\nelist{\Impl}{;}}$
\item a functor $\functor{X}{T}{M'}$, where $X$ is a module variable,
  $T$ is a module type and $M'$ is a module expression
\item an application of access paths $p' p''$
\end{itemize}

\paragraph{Signature element.} It is denoted by \Spec, it is a
specification of a constant, an assumption, an inductive, a module or
a module type abbreviation.

\paragraph{Module type}, denoted by $T$ can be:
\begin{itemize}
\item a module type name
\item an access path $p$
\item a signature $\sig{\nelist{\Spec}{;}}$
\item a functor type $\funsig{X}{T'}{T''}$, where $T'$ and $T''$ are
  module types
\end{itemize}

\paragraph{Module definition}, written $\Mod{X}{T}{M}$ can be a
structure element. It consists of a module variable $X$, a module type
$T$ and a module expression $M$.

\paragraph{Module specification}, written $\ModS{X}{T}$ or
$\ModSEq{X}{T}{p}$ can be a signature element or a part of an
environment. It consists of a module variable $X$, a module type $T$
and, optionally, a module path $p$. 

\paragraph{Module type abbreviation}, written $\ModType{S}{T}$, where
$S$ is a module type name and $T$ is a module type.


\section{Typing Modules}

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

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

\item \WTM{E}{M}{T}, denoting that a module expression $M$ has type $T$ in
environment $E$.

\item \WTM{E}{\Impl}{\Spec}, denoting that an implementation $\Impl$
  verifies a specification $\Spec$

\item \WS{E}{T_1}{T_2}, denoting that a module type $T_1$ is a subtype of a
module type $T_2$.

\item \WS{E}{\Spec_1}{\Spec_2}, denoting that a specification
  $\Spec_1$ is more precise that a specification $\Spec_2$.
\end{itemize}
The rules for forming module types are the following:
\begin{itemize}
\item [WF-SIG]
\inference{%
  \frac{
    \WF{E;E'}{}
  }{%%%%%%%%%%%%%%%%%%%%%
    \WFT{E}{\sig{E'}}
  }
}
\item [WF-FUN]
\inference{%
  \frac{
    \WFT{E;\ModS{X}{T}}{T'}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WFT{E}{\funsig{X}{T}{T'}}
  }
}
\end{itemize}
Rules for typing module expressions:
\begin{itemize}
\item [MT-STRUCT]
\inference{%
  \frac{
    \begin{array}{c}
      \WFT{E}{\sig{\Spec_1;\dots;\Spec_n}}\\
      \WTM{E;\Spec_1;\dots;\Spec_{i-1}}{\Impl_i}{\Spec_i}
                                              \textrm{ \ \ for } i=1\dots n
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WTM{E}{\struct{\Impl_1;\dots;\Impl_n}}{\sig{\Spec_1;\dots;\Spec_n}}
  }
}
\item [MT-FUN]
\inference{%
  \frac{
    \WTM{E;\ModS{X}{T}}{M}{T'}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WTM{E}{\functor{X}{T}{M}}{\funsig{X}{T}{T'}}
  }
}
\item [MT-APP]
\inference{%
  \frac{
    \WTM{E}{p'}{\funsig{X}{T}{T'}}~~~~~~~~~~~\WTM{E}{p''}{T}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WTM{E}{p' p''}{T'\{X/p''\}}
  }
}
\item [MT-SUB]
\inference{%
  \frac{
    \WTM{E}{M}{T}~~~~~~~~~~~~\WS{E}{T}{T'}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WTM{E}{M}{T'}
  }
}
\item [MT-STR]
\inference{%
  \frac{
    \WTM{E}{p}{T}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WTM{E}{p}{T/p}
  }
}
\end{itemize}
The last rule, called strengthenning is used to make all module fields
manifestly equal to themselves. The notation $T/p$ has the following
meaning:
\begin{itemize}
\item if $T=\sig{\Spec_1;\dots;\Spec_n}$ then
  $T/p=\sig{\Spec_1/p;\dots;\Spec_n/p}$ where $\Spec/p$ is defined as
  follows:
  \begin{itemize}
  \item $\Def{}{c}{U}{t}/p ~=~ \Def{}{c}{U}{t}$
  \item $\Assum{}{c}{U}/p ~=~ \Def{}{c}{U}{p.c}$
  \item $\ModS{X}{T}/p ~=~ \ModSEq{X}{T/p.X}{p.X}$
  \item $\ModSEq{X}{T}{p'}/p ~=~ \ModSEq{X}{T}{p'}$
  \item $\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}/p ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$
  \item $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}/p ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}$
  \end{itemize}
\item if $T=\funsig{X}{T}{T'}$ then $T/p=T$
\item if $T$ is an access path or a module type name, then we have to
  unfold its definition and proceed according to the rules above. 
\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{itemize}
\item [MSUB-SIG]
\inference{%
  \frac{
    \begin{array}{c}
      \WS{E;\Spec_1;\dots;\Spec_n}{\Spec_i}{\Spec'_{\sigma(i)}} 
                                  \textrm{ \ for } i=1..n \\
      \sigma : \{1\dots n\} \ra \{1\dots m\} \textrm{ \ injective}
    \end{array}
  }{
    \WS{E}{\sig{\Spec_1;\dots;\Spec_n}}{\sig{\Spec'_1;\dots;\Spec'_m}}
  }
}
\item [MSUB-FUN]
\inference{%       T_1 -> T_2 <: T_1' -> T_2'
  \frac{
    \WS{E}{T_1'}{T_1}~~~~~~~~~~\WS{E;\ModS{X}{T_1'}}{T_2}{T_2'}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WS{E}{\funsig{X}{T_1}{T_2}}{\funsig{X}{T_1'}{T_2'}}
  }
}
\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{itemize}
Specification subtyping rules:
\begin{itemize}
\item [ASSUM-ASSUM]
\inference{%
  \frac{
    \WTELECONV{}{U_1}{U_2}
  }{
    \WSE{\Assum{}{c}{U_1}}{\Assum{}{c}{U_2}}
  }
}
\item [DEF-ASSUM]
\inference{%
  \frac{
    \WTELECONV{}{U_1}{U_2}
  }{
    \WSE{\Def{}{c}{U_1}{t}}{\Assum{}{c}{U_2}}
  }
}
\item [ASSUM-DEF]
\inference{%
  \frac{
    \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{c}{t_2}
  }{
    \WSE{\Assum{}{c}{U_1}}{\Def{}{c}{U_2}{t_2}}
  }
}
\item [DEF-DEF]
\inference{%
  \frac{
    \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{t_1}{t_2}
  }{
    \WSE{\Def{}{c}{U_1}{t_1}}{\Def{}{c}{U_2}{t_2}}
  }
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\item [MODS-MODS]
\inference{%
  \frac{
    \WSE{T_1}{T_2}
  }{
    \WSE{\ModS{m}{T_1}}{\ModS{m}{T_2}}
  }
}
\item [MODEQ-MODS]
\inference{%
  \frac{
    \WSE{T_1}{T_2}
  }{
    \WSE{\ModSEq{m}{T_1}{p}}{\ModS{m}{T_2}}
  }
}
\item [MODS-MODEQ]
\inference{%
  \frac{
    \WSE{T_1}{T_2}~~~~~~~~\WTERED{}{m}{=}{p_2}
  }{
    \WSE{\ModS{m}{T_1}}{\ModSEq{m}{T_2}{p_2}}
  }
}
\item [MODEQ-MODEQ]
\inference{%
  \frac{
    \WSE{T_1}{T_2}~~~~~~~~\WTERED{}{p_1}{=}{p_2}
  }{
    \WSE{\ModSEq{m}{T_1}{p_1}}{\ModSEq{m}{T_2}{p_2}}
  }
}
\item [MODTYPE-MODTYPE]
\inference{%
  \frac{
    \WSE{T_1}{T_2}~~~~~~~~\WSE{T_2}{T_1}
  }{
    \WSE{\ModType{S}{T_1}}{\ModType{S}{T_2}}
  }
}
\end{itemize}
Verification of the specification
\begin{itemize}
\item [IMPL-SPEC]
\inference{%
  \frac{
    \begin{array}{c}
      \WF{E;\Spec}{}\\
      \Spec \textrm{\ is one of } {\sf Def, Assum, Ind, ModType}
    \end{array}
  }{
    \WTE{}{\Spec}{\Spec}
  }
}
\item [MOD-MODS]
\inference{%
  \frac{
    \WF{E;\ModS{m}{T}}{}~~~~~~~~\WTE{}{M}{T}
  }{
    \WTE{}{\Mod{m}{T}{M}}{\ModS{m}{T}}
  }
}
\item [MOD-MODEQ]
\inference{%
  \frac{
    \WF{E;\ModSEq{m}{T}{p}}{}~~~~~~~~~~~\WTERED{}{p}{=}{p'}
  }{
    \WTE{}{\Mod{m}{T}{p'}}{\ModSEq{m}{T}{p'}}
  }
}

\end{itemize}
New environment formation rules
\begin{itemize}
\item [WF-MODS]
\inference{%
  \frac{
    \WF{E}{}~~~~~~~~\WFT{E}{T}
  }{
    \WF{E;\ModS{m}{T}}{}
  }
}
\item [WF-MODEQ]
\inference{%
  \frac{
    \WF{E}{}~~~~~~~~~~~\WTE{}{p}{T}
  }{
    \WF{E,\ModSEq{m}{T}{p}}{}
  }
}
\item [WF-MODTYPE]
\inference{%
  \frac{
    \WF{E}{}~~~~~~~~~~~\WFT{E}{T}
  }{
    \WF{E,\ModType{S}{T}}{}
  }
}
\item [WF-IND]
\inference{%
  \frac{
    \begin{array}{c}
      \WF{E;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}{}\\
      \WT{E}{}{p:\sig{\Spec_1;\dots;\Spec_n;\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'};\dots}}\\
      \WS{E}{\subst{\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}{p.l}{l}_{l
      \in \lab{Spec_1;\dots;Spec_n}}}{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}
    \end{array}
  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}\\
  }
}
\end{itemize}
Component access rules
\begin{itemize}
\item [ACC-TYPE]
\inference{%
  \frac{
    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Assum{}{c}{U};\dots}}
  }{
    \WTEG{p.c}{\subst{U}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
  }
}
\item []
\inference{%
  \frac{
    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{U}{t};\dots}}
  }{
    \WTEG{p.c}{\subst{U}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
  }
}
\item[] Notice that the following rule extends the delta rule defined in
section~\ref{delta}
\item [ACC-DELTA]
\inference{%
  \frac{
    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{U}{t};\dots}}
  }{
    \WTEGRED{p.c}{\triangleright_\delta}{\subst{t}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
  }
}
\item [] 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}{\sig{\Spec_1;\dots;\Spec_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
  }{
    \WTEG{p.I_j}{\subst{(p_1:P_1)\ldots(p_r:P_r)A_j}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
  }
}
\inference{%
  \frac{
    \WTEG{p}{\sig{\Spec_1;\dots;\Spec_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
  }{
    \WTEG{p.c_m}{\subst{(p_1:P_1)\ldots(p_r:P_r)\subst{C_m}{I_j}{(I_j~p_1\ldots
       p_r)}_{j=1\ldots k}}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
  }
}
\item [ACC-INDP]
\inference{%
  \frac{
    \WT{E}{}{p:\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
  }{
    \WTRED{E}{}{p.I_i}{\triangleright_\delta}{p'.I_i}
  }
}
\inference{%
  \frac{
    \WT{E}{}{p:\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
  }{
    \WTRED{E}{}{p.c_i}{\triangleright_\delta}{p'.c_i}
  }
}
%%%%%%%%%%%%%%%%%%%%%%%%%%% MODULES
\item [ACC-MOD]
\inference{%
  \frac{
    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModS{m}{T};\dots}}
  }{
    \WTEG{p.m}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
  }
}
\item []
\inference{%
  \frac{
    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModSEq{m}{T}{p'};\dots}}
  }{
    \WTEG{p.m}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
  }
}
\item [ACC-MODEQ]
\inference{%
  \frac{
    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModSEq{m}{T}{p'};\dots}}
  }{
    \WTEGRED{p.m}{=}{\subst{p'}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
  }
}
\item [ACC-MODTYPE]
\inference{%
  \frac{
    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModType{S}{T};\dots}}
  }{
    \WTEGRED{p.S}{=}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
  }
}
\end{itemize}
The function $\lab{}$ is used to calculate the set of label of
the set of specifications. It is defined by
$\lab{\Spec_1;\dots;\Spec_n}=\lab{\Spec_1}\cup\dots;\cup\lab{\Spec_n}$
where $\lab{\Spec}$ is defined as follows:
\begin{itemize}
\item $\lab{\Assum{\Gamma}{c}{U}}=\{c\}$,
\item $\lab{\Def{\Gamma}{c}{U}{t}}=\{c\}$,
\item
  $\lab{\Ind{\Gamma}{\Gamma_P}{\Gamma_C}{\Gamma_I}}=\dom{\Gamma_C}\cup\dom{\Gamma_I}$,
\item $\lab{\ModS{m}{T}}=\{m\}$,
\item $\lab{\ModSEq{m}{T}{M}}=\{m\}$,
\item $\lab{\ModType{S}{T}}=\{S\}$
\end{itemize}
Environment access for modules and module types
\begin{itemize}
\item [ENV-MOD]
\inference{%
  \frac{
    \WF{E;\ModS{m}{T};E'}{\Gamma}
  }{
    \WT{E;\ModS{m}{T};E'}{\Gamma}{m}{T}
  }
}
\item []
\inference{%
  \frac{
    \WF{E;\ModSEq{m}{T}{p};E'}{\Gamma}
  }{
    \WT{E;\ModSEq{m}{T}{p};E'}{\Gamma}{m}{T}
  }
}
\item [ENV-MODEQ]
\inference{%
  \frac{
    \WF{E;\ModSEq{m}{T}{p};E'}{\Gamma}
  }{
    \WTRED{E;\ModSEq{m}{T}{p};E'}{\Gamma}{m}{=}{p}
  }
}
\item [ENV-MODTYPE]
\inference{%
  \frac{
    \WF{E;\ModType{S}{T};E'}{\Gamma}
  }{
    \WTRED{E;\ModType{S}{T};E'}{\Gamma}{S}{=}{T}
  }
}
\item [ENV-INDP]
\inference{%
  \frac{
    \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
  }{
    \WTRED{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}{I_i}{\triangleright_\delta}{p.I_i}
  }
}
\inference{%
  \frac{
    \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
  }{
    \WTRED{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}{c_i}{\triangleright_\delta}{p.c_i}
  }
}
\end{itemize}
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}


% $Id$

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