43 open Hints_declaration
79 type identifier = PreIdentifiers.identifier
82 PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier
84 type addressing_mode =
85 | DIRECT of BitVector.byte
86 | INDIRECT of BitVector.bit
87 | EXT_INDIRECT of BitVector.bit
88 | REGISTER of BitVector.bitVector
92 | DATA of BitVector.byte
93 | DATA16 of BitVector.word
99 | BIT_ADDR of BitVector.byte
100 | N_BIT_ADDR of BitVector.byte
101 | RELATIVE of BitVector.byte
102 | ADDR11 of BitVector.word11
103 | ADDR16 of BitVector.word
105 val addressing_mode_rect_Type4 :
106 (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
107 -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
108 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
109 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
110 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
111 addressing_mode -> 'a1
113 val addressing_mode_rect_Type5 :
114 (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
115 -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
116 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
117 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
118 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
119 addressing_mode -> 'a1
121 val addressing_mode_rect_Type3 :
122 (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
123 -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
124 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
125 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
126 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
127 addressing_mode -> 'a1
129 val addressing_mode_rect_Type2 :
130 (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
131 -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
132 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
133 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
134 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
135 addressing_mode -> 'a1
137 val addressing_mode_rect_Type1 :
138 (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
139 -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
140 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
141 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
142 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
143 addressing_mode -> 'a1
145 val addressing_mode_rect_Type0 :
146 (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> 'a1)
147 -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (BitVector.byte ->
148 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
149 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (BitVector.byte ->
150 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word -> 'a1) ->
151 addressing_mode -> 'a1
153 val addressing_mode_inv_rect_Type4 :
154 addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
155 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
156 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
157 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
158 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
159 (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
160 (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
162 val addressing_mode_inv_rect_Type3 :
163 addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
164 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
165 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
166 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
167 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
168 (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
169 (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
171 val addressing_mode_inv_rect_Type2 :
172 addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
173 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
174 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
175 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
176 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
177 (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
178 (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
180 val addressing_mode_inv_rect_Type1 :
181 addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
182 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
183 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
184 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
185 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
186 (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
187 (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
189 val addressing_mode_inv_rect_Type0 :
190 addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ ->
191 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> 'a1)
192 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ ->
193 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
194 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
195 (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) ->
196 (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1
198 val addressing_mode_discr : addressing_mode -> addressing_mode -> __
200 val addressing_mode_jmdiscr : addressing_mode -> addressing_mode -> __
202 val eq_addressing_mode : addressing_mode -> addressing_mode -> Bool.bool
204 type addressing_mode_tag =
225 val addressing_mode_tag_rect_Type4 :
226 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
227 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
228 addressing_mode_tag -> 'a1
230 val addressing_mode_tag_rect_Type5 :
231 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
232 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
233 addressing_mode_tag -> 'a1
235 val addressing_mode_tag_rect_Type3 :
236 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
237 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
238 addressing_mode_tag -> 'a1
240 val addressing_mode_tag_rect_Type2 :
241 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
242 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
243 addressing_mode_tag -> 'a1
245 val addressing_mode_tag_rect_Type1 :
246 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
247 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
248 addressing_mode_tag -> 'a1
250 val addressing_mode_tag_rect_Type0 :
251 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
252 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
253 addressing_mode_tag -> 'a1
255 val addressing_mode_tag_inv_rect_Type4 :
256 addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
257 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
258 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
259 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
262 val addressing_mode_tag_inv_rect_Type3 :
263 addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
264 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
265 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
266 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
269 val addressing_mode_tag_inv_rect_Type2 :
270 addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
271 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
272 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
273 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
276 val addressing_mode_tag_inv_rect_Type1 :
277 addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
278 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
279 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
280 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
283 val addressing_mode_tag_inv_rect_Type0 :
284 addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
285 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
286 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
287 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
290 val addressing_mode_tag_discr :
291 addressing_mode_tag -> addressing_mode_tag -> __
293 val addressing_mode_tag_jmdiscr :
294 addressing_mode_tag -> addressing_mode_tag -> __
296 val eq_a : addressing_mode_tag -> addressing_mode_tag -> Bool.bool
298 val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool
301 Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode ->
304 type subaddressing_mode =
306 (* singleton inductive, whose constructor was mk_subaddressing_mode *)
308 val subaddressing_mode_rect_Type4 :
309 Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
310 'a1) -> subaddressing_mode -> 'a1
312 val subaddressing_mode_rect_Type5 :
313 Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
314 'a1) -> subaddressing_mode -> 'a1
316 val subaddressing_mode_rect_Type3 :
317 Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
318 'a1) -> subaddressing_mode -> 'a1
320 val subaddressing_mode_rect_Type2 :
321 Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
322 'a1) -> subaddressing_mode -> 'a1
324 val subaddressing_mode_rect_Type1 :
325 Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
326 'a1) -> subaddressing_mode -> 'a1
328 val subaddressing_mode_rect_Type0 :
329 Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
330 'a1) -> subaddressing_mode -> 'a1
332 val subaddressing_modeel :
333 Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
336 val subaddressing_mode_inv_rect_Type4 :
337 Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
338 (addressing_mode -> __ -> __ -> 'a1) -> 'a1
340 val subaddressing_mode_inv_rect_Type3 :
341 Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
342 (addressing_mode -> __ -> __ -> 'a1) -> 'a1
344 val subaddressing_mode_inv_rect_Type2 :
345 Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
346 (addressing_mode -> __ -> __ -> 'a1) -> 'a1
348 val subaddressing_mode_inv_rect_Type1 :
349 Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
350 (addressing_mode -> __ -> __ -> 'a1) -> 'a1
352 val subaddressing_mode_inv_rect_Type0 :
353 Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
354 (addressing_mode -> __ -> __ -> 'a1) -> 'a1
356 val subaddressing_mode_discr :
357 Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
358 subaddressing_mode -> __
360 val subaddressing_mode_jmdiscr :
361 Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
362 subaddressing_mode -> __
364 val dpi1__o__subaddressing_modeel__o__inject :
365 Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
366 Types.dPair -> addressing_mode Types.sig0
368 val eject__o__subaddressing_modeel__o__inject :
369 Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
370 Types.sig0 -> addressing_mode Types.sig0
372 val subaddressing_modeel__o__inject :
373 Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode ->
374 addressing_mode Types.sig0
376 val dpi1__o__subaddressing_modeel :
377 Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
378 Types.dPair -> addressing_mode
380 val eject__o__subaddressing_modeel :
381 Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
382 Types.sig0 -> addressing_mode
384 type 'x1 dpi1__o__subaddressing_mode = subaddressing_mode
386 type eject__o__subaddressing_mode = subaddressing_mode
388 val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
389 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
390 addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
391 -> subaddressing_mode Types.sig0
393 val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
394 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
395 addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
396 -> addressing_mode Types.sig0
398 val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
399 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
400 addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
403 val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
404 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
405 addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
406 subaddressing_mode Types.sig0
408 val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
409 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
410 addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
411 addressing_mode Types.sig0
413 val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
414 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
415 addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
418 val subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
419 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
420 addressing_mode_tag Vector.vector -> subaddressing_mode ->
421 subaddressing_mode Types.sig0
423 val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
424 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
425 addressing_mode_tag Vector.vector -> subaddressing_mode -> addressing_mode
428 val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
429 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
430 addressing_mode_tag Vector.vector -> subaddressing_mode -> addressing_mode
432 val dpi1__o__mk_subaddressing_mode__o__inject :
433 Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
434 Vector.vector -> subaddressing_mode Types.sig0
436 val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
437 Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
438 Vector.vector -> addressing_mode Types.sig0
440 val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel :
441 Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
442 Vector.vector -> addressing_mode
444 val eject__o__mk_subaddressing_mode__o__inject :
445 Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
446 -> subaddressing_mode Types.sig0
448 val eject__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
449 Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
450 -> addressing_mode Types.sig0
452 val eject__o__mk_subaddressing_mode__o__subaddressing_modeel :
453 Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
456 val mk_subaddressing_mode__o__subaddressing_modeel :
457 Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
460 val mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
461 Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
462 addressing_mode Types.sig0
464 val mk_subaddressing_mode__o__inject :
465 Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
466 subaddressing_mode Types.sig0
468 val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode :
469 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
470 addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
471 -> subaddressing_mode
473 val eject__o__subaddressing_modeel__o__mk_subaddressing_mode :
474 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
475 addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
478 val subaddressing_modeel__o__mk_subaddressing_mode :
479 Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
480 addressing_mode_tag Vector.vector -> subaddressing_mode ->
483 val dpi1__o__mk_subaddressing_mode :
484 Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
485 Vector.vector -> subaddressing_mode
487 val eject__o__mk_subaddressing_mode :
488 Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
489 -> subaddressing_mode
491 type 'a preinstruction =
492 | ADD of subaddressing_mode * subaddressing_mode
493 | ADDC of subaddressing_mode * subaddressing_mode
494 | SUBB of subaddressing_mode * subaddressing_mode
495 | INC of subaddressing_mode
496 | DEC of subaddressing_mode
497 | MUL of subaddressing_mode * subaddressing_mode
498 | DIV of subaddressing_mode * subaddressing_mode
499 | DA of subaddressing_mode
502 | JB of subaddressing_mode * 'a
503 | JNB of subaddressing_mode * 'a
504 | JBC of subaddressing_mode * 'a
507 | CJNE of ((subaddressing_mode, subaddressing_mode) Types.prod,
508 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum *
510 | DJNZ of subaddressing_mode * 'a
511 | ANL of (((subaddressing_mode, subaddressing_mode) Types.prod,
512 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
513 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
514 | ORL of (((subaddressing_mode, subaddressing_mode) Types.prod,
515 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
516 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
517 | XRL of ((subaddressing_mode, subaddressing_mode) Types.prod,
518 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
519 | CLR of subaddressing_mode
520 | CPL of subaddressing_mode
521 | RL of subaddressing_mode
522 | RLC of subaddressing_mode
523 | RR of subaddressing_mode
524 | RRC of subaddressing_mode
525 | SWAP of subaddressing_mode
526 | MOV of ((((((subaddressing_mode, subaddressing_mode) Types.prod,
527 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
528 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
529 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
530 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
531 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
532 | MOVX of ((subaddressing_mode, subaddressing_mode) Types.prod,
533 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
534 | SETB of subaddressing_mode
535 | PUSH of subaddressing_mode
536 | POP of subaddressing_mode
537 | XCH of subaddressing_mode * subaddressing_mode
538 | XCHD of subaddressing_mode * subaddressing_mode
542 | JMP of subaddressing_mode
544 val preinstruction_rect_Type4 :
545 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
546 subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
547 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
548 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
549 subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
550 -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
551 (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
552 ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
553 Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
554 -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
555 ((((subaddressing_mode, subaddressing_mode) Types.prod,
556 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
557 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
558 ((((subaddressing_mode, subaddressing_mode) Types.prod,
559 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
560 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
561 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
562 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
563 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
564 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
565 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
566 (((((((subaddressing_mode, subaddressing_mode) Types.prod,
567 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
568 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
569 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
570 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
571 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
572 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
573 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
574 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
575 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
576 subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
577 'a2) -> 'a1 preinstruction -> 'a2
579 val preinstruction_rect_Type5 :
580 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
581 subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
582 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
583 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
584 subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
585 -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
586 (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
587 ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
588 Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
589 -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
590 ((((subaddressing_mode, subaddressing_mode) Types.prod,
591 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
592 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
593 ((((subaddressing_mode, subaddressing_mode) Types.prod,
594 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
595 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
596 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
597 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
598 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
599 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
600 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
601 (((((((subaddressing_mode, subaddressing_mode) Types.prod,
602 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
603 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
604 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
605 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
606 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
607 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
608 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
609 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
610 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
611 subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
612 'a2) -> 'a1 preinstruction -> 'a2
614 val preinstruction_rect_Type3 :
615 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
616 subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
617 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
618 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
619 subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
620 -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
621 (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
622 ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
623 Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
624 -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
625 ((((subaddressing_mode, subaddressing_mode) Types.prod,
626 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
627 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
628 ((((subaddressing_mode, subaddressing_mode) Types.prod,
629 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
630 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
631 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
632 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
633 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
634 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
635 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
636 (((((((subaddressing_mode, subaddressing_mode) Types.prod,
637 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
638 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
639 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
640 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
641 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
642 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
643 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
644 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
645 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
646 subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
647 'a2) -> 'a1 preinstruction -> 'a2
649 val preinstruction_rect_Type2 :
650 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
651 subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
652 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
653 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
654 subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
655 -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
656 (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
657 ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
658 Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
659 -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
660 ((((subaddressing_mode, subaddressing_mode) Types.prod,
661 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
662 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
663 ((((subaddressing_mode, subaddressing_mode) Types.prod,
664 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
665 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
666 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
667 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
668 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
669 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
670 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
671 (((((((subaddressing_mode, subaddressing_mode) Types.prod,
672 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
673 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
674 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
675 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
676 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
677 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
678 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
679 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
680 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
681 subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
682 'a2) -> 'a1 preinstruction -> 'a2
684 val preinstruction_rect_Type1 :
685 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
686 subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
687 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
688 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
689 subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
690 -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
691 (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
692 ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
693 Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
694 -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
695 ((((subaddressing_mode, subaddressing_mode) Types.prod,
696 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
697 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
698 ((((subaddressing_mode, subaddressing_mode) Types.prod,
699 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
700 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
701 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
702 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
703 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
704 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
705 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
706 (((((((subaddressing_mode, subaddressing_mode) Types.prod,
707 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
708 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
709 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
710 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
711 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
712 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
713 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
714 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
715 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
716 subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
717 'a2) -> 'a1 preinstruction -> 'a2
719 val preinstruction_rect_Type0 :
720 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
721 subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode ->
722 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
723 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
724 subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> ('a1 -> 'a2)
725 -> ('a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
726 (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
727 ('a1 -> 'a2) -> ('a1 -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
728 Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
729 -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) ->
730 ((((subaddressing_mode, subaddressing_mode) Types.prod,
731 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
732 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
733 ((((subaddressing_mode, subaddressing_mode) Types.prod,
734 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
735 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
736 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
737 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
738 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
739 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
740 (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
741 (((((((subaddressing_mode, subaddressing_mode) Types.prod,
742 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
743 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
744 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
745 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
746 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) ->
747 (((subaddressing_mode, subaddressing_mode) Types.prod, (subaddressing_mode,
748 subaddressing_mode) Types.prod) Types.sum -> 'a2) -> (subaddressing_mode ->
749 'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
750 (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
751 subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
752 'a2) -> 'a1 preinstruction -> 'a2
754 val preinstruction_inv_rect_Type4 :
755 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
756 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
757 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
758 (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
759 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
760 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
761 (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
762 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
763 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
764 -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
765 Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
766 -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
767 ((((subaddressing_mode, subaddressing_mode) Types.prod,
768 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
769 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
770 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
771 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
772 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
773 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
774 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
775 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
776 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
777 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
778 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
779 subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
780 Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
781 Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
782 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
783 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
784 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
785 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
786 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
787 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
788 subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
789 subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
790 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
792 val preinstruction_inv_rect_Type3 :
793 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
794 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
795 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
796 (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
797 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
798 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
799 (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
800 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
801 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
802 -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
803 Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
804 -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
805 ((((subaddressing_mode, subaddressing_mode) Types.prod,
806 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
807 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
808 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
809 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
810 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
811 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
812 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
813 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
814 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
815 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
816 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
817 subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
818 Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
819 Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
820 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
821 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
822 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
823 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
824 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
825 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
826 subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
827 subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
828 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
830 val preinstruction_inv_rect_Type2 :
831 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
832 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
833 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
834 (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
835 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
836 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
837 (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
838 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
839 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
840 -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
841 Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
842 -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
843 ((((subaddressing_mode, subaddressing_mode) Types.prod,
844 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
845 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
846 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
847 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
848 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
849 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
850 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
851 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
852 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
853 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
854 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
855 subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
856 Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
857 Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
858 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
859 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
860 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
861 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
862 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
863 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
864 subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
865 subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
866 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
868 val preinstruction_inv_rect_Type1 :
869 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
870 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
871 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
872 (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
873 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
874 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
875 (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
876 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
877 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
878 -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
879 Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
880 -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
881 ((((subaddressing_mode, subaddressing_mode) Types.prod,
882 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
883 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
884 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
885 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
886 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
887 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
888 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
889 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
890 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
891 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
892 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
893 subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
894 Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
895 Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
896 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
897 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
898 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
899 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
900 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
901 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
902 subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
903 subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
904 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
906 val preinstruction_inv_rect_Type0 :
907 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ ->
908 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
909 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
910 (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) ->
911 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
912 (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) ->
913 (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ ->
914 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode ->
915 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 -> __
916 -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, subaddressing_mode)
917 Types.prod, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum
918 -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) ->
919 ((((subaddressing_mode, subaddressing_mode) Types.prod,
920 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
921 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
922 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod,
923 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
924 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
925 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
926 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
927 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
928 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
929 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
930 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode,
931 subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode)
932 Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod)
933 Types.sum, (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
934 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum,
935 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
936 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod,
937 (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ ->
938 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ ->
939 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
940 subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
941 subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
942 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
944 val preinstruction_discr : 'a1 preinstruction -> 'a1 preinstruction -> __
946 val preinstruction_jmdiscr : 'a1 preinstruction -> 'a1 preinstruction -> __
948 val eq_preinstruction :
949 subaddressing_mode preinstruction -> subaddressing_mode preinstruction ->
953 | ACALL of subaddressing_mode
954 | LCALL of subaddressing_mode
955 | AJMP of subaddressing_mode
956 | LJMP of subaddressing_mode
957 | SJMP of subaddressing_mode
958 | MOVC of subaddressing_mode * subaddressing_mode
959 | RealInstruction of subaddressing_mode preinstruction
961 val instruction_rect_Type4 :
962 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
963 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
964 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
965 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
967 val instruction_rect_Type5 :
968 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
969 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
970 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
971 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
973 val instruction_rect_Type3 :
974 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
975 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
976 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
977 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
979 val instruction_rect_Type2 :
980 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
981 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
982 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
983 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
985 val instruction_rect_Type1 :
986 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
987 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
988 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
989 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
991 val instruction_rect_Type0 :
992 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
993 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
994 (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
995 'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
997 val instruction_inv_rect_Type4 :
998 instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
999 __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1000 __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1001 subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1004 val instruction_inv_rect_Type3 :
1005 instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1006 __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1007 __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1008 subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1011 val instruction_inv_rect_Type2 :
1012 instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1013 __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1014 __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1015 subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1018 val instruction_inv_rect_Type1 :
1019 instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1020 __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1021 __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1022 subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1025 val instruction_inv_rect_Type0 :
1026 instruction -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1027 __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1028 __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
1029 subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
1032 val instruction_discr : instruction -> instruction -> __
1034 val instruction_jmdiscr : instruction -> instruction -> __
1036 val dpi1__o__RealInstruction__o__inject :
1037 (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction
1040 val eject__o__RealInstruction__o__inject :
1041 subaddressing_mode preinstruction Types.sig0 -> instruction Types.sig0
1043 val realInstruction__o__inject :
1044 subaddressing_mode preinstruction -> instruction Types.sig0
1046 val dpi1__o__RealInstruction :
1047 (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction
1049 val eject__o__RealInstruction :
1050 subaddressing_mode preinstruction Types.sig0 -> instruction
1052 val eq_instruction : instruction -> instruction -> Bool.bool
1058 val word_side_rect_Type4 : 'a1 -> 'a1 -> word_side -> 'a1
1060 val word_side_rect_Type5 : 'a1 -> 'a1 -> word_side -> 'a1
1062 val word_side_rect_Type3 : 'a1 -> 'a1 -> word_side -> 'a1
1064 val word_side_rect_Type2 : 'a1 -> 'a1 -> word_side -> 'a1
1066 val word_side_rect_Type1 : 'a1 -> 'a1 -> word_side -> 'a1
1068 val word_side_rect_Type0 : 'a1 -> 'a1 -> word_side -> 'a1
1070 val word_side_inv_rect_Type4 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1072 val word_side_inv_rect_Type3 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1074 val word_side_inv_rect_Type2 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1076 val word_side_inv_rect_Type1 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1078 val word_side_inv_rect_Type0 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
1080 val word_side_discr : word_side -> word_side -> __
1082 val word_side_jmdiscr : word_side -> word_side -> __
1084 type pseudo_instruction =
1085 | Instruction of identifier preinstruction
1086 | Comment of String.string
1087 | Cost of CostLabel.costlabel
1089 | Jnz of subaddressing_mode * identifier * identifier
1090 | Call of identifier
1091 | Mov of (subaddressing_mode, (subaddressing_mode, word_side) Types.prod)
1092 Types.sum * identifier * BitVector.word
1094 val pseudo_instruction_rect_Type4 :
1095 (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1096 (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1097 -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1098 ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1099 -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1101 val pseudo_instruction_rect_Type5 :
1102 (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1103 (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1104 -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1105 ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1106 -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1108 val pseudo_instruction_rect_Type3 :
1109 (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1110 (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1111 -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1112 ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1113 -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1115 val pseudo_instruction_rect_Type2 :
1116 (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1117 (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1118 -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1119 ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1120 -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1122 val pseudo_instruction_rect_Type1 :
1123 (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1124 (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1125 -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1126 ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1127 -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1129 val pseudo_instruction_rect_Type0 :
1130 (identifier preinstruction -> 'a1) -> (String.string -> 'a1) ->
1131 (CostLabel.costlabel -> 'a1) -> (identifier -> 'a1) -> (subaddressing_mode
1132 -> identifier -> identifier -> 'a1) -> (identifier -> 'a1) ->
1133 ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1134 -> identifier -> BitVector.word -> 'a1) -> pseudo_instruction -> 'a1
1136 val pseudo_instruction_inv_rect_Type4 :
1137 pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
1138 (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1139 (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1140 identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
1141 ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1142 -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1
1144 val pseudo_instruction_inv_rect_Type3 :
1145 pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
1146 (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1147 (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1148 identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
1149 ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1150 -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1
1152 val pseudo_instruction_inv_rect_Type2 :
1153 pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
1154 (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1155 (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1156 identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
1157 ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1158 -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1
1160 val pseudo_instruction_inv_rect_Type1 :
1161 pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
1162 (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1163 (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1164 identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
1165 ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1166 -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1
1168 val pseudo_instruction_inv_rect_Type0 :
1169 pseudo_instruction -> (identifier preinstruction -> __ -> 'a1) ->
1170 (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
1171 (identifier -> __ -> 'a1) -> (subaddressing_mode -> identifier ->
1172 identifier -> __ -> 'a1) -> (identifier -> __ -> 'a1) ->
1173 ((subaddressing_mode, (subaddressing_mode, word_side) Types.prod) Types.sum
1174 -> identifier -> BitVector.word -> __ -> 'a1) -> 'a1
1176 val pseudo_instruction_discr : pseudo_instruction -> pseudo_instruction -> __
1178 val pseudo_instruction_jmdiscr :
1179 pseudo_instruction -> pseudo_instruction -> __
1181 type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj
1183 type assembly_program = instruction List.list
1185 val fetch_pseudo_instruction :
1186 labelled_instruction List.list -> BitVector.word -> (pseudo_instruction,
1187 BitVector.word) Types.prod
1189 val is_jump' : identifier preinstruction -> Bool.bool
1191 val is_relative_jump : pseudo_instruction -> Bool.bool
1193 val is_jump : pseudo_instruction -> Bool.bool
1195 val is_call : pseudo_instruction -> Bool.bool
1197 val asm_cost_label :
1198 labelled_instruction List.list -> BitVector.word Types.sig0 ->
1199 CostLabel.costlabel Types.option
1201 val aDDRESS_WIDTH : Nat.nat
1203 val mAX_CODE_SIZE : Nat.nat
1205 val code_size_opt : labelled_instruction List.list -> __ Types.option
1207 type pseudo_assembly_program = { preamble : (identifier, BitVector.word)
1208 Types.prod List.list;
1209 code : labelled_instruction List.list;
1210 renamed_symbols : (identifier, AST.ident)
1211 Types.prod List.list;
1212 final_label : identifier }
1214 val pseudo_assembly_program_rect_Type4 :
1215 ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1216 List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1217 identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1219 val pseudo_assembly_program_rect_Type5 :
1220 ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1221 List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1222 identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1224 val pseudo_assembly_program_rect_Type3 :
1225 ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1226 List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1227 identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1229 val pseudo_assembly_program_rect_Type2 :
1230 ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1231 List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1232 identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1234 val pseudo_assembly_program_rect_Type1 :
1235 ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1236 List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1237 identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1239 val pseudo_assembly_program_rect_Type0 :
1240 ((identifier, BitVector.word) Types.prod List.list -> labelled_instruction
1241 List.list -> __ -> (identifier, AST.ident) Types.prod List.list ->
1242 identifier -> __ -> __ -> 'a1) -> pseudo_assembly_program -> 'a1
1245 pseudo_assembly_program -> (identifier, BitVector.word) Types.prod
1248 val code : pseudo_assembly_program -> labelled_instruction List.list
1250 val renamed_symbols :
1251 pseudo_assembly_program -> (identifier, AST.ident) Types.prod List.list
1253 val final_label : pseudo_assembly_program -> identifier
1255 val pseudo_assembly_program_inv_rect_Type4 :
1256 pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
1257 List.list -> labelled_instruction List.list -> __ -> (identifier,
1258 AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
1261 val pseudo_assembly_program_inv_rect_Type3 :
1262 pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
1263 List.list -> labelled_instruction List.list -> __ -> (identifier,
1264 AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
1267 val pseudo_assembly_program_inv_rect_Type2 :
1268 pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
1269 List.list -> labelled_instruction List.list -> __ -> (identifier,
1270 AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
1273 val pseudo_assembly_program_inv_rect_Type1 :
1274 pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
1275 List.list -> labelled_instruction List.list -> __ -> (identifier,
1276 AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
1279 val pseudo_assembly_program_inv_rect_Type0 :
1280 pseudo_assembly_program -> ((identifier, BitVector.word) Types.prod
1281 List.list -> labelled_instruction List.list -> __ -> (identifier,
1282 AST.ident) Types.prod List.list -> identifier -> __ -> __ -> __ -> 'a1) ->
1285 val pseudo_assembly_program_jmdiscr :
1286 pseudo_assembly_program -> pseudo_assembly_program -> __
1288 type object_code = BitVector.byte List.list
1291 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
1292 (BitVector.word, BitVector.byte) Types.prod
1294 val load_code_memory0 :
1295 object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0
1297 val load_code_memory :
1298 object_code -> BitVector.byte BitVectorTrie.bitVectorTrie
1300 type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
1302 type symboltable_type = AST.ident BitVectorTrie.bitVectorTrie
1304 type labelled_object_code = { oc : object_code;
1305 cm : BitVector.byte BitVectorTrie.bitVectorTrie;
1306 costlabels : costlabel_map;
1307 symboltable : symboltable_type;
1308 final_pc : BitVector.word }
1310 val labelled_object_code_rect_Type4 :
1311 (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1312 costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1313 labelled_object_code -> 'a1
1315 val labelled_object_code_rect_Type5 :
1316 (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1317 costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1318 labelled_object_code -> 'a1
1320 val labelled_object_code_rect_Type3 :
1321 (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1322 costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1323 labelled_object_code -> 'a1
1325 val labelled_object_code_rect_Type2 :
1326 (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1327 costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1328 labelled_object_code -> 'a1
1330 val labelled_object_code_rect_Type1 :
1331 (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1332 costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1333 labelled_object_code -> 'a1
1335 val labelled_object_code_rect_Type0 :
1336 (object_code -> BitVector.byte BitVectorTrie.bitVectorTrie -> __ ->
1337 costlabel_map -> symboltable_type -> BitVector.word -> __ -> 'a1) ->
1338 labelled_object_code -> 'a1
1340 val oc : labelled_object_code -> object_code
1342 val cm : labelled_object_code -> BitVector.byte BitVectorTrie.bitVectorTrie
1344 val costlabels : labelled_object_code -> costlabel_map
1346 val symboltable : labelled_object_code -> symboltable_type
1348 val final_pc : labelled_object_code -> BitVector.word
1350 val labelled_object_code_inv_rect_Type4 :
1351 labelled_object_code -> (object_code -> BitVector.byte
1352 BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1353 BitVector.word -> __ -> __ -> 'a1) -> 'a1
1355 val labelled_object_code_inv_rect_Type3 :
1356 labelled_object_code -> (object_code -> BitVector.byte
1357 BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1358 BitVector.word -> __ -> __ -> 'a1) -> 'a1
1360 val labelled_object_code_inv_rect_Type2 :
1361 labelled_object_code -> (object_code -> BitVector.byte
1362 BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1363 BitVector.word -> __ -> __ -> 'a1) -> 'a1
1365 val labelled_object_code_inv_rect_Type1 :
1366 labelled_object_code -> (object_code -> BitVector.byte
1367 BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1368 BitVector.word -> __ -> __ -> 'a1) -> 'a1
1370 val labelled_object_code_inv_rect_Type0 :
1371 labelled_object_code -> (object_code -> BitVector.byte
1372 BitVectorTrie.bitVectorTrie -> __ -> costlabel_map -> symboltable_type ->
1373 BitVector.word -> __ -> __ -> 'a1) -> 'a1
1375 val labelled_object_code_jmdiscr :
1376 labelled_object_code -> labelled_object_code -> __