Opstack.thy

Back to the index of JVM0_ASCII
Opstack = Runtime +

(** instructions for the direct manipulation of the operand stack **)

datatype 
 op_stack = 
   Pop
 | Dup
 | Swap
	  
consts
 exec_os :: "[op_stack,opstack,p_count] => (opstack * p_count)" 

primrec 
  "exec_os Pop stk pc = (tl stk , pc+1)"

  "exec_os Dup stk pc = (hd stk # stk , pc+1)"

  "exec_os Swap stk pc = 
	(let (val1,val2) = (hd stk,hd (tl stk))
	 in
	 (val2#val1#(tl (tl stk)) , pc+1))"

end