# Theory ASM

theory ASM
imports AExp
section "Stack Machine and Compilation"

theory ASM imports AExp begin

subsection "Stack Machine"

text_raw{*\snip{ASMinstrdef}{0}{1}{% *}
text_raw{*}%endsnip*}

text_raw{*\snip{ASMstackdef}{1}{2}{% *}
type_synonym stack = "val list"
text_raw{*}%endsnip*}

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.*}

text_raw{*\snip{ASMexeconedef}{0}{1}{% *}
fun exec1 :: "instr ⇒ state ⇒ stack ⇒ stack" where
"exec1 (LOADI n) _ stk  =  n # stk" |
"exec1 (LOAD x) s stk  =  s(x) # stk" |
"exec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
text_raw{*}%endsnip*}

text_raw{*\snip{ASMexecdef}{1}{2}{% *}
fun exec :: "instr list ⇒ state ⇒ stack ⇒ stack" where
"exec [] _ stk = stk" |
"exec (i#is) s stk = exec is s (exec1 i s stk)"
text_raw{*}%endsnip*}

lemma exec_append[simp]:
"exec (is1@is2) s stk = exec is2 s (exec is1 s stk)"
apply(induction is1 arbitrary: stk)
apply (auto)
done

subsection "Compilation"

text_raw{*\snip{ASMcompdef}{0}{2}{% *}
fun comp :: "aexp ⇒ instr list" where
"comp (N n) = [LOADI n]" |
"comp (V x) = [LOAD x]" |
"comp (Plus e⇩1 e⇩2) = comp e⇩1 @ comp e⇩2 @ [ADD]"
text_raw{*}%endsnip*}

value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"

theorem exec_comp: "exec (comp a) s stk = aval a s # stk"
apply(induction a arbitrary: stk)
apply (auto)
done

end