src/HOL/MicroJava/J/Type.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 16417 9bc16273c2d4
child 35102 cc7a0b9f938c
permissions -rw-r--r--
Name.uu, Name.aT;
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
oheimb@11070
     5
*)
nipkow@8011
     6
kleing@12911
     7
header {* \isaheader{Java types} *}
nipkow@8011
     8
haftmann@16417
     9
theory Type imports JBasis begin
nipkow@8011
    10
kleing@12517
    11
typedecl cnam 
kleing@12517
    12
kleing@12517
    13
 -- "exceptions"
kleing@12517
    14
datatype 
kleing@12517
    15
  xcpt   
kleing@12517
    16
  = NullPointer
kleing@12517
    17
  | ClassCast
kleing@12517
    18
  | OutOfMemory
nipkow@8011
    19
kleing@12517
    20
-- "class names"
kleing@12517
    21
datatype cname  
kleing@12517
    22
  = Object 
kleing@12517
    23
  | Xcpt xcpt 
kleing@12951
    24
  | Cname cnam 
kleing@12517
    25
kleing@12517
    26
typedecl vnam   -- "variable or field name"
kleing@12517
    27
typedecl mname  -- "method name"
kleing@12517
    28
kleing@12517
    29
-- "names for @{text This} pointer and local/field variables"
kleing@12517
    30
datatype vname 
kleing@10061
    31
  = This
kleing@10061
    32
  | VName vnam
nipkow@8011
    33
kleing@12517
    34
-- "primitive type, cf. 4.2"
kleing@12517
    35
datatype prim_ty 
kleing@12517
    36
  = Void          -- "'result type' of void methods"
kleing@10061
    37
  | Boolean
kleing@10061
    38
  | Integer
nipkow@8011
    39
kleing@12517
    40
-- "reference type, cf. 4.3"
kleing@12517
    41
datatype ref_ty   
kleing@12517
    42
  = NullT         -- "null type, cf. 4.1"
kleing@12517
    43
  | ClassT cname  -- "class type"
kleing@10061
    44
kleing@12517
    45
-- "any type, cf. 4.1"
kleing@12517
    46
datatype ty 
kleing@12517
    47
  = PrimT prim_ty -- "primitive type"
kleing@12517
    48
  | RefT  ref_ty  -- "reference type"
nipkow@8011
    49
nipkow@8011
    50
syntax
kleing@12517
    51
  NT    :: "ty"
kleing@10069
    52
  Class :: "cname  => ty"
kleing@10061
    53
nipkow@8011
    54
translations
kleing@10069
    55
  "NT"      == "RefT NullT"
kleing@10069
    56
  "Class C" == "RefT (ClassT C)"
nipkow@8011
    57
nipkow@8011
    58
end