From 8f4d4c66134804bbf2d2fe65c893b68387272d31 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 10 Jul 2010 15:57:24 +0100 Subject: Remove non-DFSG contents --- doc/refman/RefMan-modr.tex | 565 --------------------------------------------- 1 file changed, 565 deletions(-) delete mode 100644 doc/refman/RefMan-modr.tex (limited to 'doc/refman/RefMan-modr.tex') diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex deleted file mode 100644 index b2ea232c..00000000 --- a/doc/refman/RefMan-modr.tex +++ /dev/null @@ -1,565 +0,0 @@ -\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} - - -% $Id: RefMan-modr.tex 11197 2008-07-01 13:05:41Z soubiran $ - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: - -- cgit v1.2.3