src/HOL/Bali/Value.thy
author wenzelm
Mon Jul 26 17:41:26 2010 +0200 (2010-07-26)
changeset 37956 ee939247b2fb
parent 35431 8758fe1fc9f8
child 41778 5f79a9e42507
permissions -rw-r--r--
modernized/unified some specifications;
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
wenzelm@37956
    20
primrec the_Bool :: "val \<Rightarrow> bool"
wenzelm@37956
    21
  where "the_Bool (Bool b) = b"
wenzelm@37956
    22
wenzelm@37956
    23
primrec the_Intg :: "val \<Rightarrow> int"
wenzelm@37956
    24
  where "the_Intg (Intg i) = i"
wenzelm@37956
    25
wenzelm@37956
    26
primrec the_Addr :: "val \<Rightarrow> loc"
wenzelm@37956
    27
  where "the_Addr (Addr a) = a"
schirmer@12854
    28
wenzelm@32960
    29
types   dyn_ty      = "loc \<Rightarrow> ty option"
wenzelm@37956
    30
wenzelm@37956
    31
primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
wenzelm@37956
    32
where
wenzelm@37956
    33
  "typeof dt  Unit = Some (PrimT Void)"
wenzelm@37956
    34
| "typeof dt (Bool b) = Some (PrimT Boolean)"
wenzelm@37956
    35
| "typeof dt (Intg i) = Some (PrimT Integer)"
wenzelm@37956
    36
| "typeof dt  Null = Some NT"
wenzelm@37956
    37
| "typeof dt (Addr a) = dt a"
schirmer@12854
    38
wenzelm@37956
    39
primrec defpval :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
wenzelm@37956
    40
where
wenzelm@37956
    41
  "defpval Void = Unit"
wenzelm@37956
    42
| "defpval Boolean = Bool False"
wenzelm@37956
    43
| "defpval Integer = Intg 0"
schirmer@12854
    44
wenzelm@37956
    45
primrec default_val :: "ty \<Rightarrow> val"  --{* default value for all types *}
wenzelm@37956
    46
where
wenzelm@37956
    47
  "default_val (PrimT pt) = defpval pt"
wenzelm@37956
    48
| "default_val (RefT  r ) = Null"
schirmer@12854
    49
schirmer@12854
    50
end