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
     1 (*  Title:      HOL/MicroJava/J/Type.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     5 
     6 Java types
     7 *)
     8 
     9 Type = JBasis +
    10 
    11 types cname   (* class name *)
    12       vnam    (* variable or field name *)
    13       mname   (* method name *)
    14 
    15 arities cname, vnam, mname :: term
    16 
    17 datatype vname    (* names for This pointer and local/field variables *)
    18   = This
    19   | VName vnam
    20 
    21 datatype prim_ty  (* primitive type, cf. 4.2 *)
    22   = Void          (* 'result type' of void methods *)
    23   | Boolean
    24   | Integer
    25 
    26 datatype ref_ty   (* reference type, cf. 4.3 *)
    27   = NullT         (* null type, cf. 4.1 *)
    28   | ClassT cname  (* class type *)
    29 
    30 datatype ty       (* any type, cf. 4.1 *)
    31   = PrimT prim_ty (* primitive type *)
    32   | RefT  ref_ty  (* reference type *)
    33 
    34 syntax
    35   NT    :: "          ty"
    36   Class :: "cname  => ty"
    37 
    38 translations
    39   "NT"      == "RefT NullT"
    40   "Class C" == "RefT (ClassT C)"
    41 
    42 end