src/HOL/MicroJava/J/Type.thy
author wenzelm
Sat Dec 01 18:52:32 2001 +0100 (2001-12-01)
changeset 12338 de0f4a63baa5
parent 11070 cc421547e744
child 12517 360e3215f029
permissions -rw-r--r--
renamed class "term" to "type" (actually "HOL.type");
     1 (*  Title:      HOL/MicroJava/J/Type.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     6 
     7 header "Java types"
     8 
     9 theory Type = JBasis:
    10 
    11 typedecl cname  (* class name *)
    12 typedecl vnam   (* variable or field name *)
    13 typedecl mname  (* method name *)
    14 
    15 datatype vname    (* names for This pointer and local/field variables *)
    16   = This
    17   | VName vnam
    18 
    19 datatype prim_ty  (* primitive type, cf. 4.2 *)
    20   = Void          (* 'result type' of void methods *)
    21   | Boolean
    22   | Integer
    23 
    24 datatype ref_ty   (* reference type, cf. 4.3 *)
    25   = NullT         (* null type, cf. 4.1 *)
    26   | ClassT cname  (* class type *)
    27 
    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 
    36 translations
    37   "NT"      == "RefT NullT"
    38   "Class C" == "RefT (ClassT C)"
    39 
    40 end