src/HOL/IMP/ASM.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58310 91ea607a34d8
child 67079 02483f568c52
permissions -rw-r--r--
modernized header uniformly as section;
     1 section "Stack Machine and Compilation"
     2 
     3 theory ASM imports AExp begin
     4 
     5 subsection "Stack Machine"
     6 
     7 text_raw{*\snip{ASMinstrdef}{0}{1}{% *}
     8 datatype instr = LOADI val | LOAD vname | ADD
     9 text_raw{*}%endsnip*}
    10 
    11 text_raw{*\snip{ASMstackdef}{1}{2}{% *}
    12 type_synonym stack = "val list"
    13 text_raw{*}%endsnip*}
    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 
    22 text_raw{*\snip{ASMexeconedef}{0}{1}{% *}
    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{*}%endsnip*}
    28 
    29 text_raw{*\snip{ASMexecdef}{1}{2}{% *}
    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{*}%endsnip*}
    34 
    35 value "exec [LOADI 5, LOAD ''y'', ADD] <''x'' := 42, ''y'' := 43> [50]"
    36 
    37 lemma exec_append[simp]:
    38   "exec (is1@is2) s stk = exec is2 s (exec is1 s stk)"
    39 apply(induction is1 arbitrary: stk)
    40 apply (auto)
    41 done
    42 
    43 
    44 subsection "Compilation"
    45 
    46 text_raw{*\snip{ASMcompdef}{0}{2}{% *}
    47 fun comp :: "aexp \<Rightarrow> instr list" where
    48 "comp (N n) = [LOADI n]" |
    49 "comp (V x) = [LOAD x]" |
    50 "comp (Plus e\<^sub>1 e\<^sub>2) = comp e\<^sub>1 @ comp e\<^sub>2 @ [ADD]"
    51 text_raw{*}%endsnip*}
    52 
    53 value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
    54 
    55 theorem exec_comp: "exec (comp a) s stk = aval a s # stk"
    56 apply(induction a arbitrary: stk)
    57 apply (auto)
    58 done
    59 
    60 end