Data.thy

Data = Basic +

(** identifers **)

types
 ident
arities
 ident :: term

types
 cname = ident
 fname = ident
 mname = ident

consts
 Object :: cname


(** field descriptors **)

datatype			(** repr. type of a class or instance var. **)
 field_desc = I			(** integer **)
	    | L cname		(** object type **)
	    | A field_desc	(** array type **)  


(** method descriptors **)

datatype
 return_desc = V			(** void **)
	     | FT field_desc		


types
 param_desc  = field_desc list 

 method_desc = "param_desc * return_desc"

 method_loc  = "mname * param_desc"	
 field_loc   = "cname * fname"					



(** strings - distinguish between java-identifiers and field/method-descriptors **)

datatype
 string	= Id ident
	| Fd field_desc		
	| Md method_desc

constdefs
 get_Id :: "string => ident"
 "get_Id u == @mn. u = Id mn"
 get_Md :: "string => method_desc"
 "get_Md u == @ft. u = Md ft"
 get_Fd :: "string => field_desc"
 "get_Fd u == @ft. u = Fd ft"


consts
 type_of_str :: "string => field_desc"
primrec
 "type_of_str (Id idt) = L idt"
 "type_of_str (Fd fd)  = A fd"
 "type_of_str (Md md)  = arbitrary"


(** load/store instruction types **)

datatype
 ins_type = I_ | A_

end