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