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]" 


51 
"comp (Plus e1 e2) = comp e1 @ comp e2 @ [ADD]"


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
