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 | IAdd |
21 |
21 |
22 consts |
22 consts |
23 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)" |
24 |
24 |
25 primrec |
25 primrec |
34 "exec_os Swap stk pc = |
34 "exec_os Swap stk pc = |
35 (let (val1,val2) = (hd stk,hd (tl stk)) |
35 (let (val1,val2) = (hd stk,hd (tl stk)) |
36 in |
36 in |
37 (val2#val1#(tl (tl stk)) , pc+1))" |
37 (val2#val1#(tl (tl stk)) , pc+1))" |
38 |
38 |
39 "exec_os ADD stk pc = |
39 "exec_os IAdd stk pc = |
40 (let (val1,val2) = (hd stk,hd (tl stk)) |
40 (let (val1,val2) = (hd stk,hd (tl stk)) |
41 in |
41 in |
42 (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), pc+1))" |
42 (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), pc+1))" |
43 |
43 |
44 end |
44 end |