src/HOL/Bali/Type.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 16417 9bc16273c2d4
child 32960 69916a850301
permissions -rw-r--r--
simplified code generator setup
     1 (*  Title:      HOL/Bali/Type.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4 *)
     5 
     6 header {* Java types *}
     7 
     8 theory Type imports Name begin
     9 
    10 text {*
    11 simplifications:
    12 \begin{itemize}
    13 \item only the most important primitive types
    14 \item the null type is regarded as reference type
    15 \end{itemize}
    16 *}
    17 
    18 datatype prim_ty       	--{* primitive type, cf. 4.2 *}
    19 	= Void    	--{* result type of void methods *}
    20 	| Boolean
    21 	| Integer
    22 
    23 
    24 datatype ref_ty		--{* reference type, cf. 4.3 *}
    25 	= NullT		--{* null type, cf. 4.1 *}
    26 	| IfaceT qtname	--{* interface type *}
    27 	| ClassT qtname	--{* class type *}
    28 	| ArrayT ty	--{* array type *}
    29 
    30 and ty	    		--{* any type, cf. 4.1 *}
    31 	= PrimT prim_ty	--{* primitive type *}
    32 	| RefT  ref_ty	--{* reference type *}
    33 
    34 translations
    35   "prim_ty" <= (type) "Type.prim_ty"
    36   "ref_ty"  <= (type) "Type.ref_ty"
    37   "ty"      <= (type) "Type.ty"
    38 
    39 syntax
    40 	 NT	:: "       \<spacespace> ty"
    41 	 Iface	:: "qtname  \<Rightarrow> ty"
    42 	 Class	:: "qtname  \<Rightarrow> ty"
    43 	 Array	:: "ty     \<Rightarrow> ty"	("_.[]" [90] 90)
    44 
    45 translations
    46 	"NT"      == "RefT   NullT"
    47 	"Iface I" == "RefT (IfaceT I)"
    48 	"Class C" == "RefT (ClassT C)"
    49 	"T.[]"    == "RefT (ArrayT T)"
    50 
    51 constdefs
    52   the_Class :: "ty \<Rightarrow> qtname"
    53  "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
    54  
    55 lemma the_Class_eq [simp]: "the_Class (Class C)= C"
    56 by (auto simp add: the_Class_def)
    57 
    58 end