# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1227987153 18000
# Node ID e6b464e48c00f9d1c154671ddd000ed0b41607a4
# Parent  a9fba52dfce4ca672365ab883cf8962757e5e591
selfify

diff -r a9fba52dfce4 -r e6b464e48c00 doc/manual.tex
--- 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