author | nipkow |
Mon, 12 Sep 2011 07:55:43 +0200 | |
changeset 44890 | 22f665a2e91c |
parent 35416 | d8d7d1b785af |
child 45605 | a89b4bc311a5 |
permissions | -rw-r--r-- |
12516 | 1 |
(* Title: HOL/MicroJava/BV/JType.thy |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10797
diff
changeset
|
2 |
Author: Tobias Nipkow, Gerwin Klein |
10497 | 3 |
Copyright 2000 TUM |
4 |
*) |
|
5 |
||
12911 | 6 |
header {* \isaheader{The Java Type System as Semilattice} *} |
10497 | 7 |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
8 |
theory JType |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
9 |
imports "../DFA/Semilattices" "../J/WellForm" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
10 |
begin |
10497 | 11 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
12 |
definition super :: "'a prog \<Rightarrow> cname \<Rightarrow> cname" where |
12773 | 13 |
"super G C == fst (the (class G C))" |
14 |
||
15 |
lemma superI: |
|
22271 | 16 |
"G \<turnstile> C \<prec>C1 D \<Longrightarrow> super G C = D" |
12773 | 17 |
by (unfold super_def) (auto dest: subcls1D) |
18 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
19 |
definition is_ref :: "ty \<Rightarrow> bool" where |
13006 | 20 |
"is_ref T == case T of PrimT t \<Rightarrow> False | RefT r \<Rightarrow> True" |
10497 | 21 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
22 |
definition sup :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty err" where |
10497 | 23 |
"sup G T1 T2 == |
13006 | 24 |
case T1 of PrimT P1 \<Rightarrow> (case T2 of PrimT P2 \<Rightarrow> |
25 |
(if P1 = P2 then OK (PrimT P1) else Err) | RefT R \<Rightarrow> Err) |
|
26 |
| RefT R1 \<Rightarrow> (case T2 of PrimT P \<Rightarrow> Err | RefT R2 \<Rightarrow> |
|
27 |
(case R1 of NullT \<Rightarrow> (case R2 of NullT \<Rightarrow> OK NT | ClassT C \<Rightarrow> OK (Class C)) |
|
28 |
| ClassT C \<Rightarrow> (case R2 of NullT \<Rightarrow> OK (Class C) |
|
29 |
| ClassT D \<Rightarrow> OK (Class (exec_lub (subcls1 G) (super G) C D)))))" |
|
10497 | 30 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
31 |
definition subtype :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" where |
11085 | 32 |
"subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2" |
10497 | 33 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
34 |
definition is_ty :: "'c prog \<Rightarrow> ty \<Rightarrow> bool" where |
13006 | 35 |
"is_ty G T == case T of PrimT P \<Rightarrow> True | RefT R \<Rightarrow> |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
36 |
(case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (C, Object) \<in> (subcls1 G)^*)" |
10497 | 37 |
|
35102 | 38 |
abbreviation "types G == Collect (is_type G)" |
10497 | 39 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
40 |
definition esl :: "'c prog \<Rightarrow> ty esl" where |
10497 | 41 |
"esl G == (types G, subtype G, sup G)" |
42 |
||
11085 | 43 |
lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)" |
22271 | 44 |
by (auto elim: widen.cases) |
10497 | 45 |
|
11085 | 46 |
lemma PrimT_PrimT2: "(G \<turnstile> PrimT p \<preceq> xb) = (xb = PrimT p)" |
22271 | 47 |
by (auto elim: widen.cases) |
10497 | 48 |
|
49 |
lemma is_tyI: |
|
14045 | 50 |
"\<lbrakk> is_type G T; ws_prog G \<rbrakk> \<Longrightarrow> is_ty G T" |
10630 | 51 |
by (auto simp add: is_ty_def intro: subcls_C_Object |
10497 | 52 |
split: ty.splits ref_ty.splits) |
53 |
||
54 |
lemma is_type_conv: |
|
14045 | 55 |
"ws_prog G \<Longrightarrow> is_type G T = is_ty G T" |
10497 | 56 |
proof |
14045 | 57 |
assume "is_type G T" "ws_prog G" |
10497 | 58 |
thus "is_ty G T" |
59 |
by (rule is_tyI) |
|
60 |
next |
|
14045 | 61 |
assume wf: "ws_prog G" and |
10497 | 62 |
ty: "is_ty G T" |
63 |
||
64 |
show "is_type G T" |
|
65 |
proof (cases T) |
|
66 |
case PrimT |
|
67 |
thus ?thesis by simp |
|
68 |
next |
|
69 |
fix R assume R: "T = RefT R" |
|
70 |
with wf |
|
11085 | 71 |
have "R = ClassT Object \<Longrightarrow> ?thesis" by simp |
10497 | 72 |
moreover |
73 |
from R wf ty |
|
11085 | 74 |
have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis" |
12443
e56ab6134b41
Turned subcls1 into an inductive relation to make it executable.
berghofe
parents:
11085
diff
changeset
|
75 |
by (auto simp add: is_ty_def is_class_def split_tupled_all |
22271 | 76 |
elim!: subcls1.cases |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
77 |
elim: converse_rtranclE |
12443
e56ab6134b41
Turned subcls1 into an inductive relation to make it executable.
berghofe
parents:
11085
diff
changeset
|
78 |
split: ref_ty.splits) |
10497 | 79 |
ultimately |
80 |
show ?thesis by blast |
|
81 |
qed |
|
82 |
qed |
|
83 |
||
84 |
lemma order_widen: |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
85 |
"acyclic (subcls1 G) \<Longrightarrow> order (subtype G)" |
22068 | 86 |
apply (unfold Semilat.order_def lesub_def subtype_def) |
10497 | 87 |
apply (auto intro: widen_trans) |
88 |
apply (case_tac x) |
|
89 |
apply (case_tac y) |
|
90 |
apply (auto simp add: PrimT_PrimT) |
|
91 |
apply (case_tac y) |
|
92 |
apply simp |
|
93 |
apply simp |
|
94 |
apply (case_tac ref_ty) |
|
95 |
apply (case_tac ref_tya) |
|
96 |
apply simp |
|
97 |
apply simp |
|
98 |
apply (case_tac ref_tya) |
|
99 |
apply simp |
|
100 |
apply simp |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
101 |
apply (auto dest: acyclic_impl_antisym_rtrancl antisymD) |
10497 | 102 |
done |
103 |
||
10592 | 104 |
lemma wf_converse_subcls1_impl_acc_subtype: |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
105 |
"wf ((subcls1 G)^-1) \<Longrightarrow> acc (subtype G)" |
22271 | 106 |
apply (unfold Semilat.acc_def lesssub_def) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
107 |
apply (drule_tac p = "((subcls1 G)^-1) - Id" in wf_subset) |
22271 | 108 |
apply auto |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
109 |
apply (drule wf_trancl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
110 |
apply (simp add: wf_eq_minimal) |
10592 | 111 |
apply clarify |
112 |
apply (unfold lesub_def subtype_def) |
|
113 |
apply (rename_tac M T) |
|
114 |
apply (case_tac "EX C. Class C : M") |
|
115 |
prefer 2 |
|
116 |
apply (case_tac T) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
35416
diff
changeset
|
117 |
apply (fastforce simp add: PrimT_PrimT2) |
10592 | 118 |
apply simp |
119 |
apply (subgoal_tac "ref_ty = NullT") |
|
120 |
apply simp |
|
121 |
apply (rule_tac x = NT in bexI) |
|
122 |
apply (rule allI) |
|
123 |
apply (rule impI, erule conjE) |
|
124 |
apply (drule widen_RefT) |
|
125 |
apply clarsimp |
|
126 |
apply (case_tac t) |
|
127 |
apply simp |
|
128 |
apply simp |
|
129 |
apply simp |
|
130 |
apply (case_tac ref_ty) |
|
131 |
apply simp |
|
132 |
apply simp |
|
133 |
apply (erule_tac x = "{C. Class C : M}" in allE) |
|
134 |
apply auto |
|
135 |
apply (rename_tac D) |
|
136 |
apply (rule_tac x = "Class D" in bexI) |
|
137 |
prefer 2 |
|
138 |
apply assumption |
|
139 |
apply clarify |
|
140 |
apply (frule widen_RefT) |
|
141 |
apply (erule exE) |
|
142 |
apply (case_tac t) |
|
143 |
apply simp |
|
144 |
apply simp |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
145 |
apply (insert rtrancl_r_diff_Id [symmetric, standard, of "subcls1 G"]) |
10592 | 146 |
apply simp |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
147 |
apply (erule rtrancl.cases) |
10592 | 148 |
apply blast |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
149 |
apply (drule rtrancl_converseI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
150 |
apply (subgoal_tac "(subcls1 G - Id)^-1 = (subcls1 G)^-1 - Id") |
10592 | 151 |
prefer 2 |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
152 |
apply (simp add: converse_Int) apply safe[1] |
22271 | 153 |
apply simp |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
154 |
apply (blast intro: rtrancl_into_trancl2) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
155 |
done |
10592 | 156 |
|
10497 | 157 |
lemma closed_err_types: |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
158 |
"\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> |
13006 | 159 |
\<Longrightarrow> closed (err (types G)) (lift2 (sup G))" |
10497 | 160 |
apply (unfold closed_def plussub_def lift2_def sup_def) |
161 |
apply (auto split: err.split) |
|
162 |
apply (drule is_tyI, assumption) |
|
163 |
apply (auto simp add: is_ty_def is_type_conv simp del: is_type.simps |
|
12773 | 164 |
split: ty.split ref_ty.split) |
165 |
apply (blast dest!: is_lub_exec_lub is_lubD is_ubD intro!: is_ubI superI) |
|
10497 | 166 |
done |
167 |
||
168 |
||
10896 | 169 |
lemma sup_subtype_greater: |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
170 |
"\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G); |
13006 | 171 |
is_type G t1; is_type G t2; sup G t1 t2 = OK s \<rbrakk> |
172 |
\<Longrightarrow> subtype G t1 s \<and> subtype G t2 s" |
|
10497 | 173 |
proof - |
14045 | 174 |
assume ws_prog: "ws_prog G" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
175 |
assume single_valued: "single_valued (subcls1 G)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
176 |
assume acyclic: "acyclic (subcls1 G)" |
10896 | 177 |
|
10497 | 178 |
{ fix c1 c2 |
179 |
assume is_class: "is_class G c1" "is_class G c2" |
|
14045 | 180 |
with ws_prog |
10497 | 181 |
obtain |
11085 | 182 |
"G \<turnstile> c1 \<preceq>C Object" |
183 |
"G \<turnstile> c2 \<preceq>C Object" |
|
10497 | 184 |
by (blast intro: subcls_C_Object) |
14045 | 185 |
with ws_prog single_valued |
10497 | 186 |
obtain u where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
187 |
"is_lub ((subcls1 G)^* ) c1 c2 u" |
10797 | 188 |
by (blast dest: single_valued_has_lubs) |
12773 | 189 |
moreover |
190 |
note acyclic |
|
191 |
moreover |
|
22271 | 192 |
have "\<forall>x y. G \<turnstile> x \<prec>C1 y \<longrightarrow> super G x = y" |
12773 | 193 |
by (blast intro: superI) |
194 |
ultimately |
|
195 |
have "G \<turnstile> c1 \<preceq>C exec_lub (subcls1 G) (super G) c1 c2 \<and> |
|
196 |
G \<turnstile> c2 \<preceq>C exec_lub (subcls1 G) (super G) c1 c2" |
|
197 |
by (simp add: exec_lub_conv) (blast dest: is_lubD is_ubD) |
|
10896 | 198 |
} note this [simp] |
10497 | 199 |
|
10896 | 200 |
assume "is_type G t1" "is_type G t2" "sup G t1 t2 = OK s" |
201 |
thus ?thesis |
|
202 |
apply (unfold sup_def subtype_def) |
|
203 |
apply (cases s) |
|
204 |
apply (auto split: ty.split_asm ref_ty.split_asm split_if_asm) |
|
205 |
done |
|
206 |
qed |
|
10497 | 207 |
|
10896 | 208 |
lemma sup_subtype_smallest: |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
209 |
"\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G); |
10896 | 210 |
is_type G a; is_type G b; is_type G c; |
13006 | 211 |
subtype G a c; subtype G b c; sup G a b = OK d \<rbrakk> |
212 |
\<Longrightarrow> subtype G d c" |
|
10896 | 213 |
proof - |
14045 | 214 |
assume ws_prog: "ws_prog G" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
215 |
assume single_valued: "single_valued (subcls1 G)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
216 |
assume acyclic: "acyclic (subcls1 G)" |
10497 | 217 |
|
218 |
{ fix c1 c2 D |
|
219 |
assume is_class: "is_class G c1" "is_class G c2" |
|
11085 | 220 |
assume le: "G \<turnstile> c1 \<preceq>C D" "G \<turnstile> c2 \<preceq>C D" |
14045 | 221 |
from ws_prog is_class |
10497 | 222 |
obtain |
11085 | 223 |
"G \<turnstile> c1 \<preceq>C Object" |
224 |
"G \<turnstile> c2 \<preceq>C Object" |
|
10497 | 225 |
by (blast intro: subcls_C_Object) |
14045 | 226 |
with ws_prog single_valued |
10497 | 227 |
obtain u where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
228 |
lub: "is_lub ((subcls1 G)^*) c1 c2 u" |
10797 | 229 |
by (blast dest: single_valued_has_lubs) |
10497 | 230 |
with acyclic |
12773 | 231 |
have "exec_lub (subcls1 G) (super G) c1 c2 = u" |
232 |
by (blast intro: superI exec_lub_conv) |
|
10497 | 233 |
moreover |
234 |
from lub le |
|
11085 | 235 |
have "G \<turnstile> u \<preceq>C D" |
10497 | 236 |
by (simp add: is_lub_def is_ub_def) |
237 |
ultimately |
|
12773 | 238 |
have "G \<turnstile> exec_lub (subcls1 G) (super G) c1 c2 \<preceq>C D" |
10497 | 239 |
by blast |
240 |
} note this [intro] |
|
241 |
||
242 |
have [dest!]: |
|
13006 | 243 |
"\<And>C T. G \<turnstile> Class C \<preceq> T \<Longrightarrow> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D" |
10497 | 244 |
by (frule widen_Class, auto) |
245 |
||
10896 | 246 |
assume "is_type G a" "is_type G b" "is_type G c" |
247 |
"subtype G a c" "subtype G b c" "sup G a b = OK d" |
|
248 |
thus ?thesis |
|
249 |
by (auto simp add: subtype_def sup_def |
|
250 |
split: ty.split_asm ref_ty.split_asm split_if_asm) |
|
251 |
qed |
|
252 |
||
253 |
lemma sup_exists: |
|
13006 | 254 |
"\<lbrakk> subtype G a c; subtype G b c; sup G a b = Err \<rbrakk> \<Longrightarrow> False" |
10896 | 255 |
by (auto simp add: PrimT_PrimT PrimT_PrimT2 sup_def subtype_def |
256 |
split: ty.splits ref_ty.splits) |
|
10497 | 257 |
|
10896 | 258 |
lemma err_semilat_JType_esl_lemma: |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
259 |
"\<lbrakk> ws_prog G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> |
13006 | 260 |
\<Longrightarrow> err_semilat (esl G)" |
10896 | 261 |
proof - |
14045 | 262 |
assume ws_prog: "ws_prog G" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
263 |
assume single_valued: "single_valued (subcls1 G)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
264 |
assume acyclic: "acyclic (subcls1 G)" |
10896 | 265 |
|
266 |
hence "order (subtype G)" |
|
267 |
by (rule order_widen) |
|
268 |
moreover |
|
14045 | 269 |
from ws_prog single_valued acyclic |
10896 | 270 |
have "closed (err (types G)) (lift2 (sup G))" |
271 |
by (rule closed_err_types) |
|
272 |
moreover |
|
273 |
||
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
274 |
from ws_prog single_valued acyclic |
10896 | 275 |
have |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
276 |
"(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(Err.le (subtype G)) x +_(lift2 (sup G)) y) \<and> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
277 |
(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). y <=_(Err.le (subtype G)) x +_(lift2 (sup G)) y)" |
13074 | 278 |
by (auto simp add: lesub_def plussub_def Err.le_def lift2_def sup_subtype_greater split: err.split) |
10896 | 279 |
|
13074 | 280 |
moreover |
10896 | 281 |
|
14045 | 282 |
from ws_prog single_valued acyclic |
10497 | 283 |
have |
11085 | 284 |
"\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G). |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
285 |
x <=_(Err.le (subtype G)) z \<and> y <=_(Err.le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(Err.le (subtype G)) z" |
13074 | 286 |
by (unfold lift2_def plussub_def lesub_def Err.le_def) |
10896 | 287 |
(auto intro: sup_subtype_smallest sup_exists split: err.split) |
10497 | 288 |
|
289 |
ultimately |
|
290 |
||
291 |
show ?thesis |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
292 |
by (unfold esl_def semilat_def Err.sl_def) auto |
10497 | 293 |
qed |
294 |
||
10797 | 295 |
lemma single_valued_subcls1: |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
25363
diff
changeset
|
296 |
"ws_prog G \<Longrightarrow> single_valued (subcls1 G)" |
14045 | 297 |
by (auto simp add: ws_prog_def unique_def single_valued_def |
22271 | 298 |
intro: subcls1I elim!: subcls1.cases) |
10497 | 299 |
|
10592 | 300 |
theorem err_semilat_JType_esl: |
14045 | 301 |
"ws_prog G \<Longrightarrow> err_semilat (esl G)" |
10797 | 302 |
by (frule acyclic_subcls1, frule single_valued_subcls1, rule err_semilat_JType_esl_lemma) |
10497 | 303 |
|
304 |
end |