| 
5377
 | 
     1  | 
consts exec :: ('a => 'v) => 'v list => (('a,'v) instr) list => 'v list
 | 
| 
 | 
     2  | 
primrec
  | 
| 
 | 
     3  | 
"exec s vs [] = vs"
  | 
| 
 | 
     4  | 
"exec s vs (i#is) = (case i of
  | 
| 
 | 
     5  | 
    Const v  => exec s (v#vs) is
  | 
| 
 | 
     6  | 
  | Load a   => exec s ((s a)#vs) is
  | 
| 
 | 
     7  | 
  | Apply f  => exec s ( (f (hd vs) (hd(tl vs)))#(tl(tl vs)) ) is)"
  |