src/HOL/Bali/Type.thy
changeset 32960 69916a850301
parent 16417 9bc16273c2d4
child 35067 af4c18c30593
equal deleted inserted replaced
32959:23a8c5ac35f8 32960:69916a850301
    13 \item only the most important primitive types
    13 \item only the most important primitive types
    14 \item the null type is regarded as reference type
    14 \item the null type is regarded as reference type
    15 \end{itemize}
    15 \end{itemize}
    16 *}
    16 *}
    17 
    17 
    18 datatype prim_ty       	--{* primitive type, cf. 4.2 *}
    18 datatype prim_ty        --{* primitive type, cf. 4.2 *}
    19 	= Void    	--{* result type of void methods *}
    19         = Void          --{* result type of void methods *}
    20 	| Boolean
    20         | Boolean
    21 	| Integer
    21         | Integer
    22 
    22 
    23 
    23 
    24 datatype ref_ty		--{* reference type, cf. 4.3 *}
    24 datatype ref_ty         --{* reference type, cf. 4.3 *}
    25 	= NullT		--{* null type, cf. 4.1 *}
    25         = NullT         --{* null type, cf. 4.1 *}
    26 	| IfaceT qtname	--{* interface type *}
    26         | IfaceT qtname --{* interface type *}
    27 	| ClassT qtname	--{* class type *}
    27         | ClassT qtname --{* class type *}
    28 	| ArrayT ty	--{* array type *}
    28         | ArrayT ty     --{* array type *}
    29 
    29 
    30 and ty	    		--{* any type, cf. 4.1 *}
    30 and ty                  --{* any type, cf. 4.1 *}
    31 	= PrimT prim_ty	--{* primitive type *}
    31         = PrimT prim_ty --{* primitive type *}
    32 	| RefT  ref_ty	--{* reference type *}
    32         | RefT  ref_ty  --{* reference type *}
    33 
    33 
    34 translations
    34 translations
    35   "prim_ty" <= (type) "Type.prim_ty"
    35   "prim_ty" <= (type) "Type.prim_ty"
    36   "ref_ty"  <= (type) "Type.ref_ty"
    36   "ref_ty"  <= (type) "Type.ref_ty"
    37   "ty"      <= (type) "Type.ty"
    37   "ty"      <= (type) "Type.ty"
    38 
    38 
    39 syntax
    39 syntax
    40 	 NT	:: "       \<spacespace> ty"
    40          NT     :: "       \<spacespace> ty"
    41 	 Iface	:: "qtname  \<Rightarrow> ty"
    41          Iface  :: "qtname  \<Rightarrow> ty"
    42 	 Class	:: "qtname  \<Rightarrow> ty"
    42          Class  :: "qtname  \<Rightarrow> ty"
    43 	 Array	:: "ty     \<Rightarrow> ty"	("_.[]" [90] 90)
    43          Array  :: "ty     \<Rightarrow> ty"    ("_.[]" [90] 90)
    44 
    44 
    45 translations
    45 translations
    46 	"NT"      == "RefT   NullT"
    46         "NT"      == "RefT   NullT"
    47 	"Iface I" == "RefT (IfaceT I)"
    47         "Iface I" == "RefT (IfaceT I)"
    48 	"Class C" == "RefT (ClassT C)"
    48         "Class C" == "RefT (ClassT C)"
    49 	"T.[]"    == "RefT (ArrayT T)"
    49         "T.[]"    == "RefT (ArrayT T)"
    50 
    50 
    51 constdefs
    51 constdefs
    52   the_Class :: "ty \<Rightarrow> qtname"
    52   the_Class :: "ty \<Rightarrow> qtname"
    53  "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
    53  "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
    54  
    54