Mercurial > urweb

comparison doc/manual.tex @ 539:e6b464e48c00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
selfify
author Adam Chlipala <adamc@hcoop.net>
date Sat, 29 Nov 2008 14:32:33 -0500
parents a9fba52dfce4
children 9eefa0cf3219
comparison
equal deleted inserted replaced
538:a9fba52dfce4 539:e6b464e48c00
247 \item $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context. We overload this judgment to apply to sequences of declarations, as well as to signature items and sequences of signature items. 247 \item $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context. We overload this judgment to apply to sequences of declarations, as well as to signature items and sequences of signature items.
248 \item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment. 248 \item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment.
249 \item $\Gamma \vdash S \leq S$ is the signature compatibility judgment. We write $\Gamma \vdash S$ as shorthand for $\Gamma \vdash S \leq S$. 249 \item $\Gamma \vdash S \leq S$ is the signature compatibility judgment. We write $\Gamma \vdash S$ as shorthand for $\Gamma \vdash S \leq S$.
250 \item $\Gamma \vdash M : S$ is the module signature checking judgment. 250 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
251 \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}$. 251 \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}$.
252 \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.
252 \end{itemize} 253 \end{itemize}
253 254
254 \subsection{Kinding} 255 \subsection{Kinding}
255 256
256 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{ 257 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
561 & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s} 562 & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s}
562 }$$ 563 }$$
563 564
564 $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{ 565 $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{
565 \Gamma \vdash M : S 566 \Gamma \vdash M : S
566 } 567 & \textrm{ ($M$ not a $\mt{struct} \; \ldots \; \mt{end}$)}
567 \quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{ 568 }
569 \quad \infer{\Gamma \vdash \mt{structure} \; X : S = \mt{struct} \; \overline{d} \; \mt{end} \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{
570 \Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \overline{s} \; \mt{end}
571 }$$
572
573 $$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
568 \Gamma \vdash S 574 \Gamma \vdash S
569 }$$ 575 }$$
570 576
571 $$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{ 577 $$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{
572 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} 578 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
813 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\ 819 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
814 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\ 820 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
815 \mt{sigOf}(\mt{class} \; x = c) &=& \mt{class} \; x = c \\ 821 \mt{sigOf}(\mt{class} \; x = c) &=& \mt{class} \; x = c \\
816 \end{eqnarray*} 822 \end{eqnarray*}
817 823
824 \begin{eqnarray*}
825 \mt{selfify}(M, \cdot) &=& \cdot \\
826 \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, \sigma, s) \; \mt{selfify}(M, \overline{s'}) \\
827 \\
828 \mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\
829 \mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
830 \mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\
831 \mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\
832 \mt{selfify}(M, \mt{val} \; x : \tau) &=& \mt{val} \; x : \tau \\
833 \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}$)} \\
834 \mt{selfify}(M, \mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
835 \mt{selfify}(M, \mt{include} \; S) &=& \mt{include} \; S \\
836 \mt{selfify}(M, \mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
837 \mt{selfify}(M, \mt{class} \; x) &=& \mt{class} \; x = M.x \\
838 \mt{selfify}(M, \mt{class} \; x = c) &=& \mt{class} \; x = c \\
839 \end{eqnarray*}
840
818 \end{document} 841 \end{document}