45266
|
1 |
header "Stack Machine and Compilation"
|
43141
|
2 |
|
|
3 |
theory ASM imports AExp begin
|
|
4 |
|
45266
|
5 |
subsection "Stack Machine"
|
43141
|
6 |
|
45257
|
7 |
text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMinstrdef}{% *}
|
|
8 |
datatype instr = LOADI val | LOAD vname | ADD
|
|
9 |
text_raw{*}\end{isaverbatimwrite}*}
|
43141
|
10 |
|
45257
|
11 |
text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMstackdef}{% *}
|
43141
|
12 |
type_synonym stack = "val list"
|
45257
|
13 |
text_raw{*}\end{isaverbatimwrite}*}
|
43141
|
14 |
|
|
15 |
abbreviation "hd2 xs == hd(tl xs)"
|
|
16 |
abbreviation "tl2 xs == tl(tl xs)"
|
|
17 |
|
|
18 |
text{* \noindent Abbreviations are transparent: they are unfolded after
|
|
19 |
parsing and folded back again before printing. Internally, they do not
|
|
20 |
exist. *}
|
|
21 |
|
45257
|
22 |
text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMexeconedef}{% *}
|
|
23 |
fun exec1 :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
|
|
24 |
"exec1 (LOADI n) _ stk = n # stk" |
|
|
25 |
"exec1 (LOAD x) s stk = s(x) # stk" |
|
|
26 |
"exec1 ADD _ stk = (hd2 stk + hd stk) # tl2 stk"
|
|
27 |
text_raw{*}\end{isaverbatimwrite}*}
|
43141
|
28 |
|
45257
|
29 |
text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMexecdef}{% *}
|
|
30 |
fun exec :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
|
|
31 |
"exec [] _ stk = stk" |
|
|
32 |
"exec (i#is) s stk = exec is s (exec1 i s stk)"
|
|
33 |
text_raw{*}\end{isaverbatimwrite}*}
|
43141
|
34 |
|
45257
|
35 |
value "exec [LOADI 5, LOAD ''y'', ADD]
|
44036
|
36 |
<''x'' := 42, ''y'' := 43> [50]"
|
43141
|
37 |
|
45257
|
38 |
lemma exec_append[simp]:
|
|
39 |
"exec (is1@is2) s stk = exec is2 s (exec is1 s stk)"
|
45015
|
40 |
apply(induction is1 arbitrary: stk)
|
43141
|
41 |
apply (auto)
|
|
42 |
done
|
|
43 |
|
|
44 |
|
|
45 |
subsection "Compilation"
|
|
46 |
|
45257
|
47 |
text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMcompdef}{% *}
|
|
48 |
fun comp :: "aexp \<Rightarrow> instr list" where
|
|
49 |
"comp (N n) = [LOADI n]" |
|
|
50 |
"comp (V x) = [LOAD x]" |
|
45275
|
51 |
"comp (Plus e\<^isub>1 e\<^isub>2) = comp e\<^isub>1 @ comp e\<^isub>2 @ [ADD]"
|
45257
|
52 |
text_raw{*}\end{isaverbatimwrite}*}
|
43141
|
53 |
|
45257
|
54 |
value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
|
43141
|
55 |
|
45257
|
56 |
theorem exec_comp: "exec (comp a) s stk = aval a s # stk"
|
45015
|
57 |
apply(induction a arbitrary: stk)
|
43141
|
58 |
apply (auto)
|
|
59 |
done
|
|
60 |
|
|
61 |
end
|