Mercurial > urweb
changeset 539:e6b464e48c00
selfify
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 29 Nov 2008 14:32:33 -0500 (2008-11-29) |
parents | a9fba52dfce4 |
children | 9eefa0cf3219 |
files | doc/manual.tex |
diffstat | 1 files changed, 24 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/doc/manual.tex Sat Nov 29 14:09:43 2008 -0500 +++ b/doc/manual.tex Sat Nov 29 14:32:33 2008 -0500 @@ -249,6 +249,7 @@ \item $\Gamma \vdash S \leq S$ is the signature compatibility judgment. We write $\Gamma \vdash S$ as shorthand for $\Gamma \vdash S \leq S$. \item $\Gamma \vdash M : S$ is the module signature checking judgment. \item $\mt{proj}(M, \overline{s}, V)$ is a partial function for projecting a signature item from $\overline{s}$, given the module $M$ that we project from. $V$ may be $\mt{con} \; x$, $\mt{datatype} \; x$, $\mt{val} \; x$, $\mt{signature} \; X$, or $\mt{structure} \; X$. The parameter $M$ is needed because the projected signature item may refer to other items from $\overline{s}$. +\item $\mt{selfify}(M, \overline{s})$ adds information to signature items $\overline{s}$ to reflect the fact that we are concerned with the particular module $M$. This function is overloaded to work over individual signature items as well. \end{itemize} \subsection{Kinding} @@ -563,8 +564,13 @@ $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{ \Gamma \vdash M : S + & \textrm{ ($M$ not a $\mt{struct} \; \ldots \; \mt{end}$)} } -\quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{ +\quad \infer{\Gamma \vdash \mt{structure} \; X : S = \mt{struct} \; \overline{d} \; \mt{end} \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{ + \Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \overline{s} \; \mt{end} +}$$ + +$$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{ \Gamma \vdash S }$$ @@ -815,4 +821,21 @@ \mt{sigOf}(\mt{class} \; x = c) &=& \mt{class} \; x = c \\ \end{eqnarray*} +\begin{eqnarray*} + \mt{selfify}(M, \cdot) &=& \cdot \\ + \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, \sigma, s) \; \mt{selfify}(M, \overline{s'}) \\ + \\ + \mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\ + \mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\ + \mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\ + \mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\ + \mt{selfify}(M, \mt{val} \; x : \tau) &=& \mt{val} \; x : \tau \\ + \mt{selfify}(M, \mt{structure} \; X : S) &=& \mt{structure} \; X : \mt{selfify}(M.X, \overline{s}) \textrm{ (where $\Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}$)} \\ + \mt{selfify}(M, \mt{signature} \; X = S) &=& \mt{signature} \; X = S \\ + \mt{selfify}(M, \mt{include} \; S) &=& \mt{include} \; S \\ + \mt{selfify}(M, \mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\ + \mt{selfify}(M, \mt{class} \; x) &=& \mt{class} \; x = M.x \\ + \mt{selfify}(M, \mt{class} \; x = c) &=& \mt{class} \; x = c \\ +\end{eqnarray*} + \end{document} \ No newline at end of file