1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
\newif\ifprintrule
\printruletrue
\long\def\printrule#1#2#3{$$
\begin{prooftree}
#1
\ifprintrule
\using#2
\else
\using{}
\fi
\qquad\text{#3}
\end{prooftree}
$$}
\def\rcatnstree{
\trans
{\pgm}{\ip}{(\push{s_1~s_2}{\stk''}, \str)}
{\ip'}{\op}{\st}
\justifies
\trans
{\StmCat:\pgm}{\ip}{(\stk,\str)}
{\ip'}{\op}{\st}
}
\long\def\thercatns{
\printrule\rcatnstree\rcatns{met\enspace
\parbox{36mm}{$\pop{\stk} = (s_2,\stk') $,\\$ \pop{\stk'} = (s_1,\stk'')$.}}
}
\def\rexecnstree{
\trans
{\pgm'}{\ip}{(\Nil, \emptystore)}
{\ip'}{\op}{\st}
\justifies
\trans
{\StmExec:\pgm}{\ip}{(\stk,\str)}
{\ip'}{\op}{\st}
}
\long\def\therexecns{
\printrule\rexecnstree\rexecns{met\enspace
\parbox{36mm}{$ \pop{\stk} =(\var,\stk')$,\\
$\pgm' = \parsepgm{\var'}$.}
}
}
\def\rgetnstree{
\trans
{\pgm}{\ip}{(\push{\str~\var}{\stk'}, \str)}
{\ip'}{\op}{\st}
\justifies
\trans
{\StmGet:\pgm}{\ip}{(\stk,\str)}
{\ip'}{\op}{\st}
}
\long\def\thergetns{
\printrule\rgetnstree\rgetns{met $\pop{\stk}= (\var,\stk')$.}
}
\def\rheadnstree{
\trans
{\pgm}{\ip}{(\push{c}{\stk'}, \str)}
{\ip'}{\op}{\st}
\justifies
\trans
{\StmHead:\pgm}{\ip}{(\stk,\str)}
{\ip'}{\op}{\st}
}
\long\def\therheadns{
\printrule\rheadnstree\rheadns{met $\pop{\stk} = (c~s,\stk')$.}
}
\def\rinputnstree{
\trans
{\pgm}{\ip'}{(\push\val\stk, \str)}
{\ip''}{\op}{\st}
\justifies
\trans
{\StmInput:\pgm}{\ip}{(\stk,\str)}
{\ip''}{\op}{\st}
}
\long\def\therinputns{
\printrule\rinputnstree\rinputns{met $\pop\ip = (\val,\ip')$.}
}
\def\rlambdanstree{
\axjustifies
\trans
{\lambda}{\ip}{\st}
{\ip}{\Nil}{\st}
}
\long\def\therlambdans{\printrule\rlambdanstree\rlambdans{}}
\def\routputnstree{
\trans
{\pgm}{\ip}{(\stk',\str)}
{\ip'}{\op}{\st}
\justifies
\trans
{\StmOutput:\pgm}{\ip}{(\stk,\str)}
{\ip'}{\push{s}{\op}}{\st}
}
\long\def\theroutputns{
\printrule\routputnstree\routputns{met $\pop{\stk} = (s,\stk') $,}
}
\def\rpushnstree{
\trans
{\pgm}{\ip}{(\push{s}{\stk}), \str)}
{\ip'}{\op}{\st}
\justifies
\trans
{\StmPush~s:\pgm}{\ip}{(\stk,\str)}
{\ip'}{\op}{\st}
}
\long\def\therpushns{\printrule\rpushnstree\rpushns{}}
\def\rputnstree{
\trans
{\pgm}{\ip}{(\stk'', \smurfput\var\val\str)}
{\ip'}{\op}{\st}
\justifies
\trans
{\StmPut:\pgm}{\ip}{(\stk,\str)}
{\ip'}{\op}{\st}
}
\long\def\therputns{
\printrule\rputnstree\rputns{met\enspace
\parbox{36mm}{$\pop{\stk} = (\var,\stk')$,
\\$\pop{\stk'}= (\val,\stk'')$.}}
}
\def\rquotifynstree{
\trans
{\pgm}{\ip}{(\push{\texttt{"}\escape{s}\texttt{"}}{\stk'}, \str) }
{\ip'}{\op}{\st}
\justifies
\trans
{\StmQuotify:\pgm}{\ip}{(\stk,\str)}
{\ip'}{\op}{\st}
}
\long\def\therquotifyns{
\printrule\rquotifynstree\rquotifyns{met $\pop{\stk} = (s, stk')$.}
}
\def\rtailnstree{
\trans
{\pgm}{\ip}{(\push{s}{\stk'}, \str)}
{\ip'}{\op}{\st}
\justifies
\trans
{\StmTail:\pgm}{\ip}{(\stk,\str)}
{\ip'}{\op}{\st}
}
\long\def\thertailns{
\printrule\rtailnstree\rtailns{met $ \pop{\stk} = (c~s,\stk') $.}
}
|
