1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{CodeGen}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isamarkupsection{Case Study: Compiling Expressions% |
|
19 } |
|
20 \isamarkuptrue% |
|
21 % |
|
22 \begin{isamarkuptext}% |
|
23 \label{sec:ExprCompiler} |
|
24 \index{compiling expressions example|(}% |
|
25 The task is to develop a compiler from a generic type of expressions (built |
|
26 from variables, constants and binary operations) to a stack machine. This |
|
27 generic type of expressions is a generalization of the boolean expressions in |
|
28 \S\ref{sec:boolex}. This time we do not commit ourselves to a particular |
|
29 type of variables or values but make them type parameters. Neither is there |
|
30 a fixed set of binary operations: instead the expression contains the |
|
31 appropriate function itself.% |
|
32 \end{isamarkuptext}% |
|
33 \isamarkuptrue% |
|
34 \isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse% |
|
35 \ {\isaliteral{27}{\isacharprime}}v\ binop\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}v\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}v\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}v{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
36 \isacommand{datatype}\isamarkupfalse% |
|
37 \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}expr\ {\isaliteral{3D}{\isacharequal}}\ Cex\ {\isaliteral{27}{\isacharprime}}v\isanewline |
|
38 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Vex\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
39 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Bex\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}v\ binop{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}expr{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}expr{\isaliteral{22}{\isachardoublequoteclose}}% |
|
40 \begin{isamarkuptext}% |
|
41 \noindent |
|
42 The three constructors represent constants, variables and the application of |
|
43 a binary operation to two subexpressions. |
|
44 |
|
45 The value of an expression with respect to an environment that maps variables to |
|
46 values is easily defined:% |
|
47 \end{isamarkuptext}% |
|
48 \isamarkuptrue% |
|
49 \isacommand{primrec}\isamarkupfalse% |
|
50 \ {\isaliteral{22}{\isachardoublequoteopen}}value{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}expr\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}v{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
51 {\isaliteral{22}{\isachardoublequoteopen}}value\ {\isaliteral{28}{\isacharparenleft}}Cex\ v{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ v{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
52 {\isaliteral{22}{\isachardoublequoteopen}}value\ {\isaliteral{28}{\isacharparenleft}}Vex\ a{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ env\ a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
53 {\isaliteral{22}{\isachardoublequoteopen}}value\ {\isaliteral{28}{\isacharparenleft}}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}value\ e{\isadigit{1}}\ env{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}value\ e{\isadigit{2}}\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
54 \begin{isamarkuptext}% |
|
55 The stack machine has three instructions: load a constant value onto the |
|
56 stack, load the contents of an address onto the stack, and apply a |
|
57 binary operation to the two topmost elements of the stack, replacing them by |
|
58 the result. As for \isa{expr}, addresses and values are type parameters:% |
|
59 \end{isamarkuptext}% |
|
60 \isamarkuptrue% |
|
61 \isacommand{datatype}\isamarkupfalse% |
|
62 \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}\ instr\ {\isaliteral{3D}{\isacharequal}}\ Const\ {\isaliteral{27}{\isacharprime}}v\isanewline |
|
63 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Load\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
64 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Apply\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}v\ binop{\isaliteral{22}{\isachardoublequoteclose}}% |
|
65 \begin{isamarkuptext}% |
|
66 The execution of the stack machine is modelled by a function |
|
67 \isa{exec} that takes a list of instructions, a store (modelled as a |
|
68 function from addresses to values, just like the environment for |
|
69 evaluating expressions), and a stack (modelled as a list) of values, |
|
70 and returns the stack at the end of the execution --- the store remains |
|
71 unchanged:% |
|
72 \end{isamarkuptext}% |
|
73 \isamarkuptrue% |
|
74 \isacommand{primrec}\isamarkupfalse% |
|
75 \ exec\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}instr\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}v\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}v\ list{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
76 \isakeyword{where}\isanewline |
|
77 {\isaliteral{22}{\isachardoublequoteopen}}exec\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ s\ vs\ {\isaliteral{3D}{\isacharequal}}\ vs{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
78 {\isaliteral{22}{\isachardoublequoteopen}}exec\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{23}{\isacharhash}}is{\isaliteral{29}{\isacharparenright}}\ s\ vs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}case\ i\ of\isanewline |
|
79 \ \ \ \ Const\ v\ \ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ exec\ is\ s\ {\isaliteral{28}{\isacharparenleft}}v{\isaliteral{23}{\isacharhash}}vs{\isaliteral{29}{\isacharparenright}}\isanewline |
|
80 \ \ {\isaliteral{7C}{\isacharbar}}\ Load\ a\ \ \ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ exec\ is\ s\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}s\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{23}{\isacharhash}}vs{\isaliteral{29}{\isacharparenright}}\isanewline |
|
81 \ \ {\isaliteral{7C}{\isacharbar}}\ Apply\ f\ \ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ exec\ is\ s\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}hd\ vs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}hd{\isaliteral{28}{\isacharparenleft}}tl\ vs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{23}{\isacharhash}}{\isaliteral{28}{\isacharparenleft}}tl{\isaliteral{28}{\isacharparenleft}}tl\ vs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
82 \begin{isamarkuptext}% |
|
83 \noindent |
|
84 Recall that \isa{hd} and \isa{tl} |
|
85 return the first element and the remainder of a list. |
|
86 Because all functions are total, \cdx{hd} is defined even for the empty |
|
87 list, although we do not know what the result is. Thus our model of the |
|
88 machine always terminates properly, although the definition above does not |
|
89 tell us much about the result in situations where \isa{Apply} was executed |
|
90 with fewer than two elements on the stack. |
|
91 |
|
92 The compiler is a function from expressions to a list of instructions. Its |
|
93 definition is obvious:% |
|
94 \end{isamarkuptext}% |
|
95 \isamarkuptrue% |
|
96 \isacommand{primrec}\isamarkupfalse% |
|
97 \ compile\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}expr\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}instr\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
98 {\isaliteral{22}{\isachardoublequoteopen}}compile\ {\isaliteral{28}{\isacharparenleft}}Cex\ v{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}Const\ v{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
99 {\isaliteral{22}{\isachardoublequoteopen}}compile\ {\isaliteral{28}{\isacharparenleft}}Vex\ a{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}Load\ a{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
100 {\isaliteral{22}{\isachardoublequoteopen}}compile\ {\isaliteral{28}{\isacharparenleft}}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}compile\ e{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{28}{\isacharparenleft}}compile\ e{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}Apply\ f{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
101 \begin{isamarkuptext}% |
|
102 Now we have to prove the correctness of the compiler, i.e.\ that the |
|
103 execution of a compiled expression results in the value of the expression:% |
|
104 \end{isamarkuptext}% |
|
105 \isamarkuptrue% |
|
106 \isacommand{theorem}\isamarkupfalse% |
|
107 \ {\isaliteral{22}{\isachardoublequoteopen}}exec\ {\isaliteral{28}{\isacharparenleft}}compile\ e{\isaliteral{29}{\isacharparenright}}\ s\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}value\ e\ s{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
108 \isadelimproof |
|
109 % |
|
110 \endisadelimproof |
|
111 % |
|
112 \isatagproof |
|
113 % |
|
114 \endisatagproof |
|
115 {\isafoldproof}% |
|
116 % |
|
117 \isadelimproof |
|
118 % |
|
119 \endisadelimproof |
|
120 % |
|
121 \begin{isamarkuptext}% |
|
122 \noindent |
|
123 This theorem needs to be generalized:% |
|
124 \end{isamarkuptext}% |
|
125 \isamarkuptrue% |
|
126 \isacommand{theorem}\isamarkupfalse% |
|
127 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}vs{\isaliteral{2E}{\isachardot}}\ exec\ {\isaliteral{28}{\isacharparenleft}}compile\ e{\isaliteral{29}{\isacharparenright}}\ s\ vs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}value\ e\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ vs{\isaliteral{22}{\isachardoublequoteclose}}% |
|
128 \isadelimproof |
|
129 % |
|
130 \endisadelimproof |
|
131 % |
|
132 \isatagproof |
|
133 % |
|
134 \begin{isamarkuptxt}% |
|
135 \noindent |
|
136 It will be proved by induction on \isa{e} followed by simplification. |
|
137 First, we must prove a lemma about executing the concatenation of two |
|
138 instruction sequences:% |
|
139 \end{isamarkuptxt}% |
|
140 \isamarkuptrue% |
|
141 % |
|
142 \endisatagproof |
|
143 {\isafoldproof}% |
|
144 % |
|
145 \isadelimproof |
|
146 % |
|
147 \endisadelimproof |
|
148 \isacommand{lemma}\isamarkupfalse% |
|
149 \ exec{\isaliteral{5F}{\isacharunderscore}}app{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
150 \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}vs{\isaliteral{2E}{\isachardot}}\ exec\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{40}{\isacharat}}ys{\isaliteral{29}{\isacharparenright}}\ s\ vs\ {\isaliteral{3D}{\isacharequal}}\ exec\ ys\ s\ {\isaliteral{28}{\isacharparenleft}}exec\ xs\ s\ vs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
151 \isadelimproof |
|
152 % |
|
153 \endisadelimproof |
|
154 % |
|
155 \isatagproof |
|
156 % |
|
157 \begin{isamarkuptxt}% |
|
158 \noindent |
|
159 This requires induction on \isa{xs} and ordinary simplification for the |
|
160 base cases. In the induction step, simplification leaves us with a formula |
|
161 that contains two \isa{case}-expressions over instructions. Thus we add |
|
162 automatic case splitting, which finishes the proof:% |
|
163 \end{isamarkuptxt}% |
|
164 \isamarkuptrue% |
|
165 \isacommand{apply}\isamarkupfalse% |
|
166 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{2C}{\isacharcomma}}\ simp\ split{\isaliteral{3A}{\isacharcolon}}\ instr{\isaliteral{2E}{\isachardot}}split{\isaliteral{29}{\isacharparenright}}% |
|
167 \endisatagproof |
|
168 {\isafoldproof}% |
|
169 % |
|
170 \isadelimproof |
|
171 % |
|
172 \endisadelimproof |
|
173 % |
|
174 \begin{isamarkuptext}% |
|
175 \noindent |
|
176 Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can |
|
177 be modified in the same way as \isa{simp}. Thus the proof can be |
|
178 rewritten as% |
|
179 \end{isamarkuptext}% |
|
180 \isamarkuptrue% |
|
181 % |
|
182 \isadelimproof |
|
183 % |
|
184 \endisadelimproof |
|
185 % |
|
186 \isatagproof |
|
187 \isacommand{apply}\isamarkupfalse% |
|
188 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\ split{\isaliteral{3A}{\isacharcolon}}\ instr{\isaliteral{2E}{\isachardot}}split{\isaliteral{29}{\isacharparenright}}% |
|
189 \endisatagproof |
|
190 {\isafoldproof}% |
|
191 % |
|
192 \isadelimproof |
|
193 % |
|
194 \endisadelimproof |
|
195 % |
|
196 \begin{isamarkuptext}% |
|
197 \noindent |
|
198 Although this is more compact, it is less clear for the reader of the proof. |
|
199 |
|
200 We could now go back and prove \isa{exec\ {\isaliteral{28}{\isacharparenleft}}compile\ e{\isaliteral{29}{\isacharparenright}}\ s\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}value\ e\ s{\isaliteral{5D}{\isacharbrackright}}} |
|
201 merely by simplification with the generalized version we just proved. |
|
202 However, this is unnecessary because the generalized version fully subsumes |
|
203 its instance.% |
|
204 \index{compiling expressions example|)}% |
|
205 \end{isamarkuptext}% |
|
206 \isamarkuptrue% |
|
207 % |
|
208 \isadelimproof |
|
209 % |
|
210 \endisadelimproof |
|
211 % |
|
212 \isatagproof |
|
213 % |
|
214 \endisatagproof |
|
215 {\isafoldproof}% |
|
216 % |
|
217 \isadelimproof |
|
218 % |
|
219 \endisadelimproof |
|
220 % |
|
221 \isadelimtheory |
|
222 % |
|
223 \endisadelimtheory |
|
224 % |
|
225 \isatagtheory |
|
226 % |
|
227 \endisatagtheory |
|
228 {\isafoldtheory}% |
|
229 % |
|
230 \isadelimtheory |
|
231 % |
|
232 \endisadelimtheory |
|
233 \end{isabellebody}% |
|
234 %%% Local Variables: |
|
235 %%% mode: latex |
|
236 %%% TeX-master: "root" |
|
237 %%% End: |
|