equal
deleted
inserted
replaced
15 Pop |
15 Pop |
16 | Dup |
16 | Dup |
17 | Dup_x1 |
17 | Dup_x1 |
18 | Dup_x2 |
18 | Dup_x2 |
19 | Swap |
19 | Swap |
|
20 | ADD |
20 |
21 |
21 consts |
22 consts |
22 exec_os :: "[op_stack,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)" |
23 exec_os :: "[op_stack,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)" |
23 |
24 |
24 primrec |
25 primrec |
33 "exec_os Swap stk pc = |
34 "exec_os Swap stk pc = |
34 (let (val1,val2) = (hd stk,hd (tl stk)) |
35 (let (val1,val2) = (hd stk,hd (tl stk)) |
35 in |
36 in |
36 (val2#val1#(tl (tl stk)) , pc+1))" |
37 (val2#val1#(tl (tl stk)) , pc+1))" |
37 |
38 |
|
39 "exec_os ADD 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 |
38 end |
44 end |