110 "append_name" ("\"append\"") |
110 "append_name" ("\"append\"") |
111 "makelist_name" ("\"makelist\"") |
111 "makelist_name" ("\"makelist\"") |
112 "val_nam" ("\"val\"") |
112 "val_nam" ("\"val\"") |
113 "next_nam" ("\"next\"") |
113 "next_nam" ("\"next\"") |
114 |
114 |
|
115 code_type cnam and vnam and mname and loc_ |
|
116 (SML target_atom "string" and target_atom "string" and target_atom "string" and target_atom "IntInf.int") |
|
117 |
|
118 instance cnam :: eq |
|
119 and cname :: eq |
|
120 and vname :: eq |
|
121 and mname :: eq |
|
122 and ty :: eq |
|
123 and instr :: eq .. |
|
124 |
|
125 definition |
|
126 arbitrary_val :: val |
|
127 "arbitrary_val = arbitrary" |
|
128 arbitrary_cname :: cname |
|
129 "arbitrary_cname = arbitrary" |
|
130 |
|
131 declare arbitrary_val_def [symmetric, code inline] |
|
132 declare arbitrary_cname_def [symmetric, code inline] |
|
133 |
|
134 definition |
|
135 "unit' = Unit" |
|
136 "object' = Object" |
|
137 |
|
138 code_constsubst |
|
139 arbitrary_val \<equiv> unit' |
|
140 arbitrary_cname \<equiv> object' |
|
141 |
|
142 code_const list_nam and test_nam and append_name and makelist_name and val_nam and next_nam |
|
143 (SML target_atom "\"list\"" and target_atom "\"test\"" and target_atom "\"append\"" |
|
144 and target_atom "\"makelist\"" and target_atom "\"val\"" and target_atom "\"next\"") |
|
145 |
|
146 axiomatization |
|
147 incr_loc :: "loc_ \<Rightarrow> loc_" |
|
148 and zero_loc :: "loc_" |
|
149 |
|
150 code_const incr_loc and zero_loc |
|
151 (SML target_atom "(_ + 1)" and target_atom "0") |
|
152 |
|
153 axiomatization |
|
154 test_loc :: "(loc_ \<Rightarrow> bool) \<Rightarrow> (loc_ \<Rightarrow> 'a) \<Rightarrow> loc_ \<Rightarrow> 'a" where |
|
155 "test_loc p v l = (if p l then v l else test_loc p v (incr l))" |
|
156 |
|
157 definition |
|
158 new_addr' :: "(loc \<Rightarrow> (cname \<times> (vname \<times> cname \<Rightarrow> val option)) option) \<Rightarrow> loc \<times> val option" |
|
159 "new_addr' hp = |
|
160 test_loc (\<lambda>i. is_none (hp (Loc i) )) (\<lambda>i. (Loc i, None)) zero_loc" |
|
161 |
|
162 lemma [code func]: |
|
163 "wf_class = wf_class" .. |
|
164 |
|
165 code_const |
|
166 wf_class (SML target_atom "(fn _ => true)") |
|
167 |
|
168 code_constsubst |
|
169 new_Addr \<equiv> new_addr' |
|
170 |
|
171 definition |
|
172 "test = exec (E, start_state E test_name makelist_name)" |
|
173 |
|
174 |
115 subsection {* Single step execution *} |
175 subsection {* Single step execution *} |
116 |
176 |
117 code_module JVM |
177 code_module JVM |
118 contains |
178 contains |
119 test = "exec (E, start_state E test_name makelist_name)" |
179 test = "exec (E, start_state E test_name makelist_name)" |