Cpool.thy

Cpool = Data +


(****************** constant pool p.92 ******************)

types
 cl_idx  = nat                                  (** idx to Class entry **)
 fr_idx  = nat                                  (** idx to Fieldref entry **)
 mr_idx  = nat                                  (** idx to Methodref entry **)
 im_idx  = nat                                  (** idx to InterMethref entry **)
 nt_idx  = nat                                  (** idx to NameAndType entry **)
 nm_idx  = nat                                  (** idx to Utf8 entry **)

datatype        
 cp_info = Class        nm_idx                
         | Fieldref     cl_idx nt_idx         
         | Methodref    cl_idx nt_idx         
         | InterMethref cl_idx nt_idx         
         | NameAndType  nm_idx nm_idx         
         | Utf8         string 


constdefs
 get_Class :: "cp_info => nm_idx" 
 "get_Class c == @i. c = Class i"

 get_Fieldref :: "cp_info => cl_idx * nt_idx" 
 "get_Fieldref c == @(i,j). c = Fieldref i j"

 get_Methodref :: "cp_info => cl_idx * nt_idx" 
 "get_Methodref c == @(i,j). c = Methodref i j"

 get_InterMethref :: "cp_info => cl_idx * nt_idx" 
 "get_InterMethref c == @(i,j). c = InterMethref i j"

 get_NameAndType :: "cp_info => nm_idx * nm_idx" 
 "get_NameAndType c == @(i,j). c = NameAndType i j"

 get_Utf8 :: "cp_info => string" 
 "get_Utf8 c == @i. c = Utf8 i"


types
 cpool	= cp_info list		


constdefs
 extract_Class :: "[cpool,cl_idx] => string"
 "extract_Class (cp::cpool) idx == 
	(let n_idx	= get_Class (cp ! idx);
	     cstr	= get_Utf8 (cp ! n_idx)
	 in
	 cstr)"


 extract_Fieldref :: "[cpool,fr_idx] => (cname * fname * field_desc)"
 "extract_Fieldref (cp::cpool) idx ==
	(let (c_idx,nt_idx)	= get_Fieldref (cp ! idx);
	     cid		= get_Id (extract_Class cp c_idx);
	     (n_idx,d_idx)	= get_NameAndType (cp ! nt_idx);
	     fid		= get_Id (get_Utf8 (cp ! n_idx));
	     fd			= get_Fd (get_Utf8 (cp ! d_idx))
	 in
         (cid,fid,fd))"


 extract_Methodref :: "[cpool,mr_idx] => (cname * mname * method_desc)"
 "extract_Methodref (cp::cpool) idx ==
	(let (c_idx,nt_idx)	= get_Methodref (cp ! idx);
	     cid		= get_Id (extract_Class cp c_idx);
	     (n_idx,d_idx)	= get_NameAndType (cp ! nt_idx);
	     mid		= get_Id (get_Utf8 (cp ! n_idx));
	     md			= get_Md (get_Utf8 (cp ! d_idx))
	 in
         (cid,mid,md))"
	
     
 extract_InterMethref :: "[cpool,im_idx] => (cname * mname * method_desc)"
   "extract_InterMethref (cp::cpool) idx ==
	(let (c_idx,nt_idx)	= get_InterMethref (cp ! idx);
	     cid		= get_Id (extract_Class cp c_idx);
	     (n_idx,d_idx)	= get_NameAndType (cp ! nt_idx);
	     mid		= get_Id (get_Utf8 (cp ! n_idx));
	     md			= get_Md (get_Utf8 (cp ! d_idx))
	 in
         (cid,mid,md))"

end