Theory JavaType

(*  Title:       Jive Data and Store Model
    ID:          $Id: JavaType.thy,v 1.4 2006/05/18 14:19:23 lsf37 Exp $
    Author:      Norbert Schirmer <schirmer at informatik.tu-muenchen.de>, 2003
    Maintainer:  Nicole Rauch <rauch at informatik.uni-kl.de>
    License:     LGPL
*)

header {* Java-Type *}
 
theory JavaType imports TypeIds  begin

text {* This theory formalizes the types that appear in a Java program. Note that
the types defined by the classes and interfaces are formalized via their identifiers.
This way, this theory is program-independent.
*}

text {* We only want to formalize one-dimensional arrays. Therefore, we 
describe the types that can be used as element types of arrays. This excludes
the \texttt{null} type and array types themselves. This way, we get a finite 
number
of types in our type hierarchy, and the subtype relations can be given
explicitly (see Sec. \ref{direct_subtype_relations}). 
If desired, this can be extended in the future by using Javatype as argument
type of the @{text ArrT} type constructor. This will yield infinitely many
types.
*}

datatype Arraytype = BoolAT | IntgAT | ShortAT | ByteAT
                  | CClassAT CTypeId | AClassAT ATypeId
                  | InterfaceAT ITypeId

datatype Javatype = BoolT | IntgT | ShortT | ByteT | NullT | ArrT Arraytype
                  | CClassT CTypeId | AClassT ATypeId
                  | InterfaceT ITypeId

text {* We need a function that widens @{typ Arraytype} to @{typ Javatype}.
*}

constdefs
  at2jt :: "Arraytype => Javatype"
  "at2jt at == case at of 
         BoolAT               => BoolT
       | IntgAT               => IntgT
       | ShortAT              => ShortT
       | ByteAT               => ByteT
       | CClassAT CTypeId     => CClassT CTypeId
       | AClassAT ATypeId     => AClassT ATypeId
       | InterfaceAT ITypeId  => InterfaceT ITypeId"
  
text {* We define two predicates that separate the primitive types and the 
class types.
*}
                             
consts 
   isprimitive:: "Javatype => bool"
   isclass:: "Javatype => bool"

primrec
"isprimitive BoolT = True"
"isprimitive IntgT = True"
"isprimitive ShortT = True"
"isprimitive ByteT = True"
"isprimitive NullT = False"
"isprimitive (ArrT T) = False"
"isprimitive (CClassT c) = False"
"isprimitive (AClassT c) = False"
"isprimitive (InterfaceT i) = False" 

primrec
"isclass BoolT = False"
"isclass IntgT = False"
"isclass ShortT = False"
"isclass ByteT = False"
"isclass NullT = False"
"isclass (ArrT T) = False"
"isclass (CClassT c) = True"
"isclass (AClassT c) = True"
"isclass (InterfaceT i) = False" 

end