Type.thy

(*  Title:      isabelle/Bali/Type.thy
    ID:         $Id: Type.thy,v 1.7 1998/04/08 15:27:09 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

Java types

simplifications:
* few primitive types yet
* arrays do not have special methods and fields like length
*)

Type = Table +

(* for names, cf. 6.5 *)
types	tnam		(* type name, i.e. class or interface name *)
        enam		(* expression name, i.e. variable or field name *)
	mname		(* method name *)
arities tnam, enam, mname :: term

datatype xname		(* names of system exceptions *)
	= Throwable
	| NullPointer | OutOfMemory | ClassCast   
	| NegArrSize  | IndOutBound | ArrStore

datatype tname		(* type names for system classes and other type names *)
	= Object
	| SXcpt   xname
	| TName   tnam

datatype ename		(* names for the This pointer and local variables *)
	= This
	| EName   enam


datatype prim_ty       	(* primitive type, cf. 4.2 *)
	= Void    	(* 'result type' of void methods *)
	| Boolean
	| IntDefer

(** parameter 'a circumvents mutual recursion with datatype ty **)
datatype 'a Rt 		(* reference type, cf. 4.3 *)
	= NullT		(* null type, cf. 4.1 *)
	| IfaceT tname	(* interface type *)
	| ClassT tname	(* class type *)
	| ArrayT 'a	(* array type *)

datatype ty    		(* any type, cf. 4.1 *)
	= PrimT prim_ty	(* primitive type *)
	| RefT (ty Rt)	(* reference type *)






types
	 ref_ty = ty Rt

translations
	"ref_ty" <= (type) "ty Rt"

syntax
	 NT	:: "          ty"
	 Iface	:: "tname  => ty"
	 Class	:: "tname  => ty"
	 Array	:: "ref_ty => ty"	("_[.]" [90] 90)

translations
	"NT"      == "RefT   NullT"
	"Iface I" == "RefT (IfaceT I)"
	"Class C" == "RefT (ClassT C)"
	"T[.]"    == "RefT (ArrayT T)"

end