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 **) let rec argument_rect_Type4 h_Reg h_Imm = function | Reg x_16867 -> h_Reg x_16867 | Imm x_16868 -> h_Imm x_16868 (** val argument_rect_Type5 : ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **) let rec argument_rect_Type5 h_Reg h_Imm = function | Reg x_16872 -> h_Reg x_16872 | Imm x_16873 -> h_Imm x_16873 (** val argument_rect_Type3 : ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **) let rec argument_rect_Type3 h_Reg h_Imm = function | Reg x_16877 -> h_Reg x_16877 | Imm x_16878 -> h_Imm x_16878 (** val argument_rect_Type2 : ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **) let rec argument_rect_Type2 h_Reg h_Imm = function | Reg x_16882 -> h_Reg x_16882 | Imm x_16883 -> h_Imm x_16883 (** val argument_rect_Type1 : ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **) let rec argument_rect_Type1 h_Reg h_Imm = function | Reg x_16887 -> h_Reg x_16887 | Imm x_16888 -> h_Imm x_16888 (** val argument_rect_Type0 : ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **) let rec argument_rect_Type0 h_Reg h_Imm = function | Reg x_16892 -> h_Reg x_16892 | Imm x_16893 -> h_Imm x_16893 (** val argument_inv_rect_Type4 : 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2 **) let argument_inv_rect_Type4 hterm h1 h2 = let hcut = argument_rect_Type4 h1 h2 hterm in hcut __ (** val argument_inv_rect_Type3 : 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2 **) let argument_inv_rect_Type3 hterm h1 h2 = let hcut = argument_rect_Type3 h1 h2 hterm in hcut __ (** val argument_inv_rect_Type2 : 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2 **) let argument_inv_rect_Type2 hterm h1 h2 = let hcut = argument_rect_Type2 h1 h2 hterm in hcut __ (** val argument_inv_rect_Type1 : 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2 **) let argument_inv_rect_Type1 hterm h1 h2 = let hcut = argument_rect_Type1 h1 h2 hterm in hcut __ (** val argument_inv_rect_Type0 : 'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2 **) let argument_inv_rect_Type0 hterm h1 h2 = let hcut = argument_rect_Type0 h1 h2 hterm in hcut __ (** val argument_discr : 'a1 argument -> 'a1 argument -> __ **) let argument_discr x y = Logic.eq_rect_Type2 x (match x with | Reg a0 -> Obj.magic (fun _ dH -> dH __) | Imm a0 -> Obj.magic (fun _ dH -> dH __)) y (** val argument_jmdiscr : 'a1 argument -> 'a1 argument -> __ **) let argument_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | Reg a0 -> Obj.magic (fun _ dH -> dH __) | Imm a0 -> Obj.magic (fun _ dH -> dH __)) y type psd_argument = Registers.register argument (** val psd_argument_from_reg : Registers.register -> psd_argument **) let psd_argument_from_reg x = Reg x (** val dpi1__o__reg_to_psd_argument__o__inject : (Registers.register, 'a1) Types.dPair -> psd_argument Types.sig0 **) let dpi1__o__reg_to_psd_argument__o__inject x2 = psd_argument_from_reg x2.Types.dpi1 (** val eject__o__reg_to_psd_argument__o__inject : Registers.register Types.sig0 -> psd_argument Types.sig0 **) let eject__o__reg_to_psd_argument__o__inject x2 = psd_argument_from_reg (Types.pi1 x2) (** val reg_to_psd_argument__o__inject : Registers.register -> psd_argument Types.sig0 **) let reg_to_psd_argument__o__inject x1 = psd_argument_from_reg x1 (** val dpi1__o__reg_to_psd_argument : (Registers.register, 'a1) Types.dPair -> psd_argument **) let dpi1__o__reg_to_psd_argument x1 = psd_argument_from_reg x1.Types.dpi1 (** val eject__o__reg_to_psd_argument : Registers.register Types.sig0 -> psd_argument **) let eject__o__reg_to_psd_argument x1 = psd_argument_from_reg (Types.pi1 x1) (** val psd_argument_from_byte : BitVector.byte -> psd_argument **) let psd_argument_from_byte x = Imm x (** val dpi1__o__byte_to_psd_argument__o__inject : (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0 **) let dpi1__o__byte_to_psd_argument__o__inject x2 = psd_argument_from_byte x2.Types.dpi1 (** val eject__o__byte_to_psd_argument__o__inject : BitVector.byte Types.sig0 -> psd_argument Types.sig0 **) let eject__o__byte_to_psd_argument__o__inject x2 = psd_argument_from_byte (Types.pi1 x2) (** val byte_to_psd_argument__o__inject : BitVector.byte -> psd_argument Types.sig0 **) let byte_to_psd_argument__o__inject x1 = psd_argument_from_byte x1 (** val dpi1__o__byte_to_psd_argument : (BitVector.byte, 'a1) Types.dPair -> psd_argument **) let dpi1__o__byte_to_psd_argument x1 = psd_argument_from_byte x1.Types.dpi1 (** val eject__o__byte_to_psd_argument : BitVector.byte Types.sig0 -> psd_argument **) let eject__o__byte_to_psd_argument x1 = psd_argument_from_byte (Types.pi1 x1) type hdw_argument = I8051.register argument (** val hdw_argument_from_reg : I8051.register -> hdw_argument **) let hdw_argument_from_reg x = Reg x (** val dpi1__o__reg_to_hdw_argument__o__inject : (I8051.register, 'a1) Types.dPair -> hdw_argument Types.sig0 **) let dpi1__o__reg_to_hdw_argument__o__inject x2 = hdw_argument_from_reg x2.Types.dpi1 (** val eject__o__reg_to_hdw_argument__o__inject : I8051.register Types.sig0 -> hdw_argument Types.sig0 **) let eject__o__reg_to_hdw_argument__o__inject x2 = hdw_argument_from_reg (Types.pi1 x2) (** val reg_to_hdw_argument__o__inject : I8051.register -> hdw_argument Types.sig0 **) let reg_to_hdw_argument__o__inject x1 = hdw_argument_from_reg x1 (** val dpi1__o__reg_to_hdw_argument : (I8051.register, 'a1) Types.dPair -> hdw_argument **) let dpi1__o__reg_to_hdw_argument x1 = hdw_argument_from_reg x1.Types.dpi1 (** val eject__o__reg_to_hdw_argument : I8051.register Types.sig0 -> hdw_argument **) let eject__o__reg_to_hdw_argument x1 = hdw_argument_from_reg (Types.pi1 x1) (** val hdw_argument_from_byte : BitVector.byte -> hdw_argument **) let hdw_argument_from_byte x = Imm x (** val dpi1__o__byte_to_hdw_argument__o__inject : (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0 **) let dpi1__o__byte_to_hdw_argument__o__inject x2 = psd_argument_from_byte x2.Types.dpi1 (** val eject__o__byte_to_hdw_argument__o__inject : BitVector.byte Types.sig0 -> psd_argument Types.sig0 **) let eject__o__byte_to_hdw_argument__o__inject x2 = psd_argument_from_byte (Types.pi1 x2) (** val byte_to_hdw_argument__o__inject : BitVector.byte -> psd_argument Types.sig0 **) let byte_to_hdw_argument__o__inject x1 = psd_argument_from_byte x1 (** val dpi1__o__byte_to_hdw_argument : (BitVector.byte, 'a1) Types.dPair -> psd_argument **) let dpi1__o__byte_to_hdw_argument x1 = psd_argument_from_byte x1.Types.dpi1 (** val eject__o__byte_to_hdw_argument : BitVector.byte Types.sig0 -> psd_argument **) let eject__o__byte_to_hdw_argument x1 = psd_argument_from_byte (Types.pi1 x1) (** val byte_of_nat : Nat.nat -> BitVector.byte **) let byte_of_nat = Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (** val zero_byte : BitVector.byte **) let zero_byte = BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) 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 **) let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_16928 = let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = x_16928 in h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ ext_seq_labels0 has_tailcalls0 __ (** val unserialized_params_rect_Type5 : (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) -> unserialized_params -> 'a1 **) let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_16930 = let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = x_16930 in h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ ext_seq_labels0 has_tailcalls0 __ (** val unserialized_params_rect_Type3 : (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) -> unserialized_params -> 'a1 **) let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_16932 = let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = x_16932 in h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ ext_seq_labels0 has_tailcalls0 __ (** val unserialized_params_rect_Type2 : (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) -> unserialized_params -> 'a1 **) let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_16934 = let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = x_16934 in h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ ext_seq_labels0 has_tailcalls0 __ (** val unserialized_params_rect_Type1 : (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) -> unserialized_params -> 'a1 **) let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_16936 = let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = x_16936 in h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ ext_seq_labels0 has_tailcalls0 __ (** val unserialized_params_rect_Type0 : (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) -> unserialized_params -> 'a1 **) let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_16938 = let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } = x_16938 in h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __ ext_seq_labels0 has_tailcalls0 __ 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 **) let rec ext_seq_labels xxx = xxx.ext_seq_labels (** val has_tailcalls : unserialized_params -> Bool.bool **) let rec has_tailcalls xxx = xxx.has_tailcalls type paramsT = __ (** val unserialized_params_inv_rect_Type4 : unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> __ -> 'a1) -> 'a1 **) let unserialized_params_inv_rect_Type4 hterm h1 = let hcut = unserialized_params_rect_Type4 h1 hterm in hcut __ (** val unserialized_params_inv_rect_Type3 : unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> __ -> 'a1) -> 'a1 **) let unserialized_params_inv_rect_Type3 hterm h1 = let hcut = unserialized_params_rect_Type3 h1 hterm in hcut __ (** val unserialized_params_inv_rect_Type2 : unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> __ -> 'a1) -> 'a1 **) let unserialized_params_inv_rect_Type2 hterm h1 = let hcut = unserialized_params_rect_Type2 h1 hterm in hcut __ (** val unserialized_params_inv_rect_Type1 : unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> __ -> 'a1) -> 'a1 **) let unserialized_params_inv_rect_Type1 hterm h1 = let hcut = unserialized_params_rect_Type1 h1 hterm in hcut __ (** val unserialized_params_inv_rect_Type0 : unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> __ -> 'a1) -> 'a1 **) let unserialized_params_inv_rect_Type0 hterm h1 = let hcut = unserialized_params_rect_Type0 h1 hterm in hcut __ (** val unserialized_params_jmdiscr : unserialized_params -> unserialized_params -> __ **) let unserialized_params_jmdiscr x y = Logic.eq_rect_Type2 x (let { ext_seq_labels = a13; has_tailcalls = a14 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y 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 **) let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_16955 = let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args = snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = params_regs0 } = x_16955 in h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0 (** 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 **) let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_16957 = let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args = snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = params_regs0 } = x_16957 in h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0 (** 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 **) let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_16959 = let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args = snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = params_regs0 } = x_16959 in h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0 (** 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 **) let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_16961 = let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args = snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = params_regs0 } = x_16961 in h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0 (** 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 **) let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_16963 = let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args = snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = params_regs0 } = x_16963 in h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0 (** 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 **) let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_16965 = let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args = acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs = dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args = snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0; f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs = params_regs0 } = x_16965 in h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0 dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0 f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0 (** val acc_a_regs : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec acc_a_regs p xxx = xxx.acc_a_regs (** val acc_b_regs : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec acc_b_regs p xxx = xxx.acc_b_regs (** val acc_a_args : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec acc_a_args p xxx = xxx.acc_a_args (** val acc_b_args : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec acc_b_args p xxx = xxx.acc_b_args (** val dpl_regs : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec dpl_regs p xxx = xxx.dpl_regs (** val dph_regs : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec dph_regs p xxx = xxx.dph_regs (** val dpl_args : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec dpl_args p xxx = xxx.dpl_args (** val dph_args : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec dph_args p xxx = xxx.dph_args (** val snd_args : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec snd_args p xxx = xxx.snd_args (** val pair_move_regs : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec pair_move_regs p xxx = xxx.pair_move_regs (** val f_call_args : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec f_call_args p xxx = xxx.f_call_args (** val f_call_dest : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec f_call_dest p xxx = xxx.f_call_dest (** val ext_seq_regs : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec ext_seq_regs p xxx = xxx.ext_seq_regs (** val params_regs : unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register List.list **) let rec params_regs p xxx = xxx.params_regs (** 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 **) let get_pseudo_reg_functs_inv_rect_Type4 x1 hterm h1 = let hcut = get_pseudo_reg_functs_rect_Type4 x1 h1 hterm in hcut __ (** 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 **) let get_pseudo_reg_functs_inv_rect_Type3 x1 hterm h1 = let hcut = get_pseudo_reg_functs_rect_Type3 x1 h1 hterm in hcut __ (** 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 **) let get_pseudo_reg_functs_inv_rect_Type2 x1 hterm h1 = let hcut = get_pseudo_reg_functs_rect_Type2 x1 h1 hterm in hcut __ (** 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 **) let get_pseudo_reg_functs_inv_rect_Type1 x1 hterm h1 = let hcut = get_pseudo_reg_functs_rect_Type1 x1 h1 hterm in hcut __ (** 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 **) let get_pseudo_reg_functs_inv_rect_Type0 x1 hterm h1 = let hcut = get_pseudo_reg_functs_rect_Type0 x1 h1 hterm in hcut __ (** val get_pseudo_reg_functs_jmdiscr : unserialized_params -> get_pseudo_reg_functs -> get_pseudo_reg_functs -> __ **) let get_pseudo_reg_functs_jmdiscr a1 x y = Logic.eq_rect_Type2 x (let { acc_a_regs = a0; acc_b_regs = a10; acc_a_args = a2; acc_b_args = a3; dpl_regs = a4; dph_regs = a5; dpl_args = a6; dph_args = a7; snd_args = a8; pair_move_regs = a9; f_call_args = a100; f_call_dest = a11; ext_seq_regs = a12; params_regs = a13 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y 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 **) let rec uns_params_rect_Type4 h_mk_uns_params x_16995 = let { u_pars = u_pars0; functs = functs0 } = x_16995 in h_mk_uns_params u_pars0 functs0 (** val uns_params_rect_Type5 : (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1 **) let rec uns_params_rect_Type5 h_mk_uns_params x_16997 = let { u_pars = u_pars0; functs = functs0 } = x_16997 in h_mk_uns_params u_pars0 functs0 (** val uns_params_rect_Type3 : (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1 **) let rec uns_params_rect_Type3 h_mk_uns_params x_16999 = let { u_pars = u_pars0; functs = functs0 } = x_16999 in h_mk_uns_params u_pars0 functs0 (** val uns_params_rect_Type2 : (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1 **) let rec uns_params_rect_Type2 h_mk_uns_params x_17001 = let { u_pars = u_pars0; functs = functs0 } = x_17001 in h_mk_uns_params u_pars0 functs0 (** val uns_params_rect_Type1 : (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1 **) let rec uns_params_rect_Type1 h_mk_uns_params x_17003 = let { u_pars = u_pars0; functs = functs0 } = x_17003 in h_mk_uns_params u_pars0 functs0 (** val uns_params_rect_Type0 : (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params -> 'a1 **) let rec uns_params_rect_Type0 h_mk_uns_params x_17005 = let { u_pars = u_pars0; functs = functs0 } = x_17005 in h_mk_uns_params u_pars0 functs0 (** val u_pars : uns_params -> unserialized_params **) let rec u_pars xxx = xxx.u_pars (** val functs : uns_params -> get_pseudo_reg_functs **) let rec functs xxx = xxx.functs (** val uns_params_inv_rect_Type4 : uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1) -> 'a1 **) let uns_params_inv_rect_Type4 hterm h1 = let hcut = uns_params_rect_Type4 h1 hterm in hcut __ (** val uns_params_inv_rect_Type3 : uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1) -> 'a1 **) let uns_params_inv_rect_Type3 hterm h1 = let hcut = uns_params_rect_Type3 h1 hterm in hcut __ (** val uns_params_inv_rect_Type2 : uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1) -> 'a1 **) let uns_params_inv_rect_Type2 hterm h1 = let hcut = uns_params_rect_Type2 h1 hterm in hcut __ (** val uns_params_inv_rect_Type1 : uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1) -> 'a1 **) let uns_params_inv_rect_Type1 hterm h1 = let hcut = uns_params_rect_Type1 h1 hterm in hcut __ (** val uns_params_inv_rect_Type0 : uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1) -> 'a1 **) let uns_params_inv_rect_Type0 hterm h1 = let hcut = uns_params_rect_Type0 h1 hterm in hcut __ (** val uns_params_jmdiscr : uns_params -> uns_params -> __ **) let uns_params_jmdiscr x y = Logic.eq_rect_Type2 x (let { u_pars = a0; functs = a1 } = x in Obj.magic (fun _ dH -> dH __ __)) y 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 **) let rec joint_seq_rect_Type4 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function | COMMENT x_17061 -> h_COMMENT x_17061 | MOVE x_17062 -> h_MOVE x_17062 | POP x_17063 -> h_POP x_17063 | PUSH x_17064 -> h_PUSH x_17064 | ADDRESS (i, x_17067, x_17066, x_17065) -> h_ADDRESS i __ x_17067 x_17066 x_17065 | OPACCS (x_17073, x_17072, x_17071, x_17070, x_17069) -> h_OPACCS x_17073 x_17072 x_17071 x_17070 x_17069 | OP1 (x_17076, x_17075, x_17074) -> h_OP1 x_17076 x_17075 x_17074 | OP2 (x_17080, x_17079, x_17078, x_17077) -> h_OP2 x_17080 x_17079 x_17078 x_17077 | CLEAR_CARRY -> h_CLEAR_CARRY | SET_CARRY -> h_SET_CARRY | LOAD (x_17083, x_17082, x_17081) -> h_LOAD x_17083 x_17082 x_17081 | STORE (x_17086, x_17085, x_17084) -> h_STORE x_17086 x_17085 x_17084 | Extension_seq x_17087 -> h_extension_seq x_17087 (** 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 **) let rec joint_seq_rect_Type5 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function | COMMENT x_17102 -> h_COMMENT x_17102 | MOVE x_17103 -> h_MOVE x_17103 | POP x_17104 -> h_POP x_17104 | PUSH x_17105 -> h_PUSH x_17105 | ADDRESS (i, x_17108, x_17107, x_17106) -> h_ADDRESS i __ x_17108 x_17107 x_17106 | OPACCS (x_17114, x_17113, x_17112, x_17111, x_17110) -> h_OPACCS x_17114 x_17113 x_17112 x_17111 x_17110 | OP1 (x_17117, x_17116, x_17115) -> h_OP1 x_17117 x_17116 x_17115 | OP2 (x_17121, x_17120, x_17119, x_17118) -> h_OP2 x_17121 x_17120 x_17119 x_17118 | CLEAR_CARRY -> h_CLEAR_CARRY | SET_CARRY -> h_SET_CARRY | LOAD (x_17124, x_17123, x_17122) -> h_LOAD x_17124 x_17123 x_17122 | STORE (x_17127, x_17126, x_17125) -> h_STORE x_17127 x_17126 x_17125 | Extension_seq x_17128 -> h_extension_seq x_17128 (** 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 **) let rec joint_seq_rect_Type3 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function | COMMENT x_17143 -> h_COMMENT x_17143 | MOVE x_17144 -> h_MOVE x_17144 | POP x_17145 -> h_POP x_17145 | PUSH x_17146 -> h_PUSH x_17146 | ADDRESS (i, x_17149, x_17148, x_17147) -> h_ADDRESS i __ x_17149 x_17148 x_17147 | OPACCS (x_17155, x_17154, x_17153, x_17152, x_17151) -> h_OPACCS x_17155 x_17154 x_17153 x_17152 x_17151 | OP1 (x_17158, x_17157, x_17156) -> h_OP1 x_17158 x_17157 x_17156 | OP2 (x_17162, x_17161, x_17160, x_17159) -> h_OP2 x_17162 x_17161 x_17160 x_17159 | CLEAR_CARRY -> h_CLEAR_CARRY | SET_CARRY -> h_SET_CARRY | LOAD (x_17165, x_17164, x_17163) -> h_LOAD x_17165 x_17164 x_17163 | STORE (x_17168, x_17167, x_17166) -> h_STORE x_17168 x_17167 x_17166 | Extension_seq x_17169 -> h_extension_seq x_17169 (** 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 **) let rec joint_seq_rect_Type2 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function | COMMENT x_17184 -> h_COMMENT x_17184 | MOVE x_17185 -> h_MOVE x_17185 | POP x_17186 -> h_POP x_17186 | PUSH x_17187 -> h_PUSH x_17187 | ADDRESS (i, x_17190, x_17189, x_17188) -> h_ADDRESS i __ x_17190 x_17189 x_17188 | OPACCS (x_17196, x_17195, x_17194, x_17193, x_17192) -> h_OPACCS x_17196 x_17195 x_17194 x_17193 x_17192 | OP1 (x_17199, x_17198, x_17197) -> h_OP1 x_17199 x_17198 x_17197 | OP2 (x_17203, x_17202, x_17201, x_17200) -> h_OP2 x_17203 x_17202 x_17201 x_17200 | CLEAR_CARRY -> h_CLEAR_CARRY | SET_CARRY -> h_SET_CARRY | LOAD (x_17206, x_17205, x_17204) -> h_LOAD x_17206 x_17205 x_17204 | STORE (x_17209, x_17208, x_17207) -> h_STORE x_17209 x_17208 x_17207 | Extension_seq x_17210 -> h_extension_seq x_17210 (** 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 **) let rec joint_seq_rect_Type1 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function | COMMENT x_17225 -> h_COMMENT x_17225 | MOVE x_17226 -> h_MOVE x_17226 | POP x_17227 -> h_POP x_17227 | PUSH x_17228 -> h_PUSH x_17228 | ADDRESS (i, x_17231, x_17230, x_17229) -> h_ADDRESS i __ x_17231 x_17230 x_17229 | OPACCS (x_17237, x_17236, x_17235, x_17234, x_17233) -> h_OPACCS x_17237 x_17236 x_17235 x_17234 x_17233 | OP1 (x_17240, x_17239, x_17238) -> h_OP1 x_17240 x_17239 x_17238 | OP2 (x_17244, x_17243, x_17242, x_17241) -> h_OP2 x_17244 x_17243 x_17242 x_17241 | CLEAR_CARRY -> h_CLEAR_CARRY | SET_CARRY -> h_SET_CARRY | LOAD (x_17247, x_17246, x_17245) -> h_LOAD x_17247 x_17246 x_17245 | STORE (x_17250, x_17249, x_17248) -> h_STORE x_17250 x_17249 x_17248 | Extension_seq x_17251 -> h_extension_seq x_17251 (** 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 **) let rec joint_seq_rect_Type0 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function | COMMENT x_17266 -> h_COMMENT x_17266 | MOVE x_17267 -> h_MOVE x_17267 | POP x_17268 -> h_POP x_17268 | PUSH x_17269 -> h_PUSH x_17269 | ADDRESS (i, x_17272, x_17271, x_17270) -> h_ADDRESS i __ x_17272 x_17271 x_17270 | OPACCS (x_17278, x_17277, x_17276, x_17275, x_17274) -> h_OPACCS x_17278 x_17277 x_17276 x_17275 x_17274 | OP1 (x_17281, x_17280, x_17279) -> h_OP1 x_17281 x_17280 x_17279 | OP2 (x_17285, x_17284, x_17283, x_17282) -> h_OP2 x_17285 x_17284 x_17283 x_17282 | CLEAR_CARRY -> h_CLEAR_CARRY | SET_CARRY -> h_SET_CARRY | LOAD (x_17288, x_17287, x_17286) -> h_LOAD x_17288 x_17287 x_17286 | STORE (x_17291, x_17290, x_17289) -> h_STORE x_17291 x_17290 x_17289 | Extension_seq x_17292 -> h_extension_seq x_17292 (** 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 **) let joint_seq_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 = let hcut = joint_seq_rect_Type4 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm in hcut __ (** 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 **) let joint_seq_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 = let hcut = joint_seq_rect_Type3 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm in hcut __ (** 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 **) let joint_seq_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 = let hcut = joint_seq_rect_Type2 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm in hcut __ (** 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 **) let joint_seq_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 = let hcut = joint_seq_rect_Type1 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm in hcut __ (** 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 **) let joint_seq_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 = let hcut = joint_seq_rect_Type0 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm in hcut __ (** val joint_seq_discr : unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __ **) let joint_seq_discr a1 a2 x y = Logic.eq_rect_Type2 x (match x with | COMMENT a0 -> Obj.magic (fun _ dH -> dH __) | MOVE a0 -> Obj.magic (fun _ dH -> dH __) | POP a0 -> Obj.magic (fun _ dH -> dH __) | PUSH a0 -> Obj.magic (fun _ dH -> dH __) | ADDRESS (a0, a20, a3, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __) | OPACCS (a0, a10, a20, a3, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __) | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __) | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __) | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH) | SET_CARRY -> Obj.magic (fun _ dH -> dH) | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __) | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __) | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y (** val joint_seq_jmdiscr : unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __ **) let joint_seq_jmdiscr a1 a2 x y = Logic.eq_rect_Type2 x (match x with | COMMENT a0 -> Obj.magic (fun _ dH -> dH __) | MOVE a0 -> Obj.magic (fun _ dH -> dH __) | POP a0 -> Obj.magic (fun _ dH -> dH __) | PUSH a0 -> Obj.magic (fun _ dH -> dH __) | ADDRESS (a0, a20, a3, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __) | OPACCS (a0, a10, a20, a3, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __) | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __) | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __) | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH) | SET_CARRY -> Obj.magic (fun _ dH -> dH) | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __) | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __) | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y (** val get_used_registers_from_seq : unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs -> joint_seq -> Registers.register List.list **) let get_used_registers_from_seq p globals functs0 = function | COMMENT x -> List.Nil | MOVE pm -> functs0.pair_move_regs pm | POP r -> functs0.acc_a_regs r | PUSH r -> functs0.acc_a_args r | ADDRESS (x, x1, r1, r2) -> List.append (functs0.dpl_regs r1) (functs0.dph_regs r2) | OPACCS (o, r1, r2, r3, r4) -> List.append (functs0.acc_a_regs r1) (List.append (functs0.acc_b_regs r2) (List.append (functs0.acc_a_args r3) (functs0.acc_b_args r4))) | OP1 (o, r1, r2) -> List.append (functs0.acc_a_regs r1) (functs0.acc_a_regs r2) | OP2 (o, r1, r2, r3) -> List.append (functs0.acc_a_regs r1) (List.append (functs0.acc_a_args r2) (functs0.snd_args r3)) | CLEAR_CARRY -> List.Nil | SET_CARRY -> List.Nil | LOAD (r1, r2, r3) -> List.append (functs0.acc_a_regs r1) (List.append (functs0.dpl_args r2) (functs0.dph_args r3)) | STORE (r1, r2, r3) -> List.append (functs0.dpl_args r1) (List.append (functs0.dph_args r2) (functs0.acc_a_args r3)) | Extension_seq ext -> functs0.ext_seq_regs ext (** val nOOP : unserialized_params -> AST.ident List.list -> joint_seq **) let nOOP p globals = COMMENT String.EmptyString (** val dpi1__o__extension_seq_to_seq__o__inject : unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair -> joint_seq Types.sig0 **) let dpi1__o__extension_seq_to_seq__o__inject x0 x1 x4 = Extension_seq x4.Types.dpi1 (** val eject__o__extension_seq_to_seq__o__inject : unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq Types.sig0 **) let eject__o__extension_seq_to_seq__o__inject x0 x1 x4 = Extension_seq (Types.pi1 x4) (** val extension_seq_to_seq__o__inject : unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0 **) let extension_seq_to_seq__o__inject x0 x1 x3 = Extension_seq x3 (** val dpi1__o__extension_seq_to_seq : unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair -> joint_seq **) let dpi1__o__extension_seq_to_seq x0 x1 x3 = Extension_seq x3.Types.dpi1 (** val eject__o__extension_seq_to_seq : unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq **) let eject__o__extension_seq_to_seq x0 x1 x3 = Extension_seq (Types.pi1 x3) 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 **) let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function | COST_LABEL x_17565 -> h_COST_LABEL x_17565 | CALL (x_17568, x_17567, x_17566) -> h_CALL x_17568 x_17567 x_17566 | COND (x_17570, x_17569) -> h_COND x_17570 x_17569 | Step_seq x_17571 -> h_step_seq x_17571 (** 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 **) let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function | COST_LABEL x_17577 -> h_COST_LABEL x_17577 | CALL (x_17580, x_17579, x_17578) -> h_CALL x_17580 x_17579 x_17578 | COND (x_17582, x_17581) -> h_COND x_17582 x_17581 | Step_seq x_17583 -> h_step_seq x_17583 (** 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 **) let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function | COST_LABEL x_17589 -> h_COST_LABEL x_17589 | CALL (x_17592, x_17591, x_17590) -> h_CALL x_17592 x_17591 x_17590 | COND (x_17594, x_17593) -> h_COND x_17594 x_17593 | Step_seq x_17595 -> h_step_seq x_17595 (** 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 **) let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function | COST_LABEL x_17601 -> h_COST_LABEL x_17601 | CALL (x_17604, x_17603, x_17602) -> h_CALL x_17604 x_17603 x_17602 | COND (x_17606, x_17605) -> h_COND x_17606 x_17605 | Step_seq x_17607 -> h_step_seq x_17607 (** 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 **) let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function | COST_LABEL x_17613 -> h_COST_LABEL x_17613 | CALL (x_17616, x_17615, x_17614) -> h_CALL x_17616 x_17615 x_17614 | COND (x_17618, x_17617) -> h_COND x_17618 x_17617 | Step_seq x_17619 -> h_step_seq x_17619 (** 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 **) let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function | COST_LABEL x_17625 -> h_COST_LABEL x_17625 | CALL (x_17628, x_17627, x_17626) -> h_CALL x_17628 x_17627 x_17626 | COND (x_17630, x_17629) -> h_COND x_17630 x_17629 | Step_seq x_17631 -> h_step_seq x_17631 (** 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 **) let joint_step_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 = let hcut = joint_step_rect_Type4 x1 x2 h1 h2 h3 h4 hterm in hcut __ (** 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 **) let joint_step_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 = let hcut = joint_step_rect_Type3 x1 x2 h1 h2 h3 h4 hterm in hcut __ (** 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 **) let joint_step_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 = let hcut = joint_step_rect_Type2 x1 x2 h1 h2 h3 h4 hterm in hcut __ (** 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 **) let joint_step_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 = let hcut = joint_step_rect_Type1 x1 x2 h1 h2 h3 h4 hterm in hcut __ (** 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 **) let joint_step_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 = let hcut = joint_step_rect_Type0 x1 x2 h1 h2 h3 h4 hterm in hcut __ (** val joint_step_discr : unserialized_params -> AST.ident List.list -> joint_step -> joint_step -> __ **) let joint_step_discr a1 a2 x y = Logic.eq_rect_Type2 x (match x with | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __) | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __) | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y (** val joint_step_jmdiscr : unserialized_params -> AST.ident List.list -> joint_step -> joint_step -> __ **) let joint_step_jmdiscr a1 a2 x y = Logic.eq_rect_Type2 x (match x with | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __) | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __) | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y (** val get_used_registers_from_step : unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs -> joint_step -> Registers.register List.list **) let get_used_registers_from_step p globals functs0 = function | COST_LABEL c -> List.Nil | CALL (id, args, dest) -> let r_id = match id with | Types.Inl x -> List.Nil | Types.Inr ptr -> List.append (functs0.dpl_args ptr.Types.fst) (functs0.dph_args ptr.Types.snd) in List.append r_id (List.append (functs0.f_call_args args) (functs0.f_call_dest dest)) | COND (r, lbl) -> functs0.acc_a_regs r | Step_seq s -> get_used_registers_from_seq p globals functs0 s (** 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 **) let dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 = Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x4) (** 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 **) let eject__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 = Step_seq (eject__o__extension_seq_to_seq x0 x1 x4) (** val extension_seq_to_seq__o__seq_to_step__o__inject : unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0 **) let extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x2 = Step_seq (Extension_seq x2) (** val dpi1__o__seq_to_step__o__inject : unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair -> joint_step Types.sig0 **) let dpi1__o__seq_to_step__o__inject x0 x1 x4 = Step_seq x4.Types.dpi1 (** val eject__o__seq_to_step__o__inject : unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 -> joint_step Types.sig0 **) let eject__o__seq_to_step__o__inject x0 x1 x4 = Step_seq (Types.pi1 x4) (** val seq_to_step__o__inject : unserialized_params -> AST.ident List.list -> joint_seq -> joint_step Types.sig0 **) let seq_to_step__o__inject x0 x1 x3 = Step_seq x3 (** val dpi1__o__extension_seq_to_seq__o__seq_to_step : unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair -> joint_step **) let dpi1__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 = Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x3) (** val eject__o__extension_seq_to_seq__o__seq_to_step : unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step **) let eject__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 = Step_seq (eject__o__extension_seq_to_seq x0 x1 x3) (** val extension_seq_to_seq__o__seq_to_step : unserialized_params -> AST.ident List.list -> __ -> joint_step **) let extension_seq_to_seq__o__seq_to_step x0 x1 x2 = Step_seq (Extension_seq x2) (** val dpi1__o__seq_to_step : unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair -> joint_step **) let dpi1__o__seq_to_step x0 x1 x3 = Step_seq x3.Types.dpi1 (** val eject__o__seq_to_step : unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 -> joint_step **) let eject__o__seq_to_step x0 x1 x3 = Step_seq (Types.pi1 x3) (** val step_labels : unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label List.list **) let step_labels p globals = function | COST_LABEL x -> List.Nil | CALL (x, x0, x1) -> List.Nil | COND (x, l) -> List.Cons (l, List.Nil) | Step_seq s0 -> (match s0 with | COMMENT x -> List.Nil | MOVE x -> List.Nil | POP x -> List.Nil | PUSH x -> List.Nil | ADDRESS (x, x1, x2, x3) -> List.Nil | OPACCS (x, x0, x1, x2, x3) -> List.Nil | OP1 (x, x0, x1) -> List.Nil | OP2 (x, x0, x1, x2) -> List.Nil | CLEAR_CARRY -> List.Nil | SET_CARRY -> List.Nil | LOAD (x, x0, x1) -> List.Nil | STORE (x, x0, x1) -> List.Nil | Extension_seq ext -> p.ext_seq_labels ext) 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 **) let rec stmt_params_rect_Type4 h_mk_stmt_params x_17710 = let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = has_fcond0 } = x_17710 in h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 (** val stmt_params_rect_Type5 : (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1) -> stmt_params -> 'a1 **) let rec stmt_params_rect_Type5 h_mk_stmt_params x_17712 = let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = has_fcond0 } = x_17712 in h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 (** val stmt_params_rect_Type3 : (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1) -> stmt_params -> 'a1 **) let rec stmt_params_rect_Type3 h_mk_stmt_params x_17714 = let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = has_fcond0 } = x_17714 in h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 (** val stmt_params_rect_Type2 : (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1) -> stmt_params -> 'a1 **) let rec stmt_params_rect_Type2 h_mk_stmt_params x_17716 = let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = has_fcond0 } = x_17716 in h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 (** val stmt_params_rect_Type1 : (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1) -> stmt_params -> 'a1 **) let rec stmt_params_rect_Type1 h_mk_stmt_params x_17718 = let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = has_fcond0 } = x_17718 in h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 (** val stmt_params_rect_Type0 : (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> 'a1) -> stmt_params -> 'a1 **) let rec stmt_params_rect_Type0 h_mk_stmt_params x_17720 = let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond = has_fcond0 } = x_17720 in h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0 (** val uns_pars : stmt_params -> uns_params **) let rec uns_pars xxx = xxx.uns_pars type succ = __ (** val succ_label : stmt_params -> __ -> Graphs.label Types.option **) let rec succ_label xxx = xxx.succ_label (** val has_fcond : stmt_params -> Bool.bool **) let rec has_fcond xxx = xxx.has_fcond (** val stmt_params_inv_rect_Type4 : stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **) let stmt_params_inv_rect_Type4 hterm h1 = let hcut = stmt_params_rect_Type4 h1 hterm in hcut __ (** val stmt_params_inv_rect_Type3 : stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **) let stmt_params_inv_rect_Type3 hterm h1 = let hcut = stmt_params_rect_Type3 h1 hterm in hcut __ (** val stmt_params_inv_rect_Type2 : stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **) let stmt_params_inv_rect_Type2 hterm h1 = let hcut = stmt_params_rect_Type2 h1 hterm in hcut __ (** val stmt_params_inv_rect_Type1 : stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **) let stmt_params_inv_rect_Type1 hterm h1 = let hcut = stmt_params_rect_Type1 h1 hterm in hcut __ (** val stmt_params_inv_rect_Type0 : stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **) let stmt_params_inv_rect_Type0 hterm h1 = let hcut = stmt_params_rect_Type0 h1 hterm in hcut __ (** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **) let stmt_params_jmdiscr x y = Logic.eq_rect_Type2 x (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val uns_pars__o__u_pars : stmt_params -> unserialized_params **) let uns_pars__o__u_pars x0 = x0.uns_pars.u_pars 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 **) let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function | GOTO x_17744 -> h_GOTO x_17744 | RETURN -> h_RETURN | TAILCALL (x_17746, x_17745) -> h_TAILCALL __ x_17746 x_17745 (** val joint_fin_step_rect_Type5 : unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **) let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function | GOTO x_17752 -> h_GOTO x_17752 | RETURN -> h_RETURN | TAILCALL (x_17754, x_17753) -> h_TAILCALL __ x_17754 x_17753 (** val joint_fin_step_rect_Type3 : unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **) let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function | GOTO x_17760 -> h_GOTO x_17760 | RETURN -> h_RETURN | TAILCALL (x_17762, x_17761) -> h_TAILCALL __ x_17762 x_17761 (** val joint_fin_step_rect_Type2 : unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **) let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function | GOTO x_17768 -> h_GOTO x_17768 | RETURN -> h_RETURN | TAILCALL (x_17770, x_17769) -> h_TAILCALL __ x_17770 x_17769 (** val joint_fin_step_rect_Type1 : unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **) let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function | GOTO x_17776 -> h_GOTO x_17776 | RETURN -> h_RETURN | TAILCALL (x_17778, x_17777) -> h_TAILCALL __ x_17778 x_17777 (** val joint_fin_step_rect_Type0 : unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **) let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function | GOTO x_17784 -> h_GOTO x_17784 | RETURN -> h_RETURN | TAILCALL (x_17786, x_17785) -> h_TAILCALL __ x_17786 x_17785 (** val joint_fin_step_inv_rect_Type4 : unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> 'a1 **) let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 = let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __ (** val joint_fin_step_inv_rect_Type3 : unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> 'a1 **) let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 = let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __ (** val joint_fin_step_inv_rect_Type2 : unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> 'a1 **) let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 = let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __ (** val joint_fin_step_inv_rect_Type1 : unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> 'a1 **) let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 = let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __ (** val joint_fin_step_inv_rect_Type0 : unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> 'a1 **) let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 = let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __ (** val joint_fin_step_discr : unserialized_params -> joint_fin_step -> joint_fin_step -> __ **) let joint_fin_step_discr a1 x y = Logic.eq_rect_Type2 x (match x with | GOTO a0 -> Obj.magic (fun _ dH -> dH __) | RETURN -> Obj.magic (fun _ dH -> dH) | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y (** val joint_fin_step_jmdiscr : unserialized_params -> joint_fin_step -> joint_fin_step -> __ **) let joint_fin_step_jmdiscr a1 x y = Logic.eq_rect_Type2 x (match x with | GOTO a0 -> Obj.magic (fun _ dH -> dH __) | RETURN -> Obj.magic (fun _ dH -> dH) | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y (** val fin_step_labels : unserialized_params -> joint_fin_step -> Graphs.label List.list **) let fin_step_labels p = function | GOTO l -> List.Cons (l, List.Nil) | RETURN -> List.Nil | TAILCALL (x0, x1) -> List.Nil 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 **) let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function | Sequential (x_17852, x_17851) -> h_sequential x_17852 x_17851 | Final x_17853 -> h_final x_17853 | FCOND (x_17856, x_17855, x_17854) -> h_FCOND __ x_17856 x_17855 x_17854 (** 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 **) let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function | Sequential (x_17863, x_17862) -> h_sequential x_17863 x_17862 | Final x_17864 -> h_final x_17864 | FCOND (x_17867, x_17866, x_17865) -> h_FCOND __ x_17867 x_17866 x_17865 (** 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 **) let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function | Sequential (x_17874, x_17873) -> h_sequential x_17874 x_17873 | Final x_17875 -> h_final x_17875 | FCOND (x_17878, x_17877, x_17876) -> h_FCOND __ x_17878 x_17877 x_17876 (** 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 **) let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function | Sequential (x_17885, x_17884) -> h_sequential x_17885 x_17884 | Final x_17886 -> h_final x_17886 | FCOND (x_17889, x_17888, x_17887) -> h_FCOND __ x_17889 x_17888 x_17887 (** 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 **) let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function | Sequential (x_17896, x_17895) -> h_sequential x_17896 x_17895 | Final x_17897 -> h_final x_17897 | FCOND (x_17900, x_17899, x_17898) -> h_FCOND __ x_17900 x_17899 x_17898 (** 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 **) let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function | Sequential (x_17907, x_17906) -> h_sequential x_17907 x_17906 | Final x_17908 -> h_final x_17908 | FCOND (x_17911, x_17910, x_17909) -> h_FCOND __ x_17911 x_17910 x_17909 (** 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 **) let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 = let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __ (** 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 **) let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 = let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __ (** 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 **) let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 = let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __ (** 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 **) let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 = let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __ (** 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 **) let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 = let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __ (** val joint_statement_discr : stmt_params -> AST.ident List.list -> joint_statement -> joint_statement -> __ **) let joint_statement_discr a1 a2 x y = Logic.eq_rect_Type2 x (match x with | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) | Final a0 -> Obj.magic (fun _ dH -> dH __) | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val joint_statement_jmdiscr : stmt_params -> AST.ident List.list -> joint_statement -> joint_statement -> __ **) let joint_statement_jmdiscr a1 a2 x y = Logic.eq_rect_Type2 x (match x with | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) | Final a0 -> Obj.magic (fun _ dH -> dH __) | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y (** 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 **) let dpi1__o__fin_step_to_stmt__o__inject x0 x1 x4 = Final x4.Types.dpi1 (** val eject__o__fin_step_to_stmt__o__inject : stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 -> joint_statement Types.sig0 **) let eject__o__fin_step_to_stmt__o__inject x0 x1 x4 = Final (Types.pi1 x4) (** val fin_step_to_stmt__o__inject : stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement Types.sig0 **) let fin_step_to_stmt__o__inject x0 x1 x3 = Final x3 (** val dpi1__o__fin_step_to_stmt : stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair -> joint_statement **) let dpi1__o__fin_step_to_stmt x0 x1 x3 = Final x3.Types.dpi1 (** val eject__o__fin_step_to_stmt : stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 -> joint_statement **) let eject__o__fin_step_to_stmt x0 x1 x3 = Final (Types.pi1 x3) 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 **) let rec params_rect_Type4 h_mk_params x_17984 = let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = point_of_label0; point_of_succ = point_of_succ0 } = x_17984 in h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 (** 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 **) let rec params_rect_Type5 h_mk_params x_17986 = let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = point_of_label0; point_of_succ = point_of_succ0 } = x_17986 in h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 (** 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 **) let rec params_rect_Type3 h_mk_params x_17988 = let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = point_of_label0; point_of_succ = point_of_succ0 } = x_17988 in h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 (** 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 **) let rec params_rect_Type2 h_mk_params x_17990 = let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = point_of_label0; point_of_succ = point_of_succ0 } = x_17990 in h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 (** 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 **) let rec params_rect_Type1 h_mk_params x_17992 = let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = point_of_label0; point_of_succ = point_of_succ0 } = x_17992 in h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 (** 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 **) let rec params_rect_Type0 h_mk_params x_17994 = let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label = point_of_label0; point_of_succ = point_of_succ0 } = x_17994 in h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0 (** val stmt_pars : params -> stmt_params **) let rec stmt_pars xxx = xxx.stmt_pars type codeT = __ type code_point = __ (** val stmt_at : params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **) let rec stmt_at xxx = xxx.stmt_at (** val point_of_label : params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **) let rec point_of_label xxx = xxx.point_of_label (** val point_of_succ : params -> __ -> __ -> __ **) let rec point_of_succ xxx = xxx.point_of_succ (** 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 **) let params_inv_rect_Type4 hterm h1 = let hcut = params_rect_Type4 h1 hterm in hcut __ (** 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 **) let params_inv_rect_Type3 hterm h1 = let hcut = params_rect_Type3 h1 hterm in hcut __ (** 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 **) let params_inv_rect_Type2 hterm h1 = let hcut = params_rect_Type2 h1 hterm in hcut __ (** 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 **) let params_inv_rect_Type1 hterm h1 = let hcut = params_rect_Type1 h1 hterm in hcut __ (** 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 **) let params_inv_rect_Type0 hterm h1 = let hcut = params_rect_Type0 h1 hterm in hcut __ (** val params_jmdiscr : params -> params -> __ **) let params_jmdiscr x y = Logic.eq_rect_Type2 x (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ = a5 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y (** val stmt_pars__o__uns_pars : params -> uns_params **) let stmt_pars__o__uns_pars x0 = x0.stmt_pars.uns_pars (** val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params **) let stmt_pars__o__uns_pars__o__u_pars x0 = uns_pars__o__u_pars x0.stmt_pars (** val code_has_point : params -> AST.ident List.list -> __ -> __ -> Bool.bool **) let code_has_point p globals c pt = match p.stmt_at globals c pt with | Types.None -> Bool.False | Types.Some x -> Bool.True (** val code_has_label : params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **) let code_has_label p globals c l = match p.point_of_label globals c l with | Types.None -> Bool.False | Types.Some pt -> code_has_point p globals c pt (** val stmt_explicit_labels : stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label List.list **) let stmt_explicit_labels p globals = function | Sequential (c, x) -> step_labels (uns_pars__o__u_pars p) globals c | Final c -> fin_step_labels (uns_pars__o__u_pars p) c | FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil))) (** val stmt_implicit_label : stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label Types.option **) let stmt_implicit_label p globals = function | Sequential (x, s0) -> p.succ_label s0 | Final x -> Types.None | FCOND (x0, x1, x2) -> Types.None (** val stmt_labels : stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label List.list **) let stmt_labels p g stmt = List.append (match stmt_implicit_label p g stmt with | Types.None -> List.Nil | Types.Some l -> List.Cons (l, List.Nil)) (stmt_explicit_labels p g stmt) (** val stmt_registers : stmt_params -> AST.ident List.list -> joint_statement -> Registers.register List.list **) let stmt_registers p globals = function | Sequential (c, x) -> get_used_registers_from_step p.uns_pars.u_pars globals p.uns_pars.functs c | Final c -> (match c with | GOTO x -> List.Nil | RETURN -> List.Nil | TAILCALL (x0, r) -> p.uns_pars.functs.f_call_args r) | FCOND (r, x0, x1) -> p.uns_pars.functs.acc_a_regs r type lin_params = uns_params (* singleton inductive, whose constructor was mk_lin_params *) (** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **) let rec lin_params_rect_Type4 h_mk_lin_params x_18017 = let l_u_pars = x_18017 in h_mk_lin_params l_u_pars (** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **) let rec lin_params_rect_Type5 h_mk_lin_params x_18019 = let l_u_pars = x_18019 in h_mk_lin_params l_u_pars (** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **) let rec lin_params_rect_Type3 h_mk_lin_params x_18021 = let l_u_pars = x_18021 in h_mk_lin_params l_u_pars (** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **) let rec lin_params_rect_Type2 h_mk_lin_params x_18023 = let l_u_pars = x_18023 in h_mk_lin_params l_u_pars (** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **) let rec lin_params_rect_Type1 h_mk_lin_params x_18025 = let l_u_pars = x_18025 in h_mk_lin_params l_u_pars (** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **) let rec lin_params_rect_Type0 h_mk_lin_params x_18027 = let l_u_pars = x_18027 in h_mk_lin_params l_u_pars (** val l_u_pars : lin_params -> uns_params **) let rec l_u_pars xxx = let yyy = xxx in yyy (** val lin_params_inv_rect_Type4 : lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **) let lin_params_inv_rect_Type4 hterm h1 = let hcut = lin_params_rect_Type4 h1 hterm in hcut __ (** val lin_params_inv_rect_Type3 : lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **) let lin_params_inv_rect_Type3 hterm h1 = let hcut = lin_params_rect_Type3 h1 hterm in hcut __ (** val lin_params_inv_rect_Type2 : lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **) let lin_params_inv_rect_Type2 hterm h1 = let hcut = lin_params_rect_Type2 h1 hterm in hcut __ (** val lin_params_inv_rect_Type1 : lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **) let lin_params_inv_rect_Type1 hterm h1 = let hcut = lin_params_rect_Type1 h1 hterm in hcut __ (** val lin_params_inv_rect_Type0 : lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **) let lin_params_inv_rect_Type0 hterm h1 = let hcut = lin_params_rect_Type0 h1 hterm in hcut __ (** val lin_params_jmdiscr : lin_params -> lin_params -> __ **) let lin_params_jmdiscr x y = Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y (** val lin_params_to_params : lin_params -> params **) let lin_params_to_params lp = { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x -> Types.None); has_fcond = Bool.True }; stmt_at = (fun globals code point -> Obj.magic (Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code))) (fun ls -> Monad.m_return0 (Monad.max_def Option.option) ls.Types.snd))); point_of_label = (fun globals c lbl -> Util.if_then_else_safe (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl (Obj.magic c)) (fun _ -> Obj.magic (Monad.m_return0 (Monad.max_def Option.option) (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ = (fun current x -> Obj.magic (Nat.S (Obj.magic current))) } (** val lp_to_p__o__stmt_pars : lin_params -> stmt_params **) let lp_to_p__o__stmt_pars x0 = (lin_params_to_params x0).stmt_pars (** val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params **) let lp_to_p__o__stmt_pars__o__uns_pars x0 = stmt_pars__o__uns_pars (lin_params_to_params x0) (** val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars : lin_params -> unserialized_params **) let lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 = stmt_pars__o__uns_pars__o__u_pars (lin_params_to_params x0) type graph_params = uns_params (* singleton inductive, whose constructor was mk_graph_params *) (** val graph_params_rect_Type4 : (uns_params -> 'a1) -> graph_params -> 'a1 **) let rec graph_params_rect_Type4 h_mk_graph_params x_18043 = let g_u_pars = x_18043 in h_mk_graph_params g_u_pars (** val graph_params_rect_Type5 : (uns_params -> 'a1) -> graph_params -> 'a1 **) let rec graph_params_rect_Type5 h_mk_graph_params x_18045 = let g_u_pars = x_18045 in h_mk_graph_params g_u_pars (** val graph_params_rect_Type3 : (uns_params -> 'a1) -> graph_params -> 'a1 **) let rec graph_params_rect_Type3 h_mk_graph_params x_18047 = let g_u_pars = x_18047 in h_mk_graph_params g_u_pars (** val graph_params_rect_Type2 : (uns_params -> 'a1) -> graph_params -> 'a1 **) let rec graph_params_rect_Type2 h_mk_graph_params x_18049 = let g_u_pars = x_18049 in h_mk_graph_params g_u_pars (** val graph_params_rect_Type1 : (uns_params -> 'a1) -> graph_params -> 'a1 **) let rec graph_params_rect_Type1 h_mk_graph_params x_18051 = let g_u_pars = x_18051 in h_mk_graph_params g_u_pars (** val graph_params_rect_Type0 : (uns_params -> 'a1) -> graph_params -> 'a1 **) let rec graph_params_rect_Type0 h_mk_graph_params x_18053 = let g_u_pars = x_18053 in h_mk_graph_params g_u_pars (** val g_u_pars : graph_params -> uns_params **) let rec g_u_pars xxx = let yyy = xxx in yyy (** val graph_params_inv_rect_Type4 : graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **) let graph_params_inv_rect_Type4 hterm h1 = let hcut = graph_params_rect_Type4 h1 hterm in hcut __ (** val graph_params_inv_rect_Type3 : graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **) let graph_params_inv_rect_Type3 hterm h1 = let hcut = graph_params_rect_Type3 h1 hterm in hcut __ (** val graph_params_inv_rect_Type2 : graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **) let graph_params_inv_rect_Type2 hterm h1 = let hcut = graph_params_rect_Type2 h1 hterm in hcut __ (** val graph_params_inv_rect_Type1 : graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **) let graph_params_inv_rect_Type1 hterm h1 = let hcut = graph_params_rect_Type1 h1 hterm in hcut __ (** val graph_params_inv_rect_Type0 : graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **) let graph_params_inv_rect_Type0 hterm h1 = let hcut = graph_params_rect_Type0 h1 hterm in hcut __ (** val graph_params_jmdiscr : graph_params -> graph_params -> __ **) let graph_params_jmdiscr x y = Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y (** val graph_params_to_params : graph_params -> params **) let graph_params_to_params gp = { stmt_pars = { uns_pars = (g_u_pars gp); succ_label = (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at = (fun globals code -> Obj.magic (Identifiers.lookup PreIdentifiers.LabelTag (Obj.magic code))); point_of_label = (fun x x0 lbl -> Obj.magic (Monad.m_return0 (Monad.max_def Option.option) lbl)); point_of_succ = (fun x lbl -> lbl) } (** val gp_to_p__o__stmt_pars : graph_params -> stmt_params **) let gp_to_p__o__stmt_pars x0 = (graph_params_to_params x0).stmt_pars (** val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params **) let gp_to_p__o__stmt_pars__o__uns_pars x0 = stmt_pars__o__uns_pars (graph_params_to_params x0) (** val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars : graph_params -> unserialized_params **) let gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 = stmt_pars__o__uns_pars__o__u_pars (graph_params_to_params x0) 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 **) let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_18069 = let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = joint_if_runiverse0; joint_if_result = joint_if_result0; joint_if_params = joint_if_params0; joint_if_stacksize = joint_if_stacksize0; joint_if_local_stacksize = joint_if_local_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = joint_if_entry0 } = x_18069 in h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0 (** val joint_internal_function_rect_Type5 : params -> AST.ident List.list -> (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> joint_internal_function -> 'a1 **) let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_18071 = let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = joint_if_runiverse0; joint_if_result = joint_if_result0; joint_if_params = joint_if_params0; joint_if_stacksize = joint_if_stacksize0; joint_if_local_stacksize = joint_if_local_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = joint_if_entry0 } = x_18071 in h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0 (** val joint_internal_function_rect_Type3 : params -> AST.ident List.list -> (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> joint_internal_function -> 'a1 **) let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_18073 = let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = joint_if_runiverse0; joint_if_result = joint_if_result0; joint_if_params = joint_if_params0; joint_if_stacksize = joint_if_stacksize0; joint_if_local_stacksize = joint_if_local_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = joint_if_entry0 } = x_18073 in h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0 (** val joint_internal_function_rect_Type2 : params -> AST.ident List.list -> (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> joint_internal_function -> 'a1 **) let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_18075 = let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = joint_if_runiverse0; joint_if_result = joint_if_result0; joint_if_params = joint_if_params0; joint_if_stacksize = joint_if_stacksize0; joint_if_local_stacksize = joint_if_local_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = joint_if_entry0 } = x_18075 in h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0 (** val joint_internal_function_rect_Type1 : params -> AST.ident List.list -> (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> joint_internal_function -> 'a1 **) let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_18077 = let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = joint_if_runiverse0; joint_if_result = joint_if_result0; joint_if_params = joint_if_params0; joint_if_stacksize = joint_if_stacksize0; joint_if_local_stacksize = joint_if_local_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = joint_if_entry0 } = x_18077 in h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0 (** val joint_internal_function_rect_Type0 : params -> AST.ident List.list -> (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ -> 'a1) -> joint_internal_function -> 'a1 **) let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_18079 = let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse = joint_if_runiverse0; joint_if_result = joint_if_result0; joint_if_params = joint_if_params0; joint_if_stacksize = joint_if_stacksize0; joint_if_local_stacksize = joint_if_local_stacksize0; joint_if_code = joint_if_code0; joint_if_entry = joint_if_entry0 } = x_18079 in h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0 joint_if_result0 joint_if_params0 joint_if_stacksize0 joint_if_local_stacksize0 joint_if_code0 joint_if_entry0 (** val joint_if_luniverse : params -> AST.ident List.list -> joint_internal_function -> Identifiers.universe **) let rec joint_if_luniverse p globals xxx = xxx.joint_if_luniverse (** val joint_if_runiverse : params -> AST.ident List.list -> joint_internal_function -> Identifiers.universe **) let rec joint_if_runiverse p globals xxx = xxx.joint_if_runiverse (** val joint_if_result : params -> AST.ident List.list -> joint_internal_function -> __ **) let rec joint_if_result p globals xxx = xxx.joint_if_result (** val joint_if_params : params -> AST.ident List.list -> joint_internal_function -> __ **) let rec joint_if_params p globals xxx = xxx.joint_if_params (** val joint_if_stacksize : params -> AST.ident List.list -> joint_internal_function -> Nat.nat **) let rec joint_if_stacksize p globals xxx = xxx.joint_if_stacksize (** val joint_if_local_stacksize : params -> AST.ident List.list -> joint_internal_function -> Nat.nat **) let rec joint_if_local_stacksize p globals xxx = xxx.joint_if_local_stacksize (** val joint_if_code : params -> AST.ident List.list -> joint_internal_function -> __ **) let rec joint_if_code p globals xxx = xxx.joint_if_code (** val joint_if_entry : params -> AST.ident List.list -> joint_internal_function -> __ **) let rec joint_if_entry p globals xxx = xxx.joint_if_entry (** 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 **) let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 = let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __ (** 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 **) let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 = let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __ (** 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 **) let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 = let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __ (** 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 **) let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 = let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __ (** 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 **) let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 = let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __ (** val joint_internal_function_jmdiscr : params -> AST.ident List.list -> joint_internal_function -> joint_internal_function -> __ **) let joint_internal_function_jmdiscr a1 a2 x y = Logic.eq_rect_Type2 x (let { joint_if_luniverse = a0; joint_if_runiverse = a10; joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4; joint_if_local_stacksize = a5; joint_if_code = a6; joint_if_entry = a7 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y (** val good_if_rect_Type4 : params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let rec good_if_rect_Type4 p globals def h_mk_good_if = h_mk_good_if __ __ __ __ __ (** val good_if_rect_Type5 : params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let rec good_if_rect_Type5 p globals def h_mk_good_if = h_mk_good_if __ __ __ __ __ (** val good_if_rect_Type3 : params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let rec good_if_rect_Type3 p globals def h_mk_good_if = h_mk_good_if __ __ __ __ __ (** val good_if_rect_Type2 : params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let rec good_if_rect_Type2 p globals def h_mk_good_if = h_mk_good_if __ __ __ __ __ (** val good_if_rect_Type1 : params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let rec good_if_rect_Type1 p globals def h_mk_good_if = h_mk_good_if __ __ __ __ __ (** val good_if_rect_Type0 : params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let rec good_if_rect_Type0 p globals def h_mk_good_if = h_mk_good_if __ __ __ __ __ (** val good_if_inv_rect_Type4 : params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let good_if_inv_rect_Type4 x1 x2 x3 h1 = let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __ (** val good_if_inv_rect_Type3 : params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let good_if_inv_rect_Type3 x1 x2 x3 h1 = let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __ (** val good_if_inv_rect_Type2 : params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let good_if_inv_rect_Type2 x1 x2 x3 h1 = let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __ (** val good_if_inv_rect_Type1 : params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let good_if_inv_rect_Type1 x1 x2 x3 h1 = let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __ (** val good_if_inv_rect_Type0 : params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) let good_if_inv_rect_Type0 x1 x2 x3 h1 = let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __ (** val good_if_discr : params -> AST.ident List.list -> joint_internal_function -> __ **) let good_if_discr a1 a2 a3 = Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __ (** val good_if_jmdiscr : params -> AST.ident List.list -> joint_internal_function -> __ **) let good_if_jmdiscr a1 a2 a3 = Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __ 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 **) let set_joint_code globals pars int_fun graph entry = { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse = int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result; joint_if_params = int_fun.joint_if_params; joint_if_stacksize = int_fun.joint_if_stacksize; joint_if_local_stacksize = int_fun.joint_if_local_stacksize; joint_if_code = graph; joint_if_entry = entry } (** val set_luniverse : params -> AST.ident List.list -> joint_internal_function -> Identifiers.universe -> joint_internal_function **) let set_luniverse globals pars p luniverse = { joint_if_luniverse = luniverse; joint_if_runiverse = p.joint_if_runiverse; joint_if_result = p.joint_if_result; joint_if_params = p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize; joint_if_local_stacksize = p.joint_if_local_stacksize; joint_if_code = p.joint_if_code; joint_if_entry = p.joint_if_entry } (** val set_runiverse : params -> AST.ident List.list -> joint_internal_function -> Identifiers.universe -> joint_internal_function **) let set_runiverse globals pars p runiverse = { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse = runiverse; joint_if_result = p.joint_if_result; joint_if_params = p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize; joint_if_local_stacksize = p.joint_if_local_stacksize; joint_if_code = p.joint_if_code; joint_if_entry = p.joint_if_entry } (** val add_graph : graph_params -> AST.ident List.list -> Graphs.label -> joint_statement -> joint_internal_function -> joint_internal_function **) let add_graph g_pars globals l stmt p = let code = Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l stmt in { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse = p.joint_if_runiverse; joint_if_result = p.joint_if_result; joint_if_params = p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize; joint_if_local_stacksize = p.joint_if_local_stacksize; joint_if_code = (Obj.magic code); joint_if_entry = p.joint_if_entry } 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 **) let rec joint_program_rect_Type4 p h_mk_joint_program x_18121 = let { jp_functions = jp_functions0; joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = x_18121 in h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __ (** 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 **) let rec joint_program_rect_Type5 p h_mk_joint_program x_18123 = let { jp_functions = jp_functions0; joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = x_18123 in h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __ (** 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 **) let rec joint_program_rect_Type3 p h_mk_joint_program x_18125 = let { jp_functions = jp_functions0; joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = x_18125 in h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __ (** 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 **) let rec joint_program_rect_Type2 p h_mk_joint_program x_18127 = let { jp_functions = jp_functions0; joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = x_18127 in h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __ (** 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 **) let rec joint_program_rect_Type1 p h_mk_joint_program x_18129 = let { jp_functions = jp_functions0; joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = x_18129 in h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __ (** 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 **) let rec joint_program_rect_Type0 p h_mk_joint_program x_18131 = let { jp_functions = jp_functions0; joint_prog = joint_prog0; init_cost_label = init_cost_label0 } = x_18131 in h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __ (** val jp_functions : params -> joint_program -> AST.ident List.list **) let rec jp_functions p xxx = xxx.jp_functions (** val joint_prog : params -> joint_program -> (joint_function, AST.init_data List.list) AST.program **) let rec joint_prog p xxx = xxx.joint_prog (** val init_cost_label : params -> joint_program -> CostLabel.costlabel **) let rec init_cost_label p xxx = xxx.init_cost_label (** 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 **) let joint_program_inv_rect_Type4 x1 hterm h1 = let hcut = joint_program_rect_Type4 x1 h1 hterm in hcut __ (** 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 **) let joint_program_inv_rect_Type3 x1 hterm h1 = let hcut = joint_program_rect_Type3 x1 h1 hterm in hcut __ (** 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 **) let joint_program_inv_rect_Type2 x1 hterm h1 = let hcut = joint_program_rect_Type2 x1 h1 hterm in hcut __ (** 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 **) let joint_program_inv_rect_Type1 x1 hterm h1 = let hcut = joint_program_rect_Type1 x1 h1 hterm in hcut __ (** 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 **) let joint_program_inv_rect_Type0 x1 hterm h1 = let hcut = joint_program_rect_Type0 x1 h1 hterm in hcut __ (** val joint_program_discr : params -> joint_program -> joint_program -> __ **) let joint_program_discr a1 x y = Logic.eq_rect_Type2 x (let { jp_functions = a0; joint_prog = a10; init_cost_label = a2 } = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val joint_program_jmdiscr : params -> joint_program -> joint_program -> __ **) let joint_program_jmdiscr a1 x y = Logic.eq_rect_Type2 x (let { jp_functions = a0; joint_prog = a10; init_cost_label = a2 } = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val dpi1__o__joint_prog__o__inject : params -> (joint_program, 'a1) Types.dPair -> (joint_function, AST.init_data List.list) AST.program Types.sig0 **) let dpi1__o__joint_prog__o__inject x0 x2 = x2.Types.dpi1.joint_prog (** val eject__o__joint_prog__o__inject : params -> joint_program Types.sig0 -> (joint_function, AST.init_data List.list) AST.program Types.sig0 **) let eject__o__joint_prog__o__inject x0 x2 = (Types.pi1 x2).joint_prog (** val joint_prog__o__inject : params -> joint_program -> (joint_function, AST.init_data List.list) AST.program Types.sig0 **) let joint_prog__o__inject x0 x1 = x1.joint_prog (** val dpi1__o__joint_prog : params -> (joint_program, 'a1) Types.dPair -> (joint_function, AST.init_data List.list) AST.program **) let dpi1__o__joint_prog x0 x2 = x2.Types.dpi1.joint_prog (** val eject__o__joint_prog : params -> joint_program Types.sig0 -> (joint_function, AST.init_data List.list) AST.program **) let eject__o__joint_prog x0 x2 = (Types.pi1 x2).joint_prog (** val prog_names : params -> joint_program -> AST.ident List.list **) let prog_names pars p = List.append (AST.prog_var_names p.joint_prog) p.jp_functions (** val transform_joint_program : params -> params -> (AST.ident List.list -> joint_closed_internal_function -> joint_closed_internal_function) -> joint_program -> joint_program **) let transform_joint_program src dst trans prog_in = { jp_functions = prog_in.jp_functions; joint_prog = (AST.transform_program prog_in.joint_prog (fun vars -> AST.transf_fundef (trans (List.append vars prog_in.jp_functions)))); init_cost_label = prog_in.init_cost_label } type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list (** val stack_cost : params -> joint_program -> stack_cost_model **) let stack_cost p pr = List.foldr (fun id_fun acc -> let { Types.fst = id; Types.snd = fun0 } = id_fun in (match fun0 with | AST.Internal jif -> List.Cons ({ Types.fst = id; Types.snd = (Types.pi1 jif).joint_if_stacksize }, acc) | AST.External x -> acc)) List.Nil pr.joint_prog.AST.prog_funct open Extra_bool open Coqlib open Values open FrontEndVal open GenMem open FrontEndMem open Globalenvs (** val globals_stacksize : params -> joint_program -> Nat.nat **) let globals_stacksize pars p = List.fold Nat.plus Nat.O (fun entry -> Bool.True) (fun entry -> Globalenvs.size_init_data_list entry.Types.snd) p.joint_prog.AST.prog_vars