open Preamble

open Hide

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open BitVectorZ

open Pointers

open ByteValues

open BackEndOps

open CostLabel

open Order

open Registers

open I8051

open BitVectorTrie

open Graphs

open LabelledObjects

open Sets

open Listb

open String

type 't argument =
| Reg of 't
| Imm of BitVector.byte

val argument_rect_Type4 :
  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2

val argument_rect_Type5 :
  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2

val argument_rect_Type3 :
  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2

val argument_rect_Type2 :
  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2

val argument_rect_Type1 :
  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2

val argument_rect_Type0 :
  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2

val argument_inv_rect_Type4 :
  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2

val argument_inv_rect_Type3 :
  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2

val argument_inv_rect_Type2 :
  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2

val argument_inv_rect_Type1 :
  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2

val argument_inv_rect_Type0 :
  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2

val argument_discr : 'a1 argument -> 'a1 argument -> __

val argument_jmdiscr : 'a1 argument -> 'a1 argument -> __

type psd_argument = Registers.register argument

val psd_argument_from_reg : Registers.register -> psd_argument

val dpi1__o__reg_to_psd_argument__o__inject :
  (Registers.register, 'a1) Types.dPair -> psd_argument Types.sig0

val eject__o__reg_to_psd_argument__o__inject :
  Registers.register Types.sig0 -> psd_argument Types.sig0

val reg_to_psd_argument__o__inject :
  Registers.register -> psd_argument Types.sig0

val dpi1__o__reg_to_psd_argument :
  (Registers.register, 'a1) Types.dPair -> psd_argument

val eject__o__reg_to_psd_argument :
  Registers.register Types.sig0 -> psd_argument

val psd_argument_from_byte : BitVector.byte -> psd_argument

val dpi1__o__byte_to_psd_argument__o__inject :
  (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0

val eject__o__byte_to_psd_argument__o__inject :
  BitVector.byte Types.sig0 -> psd_argument Types.sig0

val byte_to_psd_argument__o__inject :
  BitVector.byte -> psd_argument Types.sig0

val dpi1__o__byte_to_psd_argument :
  (BitVector.byte, 'a1) Types.dPair -> psd_argument

val eject__o__byte_to_psd_argument :
  BitVector.byte Types.sig0 -> psd_argument

type hdw_argument = I8051.register argument

val hdw_argument_from_reg : I8051.register -> hdw_argument

val dpi1__o__reg_to_hdw_argument__o__inject :
  (I8051.register, 'a1) Types.dPair -> hdw_argument Types.sig0

val eject__o__reg_to_hdw_argument__o__inject :
  I8051.register Types.sig0 -> hdw_argument Types.sig0

val reg_to_hdw_argument__o__inject :
  I8051.register -> hdw_argument Types.sig0

val dpi1__o__reg_to_hdw_argument :
  (I8051.register, 'a1) Types.dPair -> hdw_argument

val eject__o__reg_to_hdw_argument : I8051.register Types.sig0 -> hdw_argument

val hdw_argument_from_byte : BitVector.byte -> hdw_argument

val dpi1__o__byte_to_hdw_argument__o__inject :
  (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0

val eject__o__byte_to_hdw_argument__o__inject :
  BitVector.byte Types.sig0 -> psd_argument Types.sig0

val byte_to_hdw_argument__o__inject :
  BitVector.byte -> psd_argument Types.sig0

val dpi1__o__byte_to_hdw_argument :
  (BitVector.byte, 'a1) Types.dPair -> psd_argument

val eject__o__byte_to_hdw_argument :
  BitVector.byte Types.sig0 -> psd_argument

val byte_of_nat : Nat.nat -> BitVector.byte

val zero_byte : BitVector.byte

type unserialized_params = { ext_seq_labels : (__ -> Graphs.label List.list);
                             has_tailcalls : Bool.bool }

val unserialized_params_rect_Type4 :
  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
  unserialized_params -> 'a1

val unserialized_params_rect_Type5 :
  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
  unserialized_params -> 'a1

val unserialized_params_rect_Type3 :
  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
  unserialized_params -> 'a1

val unserialized_params_rect_Type2 :
  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
  unserialized_params -> 'a1

val unserialized_params_rect_Type1 :
  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
  unserialized_params -> 'a1

val unserialized_params_rect_Type0 :
  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
  unserialized_params -> 'a1

type acc_a_reg 

type acc_b_reg 

type acc_a_arg 

type acc_b_arg 

type dpl_reg 

type dph_reg 

type dpl_arg 

type dph_arg 

type snd_arg 

type pair_move 

type call_args 

type call_dest 

type ext_seq 

val ext_seq_labels : unserialized_params -> __ -> Graphs.label List.list

val has_tailcalls : unserialized_params -> Bool.bool

type paramsT 

val unserialized_params_inv_rect_Type4 :
  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
  __ -> __ -> 'a1) -> 'a1

val unserialized_params_inv_rect_Type3 :
  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
  __ -> __ -> 'a1) -> 'a1

val unserialized_params_inv_rect_Type2 :
  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
  __ -> __ -> 'a1) -> 'a1

val unserialized_params_inv_rect_Type1 :
  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
  __ -> __ -> 'a1) -> 'a1

val unserialized_params_inv_rect_Type0 :
  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
  __ -> __ -> 'a1) -> 'a1

val unserialized_params_jmdiscr :
  unserialized_params -> unserialized_params -> __

type get_pseudo_reg_functs = { acc_a_regs : (__ -> Registers.register
                                            List.list);
                               acc_b_regs : (__ -> Registers.register
                                            List.list);
                               acc_a_args : (__ -> Registers.register
                                            List.list);
                               acc_b_args : (__ -> Registers.register
                                            List.list);
                               dpl_regs : (__ -> Registers.register
                                          List.list);
                               dph_regs : (__ -> Registers.register
                                          List.list);
                               dpl_args : (__ -> Registers.register
                                          List.list);
                               dph_args : (__ -> Registers.register
                                          List.list);
                               snd_args : (__ -> Registers.register
                                          List.list);
                               pair_move_regs : (__ -> Registers.register
                                                List.list);
                               f_call_args : (__ -> Registers.register
                                             List.list);
                               f_call_dest : (__ -> Registers.register
                                             List.list);
                               ext_seq_regs : (__ -> Registers.register
                                              List.list);
                               params_regs : (__ -> Registers.register
                                             List.list) }

val get_pseudo_reg_functs_rect_Type4 :
  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
  'a1

val get_pseudo_reg_functs_rect_Type5 :
  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
  'a1

val get_pseudo_reg_functs_rect_Type3 :
  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
  'a1

val get_pseudo_reg_functs_rect_Type2 :
  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
  'a1

val get_pseudo_reg_functs_rect_Type1 :
  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
  'a1

val get_pseudo_reg_functs_rect_Type0 :
  unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
  'a1

val acc_a_regs :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val acc_b_regs :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val acc_a_args :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val acc_b_args :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val dpl_regs :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val dph_regs :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val dpl_args :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val dph_args :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val snd_args :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val pair_move_regs :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val f_call_args :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val f_call_dest :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val ext_seq_regs :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val params_regs :
  unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
  List.list

val get_pseudo_reg_functs_inv_rect_Type4 :
  unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) -> __
  -> 'a1) -> 'a1

val get_pseudo_reg_functs_inv_rect_Type3 :
  unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) -> __
  -> 'a1) -> 'a1

val get_pseudo_reg_functs_inv_rect_Type2 :
  unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) -> __
  -> 'a1) -> 'a1

val get_pseudo_reg_functs_inv_rect_Type1 :
  unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) -> __
  -> 'a1) -> 'a1

val get_pseudo_reg_functs_inv_rect_Type0 :
  unserialized_params -> get_pseudo_reg_functs -> ((__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) ->
  (__ -> Registers.register List.list) -> (__ -> Registers.register
  List.list) -> (__ -> Registers.register List.list) -> (__ ->
  Registers.register List.list) -> (__ -> Registers.register List.list) -> __
  -> 'a1) -> 'a1

val get_pseudo_reg_functs_jmdiscr :
  unserialized_params -> get_pseudo_reg_functs -> get_pseudo_reg_functs -> __

type uns_params = { u_pars : unserialized_params;
                    functs : get_pseudo_reg_functs }

val uns_params_rect_Type4 :
  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1

val uns_params_rect_Type5 :
  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1

val uns_params_rect_Type3 :
  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1

val uns_params_rect_Type2 :
  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1

val uns_params_rect_Type1 :
  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1

val uns_params_rect_Type0 :
  (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1

val u_pars : uns_params -> unserialized_params

val functs : uns_params -> get_pseudo_reg_functs

val uns_params_inv_rect_Type4 :
  uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
  -> 'a1

val uns_params_inv_rect_Type3 :
  uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
  -> 'a1

val uns_params_inv_rect_Type2 :
  uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
  -> 'a1

val uns_params_inv_rect_Type1 :
  uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
  -> 'a1

val uns_params_inv_rect_Type0 :
  uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
  -> 'a1

val uns_params_jmdiscr : uns_params -> uns_params -> __

type joint_seq =
| COMMENT of String.string
| MOVE of __
| POP of __
| PUSH of __
| ADDRESS of AST.ident * BitVector.word * __ * __
| OPACCS of BackEndOps.opAccs * __ * __ * __ * __
| OP1 of BackEndOps.op1 * __ * __
| OP2 of BackEndOps.op2 * __ * __ * __
| CLEAR_CARRY
| SET_CARRY
| LOAD of __ * __ * __
| STORE of __ * __ * __
| Extension_seq of __

val joint_seq_rect_Type4 :
  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
  -> (__ -> 'a1) -> joint_seq -> 'a1

val joint_seq_rect_Type5 :
  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
  -> (__ -> 'a1) -> joint_seq -> 'a1

val joint_seq_rect_Type3 :
  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
  -> (__ -> 'a1) -> joint_seq -> 'a1

val joint_seq_rect_Type2 :
  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
  -> (__ -> 'a1) -> joint_seq -> 'a1

val joint_seq_rect_Type1 :
  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
  -> (__ -> 'a1) -> joint_seq -> 'a1

val joint_seq_rect_Type0 :
  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> BitVector.word
  -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1)
  -> (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __
  -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1)
  -> (__ -> 'a1) -> joint_seq -> 'a1

val joint_seq_inv_rect_Type4 :
  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
  'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
  (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
  -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
  -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1

val joint_seq_inv_rect_Type3 :
  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
  'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
  (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
  -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
  -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1

val joint_seq_inv_rect_Type2 :
  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
  'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
  (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
  -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
  -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1

val joint_seq_inv_rect_Type1 :
  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
  'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
  (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
  -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
  -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1

val joint_seq_inv_rect_Type0 :
  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
  'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
  (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1
  -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__
  -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1

val joint_seq_discr :
  unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __

val joint_seq_jmdiscr :
  unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __

val get_used_registers_from_seq :
  unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
  joint_seq -> Registers.register List.list

val nOOP : unserialized_params -> AST.ident List.list -> joint_seq

val dpi1__o__extension_seq_to_seq__o__inject :
  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
  joint_seq Types.sig0

val eject__o__extension_seq_to_seq__o__inject :
  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
  Types.sig0

val extension_seq_to_seq__o__inject :
  unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0

val dpi1__o__extension_seq_to_seq :
  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
  joint_seq

val eject__o__extension_seq_to_seq :
  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq

type joint_step =
| COST_LABEL of CostLabel.costlabel
| CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
| COND of __ * Graphs.label
| Step_seq of joint_seq

val joint_step_rect_Type4 :
  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1

val joint_step_rect_Type5 :
  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1

val joint_step_rect_Type3 :
  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1

val joint_step_rect_Type2 :
  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1

val joint_step_rect_Type1 :
  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1

val joint_step_rect_Type0 :
  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1

val joint_step_inv_rect_Type4 :
  unserialized_params -> AST.ident List.list -> joint_step ->
  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
  (joint_seq -> __ -> 'a1) -> 'a1

val joint_step_inv_rect_Type3 :
  unserialized_params -> AST.ident List.list -> joint_step ->
  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
  (joint_seq -> __ -> 'a1) -> 'a1

val joint_step_inv_rect_Type2 :
  unserialized_params -> AST.ident List.list -> joint_step ->
  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
  (joint_seq -> __ -> 'a1) -> 'a1

val joint_step_inv_rect_Type1 :
  unserialized_params -> AST.ident List.list -> joint_step ->
  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
  (joint_seq -> __ -> 'a1) -> 'a1

val joint_step_inv_rect_Type0 :
  unserialized_params -> AST.ident List.list -> joint_step ->
  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
  (joint_seq -> __ -> 'a1) -> 'a1

val joint_step_discr :
  unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
  __

val joint_step_jmdiscr :
  unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
  __

val get_used_registers_from_step :
  unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
  joint_step -> Registers.register List.list

val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
  joint_step Types.sig0

val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
  Types.sig0

val extension_seq_to_seq__o__seq_to_step__o__inject :
  unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0

val dpi1__o__seq_to_step__o__inject :
  unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
  -> joint_step Types.sig0

val eject__o__seq_to_step__o__inject :
  unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
  joint_step Types.sig0

val seq_to_step__o__inject :
  unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
  Types.sig0

val dpi1__o__extension_seq_to_seq__o__seq_to_step :
  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
  joint_step

val eject__o__extension_seq_to_seq__o__seq_to_step :
  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step

val extension_seq_to_seq__o__seq_to_step :
  unserialized_params -> AST.ident List.list -> __ -> joint_step

val dpi1__o__seq_to_step :
  unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
  -> joint_step

val eject__o__seq_to_step :
  unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
  joint_step

val step_labels :
  unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
  List.list

type stmt_params = { uns_pars : uns_params;
                     succ_label : (__ -> Graphs.label Types.option);
                     has_fcond : Bool.bool }

val stmt_params_rect_Type4 :
  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
  -> stmt_params -> 'a1

val stmt_params_rect_Type5 :
  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
  -> stmt_params -> 'a1

val stmt_params_rect_Type3 :
  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
  -> stmt_params -> 'a1

val stmt_params_rect_Type2 :
  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
  -> stmt_params -> 'a1

val stmt_params_rect_Type1 :
  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
  -> stmt_params -> 'a1

val stmt_params_rect_Type0 :
  (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1)
  -> stmt_params -> 'a1

val uns_pars : stmt_params -> uns_params

type succ 

val succ_label : stmt_params -> __ -> Graphs.label Types.option

val has_fcond : stmt_params -> Bool.bool

val stmt_params_inv_rect_Type4 :
  stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
  Bool.bool -> __ -> 'a1) -> 'a1

val stmt_params_inv_rect_Type3 :
  stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
  Bool.bool -> __ -> 'a1) -> 'a1

val stmt_params_inv_rect_Type2 :
  stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
  Bool.bool -> __ -> 'a1) -> 'a1

val stmt_params_inv_rect_Type1 :
  stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
  Bool.bool -> __ -> 'a1) -> 'a1

val stmt_params_inv_rect_Type0 :
  stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
  Bool.bool -> __ -> 'a1) -> 'a1

val stmt_params_jmdiscr : stmt_params -> stmt_params -> __

val uns_pars__o__u_pars : stmt_params -> unserialized_params

type joint_fin_step =
| GOTO of Graphs.label
| RETURN
| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __

val joint_fin_step_rect_Type4 :
  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1

val joint_fin_step_rect_Type5 :
  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1

val joint_fin_step_rect_Type3 :
  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1

val joint_fin_step_rect_Type2 :
  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1

val joint_fin_step_rect_Type1 :
  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1

val joint_fin_step_rect_Type0 :
  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1

val joint_fin_step_inv_rect_Type4 :
  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
  'a1) -> 'a1

val joint_fin_step_inv_rect_Type3 :
  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
  'a1) -> 'a1

val joint_fin_step_inv_rect_Type2 :
  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
  'a1) -> 'a1

val joint_fin_step_inv_rect_Type1 :
  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
  'a1) -> 'a1

val joint_fin_step_inv_rect_Type0 :
  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
  'a1) -> 'a1

val joint_fin_step_discr :
  unserialized_params -> joint_fin_step -> joint_fin_step -> __

val joint_fin_step_jmdiscr :
  unserialized_params -> joint_fin_step -> joint_fin_step -> __

val fin_step_labels :
  unserialized_params -> joint_fin_step -> Graphs.label List.list

type joint_statement =
| Sequential of joint_step * __
| Final of joint_fin_step
| FCOND of __ * Graphs.label * Graphs.label

val joint_statement_rect_Type4 :
  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
  'a1) -> joint_statement -> 'a1

val joint_statement_rect_Type5 :
  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
  'a1) -> joint_statement -> 'a1

val joint_statement_rect_Type3 :
  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
  'a1) -> joint_statement -> 'a1

val joint_statement_rect_Type2 :
  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
  'a1) -> joint_statement -> 'a1

val joint_statement_rect_Type1 :
  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
  'a1) -> joint_statement -> 'a1

val joint_statement_rect_Type0 :
  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
  'a1) -> joint_statement -> 'a1

val joint_statement_inv_rect_Type4 :
  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
  -> Graphs.label -> __ -> 'a1) -> 'a1

val joint_statement_inv_rect_Type3 :
  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
  -> Graphs.label -> __ -> 'a1) -> 'a1

val joint_statement_inv_rect_Type2 :
  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
  -> Graphs.label -> __ -> 'a1) -> 'a1

val joint_statement_inv_rect_Type1 :
  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
  -> Graphs.label -> __ -> 'a1) -> 'a1

val joint_statement_inv_rect_Type0 :
  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
  -> Graphs.label -> __ -> 'a1) -> 'a1

val joint_statement_discr :
  stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
  __

val joint_statement_jmdiscr :
  stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
  __

val dpi1__o__fin_step_to_stmt__o__inject :
  stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
  joint_statement Types.sig0

val eject__o__fin_step_to_stmt__o__inject :
  stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
  joint_statement Types.sig0

val fin_step_to_stmt__o__inject :
  stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
  Types.sig0

val dpi1__o__fin_step_to_stmt :
  stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
  joint_statement

val eject__o__fin_step_to_stmt :
  stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
  joint_statement

type params = { stmt_pars : stmt_params;
                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
                          Types.option);
                point_of_label : (AST.ident List.list -> __ -> Graphs.label
                                 -> __ Types.option);
                point_of_succ : (__ -> __ -> __) }

val params_rect_Type4 :
  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1

val params_rect_Type5 :
  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1

val params_rect_Type3 :
  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1

val params_rect_Type2 :
  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1

val params_rect_Type1 :
  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1

val params_rect_Type0 :
  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1

val stmt_pars : params -> stmt_params

type codeT 

type code_point 

val stmt_at :
  params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option

val point_of_label :
  params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option

val point_of_succ : params -> __ -> __ -> __

val params_inv_rect_Type4 :
  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1

val params_inv_rect_Type3 :
  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1

val params_inv_rect_Type2 :
  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1

val params_inv_rect_Type1 :
  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1

val params_inv_rect_Type0 :
  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1

val params_jmdiscr : params -> params -> __

val stmt_pars__o__uns_pars : params -> uns_params

val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params

val code_has_point : params -> AST.ident List.list -> __ -> __ -> Bool.bool

val code_has_label :
  params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool

val stmt_explicit_labels :
  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
  List.list

val stmt_implicit_label :
  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
  Types.option

val stmt_labels :
  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
  List.list

val stmt_registers :
  stmt_params -> AST.ident List.list -> joint_statement -> Registers.register
  List.list

type lin_params =
  uns_params
  (* singleton inductive, whose constructor was mk_lin_params *)

val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1

val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1

val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1

val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1

val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1

val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1

val l_u_pars : lin_params -> uns_params

val lin_params_inv_rect_Type4 :
  lin_params -> (uns_params -> __ -> 'a1) -> 'a1

val lin_params_inv_rect_Type3 :
  lin_params -> (uns_params -> __ -> 'a1) -> 'a1

val lin_params_inv_rect_Type2 :
  lin_params -> (uns_params -> __ -> 'a1) -> 'a1

val lin_params_inv_rect_Type1 :
  lin_params -> (uns_params -> __ -> 'a1) -> 'a1

val lin_params_inv_rect_Type0 :
  lin_params -> (uns_params -> __ -> 'a1) -> 'a1

val lin_params_jmdiscr : lin_params -> lin_params -> __

val lin_params_to_params : lin_params -> params

val lp_to_p__o__stmt_pars : lin_params -> stmt_params

val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params

val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
  lin_params -> unserialized_params

type graph_params =
  uns_params
  (* singleton inductive, whose constructor was mk_graph_params *)

val graph_params_rect_Type4 : (uns_params -> 'a1) -> graph_params -> 'a1

val graph_params_rect_Type5 : (uns_params -> 'a1) -> graph_params -> 'a1

val graph_params_rect_Type3 : (uns_params -> 'a1) -> graph_params -> 'a1

val graph_params_rect_Type2 : (uns_params -> 'a1) -> graph_params -> 'a1

val graph_params_rect_Type1 : (uns_params -> 'a1) -> graph_params -> 'a1

val graph_params_rect_Type0 : (uns_params -> 'a1) -> graph_params -> 'a1

val g_u_pars : graph_params -> uns_params

val graph_params_inv_rect_Type4 :
  graph_params -> (uns_params -> __ -> 'a1) -> 'a1

val graph_params_inv_rect_Type3 :
  graph_params -> (uns_params -> __ -> 'a1) -> 'a1

val graph_params_inv_rect_Type2 :
  graph_params -> (uns_params -> __ -> 'a1) -> 'a1

val graph_params_inv_rect_Type1 :
  graph_params -> (uns_params -> __ -> 'a1) -> 'a1

val graph_params_inv_rect_Type0 :
  graph_params -> (uns_params -> __ -> 'a1) -> 'a1

val graph_params_jmdiscr : graph_params -> graph_params -> __

val graph_params_to_params : graph_params -> params

val gp_to_p__o__stmt_pars : graph_params -> stmt_params

val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params

val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
  graph_params -> unserialized_params

type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
                                 joint_if_runiverse : Identifiers.universe;
                                 joint_if_result : __; joint_if_params : 
                                 __; joint_if_stacksize : Nat.nat;
                                 joint_if_local_stacksize : Nat.nat;
                                 joint_if_code : __; joint_if_entry : 
                                 __ }

val joint_internal_function_rect_Type4 :
  params -> AST.ident List.list -> (Identifiers.universe ->
  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
  -> joint_internal_function -> 'a1

val joint_internal_function_rect_Type5 :
  params -> AST.ident List.list -> (Identifiers.universe ->
  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
  -> joint_internal_function -> 'a1

val joint_internal_function_rect_Type3 :
  params -> AST.ident List.list -> (Identifiers.universe ->
  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
  -> joint_internal_function -> 'a1

val joint_internal_function_rect_Type2 :
  params -> AST.ident List.list -> (Identifiers.universe ->
  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
  -> joint_internal_function -> 'a1

val joint_internal_function_rect_Type1 :
  params -> AST.ident List.list -> (Identifiers.universe ->
  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
  -> joint_internal_function -> 'a1

val joint_internal_function_rect_Type0 :
  params -> AST.ident List.list -> (Identifiers.universe ->
  Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1)
  -> joint_internal_function -> 'a1

val joint_if_luniverse :
  params -> AST.ident List.list -> joint_internal_function ->
  Identifiers.universe

val joint_if_runiverse :
  params -> AST.ident List.list -> joint_internal_function ->
  Identifiers.universe

val joint_if_result :
  params -> AST.ident List.list -> joint_internal_function -> __

val joint_if_params :
  params -> AST.ident List.list -> joint_internal_function -> __

val joint_if_stacksize :
  params -> AST.ident List.list -> joint_internal_function -> Nat.nat

val joint_if_local_stacksize :
  params -> AST.ident List.list -> joint_internal_function -> Nat.nat

val joint_if_code :
  params -> AST.ident List.list -> joint_internal_function -> __

val joint_if_entry :
  params -> AST.ident List.list -> joint_internal_function -> __

val joint_internal_function_inv_rect_Type4 :
  params -> AST.ident List.list -> joint_internal_function ->
  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1

val joint_internal_function_inv_rect_Type3 :
  params -> AST.ident List.list -> joint_internal_function ->
  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1

val joint_internal_function_inv_rect_Type2 :
  params -> AST.ident List.list -> joint_internal_function ->
  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1

val joint_internal_function_inv_rect_Type1 :
  params -> AST.ident List.list -> joint_internal_function ->
  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1

val joint_internal_function_inv_rect_Type0 :
  params -> AST.ident List.list -> joint_internal_function ->
  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1

val joint_internal_function_jmdiscr :
  params -> AST.ident List.list -> joint_internal_function ->
  joint_internal_function -> __

val good_if_rect_Type4 :
  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val good_if_rect_Type5 :
  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val good_if_rect_Type3 :
  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val good_if_rect_Type2 :
  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val good_if_rect_Type1 :
  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val good_if_rect_Type0 :
  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val good_if_inv_rect_Type4 :
  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
  -> __ -> __ -> __ -> 'a1) -> 'a1

val good_if_inv_rect_Type3 :
  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
  -> __ -> __ -> __ -> 'a1) -> 'a1

val good_if_inv_rect_Type2 :
  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
  -> __ -> __ -> __ -> 'a1) -> 'a1

val good_if_inv_rect_Type1 :
  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
  -> __ -> __ -> __ -> 'a1) -> 'a1

val good_if_inv_rect_Type0 :
  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
  -> __ -> __ -> __ -> 'a1) -> 'a1

val good_if_discr :
  params -> AST.ident List.list -> joint_internal_function -> __

val good_if_jmdiscr :
  params -> AST.ident List.list -> joint_internal_function -> __

type joint_closed_internal_function = joint_internal_function Types.sig0

val set_joint_code :
  AST.ident List.list -> params -> joint_internal_function -> __ -> __ ->
  joint_internal_function

val set_luniverse :
  params -> AST.ident List.list -> joint_internal_function ->
  Identifiers.universe -> joint_internal_function

val set_runiverse :
  params -> AST.ident List.list -> joint_internal_function ->
  Identifiers.universe -> joint_internal_function

val add_graph :
  graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
  joint_internal_function -> joint_internal_function

type joint_function = joint_closed_internal_function AST.fundef

type joint_program = { jp_functions : AST.ident List.list;
                       joint_prog : (joint_function, AST.init_data List.list)
                                    AST.program;
                       init_cost_label : CostLabel.costlabel }

val joint_program_rect_Type4 :
  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1

val joint_program_rect_Type5 :
  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1

val joint_program_rect_Type3 :
  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1

val joint_program_rect_Type2 :
  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1

val joint_program_rect_Type1 :
  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1

val joint_program_rect_Type0 :
  params -> (AST.ident List.list -> (joint_function, AST.init_data List.list)
  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> joint_program -> 'a1

val jp_functions : params -> joint_program -> AST.ident List.list

val joint_prog :
  params -> joint_program -> (joint_function, AST.init_data List.list)
  AST.program

val init_cost_label : params -> joint_program -> CostLabel.costlabel

val joint_program_inv_rect_Type4 :
  params -> joint_program -> (AST.ident List.list -> (joint_function,
  AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
  'a1) -> 'a1

val joint_program_inv_rect_Type3 :
  params -> joint_program -> (AST.ident List.list -> (joint_function,
  AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
  'a1) -> 'a1

val joint_program_inv_rect_Type2 :
  params -> joint_program -> (AST.ident List.list -> (joint_function,
  AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
  'a1) -> 'a1

val joint_program_inv_rect_Type1 :
  params -> joint_program -> (AST.ident List.list -> (joint_function,
  AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
  'a1) -> 'a1

val joint_program_inv_rect_Type0 :
  params -> joint_program -> (AST.ident List.list -> (joint_function,
  AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __ ->
  'a1) -> 'a1

val joint_program_discr : params -> joint_program -> joint_program -> __

val joint_program_jmdiscr : params -> joint_program -> joint_program -> __

val dpi1__o__joint_prog__o__inject :
  params -> (joint_program, 'a1) Types.dPair -> (joint_function,
  AST.init_data List.list) AST.program Types.sig0

val eject__o__joint_prog__o__inject :
  params -> joint_program Types.sig0 -> (joint_function, AST.init_data
  List.list) AST.program Types.sig0

val joint_prog__o__inject :
  params -> joint_program -> (joint_function, AST.init_data List.list)
  AST.program Types.sig0

val dpi1__o__joint_prog :
  params -> (joint_program, 'a1) Types.dPair -> (joint_function,
  AST.init_data List.list) AST.program

val eject__o__joint_prog :
  params -> joint_program Types.sig0 -> (joint_function, AST.init_data
  List.list) AST.program

val prog_names : params -> joint_program -> AST.ident List.list

val transform_joint_program :
  params -> params -> (AST.ident List.list -> joint_closed_internal_function
  -> joint_closed_internal_function) -> joint_program -> joint_program

type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list

val stack_cost : params -> joint_program -> stack_cost_model

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open GenMem

open FrontEndMem

open Globalenvs

val globals_stacksize : params -> joint_program -> Nat.nat