src/HOL/Bali/Value.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (22 months ago)
changeset 66983 df83b66f1d94
parent 62042 6c6ccf573479
child 67443 3abf6a722518
permissions -rw-r--r--
proper merge (amending fb46c031c841);
     1 (*  Title:      HOL/Bali/Value.thy
     2     Author:     David von Oheimb
     3 *)
     4 subsection \<open>Java values\<close>
     5 
     6 
     7 
     8 theory Value imports Type begin
     9 
    10 typedecl loc            \<comment>\<open>locations, i.e. abstract references on objects\<close>
    11 
    12 datatype val
    13         = Unit          \<comment>\<open>dummy result value of void methods\<close>
    14         | Bool bool     \<comment>\<open>Boolean value\<close>
    15         | Intg int      \<comment>\<open>integer value\<close>
    16         | Null          \<comment>\<open>null reference\<close>
    17         | Addr loc      \<comment>\<open>addresses, i.e. locations of objects\<close>
    18 
    19 
    20 primrec the_Bool :: "val \<Rightarrow> bool"
    21   where "the_Bool (Bool b) = b"
    22 
    23 primrec the_Intg :: "val \<Rightarrow> int"
    24   where "the_Intg (Intg i) = i"
    25 
    26 primrec the_Addr :: "val \<Rightarrow> loc"
    27   where "the_Addr (Addr a) = a"
    28 
    29 type_synonym dyn_ty = "loc \<Rightarrow> ty option"
    30 
    31 primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
    32 where
    33   "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 :: "prim_ty \<Rightarrow> val"  \<comment>\<open>default value for primitive types\<close>
    40 where
    41   "defpval Void = Unit"
    42 | "defpval Boolean = Bool False"
    43 | "defpval Integer = Intg 0"
    44 
    45 primrec default_val :: "ty \<Rightarrow> val"  \<comment>\<open>default value for all types\<close>
    46 where
    47   "default_val (PrimT pt) = defpval pt"
    48 | "default_val (RefT  r ) = Null"
    49 
    50 end