diff options
| -rwxr-xr-x | doc/common/macros.tex | 18 | ||||
| -rw-r--r-- | doc/refman/RefMan-mod.tex | 35 | ||||
| -rw-r--r-- | doc/refman/RefMan-modr.tex | 432 | ||||
| -rw-r--r-- | kernel/modops.ml | 7 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | library/declaremods.ml | 8 |
6 files changed, 243 insertions, 259 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 3bfe09c16..47baa94a6 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -270,7 +270,6 @@ \newcommand{\T}{\texttt{T}} \newcommand{\U}{\texttt{U}} \newcommand{\real}{\textsf{Real}} -\newcommand{\Spec}{\textit{Spec}} \newcommand{\Data}{\textit{Data}} \newcommand{\In} {{\textbf{in }}} \newcommand{\AND} {{\textbf{and}}} @@ -356,6 +355,8 @@ \newcommand{\WFT}[2]{\ensuremath{#1[] \vdash {\cal W\!F}(#2)}} \newcommand{\WS}[3]{\ensuremath{#1[] \vdash #2 <: #3}} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} +\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} +\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WTRED}[5]{\mbox{$#1[#2] \vdash #3 #4 #5$}} \newcommand{\WTERED}[4]{\mbox{$E[#1] \vdash #2 #3 #4$}} @@ -404,14 +405,25 @@ \newcommand{\tristackrel}[3]{\mathrel{\mathop{#2}\limits_{#3}^{#1}}} \newcommand{\Impl}{{\it Impl}} +\newcommand{\elem}{{\it e}} \newcommand{\Mod}[3]{{\sf Mod}({#1}:{#2}:={#3})} +\newcommand{\ModS}[2]{{\sf Mod}({#1}:{#2})} \newcommand{\ModType}[2]{{\sf ModType}({#1}:={#2})} -\newcommand{\ModS}[2]{{\sf ModS}({#1}:{#2})} -\newcommand{\ModSEq}[3]{{\sf ModSEq}({#1}:{#2}=={#3})} +\newcommand{\ModA}[2]{{\sf ModA}({#1}=={#2})} \newcommand{\functor}[3]{\ensuremath{{\sf Functor}(#1:#2)\;#3}} \newcommand{\funsig}[3]{\ensuremath{{\sf Funsig}(#1:#2)\;#3}} \newcommand{\sig}[1]{\ensuremath{{\sf Sig}~#1~{\sf End}}} \newcommand{\struct}[1]{\ensuremath{{\sf Struct}~#1~{\sf End}}} +\newcommand{\structe}[1]{\ensuremath{ + {\sf Struct}~\elem_1;\ldots;\elem_i;#1;\elem_{i+2};\ldots + ;\elem_n~{\sf End}}} +\newcommand{\structes}[2]{\ensuremath{ + {\sf Struct}~\elem_1;\ldots;\elem_i;#1;\elem_{i+2}\{#2\} + ;\ldots;\elem_n\{#2\}~{\sf End}}} +\newcommand{\with}[3]{\ensuremath{#1~{\sf with}~#2 := #3}} + +\newcommand{\Spec}{{\it Spec}} +\newcommand{\ModSEq}[3]{{\sf Mod}({#1}:{#2}:={#3})} %\newbox\tempa diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index 34bc4095a..5efed7cef 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -8,12 +8,13 @@ together, as well as a mean of massive abstraction. \begin{figure}[t] \begin{centerframe} \begin{tabular}{rcl} -{\modtype} & ::= & {\ident} \\ - & $|$ & {\modtype} \texttt{ with Definition }{\ident} := {\term} \\ - & $|$ & {\modtype} \texttt{ with Module }{\ident} := {\qualid} \\ +{\modtype} & ::= & {\qualid.\ident} \\ + & $|$ & {\modtype} \texttt{ with Definition }{\qualid} := {\term} \\ + & $|$ & {\modtype} \texttt{ with Module }{\qualid} := {\qualid} \\ + & $|$ & {\qualid.\ident} \nelist{\qualid}{}\\ &&\\ -{\onemodbinding} & ::= & {\tt ( \nelist{\ident}{} : {\modtype} )}\\ +{\onemodbinding} & ::= & {\tt ( [Import|Export] \nelist{\ident}{} : {\modtype} )}\\ &&\\ {\modbindings} & ::= & \nelist{\onemodbinding}{}\\ @@ -61,7 +62,18 @@ This command is used to start an interactive module named {\ident}. the module. \end{Variants} +\subsubsection{Reserved commands inside an interactive module: +\comindex{Include}} +\begin{enumerate} +\item {\tt Include {\modexpr}} + Includes the content of {\modexpr} in the current interactive module. + +\item {\tt Include Type {\modtype}} + + Includes the content of {\modtype} in the current interactive module. + +\end{enumerate} \subsection{\tt End {\ident} \comindex{End}} @@ -123,7 +135,22 @@ This command is used to start an interactive module type {\ident}. Starts an interactive functor type with parameters given by {\modbindings}. \end{Variants} +\subsubsection{Reserved commands inside an interactive module type: +\comindex{Include}\comindex{Inline}} +\begin{enumerate} +\item {\tt Include {\modexpr}} + + Includes the content of {\modexpr} in the current interactive module type. + +\item {\tt Include Type {\modtype}} + + Includes the content of {\modtype} in the current interactive module type. + +\item {\tt {\declarationkeyword} Inline {\assums} } + + This declaration will be automatically unfolded at functor application. +\end{enumerate} \subsection{\tt End {\ident} \comindex{End}} diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex index 42dd12d60..b46a9fe25 100644 --- a/doc/refman/RefMan-modr.tex +++ b/doc/refman/RefMan-modr.tex @@ -11,43 +11,33 @@ a mean of massive abstraction. 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{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{Module expression.} It is denoted by $M$ and can be: +\paragraph{Structure expression.} It is denoted by $S$ 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''$ +\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{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 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 optionnaly a module implementation $S'$ + which can be any structure expression except a refined structure. -\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 alias,} is written $\ModA{X}{p}$ and + consists of a module variable $X$ and a module path $p$. -\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. +\paragraph{Module type abbreviation,} is written $\ModType{Y}{S}$, where +$Y$ is an identifier and $S$ is any structure expression . \section{Typing Modules} @@ -55,114 +45,174 @@ $S$ is a module type name and $T$ is a module type. 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 signature elements. +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}{T}, denoting that a module type $T$ is well-formed, +\item \WFT{E}{S}, denoting that a structure $S$ is well-formed, -\item \WTM{E}{M}{T}, denoting that a module expression $M$ has type $T$ in +\item \WTM{E}{p}{S}, denoting that the module pointed by $p$ has type $S$ in environment $E$. -\item \WTM{E}{\Impl}{\Spec}, denoting that an implementation $\Impl$ - verifies a specification $\Spec$ +\item \WEV{E}{S}{S'}, denoting that a structure $S$ is evaluated to +a structure $S'$. -\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}{S_1}{S_2}, denoting that a structure $S_1$ is a subtype of a +strucutre $S_2$. -\item \WS{E}{\Spec_1}{\Spec_2}, denoting that a specification - $\Spec_1$ is more precise that a specification $\Spec_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 module types are the following: +The rules for forming strucutres are the following: \begin{description} -\item[WF-SIG] +\item[WF-STR] \inference{% \frac{ \WF{E;E'}{} }{%%%%%%%%%%%%%%%%%%%%% - \WFT{E}{\sig{E'}} + \WFT{E}{\struct{E'}} } } \item[WF-FUN] \inference{% \frac{ - \WFT{E;\ModS{X}{T}}{T'} + \WFT{E;\ModS{X}{S}}{S'} }{%%%%%%%%%%%%%%%%%%%%%%%%%% - \WFT{E}{\funsig{X}{T}{T'}} + \WFT{E}{\functor{X}{S}{S'}} } } \end{description} -Rules for typing module expressions: +Evaluation of structures to weak head normal form: \begin{description} -\item[MT-STRUCT] +\item[WEVAL-APP] +\inference{% + \frac{ + \begin{array}{c} + \WEV{E}{S}{\functor{X}{S_1}{S_2}}\\ + \WTM{E}{p}{S_3}\qquad \WS{E}{S_3}{S_1} + \end{array} + }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \WEV{E}{S\,p}{S\{X/p\}} + } +} +\item[WEVAL-WITH-MOD] +\inference{% + \frac{ + \begin{array}{c} + \WEV{E}{S}{\structe{\ModS{X}{S_1}}}\\ + \WTM{E}{p}{S_2}\qquad \WS{E;\elem_1;\ldots;\elem_i}{S_2}{S_1} + \end{array} + }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \begin{array}{c} + \WEVT{E}{\with{S}{x}{p}}{\structes{\ModA{X}{p}}{X/p}} + \end{array} + } +} +\item[WEVAL-WITH-MOD-REC] \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 + \WEV{E}{S}{\structe{\ModS{X_1}{S_1}}}\\ + \WEV{E;\elem_1;\ldots;\elem_i}{\with{S_1}{p}{p_1}}{S_2} \end{array} }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \WTM{E}{\struct{\Impl_1;\dots;\Impl_n}}{\sig{\Spec_1;\dots;\Spec_n}} + \begin{array}{c} + \WEVT{E}{\with{S}{X_1.p}{p_1}}{\structes{\ModS{X}{S_2}}{X_1.p/p_1}} + \end{array} } } -\item[MT-FUN] +\item[WEVAL-WITH-DEF] \inference{% \frac{ - \WTM{E;\ModS{X}{T}}{M}{T'} + \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} }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \WTM{E}{\functor{X}{T}{M}}{\funsig{X}{T}{T'}} + \begin{array}{c} + \WEVT{E}{\with{S}{c}{t:T}}{\structe{\Def{}{c}{t}{T}}} + \end{array} } } -\item[MT-APP] +\item[WEVAL-WITH-DEF-REC] \inference{% \frac{ \begin{array}{c} - \WTM{E}{p}{\funsig{X_1}{T_1}{\!\dots\funsig{X_n}{T_n}{T'}}}\\ - \WTM{E}{p_i}{T_i\{X_1/p_1\dots X_{i-1}/p_{i-1}\}} - \textrm{ \ \ for } i=1\dots n + \WEV{E}{S}{\structe{\ModS{X_1}{S_1}}}\\ + \WEV{E;\elem_1;\ldots;\elem_i}{\with{S_1}{p}{p_1}}{S_2} \end{array} }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \WTM{E}{p\; p_1 \dots p_n}{T'\{X_1/p_1\dots X_n/p_n\}} + \begin{array}{c} + \WEVT{E}{\with{S}{X_1.p}{t:T}}{\structe{\ModS{X}{S_2}}} + \end{array} } } -\item[MT-SUB] + +\item[WEVAL-PATH-MOD] \inference{% \frac{ - \WTM{E}{M}{T}~~~~~~~~~~~~\WS{E}{T}{T'} + \WEV{E}{p}{\structe{{\sf Mod(X:S\left[:=S_1\right])}}} }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \WTM{E}{M}{T'} + \WEV{E}{p.X}{S} + } +} +\item[WEVAL-PATH-ALIAS] +\inference{% + \frac{ + \begin{array}{c} + \WEV{E}{p}{\structe{\ModA{X}{p_1}}}\\ + \WEV{E}{p_1}{S} + \end{array} + }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \WEV{E}{p.X}{S} + } +} +\item[WEVAL-PATH-TYPE] +\inference{% + \frac{ + \WEV{E}{p}{\structe{\ModType{Y}{S}}}\\ + }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \WEV{E}{p.Y}{S} + } +} +\end{description} + Rules for typing module: +\begin{description} +\item[MT-EVAL] +\inference{% + \frac{ + \WEV{E}{p}{S} + }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \WTM{E}{p}{S} } } \item[MT-STR] \inference{% \frac{ - \WTM{E}{p}{T} + \WTM{E}{p}{S} }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \WTM{E}{p}{T/p} + \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 $T/p$ has the following +manifestly equal to themselves. The notation $S/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 +\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}{U}{t}/p ~=~ \Def{}{c}{U}{t}$ + \item $\Def{}{c}{t}{T}/p ~=~ \Def{}{c}{t}{T}$ \item $\Assum{}{c}{U}/p ~=~ \Def{}{c}{p.c}{U}$ - \item $\ModS{X}{T}/p ~=~ \ModSEq{X}{T/p.X}{p.X}$ - \item $\ModSEq{X}{T}{p'}/p ~=~ \ModSEq{X}{T/p}{p'}$ + \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 $\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. +\item if $S\lra\funsig{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 @@ -170,28 +220,28 @@ 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 equality rules on inductive types and constructors. \\ The module subtyping rules: \begin{description} -\item[MSUB-SIG] +\item[MSUB-STR] \inference{% \frac{ \begin{array}{c} - \WS{E;\Spec_1;\dots;\Spec_n}{\Spec_{\sigma(i)}}{\Spec'_i} + \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}{\sig{\Spec_1;\dots;\Spec_n}}{\sig{\Spec'_1;\dots;\Spec'_m}} + \WS{E}{\struct{\elem_1;\dots;\elem_n}}{\sig{\elem'_1;\dots;\elem'_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}{S_1'}{S_1}~~~~~~~~~~\WS{E;\ModS{X}{S_1'}}{S_2}{S_2'} }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \WS{E}{\funsig{X}{T_1}{T_2}}{\funsig{X}{T_1'}{T_2'}} + \WS{E}{\functor{X}{S_1}{S_2}}{\functor{X}{S_1'}{S_2'}} } } % these are derived rules @@ -212,38 +262,38 @@ The module subtyping rules: % } % } \end{description} -Specification subtyping rules: +Structure element subtyping rules: \begin{description} \item[ASSUM-ASSUM] \inference{% \frac{ - \WTELECONV{}{U_1}{U_2} + \WTELECONV{}{T_1}{T_2} }{ - \WSE{\Assum{}{c}{U_1}}{\Assum{}{c}{U_2}} + \WSE{\Assum{}{c}{T_1}}{\Assum{}{c}{T_2}} } } \item[DEF-ASSUM] \inference{% \frac{ - \WTELECONV{}{U_1}{U_2} + \WTELECONV{}{T_1}{T_2} }{ - \WSE{\Def{}{c}{t}{U_1}}{\Assum{}{c}{U_2}} + \WSE{\Def{}{c}{t}{T_1}}{\Assum{}{c}{T_2}} } } \item[ASSUM-DEF] \inference{% \frac{ - \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{c}{t_2} + \WTELECONV{}{T_1}{T_2}~~~~~~~~\WTECONV{}{c}{t_2} }{ - \WSE{\Assum{}{c}{U_1}}{\Def{}{c}{t_2}{U_2}} + \WSE{\Assum{}{c}{T_1}}{\Def{}{c}{t_2}{T_2}} } } \item[DEF-DEF] \inference{% \frac{ - \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{t_1}{t_2} + \WTELECONV{}{T_1}{T_2}~~~~~~~~\WTECONV{}{t_1}{t_2} }{ - \WSE{\Def{}{c}{t_1}{U_1}}{\Def{}{c}{t_2}{U_2}} + \WSE{\Def{}{c}{t_1}{T_1}}{\Def{}{c}{t_2}{T_2}} } } \item[IND-IND] @@ -281,101 +331,84 @@ Specification subtyping rules: } } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\item[MODS-MODS] +\item[MOD-MOD] \inference{% \frac{ - \WSE{T_1}{T_2} + \WSE{S_1}{S_2} }{ - \WSE{\ModS{m}{T_1}}{\ModS{m}{T_2}} + \WSE{\ModS{X}{S_1}}{\ModS{X}{S_2}} } } -\item[MODEQ-MODS] +\item[ALIAS-MOD] \inference{% \frac{ - \WSE{T_1}{T_2} + \WTM{E}{p}{S_1}~~~~~~~~\WSE{S_1}{S_2} }{ - \WSE{\ModSEq{m}{T_1}{p}}{\ModS{m}{T_2}} + \WSE{\ModA{X}{p}}{\ModS{X}{S_2}} } } -\item[MODS-MODEQ] +\item[MOD-ALIAS] \inference{% \frac{ - \WSE{T_1}{T_2}~~~~~~~~\WTECONV{}{m}{p_2} + \WTM{E}{p}{S_2}~~~~~~~~ + \WSE{S_1}{S_2}~~~~~~~~\WTECONV{}{X}{p_2} }{ - \WSE{\ModS{m}{T_1}}{\ModSEq{m}{T_2}{p_2}} + \WSE{\ModS{X}{S_1}}{\ModA{X}{p}} } } -\item[MODEQ-MODEQ] +\item[ALIAS-ALIAS] \inference{% \frac{ - \WSE{T_1}{T_2}~~~~~~~~\WTECONV{}{p_1}{p_2} + \WTECONV{}{p_1}{p_2} }{ - \WSE{\ModSEq{m}{T_1}{p_1}}{\ModSEq{m}{T_2}{p_2}} + \WSE{\ModA{X}{p_1}}{\ModA{X}{p_2}} } } \item[MODTYPE-MODTYPE] \inference{% \frac{ - \WSE{T_1}{T_2}~~~~~~~~\WSE{T_2}{T_1} + \WSE{S_1}{S_2}~~~~~~~~\WSE{S_2}{S_1} }{ - \WSE{\ModType{S}{T_1}}{\ModType{S}{T_2}} + \WSE{\ModType{Y}{S_1}}{\ModType{Y}{S_2}} } } \end{description} -Verification of the specification +New environment formation rules \begin{description} -\item[IMPL-SPEC] +\item[WF-MOD] \inference{% \frac{ - \begin{array}{c} - \WF{E;\Spec}{}\\ - \Spec \textrm{\ is one of } {\sf Def, Assum, Ind, ModType} - \end{array} + \WF{E}{}~~~~~~~~\WFT{E}{S} }{ - \WTE{}{\Spec}{\Spec} + \WF{E;\ModS{X}{S}}{} } } -\item[MOD-MODS] +\item[WF-MOD] \inference{% \frac{ - \WF{E;\ModS{m}{T}}{}~~~~~~~~\WTE{}{M}{T} +\begin{array}{c} + \WS{E}{S_2}{S_1}\\ + \WF{E}{}~~~~~\WFT{E}{S_1}~~~~~\WFT{E}{S_2} +\end{array} }{ - \WTE{}{\Mod{m}{T}{M}}{\ModS{m}{T}} + \WF{E;\Mod{X}{S_1}{S_2}}{} } } -\item[MOD-MODEQ] -\inference{% - \frac{ - \WF{E;\ModSEq{m}{T}{p}}{}~~~~~~~~~~~\WTECONV{}{p}{p'} - }{ - \WTE{}{\Mod{m}{T}{p'}}{\ModSEq{m}{T}{p'}} - } -} -\end{description} -New environment formation rules -\begin{description} -\item[WF-MODS] -\inference{% - \frac{ - \WF{E}{}~~~~~~~~\WFT{E}{T} - }{ - \WF{E;\ModS{m}{T}}{} - } -} -\item[WF-MODEQ] + +\item[WF-ALIAS] \inference{% \frac{ - \WF{E}{}~~~~~~~~~~~\WTE{}{p}{T} + \WF{E}{}~~~~~~~~~~~\WTE{}{p}{S} }{ - \WF{E,\ModSEq{m}{T}{p}}{} + \WF{E,\ModA{X}{p}}{} } } \item[WF-MODTYPE] \inference{% \frac{ - \WF{E}{}~~~~~~~~~~~\WFT{E}{T} + \WF{E}{}~~~~~~~~~~~\WFT{E}{S} }{ - \WF{E,\ModType{S}{T}}{} + \WF{E,\ModType{Y}{S}}{} } } \item[WF-IND] @@ -383,9 +416,8 @@ New environment formation rules \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}} + \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}}{} @@ -397,17 +429,17 @@ Component access rules \item[ACC-TYPE] \inference{% \frac{ - \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Assum{}{c}{U};\dots}} + \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Assum{}{c}{T};\dots}} }{ - \WTEG{p.c}{\subst{U}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}} + \WTEG{p.c}{T} } } \\ \inference{% \frac{ - \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{t}{U};\dots}} + \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Def{}{c}{t}{T};\dots}} }{ - \WTEG{p.c}{\subst{U}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}} + \WTEG{p.c}{T} } } \item[ACC-DELTA] @@ -415,9 +447,9 @@ Notice that the following rule extends the delta rule defined in section~\ref{delta} \inference{% \frac{ - \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{t}{U};\dots}} + \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Def{}{c}{t}{U};\dots}} }{ - \WTEGRED{p.c}{\triangleright_\delta}{\subst{t}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}} + \WTEGRED{p.c}{\triangleright_\delta}{t} } } \\ @@ -427,131 +459,37 @@ In the rules below we assume $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$, \item[ACC-IND] \inference{% \frac{ - \WTEG{p}{\sig{\Spec_1;\dots;\Spec_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}} + \WTEG{p}{\struct{\elem_1;\dots;\elem_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}}} + \WTEG{p.I_j}{(p_1:P_1)\ldots(p_r:P_r)A_j} } } \inference{% \frac{ - \WTEG{p}{\sig{\Spec_1;\dots;\Spec_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}} + \WTEG{p}{\struct{\elem_1;\dots;\elem_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}}} + \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}{\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}} + \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}{\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}} + \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} } } -%%%%%%%%%%%%%%%%%%%%%%%%%%% 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}}} - } -} -\\ -\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}{\triangleright_\delta}{\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}{\triangleright_\delta}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}} - } -} -\end{description} -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}{t}{U}}=\{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{description} -\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}{\triangleright_\delta}{p} - } -} -\item[ENV-MODTYPE] -\inference{% - \frac{ - \WF{E;\ModType{S}{T};E'}{\Gamma} - }{ - \WTRED{E;\ModType{S}{T};E'}{\Gamma}{S}{\triangleright_\delta}{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{description} + % %%% replaced by \triangle_\delta % Module path equality is a transitive and reflexive closure of the % relation generated by ACC-MODEQ and ENV-MODEQ. diff --git a/kernel/modops.ml b/kernel/modops.ml index 8d74c4c30..4d0af4fee 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -258,8 +258,11 @@ let rec eval_struct env = function let mp = scrape_alias mp env in let sub_alias = (lookup_modtype mp env).typ_alias in let sub_alias = match eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias - | _ -> sub_alias in + | SEBstruct (msid,sign) -> + join_alias + (subst_key (map_msid msid mp) sub_alias) + (map_msid msid mp) + | _ -> sub_alias in let sub_alias = update_subst_alias sub_alias (map_mbid farg_id mp (None)) in let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a895e68ce..2fffa0922 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -287,8 +287,8 @@ let add_module l me senv = check_label l senv.labset; let mb = translate_module senv.env me in let mp = MPdot(senv.modinfo.modpath, l) in - let is_functor,sub = Modops.update_subst senv.env mb mp in let env' = full_add_module mp mb senv.env in + let is_functor,sub = Modops.update_subst senv.env mb mp in mp, { old = senv.old; env = env'; modinfo = diff --git a/library/declaremods.ml b/library/declaremods.ml index bc1fa6f24..14851eced 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -560,7 +560,9 @@ let rec get_modtype_substobjs env = function let mp = Environ.scrape_alias mp env in let sub_alias = (Environ.lookup_modtype mp env).typ_alias in let sub_alias = match Modops.eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias + | SEBstruct (msid,sign) -> join_alias + (subst_key (map_msid msid mp) sub_alias) + (map_msid msid mp) | _ -> sub_alias in let sub_alias = join_alias sub_alias (map_mbid farg_id mp None) in let sub_alias = update_subst_alias sub_alias @@ -866,7 +868,9 @@ let rec get_module_substobjs env = function let mp = Environ.scrape_alias mp env in let sub_alias = (Environ.lookup_modtype mp env).typ_alias in let sub_alias = match Modops.eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias + | SEBstruct (msid,sign) -> join_alias + (subst_key (map_msid msid mp) sub_alias) + (map_msid msid mp) | _ -> sub_alias in let sub_alias = join_alias sub_alias (map_mbid farg_id mp None) in let sub_alias = update_subst_alias sub_alias |