12854
|
1 |
(* Title: isabelle/Bali/Value.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
|
4 |
Copyright 1997 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
header {* Java values *}
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
theory Value = Type:
|
|
11 |
|
|
12 |
typedecl loc (* locations, i.e. abstract references on objects *)
|
|
13 |
arities loc :: "type"
|
|
14 |
|
|
15 |
datatype val
|
|
16 |
= Unit (* dummy result value of void methods *)
|
|
17 |
| Bool bool (* Boolean value *)
|
|
18 |
| Intg int (* integer value *)
|
|
19 |
| Null (* null reference *)
|
|
20 |
| Addr loc (* addresses, i.e. locations of objects *)
|
|
21 |
|
|
22 |
|
|
23 |
translations "val" <= (type) "Term.val"
|
|
24 |
"loc" <= (type) "Term.loc"
|
|
25 |
|
|
26 |
consts the_Bool :: "val \<Rightarrow> bool"
|
|
27 |
primrec "the_Bool (Bool b) = b"
|
|
28 |
consts the_Intg :: "val \<Rightarrow> int"
|
|
29 |
primrec "the_Intg (Intg i) = i"
|
|
30 |
consts the_Addr :: "val \<Rightarrow> loc"
|
|
31 |
primrec "the_Addr (Addr a) = a"
|
|
32 |
|
|
33 |
types dyn_ty = "loc \<Rightarrow> ty option"
|
|
34 |
consts
|
|
35 |
typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
|
|
36 |
defpval :: "prim_ty \<Rightarrow> val" (* default value for primitive types *)
|
|
37 |
default_val :: " ty \<Rightarrow> val" (* default value for all types *)
|
|
38 |
|
|
39 |
primrec "typeof dt Unit = Some (PrimT Void)"
|
|
40 |
"typeof dt (Bool b) = Some (PrimT Boolean)"
|
|
41 |
"typeof dt (Intg i) = Some (PrimT Integer)"
|
|
42 |
"typeof dt Null = Some NT"
|
|
43 |
"typeof dt (Addr a) = dt a"
|
|
44 |
|
|
45 |
primrec "defpval Void = Unit"
|
|
46 |
"defpval Boolean = Bool False"
|
|
47 |
"defpval Integer = Intg 0"
|
|
48 |
primrec "default_val (PrimT pt) = defpval pt"
|
|
49 |
"default_val (RefT r ) = Null"
|
|
50 |
|
|
51 |
end
|