diff options
author | 2008-11-29 10:49:47 -0500 | |
---|---|---|
committer | 2008-11-29 10:49:47 -0500 | |
commit | 73de524554aaa11c454e95cec39e8ada98c44cf4 (patch) | |
tree | 54a2938d32a93c0890171865b2968fbb56044f87 /doc/manual.tex | |
parent | 6748925a8c158e84a40b2e8f0142eaea7691d2f6 (diff) |
Pattern typing
Diffstat (limited to 'doc/manual.tex')
-rw-r--r-- | doc/manual.tex | 40 |
1 files changed, 38 insertions, 2 deletions
diff --git a/doc/manual.tex b/doc/manual.tex index dec14cd2..db679405 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -243,7 +243,7 @@ Since there is significant mutual recursion among the judgments, we introduce th \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} \; (\lambda x \Rightarrow x) \; c \equiv c}{} $$\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 @@ $$\infer{\Gamma \vdash [c_1 \sim c_2] \Rightarrow e : [c_1 \sim c_2] \Rightarrow & \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 |