Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /papers/modulespaper/design/figs/fig-statsem.tex
ViewVC logotype

Annotation of /papers/modulespaper/design/figs/fig-statsem.tex

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3564 - (view) (download) (as text)

1 : dbm 3564 %!TEX root = ../principles.tex
2 :     \begin{figure}
3 :     \centering
4 :     \fixedCodeFrame{
5 :     \small
6 :     \[
7 :     \setlength{\tabcolsep}{0ex}
8 :     \renewcommand{\arraystretch}{1.1}
9 :     \begin{array}{ll}
10 :     \infer[\rlabel{local}]{\begin{array}{l}\Gamma\vdash\local~\overline{d_1}~\inx~\overline{d_2}~\en\\
11 :     \Rightarrow(\underline{\local}~\underline{\overline{d_1}}~\inx~\underline{\overline{d_2}}~\en,entdec,\Gamma_2,\Delta)\end{array}}
12 :     {\Gamma\vdash\overline{d_1}\Rightarrow(\underline{\overline{d_1}},entdec_1,\Gamma_1,\Delta_1)\\
13 :     \Gamma\oplus\Gamma_1\vdash\overline{d_2}\Rightarrow(\underline{\overline{d_2}},entdec_2,\Gamma_2,\Delta_2)}
14 :     \\
15 :     \qquad
16 :     \\
17 :     \infer[\rlabel{type}]{\Gamma\vdash\type~\overline{\alpha}~t=\tau\Rightarrow(,entdec,\Gamma,\Delta)}
18 :     {\strut}
19 :     \\
20 :     \qquad
21 :     \\
22 :     \infer[\rlabel{sig}]{\Gamma\vdash\sig{\overline{spec}}\Rightarrow(\sig{\overline{spec}},\bullet,\Gamma',\emptyset)}{\strut}
23 :     \\
24 :     \qquad
25 :     \\
26 :     \infer[\rlabel{structure}]{\Gamma\vdash\struct{\overline{ld}}\Rightarrow\struct{\overline{ld}}}{}
27 :     \end{array}
28 :     \]
29 :     }
30 :     The underline notation denotes the elaborated version of the nonterminal, i.e., the explicitly typed and elaborated variant.
31 :     \nocaptionrule
32 :     \caption{Static Semantics}
33 :     \label{fig:statsem}
34 :     \end{figure}

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0