diff options
| -rw-r--r-- | Makefile.doc | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-modr.tex | 564 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 1 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/language/module-system.rst | 459 |
5 files changed, 461 insertions, 566 deletions
diff --git a/Makefile.doc b/Makefile.doc index 10e8522d8..6dfbade48 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -71,7 +71,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ RefMan-com.tex \ - RefMan-uti.tex RefMan-ide.tex RefMan-modr.tex \ + RefMan-uti.tex RefMan-ide.tex \ AsyncProofs.tex RefMan-ssr.tex) \ $(REFMANCOQTEXFILES) \ diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex deleted file mode 100644 index 7c672cf42..000000000 --- a/doc/refman/RefMan-modr.tex +++ /dev/null @@ -1,564 +0,0 @@ -\chapter[The Module System]{The Module System\label{chapter:Modules}} -%HEVEA\cutname{modules.html} - -The module system extends the Calculus of Inductive Constructions -providing a convenient way to structure large developments as well as -a means 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: - diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index ec36304a6..0c4c6776f 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -96,7 +96,6 @@ Options A and B of the licence are {\em not} elected.} %END LATEX \include{RefMan-gal.v}% Gallina \include{RefMan-lib.v}% The coq library -\include{RefMan-modr}% The module system \part{The proof engine} diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index 928ea85be..a83312d33 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -18,6 +18,7 @@ Table of contents language/gallina-extensions language/cic + language/module-system .. toctree:: :caption: The proof engine diff --git a/doc/sphinx/language/module-system.rst b/doc/sphinx/language/module-system.rst new file mode 100644 index 000000000..e6a673665 --- /dev/null +++ b/doc/sphinx/language/module-system.rst @@ -0,0 +1,459 @@ +.. include:: ../preamble.rst +.. include:: ../replaces.rst + +.. _themodulesystem: + +The Module System +================= + +The module system extends the Calculus of Inductive Constructions +providing a convenient way to structure large developments as well as +a means of massive abstraction. + + +Modules and module types +---------------------------- + +**Access path.** An access path is denoted by :math:`p` and can be +either a module variable :math:`X` or, if :math:`p′` is an access path +and :math:`id` an identifier, then :math:`p′.id` is an access path. + + +**Structure element.** A structure element is denoted by :math:`e` and +is either a definition of a constant, an assumption, a definition of +an inductive, a definition of a module, an alias of a module or a module +type abbreviation. + + +**Structure expression.** A structure expression is denoted by :math:`S` and can be: + ++ an access path :math:`p` ++ a plain structure :math:`\Struct~e ; … ; e~\End` ++ a functor :math:`\Functor(X:S)~S′`, where :math:`X` is a module variable, :math:`S` and :math:`S′` are + structure expressions ++ an application :math:`S~p`, where :math:`S` is a structure expression and :math:`p` an + access path ++ a refined structure :math:`S~\with~p := p`′ or :math:`S~\with~p := t:T` where :math:`S` is a + structure expression, :math:`p` and :math:`p′` are access paths, :math:`t` is a term and :math:`T` is + the type of :math:`t`. + +**Module definition.** A module definition is written :math:`\Mod{X}{S}{S'}` +and consists of a module variable :math:`X`, a module type +:math:`S` which can be any structure expression and optionally a +module implementation :math:`S′` which can be any structure expression +except a refined structure. + + +**Module alias.** A module alias is written :math:`\ModA{X}{p}` +and consists of a module variable :math:`X` and a module path +:math:`p`. + +**Module type abbreviation.** +A module type abbreviation is written :math:`\ModType{Y}{S}`, +where :math:`Y` is an identifier and :math:`S` is any structure +expression . + + +Typing Modules +------------------ + +In order to introduce the typing system we first slightly extend the syntactic +class of terms and environments given in section :ref:`The-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: + + ++ :math:`\WFT{E}{S}`, denoting that a structure :math:`S` is well-formed, ++ :math:`\WTM{E}{p}{S}`, denoting that the module pointed by :math:`p` has type :math:`S` in + environment :math:`E`. ++ :math:`\WEV{E}{S}{\ovl{S}}`, denoting that a structure :math:`S` is evaluated to a + structure :math:`S` in weak head normal form. ++ :math:`\WS{E}{S_1}{S_2}` , denoting that a structure :math:`S_1` is a subtype of a + structure :math:`S_2`. ++ :math:`\WS{E}{e_1}{e_2}` , denoting that a structure element e_1 is more + precise than a structure element e_2. + +The rules for forming structures are the following: + +.. inference:: WF-STR + + \WF{E;E′}{} + ------------------------ + \WFT{E}{ \Struct~E′ ~\End} + +.. inference:: WF-FUN + + \WFT{E; \ModS{X}{S}}{ \ovl{S′} } + -------------------------- + \WFT{E}{ \Functor(X:S)~S′} + + +Evaluation of structures to weak head normal form: + +.. inference:: WEVAL-APP + + \begin{array}{c} + \WEV{E}{S}{\Functor(X:S_1 )~S_2}~~~~~\WEV{E}{S_1}{\ovl{S_1}} \\ + \WTM{E}{p}{S_3}~~~~~ \WS{E}{S_3}{\ovl{S_1}} + \end{array} + -------------------------- + \WEV{E}{S~p}{S_2 \{p/X,t_1 /p_1 .c_1 ,…,t_n /p_n.c_n \}} + + +In the last rule, :math:`\{t_1 /p_1 .c_1 ,…,t_n /p_n .c_n \}` is the resulting +substitution from the inlining mechanism. We substitute in :math:`S` the +inlined fields :math:`p_i .c_i` from :math:`\ModS{X}{S_1 }` by the corresponding delta- +reduced term :math:`t_i` in :math:`p`. + +.. inference:: WEVAL-WITH-MOD + + \begin{array}{c} + E[] ⊢ S \lra \Struct~e_1 ;…;e_i ; \ModS{X}{S_1 };e_{i+2} ;… ;e_n ~\End \\ + E;e_1 ;…;e_i [] ⊢ S_1 \lra \ovl{S_1} ~~~~~~ + E[] ⊢ p : S_2 \\ + E;e_1 ;…;e_i [] ⊢ S_2 <: \ovl{S_1} + \end{array} + ---------------------------------- + \begin{array}{c} + \WEV{E}{S~\with~x := p}{}\\ + \Struct~e_1 ;…;e_i ; \ModA{X}{p};e_{i+2} \{p/X\} ;…;e_n \{p/X\} ~\End + \end{array} + +.. inference:: WEVAL-WITH-MOD-REC + + \begin{array}{c} + \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1}{S_1 };e_{i+2} ;… ;e_n ~\End} \\ + \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}} + \end{array} + -------------------------- + \begin{array}{c} + \WEV{E}{S~\with~X_1.p := p_1}{} \\ + \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2}};e_{i+2} \{p_1 /X_1.p\} ;…;e_n \{p_1 /X_1.p\} ~\End + \end{array} + +.. inference:: WEVAL-WITH-DEF + + \begin{array}{c} + \WEV{E}{S}{\Struct~e_1 ;…;e_i ;\Assum{}{c}{T_1};e_{i+2} ;… ;e_n ~\End} \\ + \WS{E;e_1 ;…;e_i }{Def()(c:=t:T)}{\Assum{}{c}{T_1}} + \end{array} + -------------------------- + \begin{array}{c} + \WEV{E}{S~\with~c := t:T}{} \\ + \Struct~e_1 ;…;e_i ;Def()(c:=t:T);e_{i+2} ;… ;e_n ~\End + \end{array} + +.. inference:: WEVAL-WITH-DEF-REC + + \begin{array}{c} + \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1 }{S_1 };e_{i+2} ;… ;e_n ~\End} \\ + \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}} + \end{array} + -------------------------- + \begin{array}{c} + \WEV{E}{S~\with~X_1.p := t:T}{} \\ + \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2} };e_{i+2} ;… ;e_n ~\End + \end{array} + +.. inference:: WEVAL-PATH-MOD1 + + \begin{array}{c} + \WEV{E}{p}{\Struct~e_1 ;…;e_i ; \Mod{X}{S}{S_1};e_{i+2} ;… ;e_n End} \\ + \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}} + \end{array} + -------------------------- + E[] ⊢ p.X \lra \ovl{S} + +.. inference:: WEVAL-PATH-MOD2 + + \WF{E}{} + \Mod{X}{S}{S_1}∈ E + \WEV{E}{S}{\ovl{S}} + -------------------------- + \WEV{E}{X}{\ovl{S}} + +.. inference:: WEVAL-PATH-ALIAS1 + + \begin{array}{c} + \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModA{X}{p_1};e_{i+2} ;… ;e_n End} \\ + \WEV{E;e_1 ;…;e_i }{p_1}{\ovl{S}} + \end{array} + -------------------------- + \WEV{E}{p.X}{\ovl{S}} + +.. inference:: WEVAL-PATH-ALIAS2 + + \WF{E}{} + \ModA{X}{p_1 }∈ E + \WEV{E}{p_1}{\ovl{S}} + -------------------------- + \WEV{E}{X}{\ovl{S}} + +.. inference:: WEVAL-PATH-TYPE1 + + \begin{array}{c} + \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModType{Y}{S};e_{i+2} ;… ;e_n End} \\ + \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}} + \end{array} + -------------------------- + \WEV{E}{p.Y}{\ovl{S}} + +.. inference:: WEVAL-PATH-TYPE2 + + \WF{E}{} + \ModType{Y}{S}∈ E + \WEV{E}{S}{\ovl{S}} + -------------------------- + \WEV{E}{Y}{\ovl{S}} + + +Rules for typing module: + +.. inference:: MT-EVAL + + \WEV{E}{p}{\ovl{S}} + -------------------------- + E[] ⊢ p : \ovl{S} + +.. inference:: MT-STR + + E[] ⊢ p : S + -------------------------- + E[] ⊢ p : S/p + + +The last rule, called strengthening is used to make all module fields +manifestly equal to themselves. The notation :math:`S/p` has the following +meaning: + + ++ if :math:`S\lra~\Struct~e_1 ;…;e_n ~\End` then :math:`S/p=~\Struct~e_1 /p;…;e_n /p ~\End` + where :math:`e/p` is defined as follows (note that opaque definitions are processed + as assumptions): + + + :math:`\Def{}{c}{t}{T}/p = \Def{}{c}{t}{T}` + + :math:`\Assum{}{c}{U}/p = \Def{}{c}{p.c}{U}` + + :math:`\ModS{X}{S}/p = \ModA{X}{p.X}` + + :math:`\ModA{X}{p′}/p = \ModA{X}{p′}` + + :math:`\Ind{}{Γ_P}{Γ_C}{Γ_I}/p = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` + + :math:`\Indpstr{}{Γ_P}{Γ_C}{Γ_I}{p'}{p} = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'}` + ++ if :math:`S \lra \Functor(X:S′)~S″` then :math:`S/p=S` + + +The notation :math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` +denotes an inductive definition that is definitionally equal to the +inductive definition in the module denoted by the path :math:`p`. All rules +which have :math:`\Ind{}{Γ_P}{Γ_C}{Γ_I}` as premises are also valid for +:math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}`. We give the formation rule for +:math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` +below as well as the equality rules on inductive types and +constructors. + +The module subtyping rules: + +.. inference:: MSUB-STR + + \begin{array}{c} + \WS{E;e_1 ;…;e_n }{e_{σ(i)}}{e'_i ~\for~ i=1..m} \\ + σ : \{1… m\} → \{1… n\} ~\injective + \end{array} + -------------------------- + \WS{E}{\Struct~e_1 ;…;e_n ~\End}{~\Struct~e'_1 ;…;e'_m ~\End} + +.. inference:: MSUB-FUN + + \WS{E}{\ovl{S_1'}}{\ovl{S_1}} + \WS{E; \ModS{X}{S_1'}}{\ovl{S_2}}{\ovl{S_2'}} + -------------------------- + E[] ⊢ \Functor(X:S_1 ) S_2 <: \Functor(X:S_1') S_2' + + +Structure element subtyping rules: + +.. inference:: ASSUM-ASSUM + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + -------------------------- + \WS{E}{\Assum{}{c}{T_1 }}{\Assum{}{c}{T_2 }} + +.. inference:: DEF-ASSUM + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + -------------------------- + \WS{E}{\Def{}{c}{t}{T_1 }}{\Assum{}{c}{T_2 }} + +.. inference:: ASSUM-DEF + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + E[] ⊢ c =_{βδιζη} t_2 + -------------------------- + \WS{E}{\Assum{}{c}{T_1 }}{\Def{}{c}{t_2 }{T_2 }} + +.. inference:: DEF-DEF + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + E[] ⊢ t_1 =_{βδιζη} t_2 + -------------------------- + \WS{E}{\Def{}{c}{t_1 }{T_1 }}{\Def{}{c}{t_2 }{T_2 }} + +.. inference:: IND-IND + + E[] ⊢ Γ_P =_{βδιζη} Γ_P' + E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' + E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' + -------------------------- + \WS{E}{\ind{Γ_P}{Γ_C}{Γ_I}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}} + +.. inference:: INDP-IND + + E[] ⊢ Γ_P =_{βδιζη} Γ_P' + E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' + E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' + -------------------------- + \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}} + +.. inference:: INDP-INDP + + \begin{array}{c} + E[] ⊢ Γ_P =_{βδιζη} Γ_P' + E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' \\ + E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' + E[] ⊢ p =_{βδιζη} p' + \end{array} + -------------------------- + \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\Indp{}{Γ_P'}{Γ_C'}{Γ_I'}{p'}} + +.. inference:: MOD-MOD + + \WS{E}{S_1}{S_2} + -------------------------- + \WS{E}{\ModS{X}{S_1 }}{\ModS{X}{S_2 }} + +.. inference:: ALIAS-MOD + + E[] ⊢ p : S_1 + \WS{E}{S_1}{S_2} + -------------------------- + \WS{E}{\ModA{X}{p}}{\ModS{X}{S_2 }} + +.. inference:: MOD-ALIAS + + E[] ⊢ p : S_2 + \WS{E}{S_1}{S_2} + E[] ⊢ X =_{βδιζη} p + -------------------------- + \WS{E}{\ModS{X}{S_1 }}{\ModA{X}{p}} + +.. inference:: ALIAS-ALIAS + + E[] ⊢ p_1 =_{βδιζη} p_2 + -------------------------- + \WS{E}{\ModA{X}{p_1 }}{\ModA{X}{p_2 }} + +.. inference:: MODTYPE-MODTYPE + + \WS{E}{S_1}{S_2} + \WS{E}{S_2}{S_1} + -------------------------- + \WS{E}{\ModType{Y}{S_1 }}{\ModType{Y}{S_2 }} + + +New environment formation rules + + +.. inference:: WF-MOD1 + + \WF{E}{} + \WFT{E}{S} + -------------------------- + WF(E; \ModS{X}{S})[] + +.. inference:: WF-MOD2 + + \WS{E}{S_2}{S_1} + \WF{E}{} + \WFT{E}{S_1} + \WFT{E}{S_2} + -------------------------- + \WF{E; \Mod{X}{S_1}{S_2}}{} + +.. inference:: WF-ALIAS + + \WF{E}{} + E[] ⊢ p : S + -------------------------- + \WF{E, \ModA{X}{p}}{} + +.. inference:: WF-MODTYPE + + \WF{E}{} + \WFT{E}{S} + -------------------------- + \WF{E, \ModType{Y}{S}}{} + +.. inference:: WF-IND + + \begin{array}{c} + \WF{E;\ind{Γ_P}{Γ_C}{Γ_I}}{} \\ + E[] ⊢ p:~\Struct~e_1 ;…;e_n ;\ind{Γ_P'}{Γ_C'}{Γ_I'};… ~\End : \\ + E[] ⊢ \ind{Γ_P'}{Γ_C'}{Γ_I'} <: \ind{Γ_P}{Γ_C}{Γ_I} + \end{array} + -------------------------- + \WF{E; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p} }{} + + +Component access rules + + +.. inference:: ACC-TYPE1 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Assum{}{c}{T};… ~\End + -------------------------- + E[Γ] ⊢ p.c : T + +.. inference:: ACC-TYPE2 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Def{}{c}{t}{T};… ~\End + -------------------------- + E[Γ] ⊢ p.c : T + +Notice that the following rule extends the delta rule defined in section :ref:`Conversion-rules` + +.. inference:: ACC-DELTA + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Def{}{c}{t}{U};… ~\End + -------------------------- + E[Γ] ⊢ p.c \triangleright_δ t + +In the rules below we assume +:math:`Γ_P` is :math:`[p_1 :P_1 ;…;p_r :P_r ]`, +:math:`Γ_I` is :math:`[I_1 :A_1 ;…;I_k :A_k ]`, +and :math:`Γ_C` is :math:`[c_1 :C_1 ;…;c_n :C_n ]`. + +.. inference:: ACC-IND1 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{Γ_P}{Γ_C}{Γ_I};… ~\End + -------------------------- + E[Γ] ⊢ p.I_j : (p_1 :P_1 )…(p_r :P_r )A_j + +.. inference:: ACC-IND2 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{Γ_P}{Γ_C}{Γ_I};… ~\End + -------------------------- + E[Γ] ⊢ p.c_m : (p_1 :P_1 )…(p_r :P_r )C_m I_j (I_j~p_1 …p_r )_{j=1… k} + +.. inference:: ACC-INDP1 + + E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~\End + -------------------------- + E[] ⊢ p.I_i \triangleright_δ p'.I_i + +.. inference:: ACC-INDP2 + + E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~\End + -------------------------- + E[] ⊢ p.c_i \triangleright_δ p'.c_i |