43141
|
1 |
header "Arithmetic Stack Machine and Compilation"
|
|
2 |
|
|
3 |
theory ASM imports AExp begin
|
|
4 |
|
|
5 |
subsection "Arithmetic Stack Machine"
|
|
6 |
|
|
7 |
datatype ainstr = LOADI val | LOAD string | ADD
|
|
8 |
|
|
9 |
type_synonym stack = "val list"
|
|
10 |
|
|
11 |
abbreviation "hd2 xs == hd(tl xs)"
|
|
12 |
abbreviation "tl2 xs == tl(tl xs)"
|
|
13 |
|
|
14 |
text{* \noindent Abbreviations are transparent: they are unfolded after
|
|
15 |
parsing and folded back again before printing. Internally, they do not
|
|
16 |
exist. *}
|
|
17 |
|
|
18 |
fun aexec1 :: "ainstr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
|
|
19 |
"aexec1 (LOADI n) _ stk = n # stk" |
|
|
20 |
"aexec1 (LOAD n) s stk = s(n) # stk" |
|
|
21 |
"aexec1 ADD _ stk = (hd2 stk + hd stk) # tl2 stk"
|
|
22 |
|
|
23 |
fun aexec :: "ainstr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
|
|
24 |
"aexec [] _ stk = stk" |
|
|
25 |
"aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
|
|
26 |
|
|
27 |
value "aexec [LOADI 5, LOAD ''y'', ADD]
|
43158
|
28 |
[''x'' \<rightarrow> 42, ''y'' \<rightarrow> 43] [50]"
|
43141
|
29 |
|
|
30 |
lemma aexec_append[simp]:
|
|
31 |
"aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
|
|
32 |
apply(induct is1 arbitrary: stk)
|
|
33 |
apply (auto)
|
|
34 |
done
|
|
35 |
|
|
36 |
|
|
37 |
subsection "Compilation"
|
|
38 |
|
|
39 |
fun acomp :: "aexp \<Rightarrow> ainstr list" where
|
|
40 |
"acomp (N n) = [LOADI n]" |
|
|
41 |
"acomp (V x) = [LOAD x]" |
|
|
42 |
"acomp (Plus e1 e2) = acomp e1 @ acomp e2 @ [ADD]"
|
|
43 |
|
|
44 |
value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
|
|
45 |
|
|
46 |
theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
|
|
47 |
apply(induct a arbitrary: stk)
|
|
48 |
apply (auto)
|
|
49 |
done
|
|
50 |
|
|
51 |
end
|