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