src/HOL/Bali/Value.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 17160 fb65eda72fc7
child 32960 69916a850301
permissions -rw-r--r--
simplified code generator setup
     1 (*  Title:      HOL/Bali/Value.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4 *)
     5 header {* Java values *}
     6 
     7 
     8 
     9 theory Value imports Type begin
    10 
    11 typedecl loc            --{* locations, i.e. abstract references on objects *}
    12 
    13 datatype val
    14 	= Unit          --{* dummy result value of void methods *}
    15 	| Bool bool     --{* Boolean value *}
    16 	| Intg int      --{* integer value *}
    17 	| Null          --{* null reference *}
    18 	| Addr loc      --{* addresses, i.e. locations of objects *}
    19 
    20 
    21 translations "val" <= (type) "Term.val"
    22              "loc" <= (type) "Term.loc"
    23 
    24 consts   the_Bool   :: "val \<Rightarrow> bool"  
    25 primrec "the_Bool (Bool b) = b"
    26 consts   the_Intg   :: "val \<Rightarrow> int"
    27 primrec "the_Intg (Intg i) = i"
    28 consts   the_Addr   :: "val \<Rightarrow> loc"
    29 primrec "the_Addr (Addr a) = a"
    30 
    31 types	dyn_ty      = "loc \<Rightarrow> ty option"
    32 consts
    33   typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
    34   defpval       :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
    35   default_val   :: "     ty \<Rightarrow> val"  --{* default value for all types *}
    36 
    37 primrec "typeof dt  Unit    = Some (PrimT Void)"
    38 	"typeof dt (Bool b) = Some (PrimT Boolean)"
    39 	"typeof dt (Intg i) = Some (PrimT Integer)"
    40 	"typeof dt  Null    = Some NT"
    41 	"typeof dt (Addr a) = dt a"
    42 
    43 primrec	"defpval Void    = Unit"
    44 	"defpval Boolean = Bool False"
    45 	"defpval Integer = Intg 0"
    46 primrec	"default_val (PrimT pt) = defpval pt"
    47 	"default_val (RefT  r ) = Null"
    48 
    49 end