1(*  Title:      HOL/Bali/Value.thy
2    Author:     David von Oheimb
3*)
4subsection \<open>Java values\<close>
5
6
7
8theory Value imports Type begin
9
10typedecl loc            \<comment> \<open>locations, i.e. abstract references on objects\<close>
11
12datatype 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
20primrec the_Bool :: "val \<Rightarrow> bool"
21  where "the_Bool (Bool b) = b"
22
23primrec the_Intg :: "val \<Rightarrow> int"
24  where "the_Intg (Intg i) = i"
25
26primrec the_Addr :: "val \<Rightarrow> loc"
27  where "the_Addr (Addr a) = a"
28
29type_synonym dyn_ty = "loc \<Rightarrow> ty option"
30
31primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
32where
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
39primrec defpval :: "prim_ty \<Rightarrow> val"  \<comment> \<open>default value for primitive types\<close>
40where
41  "defpval Void = Unit"
42| "defpval Boolean = Bool False"
43| "defpval Integer = Intg 0"
44
45primrec default_val :: "ty \<Rightarrow> val"  \<comment> \<open>default value for all types\<close>
46where
47  "default_val (PrimT pt) = defpval pt"
48| "default_val (RefT  r ) = Null"
49
50end
51