src/HOL/IMP/ASM.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45222 6eab55bab82f
child 45257 12063e071d92
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
nipkow@43141
     1
header "Arithmetic Stack Machine and Compilation"
nipkow@43141
     2
nipkow@43141
     3
theory ASM imports AExp begin
nipkow@43141
     4
nipkow@43141
     5
subsection "Arithmetic Stack Machine"
nipkow@43141
     6
nipkow@45222
     7
datatype ainstr = LOADI val | LOAD vname | ADD
nipkow@43141
     8
nipkow@43141
     9
type_synonym stack = "val list"
nipkow@43141
    10
nipkow@43141
    11
abbreviation "hd2 xs == hd(tl xs)"
nipkow@43141
    12
abbreviation "tl2 xs == tl(tl xs)"
nipkow@43141
    13
nipkow@43141
    14
text{* \noindent Abbreviations are transparent: they are unfolded after
nipkow@43141
    15
parsing and folded back again before printing. Internally, they do not
nipkow@43141
    16
exist. *}
nipkow@43141
    17
nipkow@43141
    18
fun aexec1 :: "ainstr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
nipkow@43141
    19
"aexec1 (LOADI n) _ stk  =  n # stk" |
nipkow@43141
    20
"aexec1 (LOAD n) s stk  =  s(n) # stk" |
nipkow@43141
    21
"aexec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
nipkow@43141
    22
nipkow@43141
    23
fun aexec :: "ainstr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
nipkow@43141
    24
"aexec [] _ stk = stk" |
nipkow@43141
    25
"aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
nipkow@43141
    26
nipkow@43141
    27
value "aexec [LOADI 5, LOAD ''y'', ADD]
kleing@44036
    28
 <''x'' := 42, ''y'' := 43> [50]"
nipkow@43141
    29
nipkow@43141
    30
lemma aexec_append[simp]:
nipkow@43141
    31
  "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
nipkow@45015
    32
apply(induction is1 arbitrary: stk)
nipkow@43141
    33
apply (auto)
nipkow@43141
    34
done
nipkow@43141
    35
nipkow@43141
    36
nipkow@43141
    37
subsection "Compilation"
nipkow@43141
    38
nipkow@43141
    39
fun acomp :: "aexp \<Rightarrow> ainstr list" where
nipkow@43141
    40
"acomp (N n) = [LOADI n]" |
nipkow@43141
    41
"acomp (V x) = [LOAD x]" |
nipkow@43141
    42
"acomp (Plus e1 e2) = acomp e1 @ acomp e2 @ [ADD]"
nipkow@43141
    43
nipkow@43141
    44
value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
nipkow@43141
    45
nipkow@43141
    46
theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
nipkow@45015
    47
apply(induction a arbitrary: stk)
nipkow@43141
    48
apply (auto)
nipkow@43141
    49
done
nipkow@43141
    50
nipkow@43141
    51
end