equal
deleted
inserted
replaced
21 "exec_mi (Invoke mn ps) G hp stk pc = |
21 "exec_mi (Invoke mn ps) G hp stk pc = |
22 (let n = length ps; |
22 (let n = length ps; |
23 argsoref = take (n+1) stk; |
23 argsoref = take (n+1) stk; |
24 oref = last argsoref; |
24 oref = last argsoref; |
25 xp' = raise_xcpt (oref=Null) NullPointer; |
25 xp' = raise_xcpt (oref=Null) NullPointer; |
26 dynT = fst(hp \\<And> (the_Addr oref)); |
26 dynT = fst(hp !! (the_Addr oref)); |
27 (dc,mh,mxl,c)= the (cmethd (G,dynT) (mn,ps)); |
27 (dc,mh,mxl,c)= the (method (G,dynT) (mn,ps)); |
28 frs' = xcpt_update xp' [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] [] |
28 frs' = if xp'=None |
|
29 then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] |
|
30 else [] |
29 in |
31 in |
30 (xp' , frs' , drop (n+1) stk , pc+1))" |
32 (xp' , frs' , drop (n+1) stk , pc+1))" |
31 |
33 |
32 |
34 |
33 datatype |
35 datatype |