# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1227973787 18000
# Node ID 65c253a9ca92fd699fc44724b2d888678637e8e6
# Parent  419f51b1e68d18547607cb504b037e04eaa44a28
Pattern typing

diff -r 419f51b1e68d -r 65c253a9ca92 doc/manual.tex
--- a/doc/manual.tex	Sat Nov 29 10:34:56 2008 -0500
+++ b/doc/manual.tex	Sat Nov 29 10:49:47 2008 -0500
@@ -243,7 +243,7 @@
 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
 \item $\Gamma \vdash c \equiv c$ proves the computational equivalence of two constructors.  This is often called a \emph{definitional equality} in the world of type theory.
 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
-\item $\Gamma \vdash p \leadsto \Gamma, \tau$ combines typing of patterns with calculation of which new variables they bind.
+\item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind.
 \item $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context.  We overload this judgment to apply to sequences of declarations.
 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
 \item $\mt{proj}(M, S, V)$ is a partial function for projecting a signature item from a signature $S$, given the module $M$ that we project from.  $V$ may be $\mt{con} \; 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 of $S$.
@@ -397,7 +397,7 @@
 
 $$\infer{\Gamma \vdash \mt{map} \; f \; (c_1 \rc c_2) \equiv \mt{map} \; f \; c_1 \rc \mt{map} \; f \; c_2}{}$$
 
-\subsection{Typing}
+\subsection{Expression Typing}
 
 We assume the existence of a function $T$ assigning types to literal constants.  It maps integer constants to $\mt{Basis}.\mt{int}$, float constants to $\mt{Basis}.\mt{float}$, and string constants to $\mt{Basis}.\mt{string}$.
 
@@ -485,4 +485,40 @@
   & \Gamma, c_1 \sim c_2 \vdash e : \tau
 }$$
 
+\subsection{Pattern Typing}
+
+$$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{}
+\quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{}
+\quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$
+
+$$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
+  X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma
+  & \textrm{$\tau$ not a function type}
+}
+\quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
+  X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma
+  & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
+}$$
+
+$$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
+  \Gamma \vdash M : S
+  & \mt{proj}(M, S, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau
+  & \textrm{$\tau$ not a function type}
+}$$
+
+$$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
+  \Gamma \vdash M : S
+  & \mt{proj}(M, S, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
+  & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
+}$$
+
+$$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
+  \Gamma_0 = \Gamma
+  & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
+}
+\quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
+  \Gamma_0 = \Gamma
+  & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
+}$$
+
 \end{document}
\ No newline at end of file