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");
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 *)
nipkow@8011
    14
kleing@10069
    15
datatype vname    (* names for This pointer and local/field variables *)
kleing@10061
    16
  = This
kleing@10061
    17
  | VName vnam
nipkow@8011
    18
kleing@10061
    19
datatype prim_ty  (* primitive type, cf. 4.2 *)
kleing@10061
    20
  = Void          (* 'result type' of void methods *)
kleing@10061
    21
  | Boolean
kleing@10061
    22
  | Integer
nipkow@8011
    23
kleing@10069
    24
datatype ref_ty   (* reference type, cf. 4.3 *)
kleing@10069
    25
  = NullT         (* null type, cf. 4.1 *)
kleing@10061
    26
  | ClassT cname  (* class type *)
kleing@10061
    27
kleing@10061
    28
datatype ty       (* any type, cf. 4.1 *)
kleing@10061
    29
  = PrimT prim_ty (* primitive type *)
kleing@10061
    30
  | RefT  ref_ty  (* reference type *)
nipkow@8011
    31
nipkow@8011
    32
syntax
kleing@10061
    33
  NT    :: "          ty"
kleing@10069
    34
  Class :: "cname  => ty"
kleing@10061
    35
nipkow@8011
    36
translations
kleing@10069
    37
  "NT"      == "RefT NullT"
kleing@10069
    38
  "Class C" == "RefT (ClassT C)"
nipkow@8011
    39
nipkow@8011
    40
end