src/HOL/Bali/Value.thy
author wenzelm
Mon Jan 28 18:50:23 2002 +0100 (2002-01-28)
changeset 12857 a4386cc9b1c3
parent 12854 00d4a435777f
child 12858 6214f03d6d27
permissions -rw-r--r--
tuned header;
     1 (*  Title:      HOL/Bali/Value.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1997 Technische Universitaet Muenchen
     5 *)
     6 header {* Java values *}
     7 
     8 
     9 
    10 theory Value = Type:
    11 
    12 typedecl loc            (* locations, i.e. abstract references on objects *)
    13 arities	 loc :: "type"
    14 
    15 datatype val
    16 	= Unit          (* dummy result value of void methods *)
    17 	| Bool bool     (* Boolean value *)
    18 	| Intg int      (* integer value *)
    19 	| Null          (* null reference *)
    20 	| Addr loc      (* addresses, i.e. locations of objects *)
    21 
    22 
    23 translations "val" <= (type) "Term.val"
    24              "loc" <= (type) "Term.loc"
    25 
    26 consts   the_Bool   :: "val \<Rightarrow> bool"  
    27 primrec "the_Bool (Bool b) = b"
    28 consts   the_Intg   :: "val \<Rightarrow> int"
    29 primrec "the_Intg (Intg i) = i"
    30 consts   the_Addr   :: "val \<Rightarrow> loc"
    31 primrec "the_Addr (Addr a) = a"
    32 
    33 types	dyn_ty      = "loc \<Rightarrow> ty option"
    34 consts
    35   typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
    36   defpval       :: "prim_ty \<Rightarrow> val"      (* default value for primitive types *)
    37   default_val   :: "     ty \<Rightarrow> val"      (* default value for all types *)
    38 
    39 primrec "typeof dt  Unit    = Some (PrimT Void)"
    40 	"typeof dt (Bool b) = Some (PrimT Boolean)"
    41 	"typeof dt (Intg i) = Some (PrimT Integer)"
    42 	"typeof dt  Null    = Some NT"
    43 	"typeof dt (Addr a) = dt a"
    44 
    45 primrec	"defpval Void    = Unit"
    46 	"defpval Boolean = Bool False"
    47 	"defpval Integer = Intg 0"
    48 primrec	"default_val (PrimT pt) = defpval pt"
    49 	"default_val (RefT  r ) = Null"
    50 
    51 end