Theory Type

(*  Title:      HOL/MicroJava/J/Type.thy
    ID:         $Id: Type.thy,v 1.12 2005/06/17 14:13:09 haftmann Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* \isaheader{Java types} *}

theory Type imports JBasis begin

-- "typedecl cnam changed to:"
types cnam = string

 -- "exceptions"
datatype 
  xcpt   
  = NullPointer
  | ClassCast
  | OutOfMemory
  | ArrayIndexOutOfBounds
  | NegativeArraySize
  | ArrayStore

-- "class names"
datatype cname  
  = Object 
  | Xcpt xcpt 
  | Cname cnam 

-- "variable or field name"
-- "typedecl vnam  changed to"
types vnam  = string

-- "method name"
-- "typedecl mname  changed to"
types mname = string 

-- "names for @{text This} pointer and local/field variables"
datatype vname 
  = This
  | VName vnam

-- "primitive type, cf. 4.2"
datatype prim_ty 
  = Void          -- "'result type' of void methods"
  | Boolean
  | Integer
  | RetA nat      -- "bytecode return addresses"

-- "reference type, cf. 4.3"
datatype ref_ty   
  = NullT         -- "null type, cf. 4.1"
  | ClassT cname  -- "class type"
  | ArrayT ty     -- "array type"
-- "any type, cf. 4.1"
and ty 
  = PrimT prim_ty -- "primitive type"
  | RefT  ref_ty  -- "reference type"

syntax
  NT    :: "ty"
  Class :: "cname  => ty"
  RA    :: "nat => ty"
  Array :: "ty => ty" ("_.[]" [90] 90)

translations
  "NT"      == "RefT NullT"
  "Class C" == "RefT (ClassT C)"
  "T.[]"    == "RefT (ArrayT T)"
  "RA pc"   == "PrimT (RetA pc)"

consts
  the_Class :: "ty => cname"
  isArray :: "ty => bool"

recdef the_Class "{}"
  "the_Class (Class C) = C"
  "the_Class (T.[]) = Object"

recdef isArray "{}"
  "isArray (T.[]) = True"
  "isArray T      = False"


end