src/HOL/MicroJava/J/Type.thy
author kleing
Thu Sep 21 10:42:49 2000 +0200 (2000-09-21)
changeset 10042 7164dc0d24d8
parent 8032 1eaae1a2f8ff
child 10061 fe82134773dc
permissions -rw-r--r--
unsymbolized
     1 (*  Title:      HOL/MicroJava/J/Type.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     5 
     6 Java types
     7 *)
     8 
     9 Type = JBasis +
    10 
    11 types	cname		(* class name *)
    12         vnam		(* variable or field name *)
    13 	mname		(* method name *)
    14 arities cname, vnam, mname :: term
    15 
    16 datatype vname		(* names for This pointer and local/field variables *)
    17 	= This
    18 	| VName   vnam
    19 
    20 datatype prim_ty       	(* primitive type, cf. 4.2 *)
    21 	= Void    	(* 'result type' of void methods *)
    22 	| Boolean
    23 	| Integer
    24 
    25 datatype ref_ty		(* reference type, cf. 4.3 *)
    26 	= NullT		(* null type, cf. 4.1 *)
    27 	| ClassT cname	(* class type *)
    28 datatype ty    		(* any type, cf. 4.1 *)
    29 	= PrimT prim_ty	(* primitive type *)
    30 	| RefT  ref_ty	(* reference type *)
    31 
    32 syntax
    33          NT     :: "          ty"
    34 	 Class	:: "cname  => ty"
    35 translations
    36 	"NT"      == "RefT   NullT"
    37 	"Class C" == "RefT (ClassT C)"
    38 
    39 end