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