src/HOL/MicroJava/J/Type.thy
author nipkow
Thu Nov 25 12:01:28 1999 +0100 (1999-11-25)
changeset 8032 1eaae1a2f8ff
parent 8011 d14c4e9e9c8e
child 10042 7164dc0d24d8
permissions -rw-r--r--
Minor mods.
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"
nipkow@8011
    34
	 Class	:: "cname  \\<Rightarrow> 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