Type.thy

(*  Title:      isabelle/Bali/Type.thy
    ID:         $Id: Type.thy,v 1.2 1997/10/22 12:00:12 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	tname		(* type name, i.e. class or interface name *)
        ename		(* expression name, i.e. variable or field name *)
	mname		(* method name *)
arities tname, ename, mname :: term

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
	 Iface	:: "tname  => ty"
	 Class	:: "tname  => ty"
	 Array	:: "ref_ty => ty"	("_[.]" [90] 90)
translations
	"Iface I" == "RefT (IfaceT I)"
	"Class C" == "RefT (ClassT C)"
	"T[.]" == "RefT (ArrayT T)"

end