23 open Hints_declaration
114 (Registers.register, AST.typ) Types.prod Identifiers.identifier_map
117 env -> Identifiers.universe -> (AST.ident, AST.typ) Types.prod List.list ->
118 (((Registers.register, AST.typ) Types.prod List.list, env) Types.prod,
119 Identifiers.universe) Types.prod
121 val lookup_reg : env -> AST.ident -> AST.typ -> Registers.register
123 type fixed = { fx_gotos : Identifiers.identifier_set; fx_env : env;
124 fx_rettyp : AST.typ Types.option }
126 val fixed_rect_Type4 :
127 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
130 val fixed_rect_Type5 :
131 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
134 val fixed_rect_Type3 :
135 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
138 val fixed_rect_Type2 :
139 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
142 val fixed_rect_Type1 :
143 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
146 val fixed_rect_Type0 :
147 (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
150 val fx_gotos : fixed -> Identifiers.identifier_set
152 val fx_env : fixed -> env
154 val fx_rettyp : fixed -> AST.typ Types.option
156 val fixed_inv_rect_Type4 :
157 fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
160 val fixed_inv_rect_Type3 :
161 fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
164 val fixed_inv_rect_Type2 :
165 fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
168 val fixed_inv_rect_Type1 :
169 fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
172 val fixed_inv_rect_Type0 :
173 fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
176 val fixed_discr : fixed -> fixed -> __
178 val fixed_jmdiscr : fixed -> fixed -> __
183 PreIdentifiers.identifier Identifiers.identifier_map
184 (* singleton inductive, whose constructor was mk_goto_map *)
186 val goto_map_rect_Type4 :
187 fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
188 Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
190 val goto_map_rect_Type5 :
191 fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
192 Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
194 val goto_map_rect_Type3 :
195 fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
196 Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
198 val goto_map_rect_Type2 :
199 fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
200 Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
202 val goto_map_rect_Type1 :
203 fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
204 Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
206 val goto_map_rect_Type0 :
207 fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
208 Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
211 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
212 PreIdentifiers.identifier Identifiers.identifier_map
214 val goto_map_inv_rect_Type4 :
215 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
216 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
219 val goto_map_inv_rect_Type3 :
220 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
221 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
224 val goto_map_inv_rect_Type2 :
225 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
226 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
229 val goto_map_inv_rect_Type1 :
230 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
231 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
234 val goto_map_inv_rect_Type0 :
235 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
236 (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
240 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map -> __
242 val goto_map_jmdiscr :
243 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map -> __
245 val dpi1__o__gm_map__o__inject :
246 fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
247 Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map
250 val eject__o__gm_map__o__inject :
251 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
252 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0
254 val gm_map__o__inject :
255 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
256 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0
258 val dpi1__o__gm_map :
259 fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
260 Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map
262 val eject__o__gm_map :
263 fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
264 PreIdentifiers.identifier Identifiers.identifier_map
266 type partial_fn = { pf_labgen : Identifiers.universe;
267 pf_reggen : Identifiers.universe;
268 pf_params : (Registers.register, AST.typ) Types.prod
270 pf_locals : (Registers.register, AST.typ) Types.prod
271 List.list; pf_result : resultok;
272 pf_stacksize : Nat.nat;
273 pf_graph : RTLabs_syntax.statement Graphs.graph;
275 pf_labels : PreIdentifiers.identifier
276 Identifiers.identifier_map Types.sig0;
277 pf_entry : Graphs.label Types.sig0;
278 pf_exit : Graphs.label Types.sig0 }
280 val partial_fn_rect_Type4 :
281 fixed -> (Identifiers.universe -> Identifiers.universe ->
282 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
283 AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
284 RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
285 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
286 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
289 val partial_fn_rect_Type5 :
290 fixed -> (Identifiers.universe -> Identifiers.universe ->
291 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
292 AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
293 RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
294 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
295 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
298 val partial_fn_rect_Type3 :
299 fixed -> (Identifiers.universe -> Identifiers.universe ->
300 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
301 AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
302 RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
303 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
304 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
307 val partial_fn_rect_Type2 :
308 fixed -> (Identifiers.universe -> Identifiers.universe ->
309 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
310 AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
311 RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
312 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
313 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
316 val partial_fn_rect_Type1 :
317 fixed -> (Identifiers.universe -> Identifiers.universe ->
318 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
319 AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
320 RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
321 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
322 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
325 val partial_fn_rect_Type0 :
326 fixed -> (Identifiers.universe -> Identifiers.universe ->
327 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
328 AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
329 RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
330 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
331 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
334 val pf_labgen : fixed -> partial_fn -> Identifiers.universe
336 val pf_reggen : fixed -> partial_fn -> Identifiers.universe
339 fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list
342 fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list
344 val pf_result : fixed -> partial_fn -> resultok
346 val pf_stacksize : fixed -> partial_fn -> Nat.nat
348 val pf_graph : fixed -> partial_fn -> RTLabs_syntax.statement Graphs.graph
350 val pf_gotos : fixed -> partial_fn -> goto_map
353 fixed -> partial_fn -> PreIdentifiers.identifier Identifiers.identifier_map
356 val pf_entry : fixed -> partial_fn -> Graphs.label Types.sig0
358 val pf_exit : fixed -> partial_fn -> Graphs.label Types.sig0
360 val partial_fn_inv_rect_Type4 :
361 fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
362 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
363 AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
364 RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
365 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
366 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
369 val partial_fn_inv_rect_Type3 :
370 fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
371 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
372 AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
373 RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
374 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
375 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
378 val partial_fn_inv_rect_Type2 :
379 fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
380 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
381 AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
382 RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
383 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
384 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
387 val partial_fn_inv_rect_Type1 :
388 fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
389 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
390 AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
391 RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
392 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
393 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
396 val partial_fn_inv_rect_Type0 :
397 fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
398 (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
399 AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
400 RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
401 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
402 Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
405 val partial_fn_jmdiscr : fixed -> partial_fn -> partial_fn -> __
407 val fn_contains_rect_Type4 :
408 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
410 val fn_contains_rect_Type5 :
411 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
413 val fn_contains_rect_Type3 :
414 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
416 val fn_contains_rect_Type2 :
417 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
419 val fn_contains_rect_Type1 :
420 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
422 val fn_contains_rect_Type0 :
423 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
425 val fn_contains_inv_rect_Type4 :
426 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
428 val fn_contains_inv_rect_Type3 :
429 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
431 val fn_contains_inv_rect_Type2 :
432 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
434 val fn_contains_inv_rect_Type1 :
435 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
437 val fn_contains_inv_rect_Type0 :
438 fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
440 val fn_contains_discr : fixed -> partial_fn -> partial_fn -> __
442 val fn_contains_jmdiscr : fixed -> partial_fn -> partial_fn -> __
444 val fill_in_statement :
445 fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
446 partial_fn Types.sig0
449 fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
450 partial_fn Types.sig0
453 fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0
455 val add_fresh_to_graph :
456 fixed -> (Graphs.label -> RTLabs_syntax.statement) -> partial_fn ->
457 partial_fn Types.sig0
460 fixed -> partial_fn -> AST.typ -> (partial_fn Types.sig0,
461 Registers.register Types.sig0) Types.dPair
464 fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> (partial_fn
465 Types.sig0, Registers.register Types.sig0) Types.dPair
467 val foldr_all : ('a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2
470 ('a1 -> __ -> 'a1 List.list -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2
472 val eject' : ('a1, 'a2) Types.dPair -> 'a1
475 fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list -> partial_fn
476 -> (partial_fn Types.sig0, Registers.register List.list Types.sig0)
479 val add_stmt_inv_rect_Type4 :
480 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
483 val add_stmt_inv_rect_Type5 :
484 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
487 val add_stmt_inv_rect_Type3 :
488 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
491 val add_stmt_inv_rect_Type2 :
492 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
495 val add_stmt_inv_rect_Type1 :
496 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
499 val add_stmt_inv_rect_Type0 :
500 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
503 val add_stmt_inv_inv_rect_Type4 :
504 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
507 val add_stmt_inv_inv_rect_Type3 :
508 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
511 val add_stmt_inv_inv_rect_Type2 :
512 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
515 val add_stmt_inv_inv_rect_Type1 :
516 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
519 val add_stmt_inv_inv_rect_Type0 :
520 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
523 val add_stmt_inv_discr :
524 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __
526 val add_stmt_inv_jmdiscr :
527 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __
529 type fn_con_because =
530 | Fn_con_eq of partial_fn
531 | Fn_con_sig of partial_fn * partial_fn * partial_fn Types.sig0
532 | Fn_con_addinv of partial_fn * partial_fn * Cminor_syntax.stmt
533 * partial_fn Types.sig0
535 val fn_con_because_rect_Type4 :
536 fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
537 partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
538 Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
539 fn_con_because -> 'a1
541 val fn_con_because_rect_Type5 :
542 fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
543 partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
544 Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
545 fn_con_because -> 'a1
547 val fn_con_because_rect_Type3 :
548 fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
549 partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
550 Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
551 fn_con_because -> 'a1
553 val fn_con_because_rect_Type2 :
554 fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
555 partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
556 Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
557 fn_con_because -> 'a1
559 val fn_con_because_rect_Type1 :
560 fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
561 partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
562 Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
563 fn_con_because -> 'a1
565 val fn_con_because_rect_Type0 :
566 fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
567 partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
568 Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
569 fn_con_because -> 'a1
571 val fn_con_because_inv_rect_Type4 :
572 fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
573 (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
574 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
575 Types.sig0 -> __ -> __ -> 'a1) -> 'a1
577 val fn_con_because_inv_rect_Type3 :
578 fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
579 (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
580 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
581 Types.sig0 -> __ -> __ -> 'a1) -> 'a1
583 val fn_con_because_inv_rect_Type2 :
584 fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
585 (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
586 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
587 Types.sig0 -> __ -> __ -> 'a1) -> 'a1
589 val fn_con_because_inv_rect_Type1 :
590 fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
591 (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
592 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
593 Types.sig0 -> __ -> __ -> 'a1) -> 'a1
595 val fn_con_because_inv_rect_Type0 :
596 fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
597 (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
598 'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
599 Types.sig0 -> __ -> __ -> 'a1) -> 'a1
601 val fn_con_because_discr :
602 fixed -> partial_fn -> fn_con_because -> fn_con_because -> __
604 val fn_con_because_jmdiscr :
605 fixed -> partial_fn -> fn_con_because -> fn_con_because -> __
607 val fn_con_because_left : fixed -> partial_fn -> fn_con_because -> partial_fn
610 fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> Registers.register
611 Types.sig0 -> partial_fn Types.sig0
614 fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
615 Registers.register List.list -> partial_fn -> partial_fn Types.sig0
617 val stmt_inv_rect_Type4 :
618 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
620 val stmt_inv_rect_Type5 :
621 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
623 val stmt_inv_rect_Type3 :
624 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
626 val stmt_inv_rect_Type2 :
627 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
629 val stmt_inv_rect_Type1 :
630 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
632 val stmt_inv_rect_Type0 :
633 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
635 val stmt_inv_inv_rect_Type4 :
636 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
638 val stmt_inv_inv_rect_Type3 :
639 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
641 val stmt_inv_inv_rect_Type2 :
642 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
644 val stmt_inv_inv_rect_Type1 :
645 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
647 val stmt_inv_inv_rect_Type0 :
648 fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
650 val stmt_inv_discr : fixed -> Cminor_syntax.stmt -> __
652 val stmt_inv_jmdiscr : fixed -> Cminor_syntax.stmt -> __
654 val expr_is_cst_ident :
655 AST.typ -> Cminor_syntax.expr -> AST.ident Types.option
657 val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __
659 val dPair_jmdiscr : ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __
662 fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option ->
663 partial_fn -> partial_fn Types.sig0
665 val record_goto_label :
666 fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn
669 fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0
672 fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn Types.sig0
674 val patch_gotos : fixed -> partial_fn -> partial_fn Types.sig0
677 Cminor_syntax.internal_function -> RTLabs_syntax.internal_function
679 val cminor_to_rtlabs :
680 Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program