65 open Hints_declaration
107 | Imm of BitVector.byte
109 val argument_rect_Type4 :
110 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
112 val argument_rect_Type5 :
113 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
115 val argument_rect_Type3 :
116 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
118 val argument_rect_Type2 :
119 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
121 val argument_rect_Type1 :
122 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
124 val argument_rect_Type0 :
125 ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
127 val argument_inv_rect_Type4 :
128 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
130 val argument_inv_rect_Type3 :
131 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
133 val argument_inv_rect_Type2 :
134 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
136 val argument_inv_rect_Type1 :
137 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
139 val argument_inv_rect_Type0 :
140 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
142 val argument_discr : 'a1 argument -> 'a1 argument -> __
144 val argument_jmdiscr : 'a1 argument -> 'a1 argument -> __
146 type psd_argument = Registers.register argument
148 val psd_argument_from_reg : Registers.register -> psd_argument
150 val dpi1__o__reg_to_psd_argument__o__inject :
151 (Registers.register, 'a1) Types.dPair -> psd_argument Types.sig0
153 val eject__o__reg_to_psd_argument__o__inject :
154 Registers.register Types.sig0 -> psd_argument Types.sig0
156 val reg_to_psd_argument__o__inject :
157 Registers.register -> psd_argument Types.sig0
159 val dpi1__o__reg_to_psd_argument :
160 (Registers.register, 'a1) Types.dPair -> psd_argument
162 val eject__o__reg_to_psd_argument :
163 Registers.register Types.sig0 -> psd_argument
165 val psd_argument_from_byte : BitVector.byte -> psd_argument
167 val dpi1__o__byte_to_psd_argument__o__inject :
168 (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0
170 val eject__o__byte_to_psd_argument__o__inject :
171 BitVector.byte Types.sig0 -> psd_argument Types.sig0
173 val byte_to_psd_argument__o__inject :
174 BitVector.byte -> psd_argument Types.sig0
176 val dpi1__o__byte_to_psd_argument :
177 (BitVector.byte, 'a1) Types.dPair -> psd_argument
179 val eject__o__byte_to_psd_argument :
180 BitVector.byte Types.sig0 -> psd_argument
182 type hdw_argument = I8051.register argument
184 val hdw_argument_from_reg : I8051.register -> hdw_argument
186 val dpi1__o__reg_to_hdw_argument__o__inject :
187 (I8051.register, 'a1) Types.dPair -> hdw_argument Types.sig0
189 val eject__o__reg_to_hdw_argument__o__inject :
190 I8051.register Types.sig0 -> hdw_argument Types.sig0
192 val reg_to_hdw_argument__o__inject :
193 I8051.register -> hdw_argument Types.sig0
195 val dpi1__o__reg_to_hdw_argument :
196 (I8051.register, 'a1) Types.dPair -> hdw_argument
198 val eject__o__reg_to_hdw_argument : I8051.register Types.sig0 -> hdw_argument
200 val hdw_argument_from_byte : BitVector.byte -> hdw_argument
202 val dpi1__o__byte_to_hdw_argument__o__inject :
203 (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0
205 val eject__o__byte_to_hdw_argument__o__inject :
206 BitVector.byte Types.sig0 -> psd_argument Types.sig0
208 val byte_to_hdw_argument__o__inject :
209 BitVector.byte -> psd_argument Types.sig0
211 val dpi1__o__byte_to_hdw_argument :
212 (BitVector.byte, 'a1) Types.dPair -> psd_argument
214 val eject__o__byte_to_hdw_argument :
215 BitVector.byte Types.sig0 -> psd_argument
217 val byte_of_nat : Nat.nat -> BitVector.byte
219 val zero_byte : BitVector.byte
221 type unserialized_params = { ext_seq_labels : (__ -> Graphs.label List.list);
222 has_tailcalls : Bool.bool }
224 val unserialized_params_rect_Type4 :
225 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
226 -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
227 unserialized_params -> 'a1
229 val unserialized_params_rect_Type5 :
230 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
231 -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
232 unserialized_params -> 'a1
234 val unserialized_params_rect_Type3 :
235 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
236 -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
237 unserialized_params -> 'a1
239 val unserialized_params_rect_Type2 :
240 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
241 -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
242 unserialized_params -> 'a1
244 val unserialized_params_rect_Type1 :
245 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
246 -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
247 unserialized_params -> 'a1
249 val unserialized_params_rect_Type0 :
250 (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
251 -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
252 unserialized_params -> 'a1
280 val ext_seq_labels : unserialized_params -> __ -> Graphs.label List.list
282 val has_tailcalls : unserialized_params -> Bool.bool
286 val unserialized_params_inv_rect_Type4 :
287 unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
288 -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
289 __ -> __ -> 'a1) -> 'a1
291 val unserialized_params_inv_rect_Type3 :
292 unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
293 -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
294 __ -> __ -> 'a1) -> 'a1
296 val unserialized_params_inv_rect_Type2 :
297 unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
298 -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
299 __ -> __ -> 'a1) -> 'a1
301 val unserialized_params_inv_rect_Type1 :
302 unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
303 -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
304 __ -> __ -> 'a1) -> 'a1
306 val unserialized_params_inv_rect_Type0 :
307 unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
308 -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
309 __ -> __ -> 'a1) -> 'a1
311 val unserialized_params_jmdiscr :
312 unserialized_params -> unserialized_params -> __
314 type get_pseudo_reg_functs = { acc_a_regs : (__ -> Registers.register
316 acc_b_regs : (__ -> Registers.register
318 acc_a_args : (__ -> Registers.register
320 acc_b_args : (__ -> Registers.register
322 dpl_regs : (__ -> Registers.register
324 dph_regs : (__ -> Registers.register
326 dpl_args : (__ -> Registers.register
328 dph_args : (__ -> Registers.register
330 snd_args : (__ -> Registers.register
332 pair_move_regs : (__ -> Registers.register
334 f_call_args : (__ -> Registers.register
336 f_call_dest : (__ -> Registers.register
338 ext_seq_regs : (__ -> Registers.register
340 params_regs : (__ -> Registers.register
343 val get_pseudo_reg_functs_rect_Type4 :
344 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
345 Registers.register List.list) -> (__ -> Registers.register List.list) ->
346 (__ -> Registers.register List.list) -> (__ -> Registers.register
347 List.list) -> (__ -> Registers.register List.list) -> (__ ->
348 Registers.register List.list) -> (__ -> Registers.register List.list) ->
349 (__ -> Registers.register List.list) -> (__ -> Registers.register
350 List.list) -> (__ -> Registers.register List.list) -> (__ ->
351 Registers.register List.list) -> (__ -> Registers.register List.list) ->
352 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
355 val get_pseudo_reg_functs_rect_Type5 :
356 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
357 Registers.register List.list) -> (__ -> Registers.register List.list) ->
358 (__ -> Registers.register List.list) -> (__ -> Registers.register
359 List.list) -> (__ -> Registers.register List.list) -> (__ ->
360 Registers.register List.list) -> (__ -> Registers.register List.list) ->
361 (__ -> Registers.register List.list) -> (__ -> Registers.register
362 List.list) -> (__ -> Registers.register List.list) -> (__ ->
363 Registers.register List.list) -> (__ -> Registers.register List.list) ->
364 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
367 val get_pseudo_reg_functs_rect_Type3 :
368 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
369 Registers.register List.list) -> (__ -> Registers.register List.list) ->
370 (__ -> Registers.register List.list) -> (__ -> Registers.register
371 List.list) -> (__ -> Registers.register List.list) -> (__ ->
372 Registers.register List.list) -> (__ -> Registers.register List.list) ->
373 (__ -> Registers.register List.list) -> (__ -> Registers.register
374 List.list) -> (__ -> Registers.register List.list) -> (__ ->
375 Registers.register List.list) -> (__ -> Registers.register List.list) ->
376 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
379 val get_pseudo_reg_functs_rect_Type2 :
380 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
381 Registers.register List.list) -> (__ -> Registers.register List.list) ->
382 (__ -> Registers.register List.list) -> (__ -> Registers.register
383 List.list) -> (__ -> Registers.register List.list) -> (__ ->
384 Registers.register List.list) -> (__ -> Registers.register List.list) ->
385 (__ -> Registers.register List.list) -> (__ -> Registers.register
386 List.list) -> (__ -> Registers.register List.list) -> (__ ->
387 Registers.register List.list) -> (__ -> Registers.register List.list) ->
388 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
391 val get_pseudo_reg_functs_rect_Type1 :
392 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
393 Registers.register List.list) -> (__ -> Registers.register List.list) ->
394 (__ -> Registers.register List.list) -> (__ -> Registers.register
395 List.list) -> (__ -> Registers.register List.list) -> (__ ->
396 Registers.register List.list) -> (__ -> Registers.register List.list) ->
397 (__ -> Registers.register List.list) -> (__ -> Registers.register
398 List.list) -> (__ -> Registers.register List.list) -> (__ ->
399 Registers.register List.list) -> (__ -> Registers.register List.list) ->
400 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
403 val get_pseudo_reg_functs_rect_Type0 :
404 unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
405 Registers.register List.list) -> (__ -> Registers.register List.list) ->
406 (__ -> Registers.register List.list) -> (__ -> Registers.register
407 List.list) -> (__ -> Registers.register List.list) -> (__ ->
408 Registers.register List.list) -> (__ -> Registers.register List.list) ->
409 (__ -> Registers.register List.list) -> (__ -> Registers.register
410 List.list) -> (__ -> Registers.register List.list) -> (__ ->
411 Registers.register List.list) -> (__ -> Registers.register List.list) ->
412 (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
416 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
420 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
424 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
428 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
432 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
436 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
440 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
444 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
448 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
452 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
456 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
460 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
464 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
468 unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
471 val get_pseudo_reg_functs_inv_rect_Type4 :
472 unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
473 List.list) -> (__ -> Registers.register List.list) -> (__ ->
474 Registers.register List.list) -> (__ -> Registers.register List.list) ->
475 (__ -> Registers.register List.list) -> (__ -> Registers.register
476 List.list) -> (__ -> Registers.register List.list) -> (__ ->
477 Registers.register List.list) -> (__ -> Registers.register List.list) ->
478 (__ -> Registers.register List.list) -> (__ -> Registers.register
479 List.list) -> (__ -> Registers.register List.list) -> (__ ->
480 Registers.register List.list) -> (__ -> Registers.register List.list) -> __
483 val get_pseudo_reg_functs_inv_rect_Type3 :
484 unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
485 List.list) -> (__ -> Registers.register List.list) -> (__ ->
486 Registers.register List.list) -> (__ -> Registers.register List.list) ->
487 (__ -> Registers.register List.list) -> (__ -> Registers.register
488 List.list) -> (__ -> Registers.register List.list) -> (__ ->
489 Registers.register List.list) -> (__ -> Registers.register List.list) ->
490 (__ -> Registers.register List.list) -> (__ -> Registers.register
491 List.list) -> (__ -> Registers.register List.list) -> (__ ->
492 Registers.register List.list) -> (__ -> Registers.register List.list) -> __
495 val get_pseudo_reg_functs_inv_rect_Type2 :
496 unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
497 List.list) -> (__ -> Registers.register List.list) -> (__ ->
498 Registers.register List.list) -> (__ -> Registers.register List.list) ->
499 (__ -> Registers.register List.list) -> (__ -> Registers.register
500 List.list) -> (__ -> Registers.register List.list) -> (__ ->
501 Registers.register List.list) -> (__ -> Registers.register List.list) ->
502 (__ -> Registers.register List.list) -> (__ -> Registers.register
503 List.list) -> (__ -> Registers.register List.list) -> (__ ->
504 Registers.register List.list) -> (__ -> Registers.register List.list) -> __
507 val get_pseudo_reg_functs_inv_rect_Type1 :
508 unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
509 List.list) -> (__ -> Registers.register List.list) -> (__ ->
510 Registers.register List.list) -> (__ -> Registers.register List.list) ->
511 (__ -> Registers.register List.list) -> (__ -> Registers.register
512 List.list) -> (__ -> Registers.register List.list) -> (__ ->
513 Registers.register List.list) -> (__ -> Registers.register List.list) ->
514 (__ -> Registers.register List.list) -> (__ -> Registers.register
515 List.list) -> (__ -> Registers.register List.list) -> (__ ->
516 Registers.register List.list) -> (__ -> Registers.register List.list) -> __
519 val get_pseudo_reg_functs_inv_rect_Type0 :
520 unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
521 List.list) -> (__ -> Registers.register List.list) -> (__ ->
522 Registers.register List.list) -> (__ -> Registers.register List.list) ->
523 (__ -> Registers.register List.list) -> (__ -> Registers.register
524 List.list) -> (__ -> Registers.register List.list) -> (__ ->
525 Registers.register List.list) -> (__ -> Registers.register List.list) ->
526 (__ -> Registers.register List.list) -> (__ -> Registers.register
527 List.list) -> (__ -> Registers.register List.list) -> (__ ->
528 Registers.register List.list) -> (__ -> Registers.register List.list) -> __
531 val get_pseudo_reg_functs_jmdiscr :
532 unserialized_params -> get_pseudo_reg_functs -> get_pseudo_reg_functs -> __
534 type uns_params = { u_pars : unserialized_params;
535 functs : get_pseudo_reg_functs }
537 val uns_params_rect_Type4 :
538 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
540 val uns_params_rect_Type5 :
541 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
543 val uns_params_rect_Type3 :
544 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
546 val uns_params_rect_Type2 :
547 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
549 val uns_params_rect_Type1 :
550 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
552 val uns_params_rect_Type0 :
553 (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1
555 val u_pars : uns_params -> unserialized_params
557 val functs : uns_params -> get_pseudo_reg_functs
559 val uns_params_inv_rect_Type4 :
560 uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
563 val uns_params_inv_rect_Type3 :
564 uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
567 val uns_params_inv_rect_Type2 :
568 uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
571 val uns_params_inv_rect_Type1 :
572 uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
575 val uns_params_inv_rect_Type0 :
576 uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
579 val uns_params_jmdiscr : uns_params -> uns_params -> __
582 | COMMENT of String.string
586 | ADDRESS of AST.ident * BitVector.word * __ * __
587 | OPACCS of BackEndOps.opAccs * __ * __ * __ * __
588 | OP1 of BackEndOps.op1 * __ * __
589 | OP2 of BackEndOps.op2 * __ * __ * __
592 | LOAD of __ * __ * __
593 | STORE of __ * __ * __
594 | Extension_seq of __
596 val joint_seq_rect_Type4 :
597 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
598 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
599 -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
600 -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
601 -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
602 -> (__ -> 'a1) -> joint_seq -> 'a1
604 val joint_seq_rect_Type5 :
605 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
606 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
607 -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
608 -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
609 -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
610 -> (__ -> 'a1) -> joint_seq -> 'a1
612 val joint_seq_rect_Type3 :
613 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
614 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
615 -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
616 -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
617 -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
618 -> (__ -> 'a1) -> joint_seq -> 'a1
620 val joint_seq_rect_Type2 :
621 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
622 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
623 -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
624 -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
625 -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
626 -> (__ -> 'a1) -> joint_seq -> 'a1
628 val joint_seq_rect_Type1 :
629 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
630 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
631 -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
632 -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
633 -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
634 -> (__ -> 'a1) -> joint_seq -> 'a1
636 val joint_seq_rect_Type0 :
637 unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
638 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
639 -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
640 -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
641 -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
642 -> (__ -> 'a1) -> joint_seq -> 'a1
644 val joint_seq_inv_rect_Type4 :
645 unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
646 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
647 'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
648 (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
649 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
650 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
651 -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
653 val joint_seq_inv_rect_Type3 :
654 unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
655 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
656 'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
657 (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
658 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
659 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
660 -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
662 val joint_seq_inv_rect_Type2 :
663 unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
664 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
665 'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
666 (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
667 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
668 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
669 -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
671 val joint_seq_inv_rect_Type1 :
672 unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
673 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
674 'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
675 (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
676 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
677 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
678 -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
680 val joint_seq_inv_rect_Type0 :
681 unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
682 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
683 'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
684 (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
685 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
686 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
687 -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1
689 val joint_seq_discr :
690 unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __
692 val joint_seq_jmdiscr :
693 unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __
695 val get_used_registers_from_seq :
696 unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
697 joint_seq -> Registers.register List.list
699 val nOOP : unserialized_params -> AST.ident List.list -> joint_seq
701 val dpi1__o__extension_seq_to_seq__o__inject :
702 unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
705 val eject__o__extension_seq_to_seq__o__inject :
706 unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
709 val extension_seq_to_seq__o__inject :
710 unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0
712 val dpi1__o__extension_seq_to_seq :
713 unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
716 val eject__o__extension_seq_to_seq :
717 unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
720 | COST_LABEL of CostLabel.costlabel
721 | CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
722 | COND of __ * Graphs.label
723 | Step_seq of joint_seq
725 val joint_step_rect_Type4 :
726 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
727 -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
728 -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
730 val joint_step_rect_Type5 :
731 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
732 -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
733 -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
735 val joint_step_rect_Type3 :
736 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
737 -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
738 -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
740 val joint_step_rect_Type2 :
741 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
742 -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
743 -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
745 val joint_step_rect_Type1 :
746 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
747 -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
748 -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
750 val joint_step_rect_Type0 :
751 unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
752 -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
753 -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
755 val joint_step_inv_rect_Type4 :
756 unserialized_params -> AST.ident List.list -> joint_step ->
757 (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
758 Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
759 (joint_seq -> __ -> 'a1) -> 'a1
761 val joint_step_inv_rect_Type3 :
762 unserialized_params -> AST.ident List.list -> joint_step ->
763 (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
764 Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
765 (joint_seq -> __ -> 'a1) -> 'a1
767 val joint_step_inv_rect_Type2 :
768 unserialized_params -> AST.ident List.list -> joint_step ->
769 (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
770 Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
771 (joint_seq -> __ -> 'a1) -> 'a1
773 val joint_step_inv_rect_Type1 :
774 unserialized_params -> AST.ident List.list -> joint_step ->
775 (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
776 Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
777 (joint_seq -> __ -> 'a1) -> 'a1
779 val joint_step_inv_rect_Type0 :
780 unserialized_params -> AST.ident List.list -> joint_step ->
781 (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
782 Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
783 (joint_seq -> __ -> 'a1) -> 'a1
785 val joint_step_discr :
786 unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
789 val joint_step_jmdiscr :
790 unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
793 val get_used_registers_from_step :
794 unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
795 joint_step -> Registers.register List.list
797 val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
798 unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
799 joint_step Types.sig0
801 val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
802 unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
805 val extension_seq_to_seq__o__seq_to_step__o__inject :
806 unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0
808 val dpi1__o__seq_to_step__o__inject :
809 unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
810 -> joint_step Types.sig0
812 val eject__o__seq_to_step__o__inject :
813 unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
814 joint_step Types.sig0
816 val seq_to_step__o__inject :
817 unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
820 val dpi1__o__extension_seq_to_seq__o__seq_to_step :
821 unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
824 val eject__o__extension_seq_to_seq__o__seq_to_step :
825 unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
827 val extension_seq_to_seq__o__seq_to_step :
828 unserialized_params -> AST.ident List.list -> __ -> joint_step
830 val dpi1__o__seq_to_step :
831 unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
834 val eject__o__seq_to_step :
835 unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
839 unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
842 type stmt_params = { uns_pars : uns_params;
843 succ_label : (__ -> Graphs.label Types.option);
844 has_fcond : Bool.bool }
846 val stmt_params_rect_Type4 :
847 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
848 -> stmt_params -> 'a1
850 val stmt_params_rect_Type5 :
851 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
852 -> stmt_params -> 'a1
854 val stmt_params_rect_Type3 :
855 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
856 -> stmt_params -> 'a1
858 val stmt_params_rect_Type2 :
859 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
860 -> stmt_params -> 'a1
862 val stmt_params_rect_Type1 :
863 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
864 -> stmt_params -> 'a1
866 val stmt_params_rect_Type0 :
867 (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
868 -> stmt_params -> 'a1
870 val uns_pars : stmt_params -> uns_params
874 val succ_label : stmt_params -> __ -> Graphs.label Types.option
876 val has_fcond : stmt_params -> Bool.bool
878 val stmt_params_inv_rect_Type4 :
879 stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
880 Bool.bool -> __ -> 'a1) -> 'a1
882 val stmt_params_inv_rect_Type3 :
883 stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
884 Bool.bool -> __ -> 'a1) -> 'a1
886 val stmt_params_inv_rect_Type2 :
887 stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
888 Bool.bool -> __ -> 'a1) -> 'a1
890 val stmt_params_inv_rect_Type1 :
891 stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
892 Bool.bool -> __ -> 'a1) -> 'a1
894 val stmt_params_inv_rect_Type0 :
895 stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
896 Bool.bool -> __ -> 'a1) -> 'a1
898 val stmt_params_jmdiscr : stmt_params -> stmt_params -> __
900 val uns_pars__o__u_pars : stmt_params -> unserialized_params
902 type joint_fin_step =
903 | GOTO of Graphs.label
905 | TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
907 val joint_fin_step_rect_Type4 :
908 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
909 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
911 val joint_fin_step_rect_Type5 :
912 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
913 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
915 val joint_fin_step_rect_Type3 :
916 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
917 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
919 val joint_fin_step_rect_Type2 :
920 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
921 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
923 val joint_fin_step_rect_Type1 :
924 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
925 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
927 val joint_fin_step_rect_Type0 :
928 unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
929 (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
931 val joint_fin_step_inv_rect_Type4 :
932 unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
933 -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
936 val joint_fin_step_inv_rect_Type3 :
937 unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
938 -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
941 val joint_fin_step_inv_rect_Type2 :
942 unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
943 -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
946 val joint_fin_step_inv_rect_Type1 :
947 unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
948 -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
951 val joint_fin_step_inv_rect_Type0 :
952 unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
953 -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
956 val joint_fin_step_discr :
957 unserialized_params -> joint_fin_step -> joint_fin_step -> __
959 val joint_fin_step_jmdiscr :
960 unserialized_params -> joint_fin_step -> joint_fin_step -> __
962 val fin_step_labels :
963 unserialized_params -> joint_fin_step -> Graphs.label List.list
965 type joint_statement =
966 | Sequential of joint_step * __
967 | Final of joint_fin_step
968 | FCOND of __ * Graphs.label * Graphs.label
970 val joint_statement_rect_Type4 :
971 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
972 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
973 'a1) -> joint_statement -> 'a1
975 val joint_statement_rect_Type5 :
976 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
977 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
978 'a1) -> joint_statement -> 'a1
980 val joint_statement_rect_Type3 :
981 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
982 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
983 'a1) -> joint_statement -> 'a1
985 val joint_statement_rect_Type2 :
986 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
987 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
988 'a1) -> joint_statement -> 'a1
990 val joint_statement_rect_Type1 :
991 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
992 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
993 'a1) -> joint_statement -> 'a1
995 val joint_statement_rect_Type0 :
996 stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
997 (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
998 'a1) -> joint_statement -> 'a1
1000 val joint_statement_inv_rect_Type4 :
1001 stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1002 -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1003 -> Graphs.label -> __ -> 'a1) -> 'a1
1005 val joint_statement_inv_rect_Type3 :
1006 stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1007 -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1008 -> Graphs.label -> __ -> 'a1) -> 'a1
1010 val joint_statement_inv_rect_Type2 :
1011 stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1012 -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1013 -> Graphs.label -> __ -> 'a1) -> 'a1
1015 val joint_statement_inv_rect_Type1 :
1016 stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1017 -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1018 -> Graphs.label -> __ -> 'a1) -> 'a1
1020 val joint_statement_inv_rect_Type0 :
1021 stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
1022 -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
1023 -> Graphs.label -> __ -> 'a1) -> 'a1
1025 val joint_statement_discr :
1026 stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
1029 val joint_statement_jmdiscr :
1030 stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
1033 val dpi1__o__fin_step_to_stmt__o__inject :
1034 stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
1035 joint_statement Types.sig0
1037 val eject__o__fin_step_to_stmt__o__inject :
1038 stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1039 joint_statement Types.sig0
1041 val fin_step_to_stmt__o__inject :
1042 stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1045 val dpi1__o__fin_step_to_stmt :
1046 stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
1049 val eject__o__fin_step_to_stmt :
1050 stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1053 type params = { stmt_pars : stmt_params;
1054 stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1056 point_of_label : (AST.ident List.list -> __ -> Graphs.label
1057 -> __ Types.option);
1058 point_of_succ : (__ -> __ -> __) }
1060 val params_rect_Type4 :
1061 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1062 joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1063 -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1065 val params_rect_Type5 :
1066 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1067 joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1068 -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1070 val params_rect_Type3 :
1071 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1072 joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1073 -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1075 val params_rect_Type2 :
1076 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1077 joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1078 -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1080 val params_rect_Type1 :
1081 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1082 joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1083 -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1085 val params_rect_Type0 :
1086 (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1087 joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1088 -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
1090 val stmt_pars : params -> stmt_params
1097 params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option
1099 val point_of_label :
1100 params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option
1102 val point_of_succ : params -> __ -> __ -> __
1104 val params_inv_rect_Type4 :
1105 params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1106 joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1107 -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1109 val params_inv_rect_Type3 :
1110 params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1111 joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1112 -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1114 val params_inv_rect_Type2 :
1115 params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1116 joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1117 -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1119 val params_inv_rect_Type1 :
1120 params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1121 joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1122 -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1124 val params_inv_rect_Type0 :
1125 params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1126 joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
1127 -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
1129 val params_jmdiscr : params -> params -> __
1131 val stmt_pars__o__uns_pars : params -> uns_params
1133 val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params
1135 val code_has_point : params -> AST.ident List.list -> __ -> __ -> Bool.bool
1137 val code_has_label :
1138 params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool
1140 val stmt_explicit_labels :
1141 stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1144 val stmt_implicit_label :
1145 stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1149 stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1152 val stmt_registers :
1153 stmt_params -> AST.ident List.list -> joint_statement -> Registers.register
1158 (* singleton inductive, whose constructor was mk_lin_params *)
1160 val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1
1162 val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1
1164 val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1
1166 val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1
1168 val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1
1170 val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1
1172 val l_u_pars : lin_params -> uns_params
1174 val lin_params_inv_rect_Type4 :
1175 lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1177 val lin_params_inv_rect_Type3 :
1178 lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1180 val lin_params_inv_rect_Type2 :
1181 lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1183 val lin_params_inv_rect_Type1 :
1184 lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1186 val lin_params_inv_rect_Type0 :
1187 lin_params -> (uns_params -> __ -> 'a1) -> 'a1
1189 val lin_params_jmdiscr : lin_params -> lin_params -> __
1191 val lin_params_to_params : lin_params -> params
1193 val lp_to_p__o__stmt_pars : lin_params -> stmt_params
1195 val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params
1197 val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
1198 lin_params -> unserialized_params
1202 (* singleton inductive, whose constructor was mk_graph_params *)
1204 val graph_params_rect_Type4 : (uns_params -> 'a1) -> graph_params -> 'a1
1206 val graph_params_rect_Type5 : (uns_params -> 'a1) -> graph_params -> 'a1
1208 val graph_params_rect_Type3 : (uns_params -> 'a1) -> graph_params -> 'a1
1210 val graph_params_rect_Type2 : (uns_params -> 'a1) -> graph_params -> 'a1
1212 val graph_params_rect_Type1 : (uns_params -> 'a1) -> graph_params -> 'a1
1214 val graph_params_rect_Type0 : (uns_params -> 'a1) -> graph_params -> 'a1
1216 val g_u_pars : graph_params -> uns_params
1218 val graph_params_inv_rect_Type4 :
1219 graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1221 val graph_params_inv_rect_Type3 :
1222 graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1224 val graph_params_inv_rect_Type2 :
1225 graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1227 val graph_params_inv_rect_Type1 :
1228 graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1230 val graph_params_inv_rect_Type0 :
1231 graph_params -> (uns_params -> __ -> 'a1) -> 'a1
1233 val graph_params_jmdiscr : graph_params -> graph_params -> __
1235 val graph_params_to_params : graph_params -> params
1237 val gp_to_p__o__stmt_pars : graph_params -> stmt_params
1239 val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params
1241 val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
1242 graph_params -> unserialized_params
1244 type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
1245 joint_if_runiverse : Identifiers.universe;
1246 joint_if_result : __; joint_if_params :
1247 __; joint_if_stacksize : Nat.nat;
1248 joint_if_local_stacksize : Nat.nat;
1249 joint_if_code : __; joint_if_entry :
1252 val joint_internal_function_rect_Type4 :
1253 params -> AST.ident List.list -> (Identifiers.universe ->
1254 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1255 -> joint_internal_function -> 'a1
1257 val joint_internal_function_rect_Type5 :
1258 params -> AST.ident List.list -> (Identifiers.universe ->
1259 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1260 -> joint_internal_function -> 'a1
1262 val joint_internal_function_rect_Type3 :
1263 params -> AST.ident List.list -> (Identifiers.universe ->
1264 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1265 -> joint_internal_function -> 'a1
1267 val joint_internal_function_rect_Type2 :
1268 params -> AST.ident List.list -> (Identifiers.universe ->
1269 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1270 -> joint_internal_function -> 'a1
1272 val joint_internal_function_rect_Type1 :
1273 params -> AST.ident List.list -> (Identifiers.universe ->
1274 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1275 -> joint_internal_function -> 'a1
1277 val joint_internal_function_rect_Type0 :
1278 params -> AST.ident List.list -> (Identifiers.universe ->
1279 Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
1280 -> joint_internal_function -> 'a1
1282 val joint_if_luniverse :
1283 params -> AST.ident List.list -> joint_internal_function ->
1284 Identifiers.universe
1286 val joint_if_runiverse :
1287 params -> AST.ident List.list -> joint_internal_function ->
1288 Identifiers.universe
1290 val joint_if_result :
1291 params -> AST.ident List.list -> joint_internal_function -> __
1293 val joint_if_params :
1294 params -> AST.ident List.list -> joint_internal_function -> __
1296 val joint_if_stacksize :
1297 params -> AST.ident List.list -> joint_internal_function -> Nat.nat
1299 val joint_if_local_stacksize :
1300 params -> AST.ident List.list -> joint_internal_function -> Nat.nat
1303 params -> AST.ident List.list -> joint_internal_function -> __
1305 val joint_if_entry :
1306 params -> AST.ident List.list -> joint_internal_function -> __
1308 val joint_internal_function_inv_rect_Type4 :
1309 params -> AST.ident List.list -> joint_internal_function ->
1310 (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1311 Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1313 val joint_internal_function_inv_rect_Type3 :
1314 params -> AST.ident List.list -> joint_internal_function ->
1315 (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1316 Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1318 val joint_internal_function_inv_rect_Type2 :
1319 params -> AST.ident List.list -> joint_internal_function ->
1320 (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1321 Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1323 val joint_internal_function_inv_rect_Type1 :
1324 params -> AST.ident List.list -> joint_internal_function ->
1325 (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1326 Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1328 val joint_internal_function_inv_rect_Type0 :
1329 params -> AST.ident List.list -> joint_internal_function ->
1330 (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
1331 Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
1333 val joint_internal_function_jmdiscr :
1334 params -> AST.ident List.list -> joint_internal_function ->
1335 joint_internal_function -> __
1337 val good_if_rect_Type4 :
1338 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1339 -> __ -> __ -> 'a1) -> 'a1
1341 val good_if_rect_Type5 :
1342 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1343 -> __ -> __ -> 'a1) -> 'a1
1345 val good_if_rect_Type3 :
1346 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1347 -> __ -> __ -> 'a1) -> 'a1
1349 val good_if_rect_Type2 :
1350 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1351 -> __ -> __ -> 'a1) -> 'a1
1353 val good_if_rect_Type1 :
1354 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1355 -> __ -> __ -> 'a1) -> 'a1
1357 val good_if_rect_Type0 :
1358 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1359 -> __ -> __ -> 'a1) -> 'a1
1361 val good_if_inv_rect_Type4 :
1362 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1363 -> __ -> __ -> __ -> 'a1) -> 'a1
1365 val good_if_inv_rect_Type3 :
1366 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1367 -> __ -> __ -> __ -> 'a1) -> 'a1
1369 val good_if_inv_rect_Type2 :
1370 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1371 -> __ -> __ -> __ -> 'a1) -> 'a1
1373 val good_if_inv_rect_Type1 :
1374 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1375 -> __ -> __ -> __ -> 'a1) -> 'a1
1377 val good_if_inv_rect_Type0 :
1378 params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1379 -> __ -> __ -> __ -> 'a1) -> 'a1
1382 params -> AST.ident List.list -> joint_internal_function -> __
1384 val good_if_jmdiscr :
1385 params -> AST.ident List.list -> joint_internal_function -> __
1387 type joint_closed_internal_function = joint_internal_function Types.sig0
1389 val set_joint_code :
1390 AST.ident List.list -> params -> joint_internal_function -> __ -> __ ->
1391 joint_internal_function
1394 params -> AST.ident List.list -> joint_internal_function ->
1395 Identifiers.universe -> joint_internal_function
1398 params -> AST.ident List.list -> joint_internal_function ->
1399 Identifiers.universe -> joint_internal_function
1402 graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
1403 joint_internal_function -> joint_internal_function
1405 type joint_function = joint_closed_internal_function AST.fundef
1407 type joint_program = { jp_functions : AST.ident List.list;
1408 joint_prog : (joint_function, AST.init_data List.list)
1410 init_cost_label : CostLabel.costlabel }
1412 val joint_program_rect_Type4 :
1413 params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1414 AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1416 val joint_program_rect_Type5 :
1417 params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1418 AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1420 val joint_program_rect_Type3 :
1421 params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1422 AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1424 val joint_program_rect_Type2 :
1425 params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1426 AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1428 val joint_program_rect_Type1 :
1429 params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1430 AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1432 val joint_program_rect_Type0 :
1433 params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
1434 AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1
1436 val jp_functions : params -> joint_program -> AST.ident List.list
1439 params -> joint_program -> (joint_function, AST.init_data List.list)
1442 val init_cost_label : params -> joint_program -> CostLabel.costlabel
1444 val joint_program_inv_rect_Type4 :
1445 params -> joint_program -> (AST.ident List.list -> (joint_function,
1446 AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
1449 val joint_program_inv_rect_Type3 :
1450 params -> joint_program -> (AST.ident List.list -> (joint_function,
1451 AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
1454 val joint_program_inv_rect_Type2 :
1455 params -> joint_program -> (AST.ident List.list -> (joint_function,
1456 AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
1459 val joint_program_inv_rect_Type1 :
1460 params -> joint_program -> (AST.ident List.list -> (joint_function,
1461 AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
1464 val joint_program_inv_rect_Type0 :
1465 params -> joint_program -> (AST.ident List.list -> (joint_function,
1466 AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
1469 val joint_program_discr : params -> joint_program -> joint_program -> __
1471 val joint_program_jmdiscr : params -> joint_program -> joint_program -> __
1473 val dpi1__o__joint_prog__o__inject :
1474 params -> (joint_program, 'a1) Types.dPair -> (joint_function,
1475 AST.init_data List.list) AST.program Types.sig0
1477 val eject__o__joint_prog__o__inject :
1478 params -> joint_program Types.sig0 -> (joint_function, AST.init_data
1479 List.list) AST.program Types.sig0
1481 val joint_prog__o__inject :
1482 params -> joint_program -> (joint_function, AST.init_data List.list)
1483 AST.program Types.sig0
1485 val dpi1__o__joint_prog :
1486 params -> (joint_program, 'a1) Types.dPair -> (joint_function,
1487 AST.init_data List.list) AST.program
1489 val eject__o__joint_prog :
1490 params -> joint_program Types.sig0 -> (joint_function, AST.init_data
1491 List.list) AST.program
1493 val prog_names : params -> joint_program -> AST.ident List.list
1495 val transform_joint_program :
1496 params -> params -> (AST.ident List.list -> joint_closed_internal_function
1497 -> joint_closed_internal_function) -> joint_program -> joint_program
1499 type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
1501 val stack_cost : params -> joint_program -> stack_cost_model
1517 val globals_stacksize : params -> joint_program -> Nat.nat