author | wenzelm |
Sun, 16 Jan 2011 15:53:03 +0100 | |
changeset 41589 | bbd861837ebc |
parent 39758 | b8a53e3a0ee2 |
child 58249 | 180f1b3508ed |
permissions | -rw-r--r-- |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
1 |
(* Title: HOL/MicroJava/J/Value.thy |
41589 | 2 |
Author: David von Oheimb, Technische Universitaet Muenchen |
11070 | 3 |
*) |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
4 |
|
12911 | 5 |
header {* \isaheader{Java Values} *} |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
6 |
|
16417 | 7 |
theory Value imports Type begin |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
8 |
|
24783 | 9 |
typedecl loc' -- "locations, i.e. abstract references on objects" |
12517 | 10 |
|
11 |
datatype loc |
|
12 |
= XcptRef xcpt -- "special locations for pre-allocated system exceptions" |
|
24783 | 13 |
| Loc loc' -- "usual locations (references on objects)" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
14 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset
|
15 |
datatype val |
12517 | 16 |
= Unit -- "dummy result value of void methods" |
17 |
| Null -- "null reference" |
|
18 |
| Bool bool -- "Boolean value" |
|
19 |
| Intg int -- "integer value, name Intg instead of Int because |
|
20 |
of clash with HOL/Set.thy" |
|
21 |
| Addr loc -- "addresses, i.e. locations of objects " |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
22 |
|
39758 | 23 |
primrec the_Bool :: "val => bool" where |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
24 |
"the_Bool (Bool b) = b" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
25 |
|
39758 | 26 |
primrec the_Intg :: "val => int" where |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
27 |
"the_Intg (Intg i) = i" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
28 |
|
39758 | 29 |
primrec the_Addr :: "val => loc" where |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
30 |
"the_Addr (Addr a) = a" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
31 |
|
39758 | 32 |
primrec defpval :: "prim_ty => val" -- "default value for primitive types" where |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
33 |
"defpval Void = Unit" |
39758 | 34 |
| "defpval Boolean = Bool False" |
35 |
| "defpval Integer = Intg 0" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
36 |
|
39758 | 37 |
primrec default_val :: "ty => val" -- "default value for all types" where |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
38 |
"default_val (PrimT pt) = defpval pt" |
39758 | 39 |
| "default_val (RefT r ) = Null" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
40 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
41 |
end |