Control.thy

Control = Runtime +

types 
 comp0 = "int => bool" 

datatype 
 cond_branch =
   If_ comp0 	int				(** Branch if val is zero/null **)
 | Ifnull    	int				(** Branch if val is not zero **)
 | Ifiacmpeq  	ins_type int (infixl 30)	(** Branch if int/ref comparison succeeds **)


datatype 
 uncond_branch =
   Goto		int

consts
 exec_cb :: "[cond_branch,opstack,p_count] => (opstack * p_count)" 
  
primrec
  "exec_cb (If_ cmp i) stk pc =
	(let val	= hd stk;
	     pc'	= if cmp (get_Intg val) then nat(int pc+i) else pc+1
	 in
	 (tl stk,pc'))"				

  "exec_cb (Ifnull i) stk pc =
	(let val	= hd stk;
	     pc'	= if val=Null then nat(int pc+i) else pc+1
	 in
	 (tl stk,pc'))"				

  "exec_cb (X Ifiacmpeq i) stk pc =
	(let (val1,val2) = (hd stk, hd (tl stk));
	     pc'	 = if val1 = val2 then nat(int pc+i) else pc+1
	 in
	 (tl (tl stk),pc'))"				


consts
 exec_ub :: "[uncond_branch,p_count] => p_count" 
primrec
  "exec_ub (Goto i) pc = nat(int pc+i)"

end