src/HOL/Bali/Value.thy
author haftmann
Fri Jun 11 17:14:02 2010 +0200 (2010-06-11)
changeset 37407 61dd8c145da7
parent 35431 8758fe1fc9f8
child 37956 ee939247b2fb
permissions -rw-r--r--
declare lex_prod_def [code del]
     1 (*  Title:      HOL/Bali/Value.thy
     2     Author:     David von Oheimb
     3 *)
     4 header {* Java values *}
     5 
     6 
     7 
     8 theory Value imports Type begin
     9 
    10 typedecl loc            --{* locations, i.e. abstract references on objects *}
    11 
    12 datatype val
    13         = Unit          --{* dummy result value of void methods *}
    14         | Bool bool     --{* Boolean value *}
    15         | Intg int      --{* integer value *}
    16         | Null          --{* null reference *}
    17         | Addr loc      --{* addresses, i.e. locations of objects *}
    18 
    19 
    20 consts   the_Bool   :: "val \<Rightarrow> bool"  
    21 primrec "the_Bool (Bool b) = b"
    22 consts   the_Intg   :: "val \<Rightarrow> int"
    23 primrec "the_Intg (Intg i) = i"
    24 consts   the_Addr   :: "val \<Rightarrow> loc"
    25 primrec "the_Addr (Addr a) = a"
    26 
    27 types   dyn_ty      = "loc \<Rightarrow> ty option"
    28 consts
    29   typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
    30   defpval       :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
    31   default_val   :: "     ty \<Rightarrow> val"  --{* default value for all types *}
    32 
    33 primrec "typeof dt  Unit    = Some (PrimT Void)"
    34         "typeof dt (Bool b) = Some (PrimT Boolean)"
    35         "typeof dt (Intg i) = Some (PrimT Integer)"
    36         "typeof dt  Null    = Some NT"
    37         "typeof dt (Addr a) = dt a"
    38 
    39 primrec "defpval Void    = Unit"
    40         "defpval Boolean = Bool False"
    41         "defpval Integer = Intg 0"
    42 primrec "default_val (PrimT pt) = defpval pt"
    43         "default_val (RefT  r ) = Null"
    44 
    45 end