|
1 \begin{isabelle}% |
|
2 % |
|
3 \begin{isamarkuptext}% |
|
4 \noindent |
|
5 The task is to develop a compiler from a generic type of expressions (built |
|
6 up from variables, constants and binary operations) to a stack machine. This |
|
7 generic type of expressions is a generalization of the boolean expressions in |
|
8 \S\ref{sec:boolex}. This time we do not commit ourselves to a particular |
|
9 type of variables or values but make them type parameters. Neither is there |
|
10 a fixed set of binary operations: instead the expression contains the |
|
11 appropriate function itself.% |
|
12 \end{isamarkuptext}% |
|
13 \isacommand{types}~'v~binop~=~{"}'v~{\isasymRightarrow}~'v~{\isasymRightarrow}~'v{"}\isanewline |
|
14 \isacommand{datatype}~('a,'v)expr~=~Cex~'v\isanewline |
|
15 ~~~~~~~~~~~~~~~~~~~~~|~Vex~'a\isanewline |
|
16 ~~~~~~~~~~~~~~~~~~~~~|~Bex~{"}'v~binop{"}~~{"}('a,'v)expr{"}~~{"}('a,'v)expr{"}% |
|
17 \begin{isamarkuptext}% |
|
18 \noindent |
|
19 The three constructors represent constants, variables and the combination of |
|
20 two subexpressions with a binary operation. |
|
21 |
|
22 The value of an expression w.r.t.\ an environment that maps variables to |
|
23 values is easily defined:% |
|
24 \end{isamarkuptext}% |
|
25 \isacommand{consts}~value~::~{"}('a~{\isasymRightarrow}~'v)~{\isasymRightarrow}~('a,'v)expr~{\isasymRightarrow}~'v{"}\isanewline |
|
26 \isacommand{primrec}\isanewline |
|
27 {"}value~env~(Cex~v)~=~v{"}\isanewline |
|
28 {"}value~env~(Vex~a)~=~env~a{"}\isanewline |
|
29 {"}value~env~(Bex~f~e1~e2)~=~f~(value~env~e1)~(value~env~e2){"}% |
|
30 \begin{isamarkuptext}% |
|
31 The stack machine has three instructions: load a constant value onto the |
|
32 stack, load the contents of a certain address onto the stack, and apply a |
|
33 binary operation to the two topmost elements of the stack, replacing them by |
|
34 the result. As for \isa{expr}, addresses and values are type parameters:% |
|
35 \end{isamarkuptext}% |
|
36 \isacommand{datatype}~('a,'v)~instr~=~Const~'v\isanewline |
|
37 ~~~~~~~~~~~~~~~~~~~~~~~|~Load~'a\isanewline |
|
38 ~~~~~~~~~~~~~~~~~~~~~~~|~Apply~{"}'v~binop{"}% |
|
39 \begin{isamarkuptext}% |
|
40 The execution of the stack machine is modelled by a function \isa{exec} |
|
41 that takes a store (modelled as a function from addresses to values, just |
|
42 like the environment for evaluating expressions), a stack (modelled as a |
|
43 list) of values, and a list of instructions, and returns the stack at the end |
|
44 of the execution---the store remains unchanged:% |
|
45 \end{isamarkuptext}% |
|
46 \isacommand{consts}~exec~::~{"}('a{\isasymRightarrow}'v)~{\isasymRightarrow}~'v~list~{\isasymRightarrow}~('a,'v)instr~list~{\isasymRightarrow}~'v~list{"}\isanewline |
|
47 \isacommand{primrec}\isanewline |
|
48 {"}exec~s~vs~[]~=~vs{"}\isanewline |
|
49 {"}exec~s~vs~(i\#is)~=~(case~i~of\isanewline |
|
50 ~~~~Const~v~~{\isasymRightarrow}~exec~s~(v\#vs)~is\isanewline |
|
51 ~~|~Load~a~~~{\isasymRightarrow}~exec~s~((s~a)\#vs)~is\isanewline |
|
52 ~~|~Apply~f~~{\isasymRightarrow}~exec~s~(~(f~(hd~vs)~(hd(tl~vs)))\#(tl(tl~vs))~)~is){"}% |
|
53 \begin{isamarkuptext}% |
|
54 \noindent |
|
55 Recall that \isa{hd} and \isa{tl} |
|
56 return the first element and the remainder of a list. |
|
57 Because all functions are total, \isa{hd} is defined even for the empty |
|
58 list, although we do not know what the result is. Thus our model of the |
|
59 machine always terminates properly, although the above definition does not |
|
60 tell us much about the result in situations where \isa{Apply} was executed |
|
61 with fewer than two elements on the stack. |
|
62 |
|
63 The compiler is a function from expressions to a list of instructions. Its |
|
64 definition is pretty much obvious:% |
|
65 \end{isamarkuptext}% |
|
66 \isacommand{consts}~comp~::~{"}('a,'v)expr~{\isasymRightarrow}~('a,'v)instr~list{"}\isanewline |
|
67 \isacommand{primrec}\isanewline |
|
68 {"}comp~(Cex~v)~~~~~~~=~[Const~v]{"}\isanewline |
|
69 {"}comp~(Vex~a)~~~~~~~=~[Load~a]{"}\isanewline |
|
70 {"}comp~(Bex~f~e1~e2)~=~(comp~e2)~@~(comp~e1)~@~[Apply~f]{"}% |
|
71 \begin{isamarkuptext}% |
|
72 Now we have to prove the correctness of the compiler, i.e.\ that the |
|
73 execution of a compiled expression results in the value of the expression:% |
|
74 \end{isamarkuptext}% |
|
75 \isacommand{theorem}~{"}exec~s~[]~(comp~e)~=~[value~s~e]{"}% |
|
76 \begin{isamarkuptext}% |
|
77 \noindent |
|
78 This theorem needs to be generalized to% |
|
79 \end{isamarkuptext}% |
|
80 \isacommand{theorem}~{"}{\isasymforall}vs.~exec~s~vs~(comp~e)~=~(value~s~e)~\#~vs{"}% |
|
81 \begin{isamarkuptxt}% |
|
82 \noindent |
|
83 which is proved by induction on \isa{e} followed by simplification, once |
|
84 we have the following lemma about executing the concatenation of two |
|
85 instruction sequences:% |
|
86 \end{isamarkuptxt}% |
|
87 \isacommand{lemma}~exec\_app[simp]:\isanewline |
|
88 ~~{"}{\isasymforall}vs.~exec~s~vs~(xs@ys)~=~exec~s~(exec~s~vs~xs)~ys{"}% |
|
89 \begin{isamarkuptxt}% |
|
90 \noindent |
|
91 This requires induction on \isa{xs} and ordinary simplification for the |
|
92 base cases. In the induction step, simplification leaves us with a formula |
|
93 that contains two \isa{case}-expressions over instructions. Thus we add |
|
94 automatic case splitting as well, which finishes the proof:% |
|
95 \end{isamarkuptxt}% |
|
96 \isacommand{apply}(induct\_tac~xs,~simp,~simp~split:~instr.split)\isacommand{.}% |
|
97 \begin{isamarkuptext}% |
|
98 \noindent |
|
99 Note that because \isaindex{auto} performs simplification, it can |
|
100 also be modified in the same way \isa{simp} can. Thus the proof can be |
|
101 rewritten as% |
|
102 \end{isamarkuptext}% |
|
103 \isacommand{apply}(induct\_tac~xs,~auto~split:~instr.split)\isacommand{.}% |
|
104 \begin{isamarkuptext}% |
|
105 \noindent |
|
106 Although this is more compact, it is less clear for the reader of the proof. |
|
107 |
|
108 We could now go back and prove \isa{exec s [] (comp e) = [value s e]} |
|
109 merely by simplification with the generalized version we just proved. |
|
110 However, this is unnecessary because the generalized version fully subsumes |
|
111 its instance.% |
|
112 \end{isamarkuptext}% |
|
113 \end{isabelle}% |