author | wenzelm |
Fri, 26 Apr 2024 13:25:44 +0200 | |
changeset 80150 | 96f60533ec1d |
parent 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
12442 | 1 |
(* Title: HOL/MicroJava/JVM/JVMListExample.thy |
2 |
Author: Stefan Berghofer |
|
3 |
*) |
|
4 |
||
61361 | 5 |
section \<open>Example for generating executable code from JVM semantics \label{sec:JVMListExample}\<close> |
12442 | 6 |
|
32356
e11cd88e6ade
temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents:
28524
diff
changeset
|
7 |
theory JVMListExample |
e11cd88e6ade
temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents:
28524
diff
changeset
|
8 |
imports "../J/SystemClasses" JVMExec |
e11cd88e6ade
temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents:
28524
diff
changeset
|
9 |
begin |
12442 | 10 |
|
61361 | 11 |
text \<open> |
69597 | 12 |
Since the types \<^typ>\<open>cnam\<close>, \<open>vnam\<close>, and \<open>mname\<close> are |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
13 |
anonymous, we describe distinctness of names in the example by axioms: |
61361 | 14 |
\<close> |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
15 |
axiomatization list_nam test_nam :: cnam |
45827 | 16 |
where distinct_classes: "list_nam \<noteq> test_nam" |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
17 |
|
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
18 |
axiomatization append_name makelist_name :: mname |
45827 | 19 |
where distinct_methods: "append_name \<noteq> makelist_name" |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
20 |
|
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
21 |
axiomatization val_nam next_nam :: vnam |
45827 | 22 |
where distinct_fields: "val_nam \<noteq> next_nam" |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
23 |
|
45827 | 24 |
axiomatization |
25 |
where nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'" |
|
12442 | 26 |
|
45827 | 27 |
definition list_name :: cname |
28 |
where "list_name = Cname list_nam" |
|
12951 | 29 |
|
45827 | 30 |
definition test_name :: cname |
31 |
where "test_name = Cname test_nam" |
|
12951 | 32 |
|
45827 | 33 |
definition val_name :: vname |
34 |
where "val_name = VName val_nam" |
|
12442 | 35 |
|
45827 | 36 |
definition next_name :: vname |
37 |
where "next_name = VName next_nam" |
|
12442 | 38 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
39 |
definition append_ins :: bytecode where |
45827 | 40 |
"append_ins = |
12442 | 41 |
[Load 0, |
42 |
Getfield next_name list_name, |
|
43 |
Dup, |
|
44 |
LitPush Null, |
|
45 |
Ifcmpeq 4, |
|
12951 | 46 |
Load 1, |
47 |
Invoke list_name append_name [Class list_name], |
|
12442 | 48 |
Return, |
49 |
Pop, |
|
50 |
Load 0, |
|
51 |
Load 1, |
|
52 |
Putfield next_name list_name, |
|
53 |
LitPush Unit, |
|
12951 | 54 |
Return]" |
12442 | 55 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
56 |
definition list_class :: "jvm_method class" where |
45827 | 57 |
"list_class = |
12951 | 58 |
(Object, |
59 |
[(val_name, PrimT Integer), (next_name, Class list_name)], |
|
60 |
[((append_name, [Class list_name]), PrimT Void, |
|
61 |
(3, 0, append_ins,[(1,2,8,Xcpt NullPointer)]))])" |
|
62 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
63 |
definition make_list_ins :: bytecode where |
45827 | 64 |
"make_list_ins = |
12442 | 65 |
[New list_name, |
66 |
Dup, |
|
67 |
Store 0, |
|
68 |
LitPush (Intg 1), |
|
69 |
Putfield val_name list_name, |
|
70 |
New list_name, |
|
71 |
Dup, |
|
72 |
Store 1, |
|
73 |
LitPush (Intg 2), |
|
74 |
Putfield val_name list_name, |
|
75 |
New list_name, |
|
76 |
Dup, |
|
77 |
Store 2, |
|
78 |
LitPush (Intg 3), |
|
79 |
Putfield val_name list_name, |
|
80 |
Load 0, |
|
81 |
Load 1, |
|
12951 | 82 |
Invoke list_name append_name [Class list_name], |
13101 | 83 |
Pop, |
12442 | 84 |
Load 0, |
85 |
Load 2, |
|
12951 | 86 |
Invoke list_name append_name [Class list_name], |
87 |
Return]" |
|
88 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
89 |
definition test_class :: "jvm_method class" where |
45827 | 90 |
"test_class = |
12951 | 91 |
(Object, [], |
92 |
[((makelist_name, []), PrimT Void, (3, 2, make_list_ins,[]))])" |
|
12442 | 93 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32356
diff
changeset
|
94 |
definition E :: jvm_prog where |
45827 | 95 |
"E = SystemClasses @ [(list_name, list_class), (test_name, test_class)]" |
12951 | 96 |
|
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
97 |
code_datatype list_nam test_nam |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
98 |
lemma equal_cnam_code [code]: |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
99 |
"HOL.equal list_nam list_nam \<longleftrightarrow> True" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
100 |
"HOL.equal test_nam test_nam \<longleftrightarrow> True" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
101 |
"HOL.equal list_nam test_nam \<longleftrightarrow> False" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
102 |
"HOL.equal test_nam list_nam \<longleftrightarrow> False" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
103 |
by(simp_all add: distinct_classes distinct_classes[symmetric] equal_cnam_def) |
12442 | 104 |
|
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
105 |
code_datatype append_name makelist_name |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
106 |
lemma equal_mname_code [code]: |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
107 |
"HOL.equal append_name append_name \<longleftrightarrow> True" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
108 |
"HOL.equal makelist_name makelist_name \<longleftrightarrow> True" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
109 |
"HOL.equal append_name makelist_name \<longleftrightarrow> False" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
110 |
"HOL.equal makelist_name append_name \<longleftrightarrow> False" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
111 |
by(simp_all add: distinct_methods distinct_methods[symmetric] equal_mname_def) |
12442 | 112 |
|
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
113 |
code_datatype val_nam next_nam |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
114 |
lemma equal_vnam_code [code]: |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
115 |
"HOL.equal val_nam val_nam \<longleftrightarrow> True" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
116 |
"HOL.equal next_nam next_nam \<longleftrightarrow> True" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
117 |
"HOL.equal val_nam next_nam \<longleftrightarrow> False" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
118 |
"HOL.equal next_nam val_nam \<longleftrightarrow> False" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
119 |
by(simp_all add: distinct_fields distinct_fields[symmetric] equal_vnam_def) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
120 |
|
12442 | 121 |
|
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
122 |
lemma equal_loc'_code [code]: |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
123 |
"HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
124 |
by(simp add: equal_loc'_def nat_to_loc'_inject) |
12442 | 125 |
|
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
126 |
definition undefined_cname :: cname |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
127 |
where [code del]: "undefined_cname = undefined" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
128 |
code_datatype Object Xcpt Cname undefined_cname |
45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
44035
diff
changeset
|
129 |
declare undefined_cname_def[symmetric, code_unfold] |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
130 |
|
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
131 |
definition undefined_val :: val |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
132 |
where [code del]: "undefined_val = undefined" |
45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
44035
diff
changeset
|
133 |
declare undefined_val_def[symmetric, code_unfold] |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
134 |
code_datatype Unit Null Bool Intg Addr undefined_val |
12442 | 135 |
|
20971 | 136 |
definition |
137 |
"test = exec (E, start_state E test_name makelist_name)" |
|
138 |
||
61361 | 139 |
ML_val \<open> |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
140 |
@{code test}; |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
141 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
142 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
143 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
144 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
145 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
146 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
147 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
148 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
149 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
150 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
151 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
152 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
153 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
154 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
155 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
156 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
157 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
158 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
159 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
160 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
161 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
162 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
163 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
164 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
165 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
166 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
167 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
168 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
169 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
170 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
171 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
172 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
173 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
174 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
175 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
176 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
177 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
178 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
179 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
180 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
181 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
182 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
183 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
184 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
185 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
186 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
187 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
188 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
189 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
190 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
191 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
192 |
@{code exec} (@{code E}, @{code the} it); |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35416
diff
changeset
|
193 |
@{code exec} (@{code E}, @{code the} it); |
61361 | 194 |
\<close> |
12442 | 195 |
|
12973 | 196 |
end |