| author | wenzelm |
| Wed, 10 Feb 2010 00:50:36 +0100 | |
| changeset 35069 | 09154b995ed8 |
| parent 32960 | 69916a850301 |
| child 35431 | 8758fe1fc9f8 |
| permissions | -rw-r--r-- |
| 12857 | 1 |
(* Title: HOL/Bali/Value.thy |
| 12854 | 2 |
Author: David von Oheimb |
3 |
*) |
|
4 |
header {* Java values *}
|
|
5 |
||
6 |
||
7 |
||
| 16417 | 8 |
theory Value imports Type begin |
| 12854 | 9 |
|
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset
|
10 |
typedecl loc --{* locations, i.e. abstract references on objects *}
|
| 12854 | 11 |
|
12 |
datatype val |
|
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
13 |
= Unit --{* dummy result value of void methods *}
|
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
14 |
| Bool bool --{* Boolean value *}
|
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
15 |
| Intg int --{* integer value *}
|
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
16 |
| Null --{* null reference *}
|
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
17 |
| Addr loc --{* addresses, i.e. locations of objects *}
|
| 12854 | 18 |
|
19 |
||
20 |
translations "val" <= (type) "Term.val" |
|
21 |
"loc" <= (type) "Term.loc" |
|
22 |
||
23 |
consts the_Bool :: "val \<Rightarrow> bool" |
|
24 |
primrec "the_Bool (Bool b) = b" |
|
25 |
consts the_Intg :: "val \<Rightarrow> int" |
|
26 |
primrec "the_Intg (Intg i) = i" |
|
27 |
consts the_Addr :: "val \<Rightarrow> loc" |
|
28 |
primrec "the_Addr (Addr a) = a" |
|
29 |
||
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
30 |
types dyn_ty = "loc \<Rightarrow> ty option" |
| 12854 | 31 |
consts |
32 |
typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option" |
|
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset
|
33 |
defpval :: "prim_ty \<Rightarrow> val" --{* default value for primitive types *}
|
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12858
diff
changeset
|
34 |
default_val :: " ty \<Rightarrow> val" --{* default value for all types *}
|
| 12854 | 35 |
|
36 |
primrec "typeof dt Unit = Some (PrimT Void)" |
|
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
37 |
"typeof dt (Bool b) = Some (PrimT Boolean)" |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
38 |
"typeof dt (Intg i) = Some (PrimT Integer)" |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
39 |
"typeof dt Null = Some NT" |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
40 |
"typeof dt (Addr a) = dt a" |
| 12854 | 41 |
|
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
42 |
primrec "defpval Void = Unit" |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
43 |
"defpval Boolean = Bool False" |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
44 |
"defpval Integer = Intg 0" |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
45 |
primrec "default_val (PrimT pt) = defpval pt" |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
17160
diff
changeset
|
46 |
"default_val (RefT r ) = Null" |
| 12854 | 47 |
|
48 |
end |