equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/JVM/Opstack.thy |
|
2 ID: $Id$ |
|
3 Author: Cornelia Pusch |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 |
|
6 Manipulation of operand stack |
|
7 *) |
|
8 |
|
9 Opstack = JVMState + |
|
10 |
|
11 (** instructions for the direct manipulation of the operand stack **) |
|
12 |
|
13 datatype |
|
14 op_stack = |
|
15 Pop |
|
16 | Dup |
|
17 | Dup_x1 |
|
18 | Dup_x2 |
|
19 | Swap |
|
20 | IAdd |
|
21 |
|
22 consts |
|
23 exec_os :: "[op_stack,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)" |
|
24 |
|
25 primrec |
|
26 "exec_os Pop stk pc = (tl stk , pc+1)" |
|
27 |
|
28 "exec_os Dup stk pc = (hd stk # stk , pc+1)" |
|
29 |
|
30 "exec_os Dup_x1 stk pc = (hd stk # hd (tl stk) # hd stk # (tl (tl stk)) , pc+1)" |
|
31 |
|
32 "exec_os Dup_x2 stk pc = (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))) , pc+1)" |
|
33 |
|
34 "exec_os Swap stk pc = |
|
35 (let (val1,val2) = (hd stk,hd (tl stk)) |
|
36 in |
|
37 (val2#val1#(tl (tl stk)) , pc+1))" |
|
38 |
|
39 "exec_os IAdd stk pc = |
|
40 (let (val1,val2) = (hd stk,hd (tl stk)) |
|
41 in |
|
42 (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), pc+1))" |
|
43 |
|
44 end |
|