Mercurial > urweb
comparison doc/manual.tex @ 538:a9fba52dfce4
Module typing
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 29 Nov 2008 14:09:43 -0500 |
| parents | a4a7cd341a1b |
| children | e6b464e48c00 |
comparison
equal
deleted
inserted
replaced
| 537:a4a7cd341a1b | 538:a9fba52dfce4 |
|---|---|
| 763 \quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{class} \; x}{} | 763 \quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{class} \; x}{} |
| 764 \quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{class} \; x = c_2}{ | 764 \quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{class} \; x = c_2}{ |
| 765 \Gamma \vdash c_1 \equiv c_2 | 765 \Gamma \vdash c_1 \equiv c_2 |
| 766 }$$ | 766 }$$ |
| 767 | 767 |
| 768 \subsection{Module Typing} | |
| 769 | |
| 770 We use a helper function $\mt{sigOf}$, which converts declarations and sequences of declarations into their principal signature items and sequences of signature items, respectively. | |
| 771 | |
| 772 $$\infer{\Gamma \vdash M : S}{ | |
| 773 \Gamma \vdash M : S' | |
| 774 & \Gamma \vdash S' \leq S | |
| 775 } | |
| 776 \quad \infer{\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \mt{sigOf}(\overline{d}) \; \mt{end}}{ | |
| 777 \Gamma \vdash \overline{d} \leadsto \Gamma' | |
| 778 } | |
| 779 \quad \infer{\Gamma \vdash X : S}{ | |
| 780 X : S \in \Gamma | |
| 781 }$$ | |
| 782 | |
| 783 $$\infer{\Gamma \vdash M.X : S}{ | |
| 784 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} | |
| 785 & \mt{proj}(M, \overline{s}, \mt{structure} \; X) = S | |
| 786 }$$ | |
| 787 | |
| 788 $$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{ | |
| 789 \Gamma \vdash M_1 : \mt{functor}(X : S_1) : S_2 | |
| 790 & \Gamma \vdash M_2 : S_1 | |
| 791 } | |
| 792 \quad \infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 = M : \mt{functor} (X : S_1) : S_2}{ | |
| 793 \Gamma \vdash S_1 | |
| 794 & \Gamma, X : S_1 \vdash S_2 | |
| 795 & \Gamma, X : S_1 \vdash M : S_2 | |
| 796 }$$ | |
| 797 | |
| 798 \begin{eqnarray*} | |
| 799 \mt{sigOf}(\cdot) &=& \cdot \\ | |
| 800 \mt{sigOf}(s \; \overline{s'}) &=& \mt{sigOf}(s) \; \mt{sigOf}(\overline{s'}) \\ | |
| 801 \\ | |
| 802 \mt{sigOf}(\mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\ | |
| 803 \mt{sigOf}(\mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \overline{dc} \\ | |
| 804 \mt{sigOf}(\mt{datatype} \; x = \mt{datatype} \; M.z) &=& \mt{datatype} \; x = \mt{datatype} \; M.z \\ | |
| 805 \mt{sigOf}(\mt{val} \; x : \tau = e) &=& \mt{val} \; x : \tau \\ | |
| 806 \mt{sigOf}(\mt{val} \; \mt{rec} \; \overline{x : \tau = e}) &=& \overline{\mt{val} \; x : \tau} \\ | |
| 807 \mt{sigOf}(\mt{structure} \; X : S = M) &=& \mt{structure} \; X : S \\ | |
| 808 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\ | |
| 809 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\ | |
| 810 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\ | |
| 811 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\ | |
| 812 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\ | |
| 813 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\ | |
| 814 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\ | |
| 815 \mt{sigOf}(\mt{class} \; x = c) &=& \mt{class} \; x = c \\ | |
| 816 \end{eqnarray*} | |
| 817 | |
| 768 \end{document} | 818 \end{document} |