author | wenzelm |
Sun, 02 Nov 2014 17:58:35 +0100 | |
changeset 58886 | 8a6cac7c7247 |
parent 58310 | 91ea607a34d8 |
child 61169 | 4de9ff3ea29a |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/Type.thy |
2 |
Author: David von Oheimb |
|
3 |
Copyright 1999 Technische Universitaet Muenchen |
|
11070 | 4 |
*) |
8011 | 5 |
|
58886 | 6 |
section {* Java types *} |
8011 | 7 |
|
16417 | 8 |
theory Type imports JBasis begin |
8011 | 9 |
|
12517 | 10 |
typedecl cnam |
47394 | 11 |
|
12 |
instantiation cnam :: equal |
|
13 |
begin |
|
14 |
||
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
15 |
definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'" |
47394 | 16 |
instance by default (simp add: equal_cnam_def) |
17 |
||
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
18 |
end |
47394 | 19 |
|
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
20 |
text {* These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME *} |
47394 | 21 |
|
22 |
instantiation cnam :: typerep |
|
23 |
begin |
|
24 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
25 |
definition "typerep_class.typerep \<equiv> \<lambda>_ :: cnam itself. Typerep.Typerep (STR ''Type.cnam'') []" |
47394 | 26 |
instance .. |
27 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
28 |
end |
47394 | 29 |
|
30 |
instantiation cnam :: term_of |
|
31 |
begin |
|
32 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
33 |
definition "term_of_class.term_of (C :: cnam) \<equiv> |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
34 |
Code_Evaluation.Const (STR ''dummy_cnam'') (Typerep.Typerep (STR ''Type.cnam'') [])" |
47394 | 35 |
instance .. |
36 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
37 |
end |
47394 | 38 |
|
39 |
instantiation cnam :: partial_term_of |
|
40 |
begin |
|
41 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
42 |
definition "partial_term_of_class.partial_term_of (C :: cnam itself) n = undefined" |
47394 | 43 |
instance .. |
44 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
45 |
end |
12517 | 46 |
|
47 |
-- "exceptions" |
|
58310 | 48 |
datatype |
12517 | 49 |
xcpt |
50 |
= NullPointer |
|
51 |
| ClassCast |
|
52 |
| OutOfMemory |
|
8011 | 53 |
|
12517 | 54 |
-- "class names" |
58310 | 55 |
datatype cname |
12517 | 56 |
= Object |
57 |
| Xcpt xcpt |
|
12951 | 58 |
| Cname cnam |
12517 | 59 |
|
60 |
typedecl vnam -- "variable or field name" |
|
47394 | 61 |
|
62 |
instantiation vnam :: equal |
|
63 |
begin |
|
64 |
||
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
65 |
definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'" |
47394 | 66 |
instance by default (simp add: equal_vnam_def) |
67 |
||
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
68 |
end |
47394 | 69 |
|
70 |
instantiation vnam :: typerep |
|
71 |
begin |
|
72 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
73 |
definition "typerep_class.typerep \<equiv> \<lambda>_ :: vnam itself. Typerep.Typerep (STR ''Type.vnam'') []" |
47394 | 74 |
instance .. |
75 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
76 |
end |
47394 | 77 |
|
78 |
instantiation vnam :: term_of |
|
79 |
begin |
|
80 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
81 |
definition "term_of_class.term_of (V :: vnam) \<equiv> |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
82 |
Code_Evaluation.Const (STR ''dummy_vnam'') (Typerep.Typerep (STR ''Type.vnam'') [])" |
47394 | 83 |
instance .. |
84 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
85 |
end |
47394 | 86 |
|
87 |
instantiation vnam :: partial_term_of |
|
88 |
begin |
|
89 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
90 |
definition "partial_term_of_class.partial_term_of (V :: vnam itself) n = undefined" |
47394 | 91 |
instance .. |
92 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
93 |
end |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
94 |
|
12517 | 95 |
typedecl mname -- "method name" |
47394 | 96 |
|
97 |
instantiation mname :: equal |
|
98 |
begin |
|
99 |
||
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
100 |
definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'" |
47394 | 101 |
instance by default (simp add: equal_mname_def) |
102 |
||
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
103 |
end |
47394 | 104 |
|
105 |
instantiation mname :: typerep |
|
106 |
begin |
|
107 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
108 |
definition "typerep_class.typerep \<equiv> \<lambda>_ :: mname itself. Typerep.Typerep (STR ''Type.mname'') []" |
47394 | 109 |
instance .. |
110 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
111 |
end |
47394 | 112 |
|
113 |
instantiation mname :: term_of |
|
114 |
begin |
|
115 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
116 |
definition "term_of_class.term_of (M :: mname) \<equiv> |
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
117 |
Code_Evaluation.Const (STR ''dummy_mname'') (Typerep.Typerep (STR ''Type.mname'') [])" |
47394 | 118 |
instance .. |
119 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
120 |
end |
47394 | 121 |
|
122 |
instantiation mname :: partial_term_of |
|
123 |
begin |
|
124 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
125 |
definition "partial_term_of_class.partial_term_of (M :: mname itself) n = undefined" |
47394 | 126 |
instance .. |
127 |
||
44037
25011c3a5c3d
replace old SML code generator by new code generator in MicroJava/J
Andreas Lochbihler
parents:
44035
diff
changeset
|
128 |
end |
12517 | 129 |
|
130 |
-- "names for @{text This} pointer and local/field variables" |
|
58310 | 131 |
datatype vname |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
132 |
= This |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
133 |
| VName vnam |
8011 | 134 |
|
12517 | 135 |
-- "primitive type, cf. 4.2" |
58310 | 136 |
datatype prim_ty |
12517 | 137 |
= Void -- "'result type' of void methods" |
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
138 |
| Boolean |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
139 |
| Integer |
8011 | 140 |
|
12517 | 141 |
-- "reference type, cf. 4.3" |
58310 | 142 |
datatype ref_ty |
12517 | 143 |
= NullT -- "null type, cf. 4.1" |
144 |
| ClassT cname -- "class type" |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
145 |
|
12517 | 146 |
-- "any type, cf. 4.1" |
58310 | 147 |
datatype ty |
12517 | 148 |
= PrimT prim_ty -- "primitive type" |
149 |
| RefT ref_ty -- "reference type" |
|
8011 | 150 |
|
35102 | 151 |
abbreviation NT :: ty |
152 |
where "NT == RefT NullT" |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
153 |
|
35102 | 154 |
abbreviation Class :: "cname => ty" |
155 |
where "Class C == RefT (ClassT C)" |
|
8011 | 156 |
|
157 |
end |