src/HOL/IMP/ASM.thy
author kleing
Mon, 06 Jun 2011 16:29:38 +0200
changeset 43158 686fa0a0696e
parent 43141 11fce8564415
child 44036 d03f9f28d01d
permissions -rw-r--r--
imported rest of new IMP
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     1
header "Arithmetic Stack Machine and Compilation"
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
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     5
subsection "Arithmetic Stack Machine"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     6
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     7
datatype ainstr = LOADI val | LOAD string | ADD
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     8
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     9
type_synonym stack = "val list"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    10
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    11
abbreviation "hd2 xs == hd(tl xs)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    12
abbreviation "tl2 xs == tl(tl xs)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    13
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    14
text{* \noindent Abbreviations are transparent: they are unfolded after
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    15
parsing and folded back again before printing. Internally, they do not
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    16
exist. *}
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
fun aexec1 :: "ainstr \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    19
"aexec1 (LOADI n) _ stk  =  n # stk" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    20
"aexec1 (LOAD n) s stk  =  s(n) # stk" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    21
"aexec1  ADD _ stk  =  (hd2 stk + hd stk) # tl2 stk"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    22
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    23
fun aexec :: "ainstr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    24
"aexec [] _ stk = stk" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    25
"aexec (i#is) s stk = aexec is s (aexec1 i s stk)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    26
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    27
value "aexec [LOADI 5, LOAD ''y'', ADD]
43158
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    28
 [''x'' \<rightarrow> 42, ''y'' \<rightarrow> 43] [50]"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    29
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    30
lemma aexec_append[simp]:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    31
  "aexec (is1@is2) s stk = aexec is2 s (aexec is1 s stk)"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    32
apply(induct is1 arbitrary: stk)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    33
apply (auto)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    34
done
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    35
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    36
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    37
subsection "Compilation"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    38
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    39
fun acomp :: "aexp \<Rightarrow> ainstr list" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    40
"acomp (N n) = [LOADI n]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    41
"acomp (V x) = [LOAD x]" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    42
"acomp (Plus e1 e2) = acomp e1 @ acomp e2 @ [ADD]"
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
value "acomp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    45
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    46
theorem aexec_acomp[simp]: "aexec (acomp a) s stk = aval a s # stk"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    47
apply(induct a arbitrary: stk)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    48
apply (auto)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    49
done
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    50
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    51
end