src/HOL/MicroJava/J/Type.thy
author kleing
Thu, 21 Sep 2000 10:42:49 +0200
changeset 10042 7164dc0d24d8
parent 8032 1eaae1a2f8ff
child 10061 fe82134773dc
permissions -rw-r--r--
unsymbolized

(*  Title:      HOL/MicroJava/J/Type.thy
    ID:         $Id$
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

Java types
*)

Type = JBasis +

types	cname		(* class name *)
        vnam		(* variable or field name *)
	mname		(* method name *)
arities cname, vnam, mname :: term

datatype vname		(* names for This pointer and local/field variables *)
	= This
	| VName   vnam

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

datatype ref_ty		(* reference type, cf. 4.3 *)
	= NullT		(* null type, cf. 4.1 *)
	| ClassT cname	(* class type *)
datatype ty    		(* any type, cf. 4.1 *)
	= PrimT prim_ty	(* primitive type *)
	| RefT  ref_ty	(* reference type *)

syntax
         NT     :: "          ty"
	 Class	:: "cname  => ty"
translations
	"NT"      == "RefT   NullT"
	"Class C" == "RefT (ClassT C)"

end