src/HOL/IMP/ASM.thy
author nipkow
Thu, 27 Oct 2011 15:59:25 +0200
changeset 45275 7f6c2db48b71
parent 45266 13b5fb92b9f5
child 49191 3601bf546775
permissions -rw-r--r--
tuned text
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45266
13b5fb92b9f5 tuned text
nipkow
parents: 45257
diff changeset
     1
header "Stack Machine and Compilation"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     2
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     3
theory ASM imports AExp begin
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     4
45266
13b5fb92b9f5 tuned text
nipkow
parents: 45257
diff changeset
     5
subsection "Stack Machine"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     6
45257
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
     7
text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMinstrdef}{% *}
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
     8
datatype instr = LOADI val | LOAD vname | ADD
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
     9
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    10
45257
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    11
text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMstackdef}{% *}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    12
type_synonym stack = "val list"
45257
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    13
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    14
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    15
abbreviation "hd2 xs == hd(tl xs)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    16
abbreviation "tl2 xs == tl(tl xs)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    17
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    18
text{* \noindent Abbreviations are transparent: they are unfolded after
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    19
parsing and folded back again before printing. Internally, they do not
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    20
exist. *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    21
45257
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    22
text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMexeconedef}{% *}
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    23
fun exec1 :: "instr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    24
"exec1 (LOADI n) _ stk  =  n # stk" |
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    25
"exec1 (LOAD x) s stk  =  s(x) # stk" |
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    26
"exec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    27
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    28
45257
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    29
text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMexecdef}{% *}
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    30
fun exec :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    31
"exec [] _ stk = stk" |
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    32
"exec (i#is) s stk = exec is s (exec1 i s stk)"
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    33
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    34
45257
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    35
value "exec [LOADI 5, LOAD ''y'', ADD]
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 43158
diff changeset
    36
 <''x'' := 42, ''y'' := 43> [50]"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    37
45257
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    38
lemma exec_append[simp]:
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    39
  "exec (is1@is2) s stk = exec is2 s (exec is1 s stk)"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44036
diff changeset
    40
apply(induction is1 arbitrary: stk)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    41
apply (auto)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    42
done
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    43
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    44
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    45
subsection "Compilation"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    46
45257
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    47
text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMcompdef}{% *}
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    48
fun comp :: "aexp \<Rightarrow> instr list" where
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    49
"comp (N n) = [LOADI n]" |
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    50
"comp (V x) = [LOAD x]" |
45275
7f6c2db48b71 tuned text
nipkow
parents: 45266
diff changeset
    51
"comp (Plus e\<^isub>1 e\<^isub>2) = comp e\<^isub>1 @ comp e\<^isub>2 @ [ADD]"
45257
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    52
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    53
45257
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    54
value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    55
45257
12063e071d92 renamed in ASM
nipkow
parents: 45222
diff changeset
    56
theorem exec_comp: "exec (comp a) s stk = aval a s # stk"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44036
diff changeset
    57
apply(induction a arbitrary: stk)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    58
apply (auto)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    59
done
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    60
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    61
end