src/HOL/MicroJava/J/Type.thy
author wenzelm
Thu Feb 11 00:45:02 2010 +0100 (2010-02-11)
changeset 35102 cc7a0b9f938c
parent 16417 9bc16273c2d4
child 44035 322d1657c40c
permissions -rwxr-xr-x
modernized translations;
     1 (*  Title:      HOL/MicroJava/J/Type.thy
     2     Author:     David von Oheimb
     3     Copyright   1999 Technische Universitaet Muenchen
     4 *)
     5 
     6 header {* \isaheader{Java types} *}
     7 
     8 theory Type imports JBasis begin
     9 
    10 typedecl cnam 
    11 
    12  -- "exceptions"
    13 datatype 
    14   xcpt   
    15   = NullPointer
    16   | ClassCast
    17   | OutOfMemory
    18 
    19 -- "class names"
    20 datatype cname  
    21   = Object 
    22   | Xcpt xcpt 
    23   | Cname cnam 
    24 
    25 typedecl vnam   -- "variable or field name"
    26 typedecl mname  -- "method name"
    27 
    28 -- "names for @{text This} pointer and local/field variables"
    29 datatype vname 
    30   = This
    31   | VName vnam
    32 
    33 -- "primitive type, cf. 4.2"
    34 datatype prim_ty 
    35   = Void          -- "'result type' of void methods"
    36   | Boolean
    37   | Integer
    38 
    39 -- "reference type, cf. 4.3"
    40 datatype ref_ty   
    41   = NullT         -- "null type, cf. 4.1"
    42   | ClassT cname  -- "class type"
    43 
    44 -- "any type, cf. 4.1"
    45 datatype ty 
    46   = PrimT prim_ty -- "primitive type"
    47   | RefT  ref_ty  -- "reference type"
    48 
    49 abbreviation NT :: ty
    50   where "NT == RefT NullT"
    51 
    52 abbreviation Class :: "cname  => ty"
    53   where "Class C == RefT (ClassT C)"
    54 
    55 end