19 open Hints_declaration
90 (** val jump_length_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
91 let rec jump_length_rect_Type4 h_short_jump h_absolute_jump h_long_jump = function
92 | Short_jump -> h_short_jump
93 | Absolute_jump -> h_absolute_jump
94 | Long_jump -> h_long_jump
96 (** val jump_length_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
97 let rec jump_length_rect_Type5 h_short_jump h_absolute_jump h_long_jump = function
98 | Short_jump -> h_short_jump
99 | Absolute_jump -> h_absolute_jump
100 | Long_jump -> h_long_jump
102 (** val jump_length_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
103 let rec jump_length_rect_Type3 h_short_jump h_absolute_jump h_long_jump = function
104 | Short_jump -> h_short_jump
105 | Absolute_jump -> h_absolute_jump
106 | Long_jump -> h_long_jump
108 (** val jump_length_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
109 let rec jump_length_rect_Type2 h_short_jump h_absolute_jump h_long_jump = function
110 | Short_jump -> h_short_jump
111 | Absolute_jump -> h_absolute_jump
112 | Long_jump -> h_long_jump
114 (** val jump_length_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
115 let rec jump_length_rect_Type1 h_short_jump h_absolute_jump h_long_jump = function
116 | Short_jump -> h_short_jump
117 | Absolute_jump -> h_absolute_jump
118 | Long_jump -> h_long_jump
120 (** val jump_length_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
121 let rec jump_length_rect_Type0 h_short_jump h_absolute_jump h_long_jump = function
122 | Short_jump -> h_short_jump
123 | Absolute_jump -> h_absolute_jump
124 | Long_jump -> h_long_jump
126 (** val jump_length_inv_rect_Type4 :
127 jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
128 let jump_length_inv_rect_Type4 hterm h1 h2 h3 =
129 let hcut = jump_length_rect_Type4 h1 h2 h3 hterm in hcut __
131 (** val jump_length_inv_rect_Type3 :
132 jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
133 let jump_length_inv_rect_Type3 hterm h1 h2 h3 =
134 let hcut = jump_length_rect_Type3 h1 h2 h3 hterm in hcut __
136 (** val jump_length_inv_rect_Type2 :
137 jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
138 let jump_length_inv_rect_Type2 hterm h1 h2 h3 =
139 let hcut = jump_length_rect_Type2 h1 h2 h3 hterm in hcut __
141 (** val jump_length_inv_rect_Type1 :
142 jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
143 let jump_length_inv_rect_Type1 hterm h1 h2 h3 =
144 let hcut = jump_length_rect_Type1 h1 h2 h3 hterm in hcut __
146 (** val jump_length_inv_rect_Type0 :
147 jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
148 let jump_length_inv_rect_Type0 hterm h1 h2 h3 =
149 let hcut = jump_length_rect_Type0 h1 h2 h3 hterm in hcut __
151 (** val jump_length_discr : jump_length -> jump_length -> __ **)
152 let jump_length_discr x y =
153 Logic.eq_rect_Type2 x
155 | Short_jump -> Obj.magic (fun _ dH -> dH)
156 | Absolute_jump -> Obj.magic (fun _ dH -> dH)
157 | Long_jump -> Obj.magic (fun _ dH -> dH)) y
159 (** val jump_length_jmdiscr : jump_length -> jump_length -> __ **)
160 let jump_length_jmdiscr x y =
161 Logic.eq_rect_Type2 x
163 | Short_jump -> Obj.magic (fun _ dH -> dH)
164 | Absolute_jump -> Obj.magic (fun _ dH -> dH)
165 | Long_jump -> Obj.magic (fun _ dH -> dH)) y
167 (** val short_jump_cond :
168 BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
170 let short_jump_cond pc_plus_jmp_length addr =
171 let { Types.fst = result; Types.snd = flags } =
172 Arithmetic.sub_16_with_carry addr pc_plus_jmp_length Bool.False
174 let { Types.fst = upper; Types.snd = lower } =
175 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
176 (Nat.S Nat.O))))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
179 (match Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags with
182 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
183 (Nat.S (Nat.S Nat.O))))))))) upper (Vector.VCons ((Nat.S (Nat.S
184 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), Bool.True,
185 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
186 Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
187 (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
188 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
189 (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S
190 (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
191 Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
192 (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))))));
193 Types.snd = (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
194 (Nat.S Nat.O))))))), Bool.True, lower)) }
197 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
198 (Nat.S (Nat.S Nat.O))))))))) upper
199 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
200 (Nat.S (Nat.S Nat.O))))))))))); Types.snd = (Vector.VCons ((Nat.S
201 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False,
204 (** val absolute_jump_cond :
205 BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
207 let absolute_jump_cond pc_plus_jmp_length addr =
208 let { Types.fst = fst_5_addr; Types.snd = rest_addr } =
209 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S
210 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
211 Nat.O))))))))))) addr
213 let { Types.fst = fst_5_pc; Types.snd = rest_pc } =
214 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S
215 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
216 Nat.O))))))))))) pc_plus_jmp_length
219 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) fst_5_addr
220 fst_5_pc); Types.snd = rest_addr }
222 (** val assembly_preinstruction :
223 ('a1 -> BitVector.byte) -> 'a1 ASM.preinstruction -> Bool.bool
224 Vector.vector List.list **)
225 let assembly_preinstruction addr_of = function
226 | ASM.ADD (addr1, addr2) ->
227 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
228 ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
229 (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
230 ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
231 Vector.VEmpty)))))))) addr2 with
233 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
234 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
235 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
236 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
237 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
238 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
239 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
240 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
241 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
243 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
244 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
245 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
246 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
247 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
248 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
249 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
250 Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
251 Vector.VEmpty)))))))))))))))), List.Nil))
252 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
255 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
256 (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
257 Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
258 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
259 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
260 (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
261 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
262 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
263 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
265 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
266 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
267 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
268 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
269 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
270 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
271 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
272 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
273 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
274 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
275 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
276 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
277 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
278 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
279 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
280 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
281 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
282 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
283 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
284 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
285 | ASM.ADDC (addr1, addr2) ->
286 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
287 ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
288 (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
289 ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
290 Vector.VEmpty)))))))) addr2 with
292 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
293 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
294 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
295 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
296 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
297 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
298 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
299 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
300 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
302 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
303 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
304 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
305 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
306 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
307 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
308 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
309 Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
310 Vector.VEmpty)))))))))))))))), List.Nil))
311 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
314 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
315 (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
316 Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
317 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
318 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
319 (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
320 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
321 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
322 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
324 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
325 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
326 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
327 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
328 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
329 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
330 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
331 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
332 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
333 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
334 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
335 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
336 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
337 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
338 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
339 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
340 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
341 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
342 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
343 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
344 | ASM.SUBB (addr1, addr2) ->
345 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
346 ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
347 (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
348 ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
349 Vector.VEmpty)))))))) addr2 with
351 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
352 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
353 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
354 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
355 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
356 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
357 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
358 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
359 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
361 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
362 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
363 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
364 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
365 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
366 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
367 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
368 Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
369 Vector.VEmpty)))))))))))))))), List.Nil))
370 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
373 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
374 (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
375 Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
376 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
377 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
378 Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
379 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
380 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
381 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
383 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
384 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
385 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
386 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
387 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
388 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
389 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
390 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
391 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
392 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
393 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
394 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
395 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
396 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
397 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
398 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
399 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
400 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
401 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
402 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
404 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
405 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Acc_a,
406 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr,
407 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons
408 ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Dptr,
409 Vector.VEmpty)))))))))) addr with
411 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
412 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
413 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
414 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
415 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
416 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
417 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
418 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
419 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
421 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
422 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
423 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
424 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
425 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
426 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
427 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
428 Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
429 Vector.VEmpty)))))))))))))))), List.Nil))
430 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
433 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
434 (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
435 Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
436 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
437 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
438 (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
440 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
441 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
442 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
443 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
444 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
445 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
446 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
447 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
448 Vector.VEmpty)))))))))))))))), List.Nil))
449 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
451 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
452 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
453 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
454 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
455 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
456 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
457 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
458 ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
459 Vector.VEmpty)))))))))))))))), List.Nil))
460 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
461 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
462 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
463 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
464 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
465 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
466 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
467 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
468 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
469 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
470 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
471 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
473 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
474 ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S
475 (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O),
476 ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
477 Vector.VEmpty)))))))) addr with
479 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
480 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
481 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
482 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
483 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
484 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
485 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
486 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
487 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
489 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
490 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
491 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
492 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
493 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
494 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
495 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
496 Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
497 Vector.VEmpty)))))))))))))))), List.Nil))
498 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
501 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
502 (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
503 Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
504 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
505 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
506 (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
508 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
509 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
510 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
511 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
512 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
513 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
514 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
515 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
516 Vector.VEmpty)))))))))))))))), List.Nil))
517 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
518 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
519 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
520 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
521 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
522 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
523 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
524 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
525 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
526 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
527 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
528 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
529 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
530 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
531 | ASM.MUL (addr1, addr2) ->
532 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
533 Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
534 (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
535 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
536 (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
537 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
538 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
539 Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
540 | ASM.DIV (addr1, addr2) ->
541 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
542 Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
543 (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
544 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
545 (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
546 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
547 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
548 Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
550 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
551 Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
552 (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
553 (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
554 (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
555 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
556 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
557 Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
559 let b1 = addr_of addr in
560 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
561 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
562 (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
563 (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
564 Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
565 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
566 ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
567 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
569 let b1 = addr_of addr in
570 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
571 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
572 (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
573 (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
574 Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
575 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
576 ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
577 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
578 | ASM.JB (addr1, addr2) ->
579 let b2 = addr_of addr2 in
580 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr,
581 Vector.VEmpty)) addr1 with
582 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
583 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
584 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
585 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
586 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
587 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
588 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
589 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
590 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
591 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
592 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
593 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
594 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
595 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
597 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
598 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
599 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
600 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
601 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
602 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
603 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
604 ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
605 Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
607 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
608 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
609 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
610 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
611 | ASM.JNB (addr1, addr2) ->
612 let b2 = addr_of addr2 in
613 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr,
614 Vector.VEmpty)) addr1 with
615 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
616 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
617 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
618 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
619 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
620 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
621 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
622 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
623 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
624 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
625 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
626 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
627 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
628 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
630 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
631 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
632 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
633 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
634 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
635 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
636 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
637 ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
638 Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
640 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
641 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
642 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
643 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
644 | ASM.JBC (addr1, addr2) ->
645 let b2 = addr_of addr2 in
646 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr,
647 Vector.VEmpty)) addr1 with
648 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
649 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
650 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
651 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
652 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
653 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
654 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
655 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
656 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
657 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
658 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
659 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
660 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
661 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
663 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
664 (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
665 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
666 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
667 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
668 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
669 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
670 ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
671 Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
673 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
674 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
675 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
676 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
678 let b1 = addr_of addr in
679 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
680 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
681 (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
682 (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
683 Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
684 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
685 ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
686 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
688 let b1 = addr_of addr in
689 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
690 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
691 (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
692 (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
693 Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
694 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
695 ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
696 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
697 | ASM.CJNE (addrs, addr3) ->
698 let b3 = addr_of addr3 in
700 | Types.Inl addrs0 ->
701 let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
702 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
703 Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Data,
704 Vector.VEmpty)))) addr2 with
706 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
707 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
708 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
709 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
710 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
711 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
712 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
713 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
714 Bool.True, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
715 (List.Cons (b3, List.Nil))))))
716 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
717 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
718 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
719 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
720 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
721 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
723 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
724 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
725 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
726 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
727 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
728 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
729 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
730 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
731 Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
732 (List.Cons (b3, List.Nil))))))
733 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
734 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
735 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
736 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
737 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
738 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
739 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
740 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
741 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
742 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
743 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
744 | Types.Inr addrs0 ->
745 let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
747 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Data,
748 Vector.VEmpty)) addr2 with
749 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
750 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
751 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
752 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
753 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
754 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
755 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
756 | ASM.DATA b2 -> (fun _ -> b2)
757 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
758 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
759 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
760 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
761 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
762 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
763 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
764 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
765 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
766 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
767 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
769 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
770 Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect,
771 Vector.VEmpty)))) addr1 with
772 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
774 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
775 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
776 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
777 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
778 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
779 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
780 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
781 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
782 Vector.VEmpty)))))))))))))))), (List.Cons (b2, (List.Cons (b3,
784 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
787 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
788 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
789 (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
790 (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
791 Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
792 (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))) r),
793 (List.Cons (b2, (List.Cons (b3, List.Nil))))))
794 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
795 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
796 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
797 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
798 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
799 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
800 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
801 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
802 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
803 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
804 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
805 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
806 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
807 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
808 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
809 | ASM.DJNZ (addr1, addr2) ->
810 let b2 = addr_of addr2 in
811 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
812 ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty))))
815 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
816 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
817 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
818 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
819 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
820 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
821 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
822 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
823 Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
825 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
826 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
829 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
830 (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
831 Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
832 Bool.True, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
833 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
834 Bool.True, Vector.VEmpty)))))))))) r), (List.Cons (b2, List.Nil))))
835 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
836 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
837 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
838 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
839 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
840 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
841 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
842 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
843 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
844 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
845 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
846 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
847 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
848 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
849 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
852 | Types.Inl addrs0 ->
854 | Types.Inl addrs1 ->
855 let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
856 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
857 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr,
858 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct,
859 (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons
860 (Nat.O, ASM.Data, Vector.VEmpty)))))))) addr2 with
862 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
863 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
864 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
865 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
866 Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
867 (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
868 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
869 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
870 (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
871 (List.Cons (b1, List.Nil))))
873 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
874 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
875 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
876 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
877 Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
878 (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
879 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
880 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
881 (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))),
883 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
886 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
887 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
888 (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
889 (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S
890 (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O),
891 Bool.True, (Vector.VCons (Nat.O, Bool.True,
892 Vector.VEmpty)))))))))) r), List.Nil))
893 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
894 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
895 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
897 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
898 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
899 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
900 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
901 Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
902 (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
903 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
904 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
905 (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
906 (List.Cons (b1, List.Nil))))
907 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
908 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
909 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
910 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
911 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
912 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
913 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
914 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
915 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
916 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
917 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
918 | Types.Inr addrs1 ->
919 let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
921 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
922 ASM.Direct, Vector.VEmpty)) addr1 with
923 | ASM.DIRECT b1 -> (fun _ -> b1)
924 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
925 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
926 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
927 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
928 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
929 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
930 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
931 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
932 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
933 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
934 | ASM.EXT_INDIRECT_DPTR ->
935 (fun _ -> assert false (* absurd case *))
936 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
937 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
938 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
939 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
940 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
941 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
942 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
944 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
945 Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
946 Vector.VEmpty)))) addr2 with
947 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
948 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
949 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
950 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
952 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
953 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
954 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
955 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
956 Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
957 (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
958 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
959 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
960 (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
961 (List.Cons (b1, List.Nil))))
962 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
963 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
965 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
966 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
967 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
968 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
969 Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
970 (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
971 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
972 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
973 (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
974 (List.Cons (b1, (List.Cons (b2, List.Nil))))))
975 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
976 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
977 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
978 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
979 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
980 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
981 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
982 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
983 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
984 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
985 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
986 | Types.Inr addrs0 ->
987 let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
988 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
989 Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr,
990 Vector.VEmpty)))) addr2 with
991 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
992 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
993 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
994 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
995 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
996 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
997 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
998 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
999 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1000 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1001 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1002 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1003 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1004 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1005 | ASM.BIT_ADDR b1 ->
1006 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1007 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1008 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1009 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1010 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1011 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1012 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1013 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1014 Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1016 | ASM.N_BIT_ADDR b1 ->
1017 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1018 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1019 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1020 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1021 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1022 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1023 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1024 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1025 Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1027 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1028 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1029 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1032 | Types.Inl addrs0 ->
1034 | Types.Inl addrs1 ->
1035 let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
1036 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
1037 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr,
1038 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Data,
1039 (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
1040 (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) addr2 with
1042 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1043 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1044 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1045 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1046 Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1047 (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1048 (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1049 Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1050 (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1051 (List.Cons (b1, List.Nil))))
1052 | ASM.INDIRECT i1 ->
1053 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1054 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1055 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1056 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1057 Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1058 (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1059 (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1060 Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1061 (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))),
1063 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1066 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1067 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
1068 (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
1069 (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S
1070 (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O),
1071 Bool.False, (Vector.VCons (Nat.O, Bool.True,
1072 Vector.VEmpty)))))))))) r), List.Nil))
1073 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1074 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1075 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1077 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1078 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1079 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1080 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1081 Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1082 (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1083 (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1084 Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1085 (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
1086 (List.Cons (b1, List.Nil))))
1087 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1088 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1089 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1090 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1091 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1092 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1093 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1094 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1095 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1096 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1097 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1098 | Types.Inr addrs1 ->
1099 let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
1101 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1102 ASM.Direct, Vector.VEmpty)) addr1 with
1103 | ASM.DIRECT b1 -> (fun _ -> b1)
1104 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1105 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1106 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1107 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1108 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1109 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1110 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1111 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1112 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1113 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1114 | ASM.EXT_INDIRECT_DPTR ->
1115 (fun _ -> assert false (* absurd case *))
1116 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1117 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1118 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1119 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1120 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1121 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1122 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1124 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1125 Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1126 Vector.VEmpty)))) addr2 with
1127 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1128 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1129 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1130 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1132 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1133 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1134 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1135 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1136 Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1137 (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1138 (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1139 Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1140 (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
1141 (List.Cons (b1, List.Nil))))
1142 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1143 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1145 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1146 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1147 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1148 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1149 Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1150 (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1151 (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1152 Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1153 (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1154 (List.Cons (b1, (List.Cons (b2, List.Nil))))))
1155 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1156 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1157 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1158 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1159 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1160 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1161 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1162 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1163 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1164 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1165 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1166 | Types.Inr addrs0 ->
1167 let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1168 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1169 Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr,
1170 Vector.VEmpty)))) addr2 with
1171 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1172 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1173 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1174 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1175 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1176 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1177 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1178 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1179 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1180 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1181 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1182 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1183 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1184 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1185 | ASM.BIT_ADDR b1 ->
1186 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1187 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1188 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1189 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1190 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1191 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1192 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1193 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1194 Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1196 | ASM.N_BIT_ADDR b1 ->
1197 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1198 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1199 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1200 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1201 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1202 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1203 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1204 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1205 Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1207 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1208 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1209 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1212 | Types.Inl addrs0 ->
1213 let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1214 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
1215 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Data,
1216 (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr,
1217 (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O,
1218 ASM.Indirect, Vector.VEmpty)))))))) addr2 with
1220 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1221 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1222 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1223 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1224 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1225 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1226 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1227 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1228 Bool.True, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1230 | ASM.INDIRECT i1 ->
1231 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1232 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1233 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1234 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1235 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1236 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1237 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1238 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
1239 Vector.VEmpty)))))))))))))))), List.Nil))
1240 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1243 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1244 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
1245 (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
1246 (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1247 Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1248 (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))) r),
1250 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1251 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1252 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1254 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1255 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1256 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1257 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1258 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1259 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1260 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1261 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1262 Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1264 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1265 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1266 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1267 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1268 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1269 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1270 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1271 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1272 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1273 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1274 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1275 | Types.Inr addrs0 ->
1276 let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1278 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1279 ASM.Direct, Vector.VEmpty)) addr1 with
1280 | ASM.DIRECT b1 -> (fun _ -> b1)
1281 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1282 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1283 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1284 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1285 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1286 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1287 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1288 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1289 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1290 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1291 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1292 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1293 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1294 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1295 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1296 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1297 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1298 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1300 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1301 Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1302 Vector.VEmpty)))) addr2 with
1303 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1304 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1305 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1306 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1308 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1309 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1310 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1311 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1312 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1313 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1314 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1315 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1316 Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1318 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1319 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1321 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1322 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1323 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1324 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1325 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1326 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1327 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1328 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1329 Bool.True, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1330 (List.Cons (b2, List.Nil))))))
1331 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1332 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1333 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1334 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1335 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1336 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1337 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1338 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1339 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1340 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1341 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1343 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
1344 (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1345 ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))))
1347 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1348 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1349 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1350 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1352 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1353 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1354 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1355 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1356 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1357 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1358 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
1359 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
1360 Vector.VEmpty)))))))))))))))), List.Nil))
1361 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1362 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1363 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1364 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1365 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1366 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1367 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1368 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1370 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1371 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1372 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1373 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
1374 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1375 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1376 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1377 ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1378 Vector.VEmpty)))))))))))))))), List.Nil))
1379 | ASM.BIT_ADDR b1 ->
1380 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1381 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1382 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1383 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
1384 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1385 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1386 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1387 ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False,
1388 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
1389 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1390 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1391 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1392 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1394 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
1395 (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1396 ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))))
1398 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1399 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1400 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1401 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1403 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1404 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1405 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1406 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1407 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1408 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1409 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
1410 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
1411 Vector.VEmpty)))))))))))))))), List.Nil))
1412 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1413 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1414 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1415 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1416 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1417 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1418 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1419 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1421 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1422 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1423 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
1424 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1425 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1426 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1427 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1428 ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1429 Vector.VEmpty)))))))))))))))), List.Nil))
1430 | ASM.BIT_ADDR b1 ->
1431 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1432 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1433 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
1434 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1435 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1436 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1437 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1438 ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False,
1439 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
1440 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1441 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1442 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1443 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1445 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1446 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1447 (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1448 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1449 (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1450 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1451 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1452 Vector.VEmpty)))))))))))))))), List.Nil)
1454 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1455 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1456 (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1457 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1458 (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1459 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1460 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1461 Vector.VEmpty)))))))))))))))), List.Nil)
1463 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1464 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1465 (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1466 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1467 (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1468 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1469 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1470 Vector.VEmpty)))))))))))))))), List.Nil)
1472 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1473 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1474 (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1475 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1476 (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1477 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1478 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1479 Vector.VEmpty)))))))))))))))), List.Nil)
1481 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1482 Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1483 (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1484 (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1485 (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1486 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1487 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1488 Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
1491 | Types.Inl addrs0 ->
1493 | Types.Inl addrs1 ->
1495 | Types.Inl addrs2 ->
1497 | Types.Inl addrs3 ->
1499 | Types.Inl addrs4 ->
1500 let { Types.fst = addr1; Types.snd = addr2 } = addrs4 in
1501 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S
1502 Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1503 Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
1504 Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
1505 ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
1506 Vector.VEmpty)))))))) addr2 with
1508 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1509 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1510 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1511 (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S
1512 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1513 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1514 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1515 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1516 Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O),
1517 Bool.False, (Vector.VCons (Nat.O, Bool.True,
1518 Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1520 | ASM.INDIRECT i1 ->
1521 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1522 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1523 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1524 (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S
1525 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1526 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1527 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1528 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1529 Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O),
1530 Bool.True, (Vector.VCons (Nat.O, i1,
1531 Vector.VEmpty)))))))))))))))), List.Nil))
1532 | ASM.EXT_INDIRECT x ->
1533 (fun _ -> assert false (* absurd case *))
1536 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1537 Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1538 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1539 Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1540 (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S
1541 (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
1542 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
1543 Vector.VEmpty)))))))))) r), List.Nil))
1544 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1545 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1546 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1548 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1549 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False,
1550 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1551 (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S
1552 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1553 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1554 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1555 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1556 Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O),
1557 Bool.False, (Vector.VCons (Nat.O, Bool.False,
1558 Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1560 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1561 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1562 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1563 | ASM.EXT_INDIRECT_DPTR ->
1564 (fun _ -> assert false (* absurd case *))
1565 | ASM.INDIRECT_DPTR ->
1566 (fun _ -> assert false (* absurd case *))
1567 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1569 (fun _ -> assert false (* absurd case *))
1570 | ASM.N_BIT_ADDR x ->
1571 (fun _ -> assert false (* absurd case *))
1573 (fun _ -> assert false (* absurd case *))
1574 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1575 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1577 | Types.Inr addrs4 ->
1578 let { Types.fst = addr1; Types.snd = addr2 } = addrs4 in
1579 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons
1580 ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O,
1581 ASM.Indirect, Vector.VEmpty)))) addr1 with
1582 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1583 | ASM.INDIRECT i1 ->
1585 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
1586 (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1587 ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1588 ASM.Direct, (Vector.VCons (Nat.O, ASM.Data,
1589 Vector.VEmpty)))))) addr2 with
1591 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S
1592 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
1593 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1594 (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1595 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1596 Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
1597 (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1598 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1599 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1600 Bool.True, (Vector.VCons ((Nat.S Nat.O),
1601 Bool.True, (Vector.VCons (Nat.O, i1,
1602 Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1604 | ASM.INDIRECT x0 ->
1605 (fun _ -> assert false (* absurd case *))
1606 | ASM.EXT_INDIRECT x0 ->
1607 (fun _ -> assert false (* absurd case *))
1608 | ASM.REGISTER x0 ->
1609 (fun _ -> assert false (* absurd case *))
1611 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S
1612 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
1613 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1614 (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1615 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1616 Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
1617 (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1618 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1619 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1620 Bool.True, (Vector.VCons ((Nat.S Nat.O),
1621 Bool.True, (Vector.VCons (Nat.O, i1,
1622 Vector.VEmpty)))))))))))))))), List.Nil))
1624 (fun _ -> assert false (* absurd case *))
1626 (fun _ -> assert false (* absurd case *))
1628 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S
1629 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
1630 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1631 (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1632 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1633 Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
1634 (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1635 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1636 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1637 Bool.True, (Vector.VCons ((Nat.S Nat.O),
1638 Bool.True, (Vector.VCons (Nat.O, i1,
1639 Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1642 (fun _ -> assert false (* absurd case *))
1644 (fun _ -> assert false (* absurd case *))
1646 (fun _ -> assert false (* absurd case *))
1647 | ASM.EXT_INDIRECT_DPTR ->
1648 (fun _ -> assert false (* absurd case *))
1649 | ASM.INDIRECT_DPTR ->
1650 (fun _ -> assert false (* absurd case *))
1652 (fun _ -> assert false (* absurd case *))
1653 | ASM.BIT_ADDR x0 ->
1654 (fun _ -> assert false (* absurd case *))
1655 | ASM.N_BIT_ADDR x0 ->
1656 (fun _ -> assert false (* absurd case *))
1657 | ASM.RELATIVE x0 ->
1658 (fun _ -> assert false (* absurd case *))
1660 (fun _ -> assert false (* absurd case *))
1662 (fun _ -> assert false (* absurd case *))) __)
1663 | ASM.EXT_INDIRECT x ->
1664 (fun _ -> assert false (* absurd case *))
1667 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
1668 (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1669 ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1670 ASM.Direct, (Vector.VCons (Nat.O, ASM.Data,
1671 Vector.VEmpty)))))) addr2 with
1674 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1675 Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1676 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1677 Nat.O)))), Bool.True, (Vector.VCons ((Nat.S
1678 (Nat.S (Nat.S Nat.O))), Bool.False,
1679 (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1680 Bool.True, (Vector.VCons ((Nat.S Nat.O),
1681 Bool.False, (Vector.VCons (Nat.O, Bool.True,
1682 Vector.VEmpty)))))))))) r), (List.Cons (b1,
1684 | ASM.INDIRECT x0 ->
1685 (fun _ -> assert false (* absurd case *))
1686 | ASM.EXT_INDIRECT x0 ->
1687 (fun _ -> assert false (* absurd case *))
1688 | ASM.REGISTER x0 ->
1689 (fun _ -> assert false (* absurd case *))
1692 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1693 Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1694 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1695 Nat.O)))), Bool.True, (Vector.VCons ((Nat.S
1696 (Nat.S (Nat.S Nat.O))), Bool.True,
1697 (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1698 Bool.True, (Vector.VCons ((Nat.S Nat.O),
1699 Bool.True, (Vector.VCons (Nat.O, Bool.True,
1700 Vector.VEmpty)))))))))) r), List.Nil))
1702 (fun _ -> assert false (* absurd case *))
1704 (fun _ -> assert false (* absurd case *))
1707 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1708 Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1709 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1710 Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
1711 (Nat.S (Nat.S Nat.O))), Bool.True,
1712 (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1713 Bool.True, (Vector.VCons ((Nat.S Nat.O),
1714 Bool.True, (Vector.VCons (Nat.O, Bool.True,
1715 Vector.VEmpty)))))))))) r), (List.Cons (b1,
1718 (fun _ -> assert false (* absurd case *))
1720 (fun _ -> assert false (* absurd case *))
1722 (fun _ -> assert false (* absurd case *))
1723 | ASM.EXT_INDIRECT_DPTR ->
1724 (fun _ -> assert false (* absurd case *))
1725 | ASM.INDIRECT_DPTR ->
1726 (fun _ -> assert false (* absurd case *))
1728 (fun _ -> assert false (* absurd case *))
1729 | ASM.BIT_ADDR x0 ->
1730 (fun _ -> assert false (* absurd case *))
1731 | ASM.N_BIT_ADDR x0 ->
1732 (fun _ -> assert false (* absurd case *))
1733 | ASM.RELATIVE x0 ->
1734 (fun _ -> assert false (* absurd case *))
1736 (fun _ -> assert false (* absurd case *))
1738 (fun _ -> assert false (* absurd case *))) __)
1739 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1740 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1741 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1742 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1743 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1744 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1745 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1746 | ASM.EXT_INDIRECT_DPTR ->
1747 (fun _ -> assert false (* absurd case *))
1748 | ASM.INDIRECT_DPTR ->
1749 (fun _ -> assert false (* absurd case *))
1750 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1752 (fun _ -> assert false (* absurd case *))
1753 | ASM.N_BIT_ADDR x ->
1754 (fun _ -> assert false (* absurd case *))
1756 (fun _ -> assert false (* absurd case *))
1757 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1758 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1760 | Types.Inr addrs3 ->
1761 let { Types.fst = addr1; Types.snd = addr2 } = addrs3 in
1763 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1764 ASM.Direct, Vector.VEmpty)) addr1 with
1765 | ASM.DIRECT b1 -> (fun _ -> b1)
1767 (fun _ -> assert false (* absurd case *))
1768 | ASM.EXT_INDIRECT x ->
1769 (fun _ -> assert false (* absurd case *))
1771 (fun _ -> assert false (* absurd case *))
1772 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1773 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1774 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1775 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1776 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1777 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1778 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1779 | ASM.EXT_INDIRECT_DPTR ->
1780 (fun _ -> assert false (* absurd case *))
1781 | ASM.INDIRECT_DPTR ->
1782 (fun _ -> assert false (* absurd case *))
1783 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1785 (fun _ -> assert false (* absurd case *))
1786 | ASM.N_BIT_ADDR x ->
1787 (fun _ -> assert false (* absurd case *))
1789 (fun _ -> assert false (* absurd case *))
1790 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1791 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1794 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S
1795 Nat.O)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1796 Nat.O)))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1797 (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
1798 (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
1799 Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
1800 Vector.VEmpty)))))))))) addr2 with
1802 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1803 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1804 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1805 Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1806 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons
1807 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1808 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1809 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1810 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
1811 (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1812 (List.Cons (b1, (List.Cons (b2, List.Nil))))))
1813 | ASM.INDIRECT i1 ->
1814 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1815 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1816 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1817 Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1818 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons
1819 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1820 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1821 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1822 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1823 (Nat.O, i1, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1825 | ASM.EXT_INDIRECT x ->
1826 (fun _ -> assert false (* absurd case *))
1829 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1830 Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
1831 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1832 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1833 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1834 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1835 (Vector.VCons (Nat.O, Bool.True,
1836 Vector.VEmpty)))))))))) r), (List.Cons (b1,
1839 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1840 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1841 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1842 Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1843 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons
1844 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1845 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1846 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1847 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
1848 (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1849 (List.Cons (b1, List.Nil))))
1850 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1851 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1853 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1854 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False,
1855 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1856 Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1857 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons
1858 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1859 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1860 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1861 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
1862 (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1863 (List.Cons (b1, (List.Cons (b2, List.Nil))))))
1864 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1865 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1866 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1867 | ASM.EXT_INDIRECT_DPTR ->
1868 (fun _ -> assert false (* absurd case *))
1869 | ASM.INDIRECT_DPTR ->
1870 (fun _ -> assert false (* absurd case *))
1871 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1872 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1873 | ASM.N_BIT_ADDR x ->
1874 (fun _ -> assert false (* absurd case *))
1875 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1876 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1877 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1879 | Types.Inr addrs2 ->
1880 let { Types.fst = addr1; Types.snd = addr2 } = addrs2 in
1881 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1882 ASM.Data16, Vector.VEmpty)) addr2 with
1883 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1884 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1885 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1886 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1887 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1888 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1889 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1890 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1894 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1895 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
1896 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) w
1898 let b1 = b1_b2.Types.fst in
1899 let b2 = b1_b2.Types.snd in
1900 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1901 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1902 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1903 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1904 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1905 Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1906 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1907 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1908 (Vector.VCons (Nat.O, Bool.False,
1909 Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons
1911 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1912 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1913 | ASM.EXT_INDIRECT_DPTR ->
1914 (fun _ -> assert false (* absurd case *))
1915 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1916 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1917 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1918 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1919 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1920 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1921 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1922 | Types.Inr addrs1 ->
1923 let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
1924 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1925 ASM.Bit_addr, Vector.VEmpty)) addr2 with
1926 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1927 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1928 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1929 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1930 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1931 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1932 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1933 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1934 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1935 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1936 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1937 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1938 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1939 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1940 | ASM.BIT_ADDR b1 ->
1941 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1942 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons
1943 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1944 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1945 Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1946 (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1947 (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1948 Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1949 (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
1950 (List.Cons (b1, List.Nil))))
1951 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1952 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1953 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1954 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1955 | Types.Inr addrs0 ->
1956 let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1957 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1958 ASM.Bit_addr, Vector.VEmpty)) addr1 with
1959 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1960 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1961 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1962 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1963 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1964 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1965 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1966 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1967 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1968 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1969 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1970 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1971 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1972 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1973 | ASM.BIT_ADDR b1 ->
1974 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1975 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1976 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1977 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1978 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1979 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1980 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1981 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1982 Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1984 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1985 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1986 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1987 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1990 | Types.Inl addrs0 ->
1991 let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1992 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1993 Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1994 ASM.Ext_indirect_dptr, Vector.VEmpty)))) addr2 with
1995 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1996 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1997 | ASM.EXT_INDIRECT i1 ->
1998 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1999 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2000 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2001 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2002 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2003 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2004 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2005 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
2006 Vector.VEmpty)))))))))))))))), List.Nil))
2007 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2008 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2009 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2010 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2011 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2012 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2013 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2014 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2015 | ASM.EXT_INDIRECT_DPTR ->
2016 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2017 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2018 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2019 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2020 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2021 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2022 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2023 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
2024 Bool.False, Vector.VEmpty)))))))))))))))), List.Nil))
2025 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2026 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2027 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2028 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2029 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2030 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2031 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2032 | Types.Inr addrs0 ->
2033 let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
2034 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
2035 Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
2036 ASM.Ext_indirect_dptr, Vector.VEmpty)))) addr1 with
2037 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2038 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2039 | ASM.EXT_INDIRECT i1 ->
2040 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2041 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2042 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2043 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2044 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2045 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2046 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2047 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
2048 Vector.VEmpty)))))))))))))))), List.Nil))
2049 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2050 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2051 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2052 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2053 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2054 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2055 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2056 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2057 | ASM.EXT_INDIRECT_DPTR ->
2058 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2059 (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2060 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2061 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2062 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2063 Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2064 Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2065 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
2066 Bool.False, Vector.VEmpty)))))))))))))))), List.Nil))
2067 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2068 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2069 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2070 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2071 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2072 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2073 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
2075 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
2076 ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))
2078 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2079 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2080 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2081 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2082 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2083 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2084 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2085 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2086 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2087 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2088 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2089 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2090 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2092 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2093 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2094 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2095 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2096 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
2097 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2098 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2099 ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
2100 Vector.VEmpty)))))))))))))))), List.Nil))
2101 | ASM.BIT_ADDR b1 ->
2102 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2103 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2104 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2105 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2106 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
2107 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2108 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2109 ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False,
2110 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
2111 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2112 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2113 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2114 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2116 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Direct,
2117 Vector.VEmpty)) addr with
2119 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2120 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2121 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2122 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2123 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
2124 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2125 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2126 ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
2127 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
2128 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2129 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2130 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2131 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2132 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2133 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2134 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2135 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2136 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2137 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2138 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2139 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2140 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2141 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2142 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2143 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2144 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2145 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2147 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Direct,
2148 Vector.VEmpty)) addr with
2150 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2151 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2152 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2153 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2154 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
2155 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2156 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2157 ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
2158 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
2159 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2160 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2161 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2162 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2163 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2164 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2165 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2166 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2167 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2168 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2169 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2170 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2171 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2172 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2173 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2174 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2175 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2176 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2177 | ASM.XCH (addr1, addr2) ->
2178 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
2179 (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O),
2180 ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
2181 Vector.VEmpty)))))) addr2 with
2183 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2184 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2185 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2186 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2187 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
2188 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2189 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
2190 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
2191 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
2192 | ASM.INDIRECT i1 ->
2193 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2194 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2195 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2196 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2197 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
2198 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2199 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
2200 Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
2201 Vector.VEmpty)))))))))))))))), List.Nil))
2202 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2205 ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
2206 (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2207 Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2208 Bool.True, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2209 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
2210 Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
2211 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2212 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2213 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2214 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2215 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2216 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2217 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2218 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2219 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2220 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2221 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2222 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2223 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2224 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2225 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2226 | ASM.XCHD (addr1, addr2) ->
2227 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Indirect,
2228 Vector.VEmpty)) addr2 with
2229 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2230 | ASM.INDIRECT i1 ->
2231 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2232 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2233 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2234 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2235 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
2236 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2237 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
2238 Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
2239 Vector.VEmpty)))))))))))))))), List.Nil))
2240 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2241 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2242 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2243 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2244 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2245 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2246 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2247 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2248 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2249 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2250 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2251 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2252 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2253 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2254 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2255 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2256 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2258 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2259 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2260 (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
2261 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2262 (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2263 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2264 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
2265 Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
2267 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2268 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2269 (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
2270 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2271 (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2272 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2273 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
2274 Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
2276 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2277 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2278 (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
2279 (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
2280 (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2281 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2282 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
2283 Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
2285 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2286 Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2287 (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2288 (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2289 (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2290 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2291 (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
2292 Vector.VEmpty)))))))))))))))), List.Nil)
2294 (** val assembly1 : ASM.instruction -> Bool.bool Vector.vector List.list **)
2295 let assembly1 = function
2297 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr11,
2298 Vector.VEmpty)) addr with
2299 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2300 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2301 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2302 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2303 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2304 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2305 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2306 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2307 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2308 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2309 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2310 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2311 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2312 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2313 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2314 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2315 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2319 Vector.vsplit (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
2320 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) w
2322 let v1 = v1_v2.Types.fst in
2323 let v2 = v1_v2.Types.snd in
2325 ((Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
2326 (Nat.S (Nat.S Nat.O))))) v1 (Vector.VCons ((Nat.S (Nat.S (Nat.S
2327 (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2328 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2329 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
2330 (Nat.O, Bool.True, Vector.VEmpty))))))))))), (List.Cons (v2,
2332 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2334 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr16,
2335 Vector.VEmpty)) addr with
2336 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2337 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2338 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2339 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2340 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2341 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2342 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2343 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2344 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2345 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2346 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2347 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2348 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2349 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2350 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2351 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2352 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2353 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2357 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2358 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2359 (Nat.S (Nat.S Nat.O)))))))) w
2361 let b1 = b1_b2.Types.fst in
2362 let b2 = b1_b2.Types.snd in
2363 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2364 (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2365 (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S
2366 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons
2367 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons
2368 ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S
2369 (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
2370 (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
2371 (List.Cons (b1, (List.Cons (b2, List.Nil))))))) __
2373 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr11,
2374 Vector.VEmpty)) addr with
2375 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2376 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2377 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2378 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2379 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2380 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2381 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2382 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2383 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2384 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2385 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2386 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2387 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2388 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2389 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2390 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2391 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2395 Vector.vsplit (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
2396 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) w
2398 let v1 = v1_v2.Types.fst in
2399 let v2 = v1_v2.Types.snd in
2401 ((Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
2402 (Nat.S (Nat.S Nat.O))))) v1 (Vector.VCons ((Nat.S (Nat.S (Nat.S
2403 (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2404 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2405 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
2406 (Nat.O, Bool.True, Vector.VEmpty))))))))))), (List.Cons (v2,
2408 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2410 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr16,
2411 Vector.VEmpty)) addr with
2412 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2413 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2414 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2415 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2416 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2417 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2418 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2419 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2420 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2421 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2422 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2423 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2424 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2425 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2426 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2427 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2428 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2429 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2433 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2434 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2435 (Nat.S (Nat.S Nat.O)))))))) w
2437 let b1 = b1_b2.Types.fst in
2438 let b2 = b1_b2.Types.snd in
2439 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2440 (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2441 (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S
2442 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons
2443 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons
2444 ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S
2445 (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
2446 (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
2447 (List.Cons (b1, (List.Cons (b2, List.Nil))))))) __
2449 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Relative,
2450 Vector.VEmpty)) addr with
2451 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2452 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2453 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2454 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2455 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2456 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2457 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2458 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2459 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2460 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2461 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2462 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2463 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2464 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2465 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2466 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2467 | ASM.RELATIVE b1 ->
2468 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2469 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2470 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
2471 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2472 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
2473 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2474 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2475 ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
2476 Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
2477 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2478 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2479 | ASM.MOVC (addr1, addr2) ->
2480 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
2481 ASM.Acc_dptr, (Vector.VCons (Nat.O, ASM.Acc_pc, Vector.VEmpty))))
2483 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2484 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2485 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2486 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2487 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2488 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2489 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2490 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2491 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2493 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2494 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2495 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
2496 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2497 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
2498 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2499 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2500 ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
2501 Vector.VEmpty)))))))))))))))), List.Nil))
2503 (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2504 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2505 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
2506 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2507 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
2508 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2509 (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2510 ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
2511 Vector.VEmpty)))))))))))))))), List.Nil))
2512 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2513 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2514 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2515 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2516 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2517 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2518 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2519 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2520 | ASM.RealInstruction instr ->
2521 assembly_preinstruction (fun x ->
2522 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Relative,
2523 Vector.VEmpty)) x with
2524 | ASM.DIRECT x0 -> (fun _ -> assert false (* absurd case *))
2525 | ASM.INDIRECT x0 -> (fun _ -> assert false (* absurd case *))
2526 | ASM.EXT_INDIRECT x0 -> (fun _ -> assert false (* absurd case *))
2527 | ASM.REGISTER x0 -> (fun _ -> assert false (* absurd case *))
2528 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2529 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2530 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2531 | ASM.DATA x0 -> (fun _ -> assert false (* absurd case *))
2532 | ASM.DATA16 x0 -> (fun _ -> assert false (* absurd case *))
2533 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2534 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2535 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2536 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2537 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2538 | ASM.BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *))
2539 | ASM.N_BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *))
2540 | ASM.RELATIVE r -> (fun _ -> r)
2541 | ASM.ADDR11 x0 -> (fun _ -> assert false (* absurd case *))
2542 | ASM.ADDR16 x0 -> (fun _ -> assert false (* absurd case *))) __) instr
2544 (** val expand_relative_jump_internal :
2545 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
2546 -> (BitVector.word -> Bool.bool) -> ASM.identifier -> BitVector.word ->
2547 (ASM.subaddressing_mode -> ASM.subaddressing_mode ASM.preinstruction) ->
2548 ASM.instruction List.list **)
2549 let expand_relative_jump_internal lookup_labels sigma policy lbl ppc i =
2550 let lookup_address = sigma (lookup_labels lbl) in
2551 let pc_plus_jmp_length =
2553 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2554 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2555 Nat.O)))))))))))))))) ppc
2556 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2557 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2558 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2560 let { Types.fst = sj_possible; Types.snd = disp } =
2561 short_jump_cond pc_plus_jmp_length lookup_address
2563 (match Bool.andb sj_possible (Bool.notb (policy ppc)) with
2565 let address = ASM.RELATIVE disp in
2566 List.Cons ((ASM.RealInstruction (i address)), List.Nil)
2568 List.Cons ((ASM.RealInstruction
2570 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2571 (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S Nat.O)))))),
2572 (List.Cons ((ASM.SJMP (ASM.RELATIVE
2573 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2574 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S Nat.O)))))),
2575 (List.Cons ((ASM.LJMP (ASM.ADDR16 lookup_address)), List.Nil))))))
2577 (** val expand_relative_jump :
2578 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
2579 -> (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier
2580 ASM.preinstruction -> ASM.instruction List.list **)
2581 let expand_relative_jump lookup_labels sigma policy ppc = function
2582 | ASM.ADD (arg1, arg2) ->
2583 List.Cons ((ASM.RealInstruction (ASM.ADD (arg1, arg2))), List.Nil)
2584 | ASM.ADDC (arg1, arg2) ->
2585 List.Cons ((ASM.RealInstruction (ASM.ADDC (arg1, arg2))), List.Nil)
2586 | ASM.SUBB (arg1, arg2) ->
2587 List.Cons ((ASM.RealInstruction (ASM.SUBB (arg1, arg2))), List.Nil)
2588 | ASM.INC arg -> List.Cons ((ASM.RealInstruction (ASM.INC arg)), List.Nil)
2589 | ASM.DEC arg -> List.Cons ((ASM.RealInstruction (ASM.DEC arg)), List.Nil)
2590 | ASM.MUL (arg1, arg2) ->
2591 List.Cons ((ASM.RealInstruction (ASM.MUL (arg1, arg2))), List.Nil)
2592 | ASM.DIV (arg1, arg2) ->
2593 List.Cons ((ASM.RealInstruction (ASM.DIV (arg1, arg2))), List.Nil)
2594 | ASM.DA arg -> List.Cons ((ASM.RealInstruction (ASM.DA arg)), List.Nil)
2596 expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2599 expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2601 | ASM.JB (baddr, jmp) ->
2602 expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2604 | ASM.JNB (baddr, jmp) ->
2605 expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2607 | ASM.JBC (baddr, jmp) ->
2608 expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2611 expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2614 expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2616 | ASM.CJNE (addr, jmp) ->
2617 expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2619 | ASM.DJNZ (addr, jmp) ->
2620 expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2622 | ASM.ANL arg -> List.Cons ((ASM.RealInstruction (ASM.ANL arg)), List.Nil)
2623 | ASM.ORL arg -> List.Cons ((ASM.RealInstruction (ASM.ORL arg)), List.Nil)
2624 | ASM.XRL arg -> List.Cons ((ASM.RealInstruction (ASM.XRL arg)), List.Nil)
2625 | ASM.CLR arg -> List.Cons ((ASM.RealInstruction (ASM.CLR arg)), List.Nil)
2626 | ASM.CPL arg -> List.Cons ((ASM.RealInstruction (ASM.CPL arg)), List.Nil)
2627 | ASM.RL arg -> List.Cons ((ASM.RealInstruction (ASM.RL arg)), List.Nil)
2628 | ASM.RLC arg -> List.Cons ((ASM.RealInstruction (ASM.RLC arg)), List.Nil)
2629 | ASM.RR arg -> List.Cons ((ASM.RealInstruction (ASM.RR arg)), List.Nil)
2630 | ASM.RRC arg -> List.Cons ((ASM.RealInstruction (ASM.RRC arg)), List.Nil)
2631 | ASM.SWAP arg -> List.Cons ((ASM.RealInstruction (ASM.SWAP arg)), List.Nil)
2632 | ASM.MOV arg -> List.Cons ((ASM.RealInstruction (ASM.MOV arg)), List.Nil)
2633 | ASM.MOVX arg -> List.Cons ((ASM.RealInstruction (ASM.MOVX arg)), List.Nil)
2634 | ASM.SETB arg -> List.Cons ((ASM.RealInstruction (ASM.SETB arg)), List.Nil)
2635 | ASM.PUSH arg -> List.Cons ((ASM.RealInstruction (ASM.PUSH arg)), List.Nil)
2636 | ASM.POP arg -> List.Cons ((ASM.RealInstruction (ASM.POP arg)), List.Nil)
2637 | ASM.XCH (arg1, arg2) ->
2638 List.Cons ((ASM.RealInstruction (ASM.XCH (arg1, arg2))), List.Nil)
2639 | ASM.XCHD (arg1, arg2) ->
2640 List.Cons ((ASM.RealInstruction (ASM.XCHD (arg1, arg2))), List.Nil)
2641 | ASM.RET -> List.Cons ((ASM.RealInstruction ASM.RET), List.Nil)
2642 | ASM.RETI -> List.Cons ((ASM.RealInstruction ASM.RETI), List.Nil)
2643 | ASM.NOP -> List.Cons ((ASM.RealInstruction ASM.NOP), List.Nil)
2644 | ASM.JMP arg -> List.Cons ((ASM.RealInstruction (ASM.JMP arg)), List.Nil)
2646 (** val is_code : AST.region -> Bool.bool **)
2647 let is_code = function
2648 | AST.XData -> Bool.False
2649 | AST.Code -> Bool.True
2651 (** val expand_pseudo_instruction :
2652 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
2653 -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
2654 (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
2655 ASM.instruction List.list **)
2656 let expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels = function
2657 | ASM.Instruction instr ->
2658 expand_relative_jump lookup_labels sigma policy ppc instr
2659 | ASM.Comment comment -> List.Nil
2660 | ASM.Cost cost -> List.Cons ((ASM.RealInstruction ASM.NOP), List.Nil)
2662 let pc_plus_jmp_length =
2664 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2665 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2666 Nat.O)))))))))))))))) ppc
2667 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2668 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2669 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2671 let do_a_long = policy ppc in
2672 let lookup_address = sigma (lookup_labels jmp) in
2673 let { Types.fst = sj_possible; Types.snd = disp } =
2674 short_jump_cond pc_plus_jmp_length lookup_address
2676 (match Bool.andb sj_possible (Bool.notb do_a_long) with
2678 let address = ASM.RELATIVE disp in
2679 List.Cons ((ASM.SJMP address), List.Nil)
2681 let { Types.fst = mj_possible; Types.snd = disp2 } =
2682 absolute_jump_cond pc_plus_jmp_length lookup_address
2684 (match Bool.andb mj_possible (Bool.notb do_a_long) with
2686 let address = ASM.ADDR11 disp2 in
2687 List.Cons ((ASM.AJMP address), List.Nil)
2689 let address = ASM.ADDR16 lookup_address in
2690 List.Cons ((ASM.LJMP address), List.Nil)))
2691 | ASM.Jnz (acc, tgt1, tgt2) ->
2692 let lookup_address1 = sigma (lookup_labels tgt1) in
2693 let lookup_address2 = sigma (lookup_labels tgt2) in
2694 List.Cons ((ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE
2695 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2696 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S Nat.O))))))), (List.Cons
2697 ((ASM.LJMP (ASM.ADDR16 lookup_address2)), (List.Cons ((ASM.LJMP (ASM.ADDR16
2698 lookup_address1)), List.Nil)))))
2700 let pc_plus_jmp_length =
2702 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2703 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2704 Nat.O)))))))))))))))) ppc
2705 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2706 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2707 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2709 let lookup_address = sigma (lookup_labels call) in
2710 let { Types.fst = mj_possible; Types.snd = disp } =
2711 absolute_jump_cond pc_plus_jmp_length lookup_address
2713 let do_a_long = policy ppc in
2714 (match Bool.andb mj_possible (Bool.notb do_a_long) with
2716 let address = ASM.ADDR11 disp in
2717 List.Cons ((ASM.ACALL address), List.Nil)
2719 let address = ASM.ADDR16 lookup_address in
2720 List.Cons ((ASM.LCALL address), List.Nil))
2721 | ASM.Mov (d, trgt, off) ->
2722 let { Types.fst = r; Types.snd = addr } = lookup_datalabels trgt in
2723 let addr0 = (Arithmetic.add_16_with_carry addr off Bool.False).Types.fst in
2725 match is_code r with
2726 | Bool.True -> sigma addr0
2727 | Bool.False -> addr0
2731 let address = ASM.DATA16 addr1 in
2732 List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
2733 (Types.Inr { Types.fst = ASM.DPTR; Types.snd = address }))))), List.Nil)
2736 (match pr.Types.snd with
2738 (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2739 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2740 (Nat.S (Nat.S Nat.O)))))))) addr1).Types.fst
2742 (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2743 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2744 (Nat.S (Nat.S Nat.O)))))))) addr1).Types.snd)
2746 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
2747 ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
2748 Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr,
2749 Vector.VEmpty)))))) pr.Types.fst with
2751 (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
2752 (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b1);
2753 Types.snd = v })))))), List.Nil))
2754 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2755 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2756 | ASM.REGISTER r0 ->
2757 (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
2758 (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
2759 (ASM.REGISTER r0); Types.snd = v }))))))), List.Nil))
2761 (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
2762 (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst =
2763 ASM.ACC_A; Types.snd = v }))))))), List.Nil))
2764 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2765 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2766 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2767 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2768 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2769 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2770 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2771 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2772 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2773 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2774 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2775 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2776 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2777 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
2779 (** val assembly_1_pseudoinstruction :
2780 (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
2781 -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
2782 (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
2783 (Nat.nat, Bool.bool Vector.vector List.list) Types.prod **)
2784 let assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels i =
2786 expand_pseudo_instruction lookup_labels sigma policy ppc
2789 let mapped = List.map assembly1 pseudos in
2790 let flattened = List.flatten mapped in
2791 let pc_len = List.length flattened in
2792 { Types.fst = pc_len; Types.snd = flattened }
2794 (** val instruction_size :
2795 (ASM.identifier -> BitVector.word) -> (ASM.identifier -> (AST.region,
2796 BitVector.word) Types.prod) -> (BitVector.word -> BitVector.word) ->
2797 (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction
2799 let instruction_size lookup_labels lookup_datalabels sigma policy ppc i =
2800 (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
2801 lookup_datalabels i).Types.fst
2804 ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
2805 (BitVector.word -> Bool.bool) -> ASM.labelled_object_code Types.sig0 **)
2806 let assembly p sigma policy =
2807 (let { Types.fst = labels_to_ppc; Types.snd = ppc_to_costs } =
2808 Fetch.create_label_cost_map p.ASM.code
2811 let preamble = p.ASM.preamble in
2812 let instr_list = p.ASM.code in
2813 let datalabels = Status.construct_datalabels preamble in
2814 let lookup_labels = fun x ->
2815 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2816 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2817 Nat.O))))))))))))))))
2818 (Identifiers.lookup_def PreIdentifiers.ASMTag labels_to_ppc x Nat.O)
2820 let lookup_datalabels = fun x ->
2821 match Identifiers.lookup PreIdentifiers.ASMTag
2822 (Status.construct_datalabels preamble) x with
2823 | Types.None -> { Types.fst = AST.Code; Types.snd = (lookup_labels x) }
2824 | Types.Some addr -> { Types.fst = AST.XData; Types.snd = addr }
2826 (let { Types.fst = next_pc; Types.snd = revcode } =
2828 (FoldStuff.foldl_strong instr_list (fun prefix hd tl _ ppc_code ->
2829 (let { Types.fst = ppc; Types.snd = code } = Types.pi1 ppc_code in
2831 (let { Types.fst = pc_delta; Types.snd = program } =
2832 assembly_1_pseudoinstruction lookup_labels sigma policy ppc
2833 lookup_datalabels hd.Types.snd
2837 Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2838 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2839 Nat.O)))))))))))))))) ppc
2840 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2841 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2842 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O))
2844 { Types.fst = new_ppc; Types.snd =
2845 (List.append (List.reverse program) code) })) __)) __) { Types.fst =
2846 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2847 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2848 Nat.O))))))))))))))))); Types.snd = List.Nil })
2851 let code = List.reverse revcode in
2852 { ASM.oc = code; ASM.cm = (ASM.load_code_memory code); ASM.costlabels =
2853 (BitVectorTrie.fold (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2854 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2855 Nat.O)))))))))))))))) (fun ppc cost pc_to_costs ->
2856 BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2857 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2858 Nat.O)))))))))))))))) (sigma ppc) cost pc_to_costs) ppc_to_costs
2859 (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2860 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2861 Nat.O)))))))))))))))))); ASM.symboltable =
2862 (Util.foldl (fun symboltable newident_oldident ->
2863 let ppc = lookup_labels newident_oldident.Types.fst in
2864 BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2865 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2866 Nat.O)))))))))))))))) (sigma ppc) newident_oldident.Types.snd
2867 symboltable) (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2868 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2869 (Nat.S Nat.O))))))))))))))))) p.ASM.renamed_symbols); ASM.final_pc =
2870 (sigma (lookup_labels p.ASM.final_label)) })) __)) __
2872 (** val ticks_of_instruction : ASM.instruction -> Nat.nat **)
2873 let ticks_of_instruction i =
2874 let trivial_code_memory = assembly1 i in
2875 let trivial_status = ASM.load_code_memory trivial_code_memory in
2876 (Fetch.fetch trivial_status
2877 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2878 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2879 Nat.O)))))))))))))))))).Types.snd
2882 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
2883 (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
2884 BitVector.word -> ASM.pseudo_instruction -> (Nat.nat, Nat.nat) Types.prod **)
2885 let ticks_of0 program lookup_labels sigma policy ppc = function
2886 | ASM.Instruction instr ->
2888 | ASM.ADD (arg1, arg2) ->
2890 ticks_of_instruction (ASM.RealInstruction (ASM.ADD (arg1, arg2)))
2892 { Types.fst = ticks; Types.snd = ticks }
2893 | ASM.ADDC (arg1, arg2) ->
2895 ticks_of_instruction (ASM.RealInstruction (ASM.ADDC (arg1, arg2)))
2897 { Types.fst = ticks; Types.snd = ticks }
2898 | ASM.SUBB (arg1, arg2) ->
2900 ticks_of_instruction (ASM.RealInstruction (ASM.SUBB (arg1, arg2)))
2902 { Types.fst = ticks; Types.snd = ticks }
2904 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.INC arg)) in
2905 { Types.fst = ticks; Types.snd = ticks }
2907 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.DEC arg)) in
2908 { Types.fst = ticks; Types.snd = ticks }
2909 | ASM.MUL (arg1, arg2) ->
2911 ticks_of_instruction (ASM.RealInstruction (ASM.MUL (arg1, arg2)))
2913 { Types.fst = ticks; Types.snd = ticks }
2914 | ASM.DIV (arg1, arg2) ->
2916 ticks_of_instruction (ASM.RealInstruction (ASM.DIV (arg1, arg2)))
2918 { Types.fst = ticks; Types.snd = ticks }
2920 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.DA arg)) in
2921 { Types.fst = ticks; Types.snd = ticks }
2923 let lookup_address = sigma (lookup_labels lbl) in
2924 let pc_plus_jmp_length =
2926 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2927 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2928 Nat.O)))))))))))))))) ppc
2929 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2930 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2931 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2933 let { Types.fst = sj_possible; Types.snd = disp } =
2934 short_jump_cond pc_plus_jmp_length lookup_address
2936 (match sj_possible with
2938 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
2941 { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
2942 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
2944 let lookup_address = sigma (lookup_labels lbl) in
2945 let pc_plus_jmp_length =
2947 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2948 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2949 Nat.O)))))))))))))))) ppc
2950 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2951 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2952 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2954 let { Types.fst = sj_possible; Types.snd = disp } =
2955 short_jump_cond pc_plus_jmp_length lookup_address
2957 (match sj_possible with
2959 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
2962 { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
2963 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
2964 | ASM.JB (bit, lbl) ->
2965 let lookup_address = sigma (lookup_labels lbl) in
2966 let pc_plus_jmp_length =
2968 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2969 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2970 Nat.O)))))))))))))))) ppc
2971 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2972 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2973 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2975 let { Types.fst = sj_possible; Types.snd = disp } =
2976 short_jump_cond pc_plus_jmp_length lookup_address
2978 (match sj_possible with
2980 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
2983 { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
2984 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
2985 | ASM.JNB (bit, lbl) ->
2986 let lookup_address = sigma (lookup_labels lbl) in
2987 let pc_plus_jmp_length =
2989 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2990 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2991 Nat.O)))))))))))))))) ppc
2992 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2993 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2994 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2996 let { Types.fst = sj_possible; Types.snd = disp } =
2997 short_jump_cond pc_plus_jmp_length lookup_address
2999 (match sj_possible with
3001 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3004 { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3005 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3006 | ASM.JBC (bit, lbl) ->
3007 let lookup_address = sigma (lookup_labels lbl) in
3008 let pc_plus_jmp_length =
3010 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3011 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3012 Nat.O)))))))))))))))) ppc
3013 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3014 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3015 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3017 let { Types.fst = sj_possible; Types.snd = disp } =
3018 short_jump_cond pc_plus_jmp_length lookup_address
3020 (match sj_possible with
3022 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3025 { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3026 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3028 let lookup_address = sigma (lookup_labels lbl) in
3029 let pc_plus_jmp_length =
3031 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3032 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3033 Nat.O)))))))))))))))) ppc
3034 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3035 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3036 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3038 let { Types.fst = sj_possible; Types.snd = disp } =
3039 short_jump_cond pc_plus_jmp_length lookup_address
3041 (match sj_possible with
3043 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3046 { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3047 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3049 let lookup_address = sigma (lookup_labels lbl) in
3050 let pc_plus_jmp_length =
3052 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3053 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3054 Nat.O)))))))))))))))) ppc
3055 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3056 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3057 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3059 let { Types.fst = sj_possible; Types.snd = disp } =
3060 short_jump_cond pc_plus_jmp_length lookup_address
3062 (match sj_possible with
3064 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3067 { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3068 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3069 | ASM.CJNE (arg, lbl) ->
3070 let lookup_address = sigma (lookup_labels lbl) in
3071 let pc_plus_jmp_length =
3073 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3074 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3075 Nat.O)))))))))))))))) ppc
3076 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3077 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3078 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3080 let { Types.fst = sj_possible; Types.snd = disp } =
3081 short_jump_cond pc_plus_jmp_length lookup_address
3083 (match sj_possible with
3085 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3088 { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3089 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3090 | ASM.DJNZ (arg, lbl) ->
3091 let lookup_address = sigma (lookup_labels lbl) in
3092 let pc_plus_jmp_length =
3094 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3095 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3096 Nat.O)))))))))))))))) ppc
3097 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3098 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3099 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3101 let { Types.fst = sj_possible; Types.snd = disp } =
3102 short_jump_cond pc_plus_jmp_length lookup_address
3104 (match sj_possible with
3106 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3109 { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3110 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3112 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.ANL arg)) in
3113 { Types.fst = ticks; Types.snd = ticks }
3115 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.ORL arg)) in
3116 { Types.fst = ticks; Types.snd = ticks }
3118 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.XRL arg)) in
3119 { Types.fst = ticks; Types.snd = ticks }
3121 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.CLR arg)) in
3122 { Types.fst = ticks; Types.snd = ticks }
3124 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.CPL arg)) in
3125 { Types.fst = ticks; Types.snd = ticks }
3127 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RL arg)) in
3128 { Types.fst = ticks; Types.snd = ticks }
3130 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RLC arg)) in
3131 { Types.fst = ticks; Types.snd = ticks }
3133 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RR arg)) in
3134 { Types.fst = ticks; Types.snd = ticks }
3136 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RRC arg)) in
3137 { Types.fst = ticks; Types.snd = ticks }
3139 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.SWAP arg)) in
3140 { Types.fst = ticks; Types.snd = ticks }
3142 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.MOV arg)) in
3143 { Types.fst = ticks; Types.snd = ticks }
3145 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.MOVX arg)) in
3146 { Types.fst = ticks; Types.snd = ticks }
3148 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.SETB arg)) in
3149 { Types.fst = ticks; Types.snd = ticks }
3151 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.PUSH arg)) in
3152 { Types.fst = ticks; Types.snd = ticks }
3154 let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.POP arg)) in
3155 { Types.fst = ticks; Types.snd = ticks }
3156 | ASM.XCH (arg1, arg2) ->
3158 ticks_of_instruction (ASM.RealInstruction (ASM.XCH (arg1, arg2)))
3160 { Types.fst = ticks; Types.snd = ticks }
3161 | ASM.XCHD (arg1, arg2) ->
3163 ticks_of_instruction (ASM.RealInstruction (ASM.XCHD (arg1, arg2)))
3165 { Types.fst = ticks; Types.snd = ticks }
3167 let ticks = ticks_of_instruction (ASM.RealInstruction ASM.RET) in
3168 { Types.fst = ticks; Types.snd = ticks }
3170 let ticks = ticks_of_instruction (ASM.RealInstruction ASM.RETI) in
3171 { Types.fst = ticks; Types.snd = ticks }
3173 let ticks = ticks_of_instruction (ASM.RealInstruction ASM.NOP) in
3174 { Types.fst = ticks; Types.snd = ticks }
3176 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) })
3177 | ASM.Comment comment -> { Types.fst = Nat.O; Types.snd = Nat.O }
3179 let ticks = ticks_of_instruction (ASM.RealInstruction ASM.NOP) in
3180 { Types.fst = ticks; Types.snd = ticks }
3182 let pc_plus_jmp_length =
3184 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3185 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3186 Nat.O)))))))))))))))) ppc
3187 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3188 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3189 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3191 let do_a_long = policy ppc in
3192 let lookup_address = sigma (lookup_labels jmp) in
3193 let { Types.fst = sj_possible; Types.snd = disp } =
3194 short_jump_cond pc_plus_jmp_length lookup_address
3196 (match Bool.andb sj_possible (Bool.notb do_a_long) with
3198 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }
3200 let { Types.fst = mj_possible; Types.snd = disp2 } =
3201 absolute_jump_cond pc_plus_jmp_length lookup_address
3203 (match Bool.andb mj_possible (Bool.notb do_a_long) with
3205 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3208 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3210 | ASM.Jnz (x, x0, x1) ->
3211 { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S
3212 (Nat.S (Nat.S (Nat.S Nat.O)))) }
3214 let pc_plus_jmp_length =
3216 (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3217 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3218 Nat.O)))))))))))))))) ppc
3219 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3220 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3221 (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3223 let lookup_address = sigma (lookup_labels call) in
3224 let { Types.fst = mj_possible; Types.snd = disp } =
3225 absolute_jump_cond pc_plus_jmp_length lookup_address
3227 let do_a_long = policy ppc in
3228 (match Bool.andb mj_possible (Bool.notb do_a_long) with
3230 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }
3232 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) })
3233 | ASM.Mov (dst, lbl, off) ->
3236 { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }
3238 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
3239 ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
3240 Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr,
3241 Vector.VEmpty)))))) pr.Types.fst with
3243 (fun _ -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S
3245 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
3246 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
3248 (fun _ -> { Types.fst = (Nat.S Nat.O); Types.snd = (Nat.S Nat.O) })
3250 (fun _ -> { Types.fst = (Nat.S Nat.O); Types.snd = (Nat.S Nat.O) })
3251 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
3252 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
3253 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
3254 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
3255 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
3256 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
3257 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3258 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3259 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
3260 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3261 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3262 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
3263 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
3264 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
3267 ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
3268 (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
3269 BitVector.word -> (Nat.nat, Nat.nat) Types.prod **)
3270 let ticks_of program addr_of sigma policy ppc =
3271 let { Types.fst = fetched; Types.snd = new_ppc } =
3272 ASM.fetch_pseudo_instruction program.ASM.code ppc
3274 ticks_of0 program addr_of sigma policy ppc fetched