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