src/HOL/IMP/ASM.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 58889 5b7a9633cfa8
child 67079 02483f568c52
permissions -rw-r--r--
Lots of new material for multivariate analysis
wenzelm@58889
     1
section "Stack Machine and Compilation"
nipkow@43141
     2
nipkow@43141
     3
theory ASM imports AExp begin
nipkow@43141
     4
nipkow@45266
     5
subsection "Stack Machine"
nipkow@43141
     6
nipkow@49191
     7
text_raw{*\snip{ASMinstrdef}{0}{1}{% *}
blanchet@58310
     8
datatype instr = LOADI val | LOAD vname | ADD
nipkow@49191
     9
text_raw{*}%endsnip*}
nipkow@43141
    10
nipkow@49191
    11
text_raw{*\snip{ASMstackdef}{1}{2}{% *}
nipkow@43141
    12
type_synonym stack = "val list"
nipkow@49191
    13
text_raw{*}%endsnip*}
nipkow@43141
    14
nipkow@43141
    15
abbreviation "hd2 xs == hd(tl xs)"
nipkow@43141
    16
abbreviation "tl2 xs == tl(tl xs)"
nipkow@43141
    17
nipkow@43141
    18
text{* \noindent Abbreviations are transparent: they are unfolded after
nipkow@43141
    19
parsing and folded back again before printing. Internally, they do not
nipkow@49191
    20
exist.*}
nipkow@43141
    21
nipkow@49191
    22
text_raw{*\snip{ASMexeconedef}{0}{1}{% *}
nipkow@45257
    23
fun exec1 :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
nipkow@45257
    24
"exec1 (LOADI n) _ stk  =  n # stk" |
nipkow@45257
    25
"exec1 (LOAD x) s stk  =  s(x) # stk" |
nipkow@45257
    26
"exec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
nipkow@49191
    27
text_raw{*}%endsnip*}
nipkow@43141
    28
nipkow@49191
    29
text_raw{*\snip{ASMexecdef}{1}{2}{% *}
nipkow@45257
    30
fun exec :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
nipkow@45257
    31
"exec [] _ stk = stk" |
nipkow@45257
    32
"exec (i#is) s stk = exec is s (exec1 i s stk)"
nipkow@49191
    33
text_raw{*}%endsnip*}
nipkow@43141
    34
nipkow@50007
    35
value "exec [LOADI 5, LOAD ''y'', ADD] <''x'' := 42, ''y'' := 43> [50]"
nipkow@43141
    36
nipkow@45257
    37
lemma exec_append[simp]:
nipkow@45257
    38
  "exec (is1@is2) s stk = exec is2 s (exec is1 s stk)"
nipkow@45015
    39
apply(induction is1 arbitrary: stk)
nipkow@43141
    40
apply (auto)
nipkow@43141
    41
done
nipkow@43141
    42
nipkow@43141
    43
nipkow@43141
    44
subsection "Compilation"
nipkow@43141
    45
nipkow@49191
    46
text_raw{*\snip{ASMcompdef}{0}{2}{% *}
nipkow@45257
    47
fun comp :: "aexp \<Rightarrow> instr list" where
nipkow@45257
    48
"comp (N n) = [LOADI n]" |
nipkow@45257
    49
"comp (V x) = [LOAD x]" |
wenzelm@53015
    50
"comp (Plus e\<^sub>1 e\<^sub>2) = comp e\<^sub>1 @ comp e\<^sub>2 @ [ADD]"
nipkow@49191
    51
text_raw{*}%endsnip*}
nipkow@43141
    52
nipkow@45257
    53
value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
nipkow@43141
    54
nipkow@45257
    55
theorem exec_comp: "exec (comp a) s stk = aval a s # stk"
nipkow@45015
    56
apply(induction a arbitrary: stk)
nipkow@43141
    57
apply (auto)
nipkow@43141
    58
done
nipkow@43141
    59
nipkow@43141
    60
end