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