src/HOL/MicroJava/J/Type.thy
author kleing
Fri Sep 22 16:28:53 2000 +0200 (2000-09-22)
changeset 10061 fe82134773dc
parent 10042 7164dc0d24d8
child 10069 c7226e6f9625
permissions -rw-r--r--
added HTML syntax; added spaces in normal syntax for better documents
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
nipkow@8011
    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
nipkow@8011
    26
datatype ref_ty		(* reference type, cf. 4.3 *)
kleing@10061
    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@10061
    36
	Class	:: "cname  => ty"
kleing@10061
    37
nipkow@8011
    38
translations
kleing@10061
    39
	"NT"      == "RefT NullT"
nipkow@8011
    40
	"Class C" == "RefT (ClassT C)"
nipkow@8011
    41
nipkow@8011
    42
end