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