From 702f7fd508257dcd7f5f1452dcb3815695648fbd Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 13 Mar 2018 15:51:55 +0100 Subject: [Sphinx] Move chapter 5 to new infrastructure --- Makefile.doc | 2 +- doc/refman/RefMan-modr.tex | 564 ---------------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/language/module-system.rst | 564 ++++++++++++++++++++++++++++++++++ 4 files changed, 565 insertions(+), 566 deletions(-) delete mode 100644 doc/refman/RefMan-modr.tex create mode 100644 doc/sphinx/language/module-system.rst 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/language/module-system.rst b/doc/sphinx/language/module-system.rst new file mode 100644 index 000000000..7c672cf42 --- /dev/null +++ b/doc/sphinx/language/module-system.rst @@ -0,0 +1,564 @@ +\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: + -- cgit v1.2.3