src/HOL/MicroJava/J/Type.thy
author oheimb
Mon Feb 05 20:14:15 2001 +0100 (2001-02-05)
changeset 11070 cc421547e744
parent 11026 a50365d21144
child 12338 de0f4a63baa5
permissions -rw-r--r--
improved document (added headers etc)
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
oheimb@11070
     7
header "Java types"
nipkow@8011
     8
oheimb@11026
     9
theory Type = JBasis:
nipkow@8011
    10
oheimb@11026
    11
typedecl cname  (* class name *)
oheimb@11026
    12
typedecl vnam   (* variable or field name *)
oheimb@11026
    13
typedecl mname  (* method name *)
oheimb@11026
    14
arities  cname :: "term"
oheimb@11026
    15
         vnam  :: "term"
oheimb@11026
    16
         mname :: "term"
nipkow@8011
    17
kleing@10069
    18
datatype vname    (* names for This pointer and local/field variables *)
kleing@10061
    19
  = This
kleing@10061
    20
  | VName vnam
nipkow@8011
    21
kleing@10061
    22
datatype prim_ty  (* primitive type, cf. 4.2 *)
kleing@10061
    23
  = Void          (* 'result type' of void methods *)
kleing@10061
    24
  | Boolean
kleing@10061
    25
  | Integer
nipkow@8011
    26
kleing@10069
    27
datatype ref_ty   (* reference type, cf. 4.3 *)
kleing@10069
    28
  = NullT         (* null type, cf. 4.1 *)
kleing@10061
    29
  | ClassT cname  (* class type *)
kleing@10061
    30
kleing@10061
    31
datatype ty       (* any type, cf. 4.1 *)
kleing@10061
    32
  = PrimT prim_ty (* primitive type *)
kleing@10061
    33
  | RefT  ref_ty  (* reference type *)
nipkow@8011
    34
nipkow@8011
    35
syntax
kleing@10061
    36
  NT    :: "          ty"
kleing@10069
    37
  Class :: "cname  => ty"
kleing@10061
    38
nipkow@8011
    39
translations
kleing@10069
    40
  "NT"      == "RefT NullT"
kleing@10069
    41
  "Class C" == "RefT (ClassT C)"
nipkow@8011
    42
nipkow@8011
    43
end