65 frs' = if xp'=None then |
65 frs' = if xp'=None then |
66 [([],rev argsoref@replicate mxl undefined,dc,(mn,ps),0)] |
66 [([],rev argsoref@replicate mxl undefined,dc,(mn,ps),0)] |
67 else [] |
67 else [] |
68 in |
68 in |
69 (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" | |
69 (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" | |
70 -- "Because exception handling needs the pc of the Invoke instruction," |
70 \<comment> "Because exception handling needs the pc of the Invoke instruction," |
71 -- "Invoke doesn't change stk and pc yet (@{text Return} does that)." |
71 \<comment> "Invoke doesn't change stk and pc yet (\<open>Return\<close> does that)." |
72 |
72 |
73 "exec_instr Return G hp stk0 vars Cl sig0 pc frs = |
73 "exec_instr Return G hp stk0 vars Cl sig0 pc frs = |
74 (if frs=[] then |
74 (if frs=[] then |
75 (None, hp, []) |
75 (None, hp, []) |
76 else |
76 else |
77 let val = hd stk0; (stk,loc,C,sig,pc) = hd frs; |
77 let val = hd stk0; (stk,loc,C,sig,pc) = hd frs; |
78 (mn,pt) = sig0; n = length pt |
78 (mn,pt) = sig0; n = length pt |
79 in |
79 in |
80 (None, hp, (val#(drop (n+1) stk),loc,C,sig,pc+1)#tl frs))" |
80 (None, hp, (val#(drop (n+1) stk),loc,C,sig,pc+1)#tl frs))" |
81 -- "Return drops arguments from the caller's stack and increases" |
81 \<comment> "Return drops arguments from the caller's stack and increases" |
82 -- "the program counter in the caller" | |
82 \<comment> "the program counter in the caller" | |
83 |
83 |
84 "exec_instr Pop G hp stk vars Cl sig pc frs = |
84 "exec_instr Pop G hp stk vars Cl sig pc frs = |
85 (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)" | |
85 (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)" | |
86 |
86 |
87 "exec_instr Dup G hp stk vars Cl sig pc frs = |
87 "exec_instr Dup G hp stk vars Cl sig pc frs = |