equal
deleted
inserted
replaced
12 instr = LS load_and_store |
12 instr = LS load_and_store |
13 | CO create_object |
13 | CO create_object |
14 | MO manipulate_object |
14 | MO manipulate_object |
15 | CH check_object |
15 | CH check_object |
16 | MI meth_inv |
16 | MI meth_inv |
17 | MR |
17 | MR meth_ret |
18 | OS op_stack |
18 | OS op_stack |
19 | BR branch |
19 | BR branch |
20 |
20 |
21 types |
21 types |
22 bytecode = instr list |
22 bytecode = instr list |
49 |
49 |
50 | MI ins \\<Rightarrow> (let (xp',frs',stk',pc') = exec_mi ins G hp stk pc |
50 | MI ins \\<Rightarrow> (let (xp',frs',stk',pc') = exec_mi ins G hp stk pc |
51 in |
51 in |
52 (xp',hp,frs'@(stk',loc,cn,ml,pc')#frs)) |
52 (xp',hp,frs'@(stk',loc,cn,ml,pc')#frs)) |
53 |
53 |
54 | MR \\<Rightarrow> (let frs' = exec_mr stk frs in |
54 | MR ins \\<Rightarrow> (let frs' = exec_mr ins stk frs in |
55 (None,hp,frs')) |
55 (None,hp,frs')) |
56 |
56 |
57 | OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc |
57 | OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc |
58 in |
58 in |
59 (None,hp,(stk',loc,cn,ml,pc')#frs)) |
59 (None,hp,(stk',loc,cn,ml,pc')#frs)) |