header "Arithmetic Stack Machine and Compilation"

theory ASM imports AExp begin

subsection "Arithmetic Stack Machine"

datatype ainstr = PUSH_N nat | PUSH_V nat | ADD

types stack = "nat list"

abbreviation "hd2 xs == hd(tl xs)"
abbreviation "tl2 xs == tl(tl xs)"

text{* \noindent Abbreviations are transparent: they are unfolded after
parsing and folded back again before printing. Internally, they do not
exist. *}

fun aexec1 :: "ainstr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
"aexec1 (PUSH_N n) _ stk  =  n # stk" |
"aexec1 (PUSH_V n) s stk  =  s(n) # stk" |
"aexec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"

fun aexec :: "ainstr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
"aexec [] _ stk = stk" |
"aexec (i#is) s stk = aexec is s (aexec1 i s stk)"

value "aexec [PUSH_N 5, PUSH_V 2, ADD] (nth[42,43,44]) [50]"

lemma aexec_append[simp]:
  "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
apply(induct is1 arbitrary: stk)
apply (auto)
done


subsection "Compilation"

fun acomp :: "aexp \<Rightarrow> ainstr list" where
"acomp (N n) = [PUSH_N n]" |
"acomp (V n) = [PUSH_V n]" |
"acomp (Plus e1 e2) = acomp e1 @ acomp e2 @ [ADD]"

value "acomp (Plus (Plus (V 0) (N 1)) (V 2))"

theorem aexec_acomp[simp]: "aexec (acomp e) s stk = aval e s # stk"
apply(induct e arbitrary: stk)
apply (auto)
done

end