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