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 |
|
21 consts |
|
22 exec_os :: "[op_stack,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)" |
|
23 |
|
24 primrec |
|
25 "exec_os Pop stk pc = (tl stk , pc+1)" |
|
26 |
|
27 "exec_os Dup stk pc = (hd stk # stk , pc+1)" |
|
28 |
|
29 "exec_os Dup_x1 stk pc = (hd stk # hd (tl stk) # hd stk # (tl (tl stk)) , pc+1)" |
|
30 |
|
31 "exec_os Dup_x2 stk pc = (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))) , pc+1)" |
|
32 |
|
33 "exec_os Swap stk pc = |
|
34 (let (val1,val2) = (hd stk,hd (tl stk)) |
|
35 in |
|
36 (val2#val1#(tl (tl stk)) , pc+1))" |
|
37 |
|
38 end |