extracted/joint.ml

   1 open Preamble
   2
   3 open Hide
   4
   5 open Proper
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open ErrorMessages
  12
  13 open PreIdentifiers
  14
  15 open Errors
  16
  17 open Extralib
  18
  19 open Lists
  20
  21 open Identifiers
  22
  23 open Integers
  24
  25 open AST
  26
  27 open Division
  28
  29 open Exp
  30
  31 open Arithmetic
  32
  33 open Setoids
  34
  35 open Monad
  36
  37 open Option
  38
  39 open Extranat
  40
  41 open Vector
  42
  43 open Div_and_mod
  44
  45 open Jmeq
  46
  47 open Russell
  48
  49 open List
  50
  51 open Util
  52
  53 open FoldStuff
  54
  55 open BitVector
  56
  57 open Types
  58
  59 open Bool
  60
  61 open Relations
  62
  63 open Nat
  64
  65 open Hints_declaration
  66
  67 open Core_notation
  68
  69 open Pts
  70
  71 open Logic
  72
  73 open Positive
  74
  75 open Z
  76
  77 open BitVectorZ
  78
  79 open Pointers
  80
  81 open ByteValues
  82
  83 open BackEndOps
  84
  85 open CostLabel
  86
  87 open Order
  88
  89 open Registers
  90
  91 open I8051
  92
  93 open BitVectorTrie
  94
  95 open Graphs
  96
  97 open LabelledObjects
  98
  99 open Sets
 100
 101 open Listb
 102
 103 open String
 104
 105 type 't argument =
 106 | Reg of 't
 107 | Imm of BitVector.byte
 108
 109 (** val argument_rect_Type4 :
 110     ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
 111 let rec argument_rect_Type4 h_Reg h_Imm = function
 112 | Reg x_16867 -> h_Reg x_16867
 113 | Imm x_16868 -> h_Imm x_16868
 114
 115 (** val argument_rect_Type5 :
 116     ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
 117 let rec argument_rect_Type5 h_Reg h_Imm = function
 118 | Reg x_16872 -> h_Reg x_16872
 119 | Imm x_16873 -> h_Imm x_16873
 120
 121 (** val argument_rect_Type3 :
 122     ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
 123 let rec argument_rect_Type3 h_Reg h_Imm = function
 124 | Reg x_16877 -> h_Reg x_16877
 125 | Imm x_16878 -> h_Imm x_16878
 126
 127 (** val argument_rect_Type2 :
 128     ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
 129 let rec argument_rect_Type2 h_Reg h_Imm = function
 130 | Reg x_16882 -> h_Reg x_16882
 131 | Imm x_16883 -> h_Imm x_16883
 132
 133 (** val argument_rect_Type1 :
 134     ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
 135 let rec argument_rect_Type1 h_Reg h_Imm = function
 136 | Reg x_16887 -> h_Reg x_16887
 137 | Imm x_16888 -> h_Imm x_16888
 138
 139 (** val argument_rect_Type0 :
 140     ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
 141 let rec argument_rect_Type0 h_Reg h_Imm = function
 142 | Reg x_16892 -> h_Reg x_16892
 143 | Imm x_16893 -> h_Imm x_16893
 144
 145 (** val argument_inv_rect_Type4 :
 146     'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
 147     'a2 **)
 148 let argument_inv_rect_Type4 hterm h1 h2 =
 149   let hcut = argument_rect_Type4 h1 h2 hterm in hcut __
 150
 151 (** val argument_inv_rect_Type3 :
 152     'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
 153     'a2 **)
 154 let argument_inv_rect_Type3 hterm h1 h2 =
 155   let hcut = argument_rect_Type3 h1 h2 hterm in hcut __
 156
 157 (** val argument_inv_rect_Type2 :
 158     'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
 159     'a2 **)
 160 let argument_inv_rect_Type2 hterm h1 h2 =
 161   let hcut = argument_rect_Type2 h1 h2 hterm in hcut __
 162
 163 (** val argument_inv_rect_Type1 :
 164     'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
 165     'a2 **)
 166 let argument_inv_rect_Type1 hterm h1 h2 =
 167   let hcut = argument_rect_Type1 h1 h2 hterm in hcut __
 168
 169 (** val argument_inv_rect_Type0 :
 170     'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) ->
 171     'a2 **)
 172 let argument_inv_rect_Type0 hterm h1 h2 =
 173   let hcut = argument_rect_Type0 h1 h2 hterm in hcut __
 174
 175 (** val argument_discr : 'a1 argument -> 'a1 argument -> __ **)
 176 let argument_discr x y =
 177   Logic.eq_rect_Type2 x
 178     (match x with
 179      | Reg a0 -> Obj.magic (fun _ dH -> dH __)
 180      | Imm a0 -> Obj.magic (fun _ dH -> dH __)) y
 181
 182 (** val argument_jmdiscr : 'a1 argument -> 'a1 argument -> __ **)
 183 let argument_jmdiscr x y =
 184   Logic.eq_rect_Type2 x
 185     (match x with
 186      | Reg a0 -> Obj.magic (fun _ dH -> dH __)
 187      | Imm a0 -> Obj.magic (fun _ dH -> dH __)) y
 188
 189 type psd_argument = Registers.register argument
 190
 191 (** val psd_argument_from_reg : Registers.register -> psd_argument **)
 192 let psd_argument_from_reg x =
 193   Reg x
 194
 195 (** val dpi1__o__reg_to_psd_argument__o__inject :
 196     (Registers.register, 'a1) Types.dPair -> psd_argument Types.sig0 **)
 197 let dpi1__o__reg_to_psd_argument__o__inject x2 =
 198   psd_argument_from_reg x2.Types.dpi1
 199
 200 (** val eject__o__reg_to_psd_argument__o__inject :
 201     Registers.register Types.sig0 -> psd_argument Types.sig0 **)
 202 let eject__o__reg_to_psd_argument__o__inject x2 =
 203   psd_argument_from_reg (Types.pi1 x2)
 204
 205 (** val reg_to_psd_argument__o__inject :
 206     Registers.register -> psd_argument Types.sig0 **)
 207 let reg_to_psd_argument__o__inject x1 =
 208   psd_argument_from_reg x1
 209
 210 (** val dpi1__o__reg_to_psd_argument :
 211     (Registers.register, 'a1) Types.dPair -> psd_argument **)
 212 let dpi1__o__reg_to_psd_argument x1 =
 213   psd_argument_from_reg x1.Types.dpi1
 214
 215 (** val eject__o__reg_to_psd_argument :
 216     Registers.register Types.sig0 -> psd_argument **)
 217 let eject__o__reg_to_psd_argument x1 =
 218   psd_argument_from_reg (Types.pi1 x1)
 219
 220 (** val psd_argument_from_byte : BitVector.byte -> psd_argument **)
 221 let psd_argument_from_byte x =
 222   Imm x
 223
 224 (** val dpi1__o__byte_to_psd_argument__o__inject :
 225     (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0 **)
 226 let dpi1__o__byte_to_psd_argument__o__inject x2 =
 227   psd_argument_from_byte x2.Types.dpi1
 228
 229 (** val eject__o__byte_to_psd_argument__o__inject :
 230     BitVector.byte Types.sig0 -> psd_argument Types.sig0 **)
 231 let eject__o__byte_to_psd_argument__o__inject x2 =
 232   psd_argument_from_byte (Types.pi1 x2)
 233
 234 (** val byte_to_psd_argument__o__inject :
 235     BitVector.byte -> psd_argument Types.sig0 **)
 236 let byte_to_psd_argument__o__inject x1 =
 237   psd_argument_from_byte x1
 238
 239 (** val dpi1__o__byte_to_psd_argument :
 240     (BitVector.byte, 'a1) Types.dPair -> psd_argument **)
 241 let dpi1__o__byte_to_psd_argument x1 =
 242   psd_argument_from_byte x1.Types.dpi1
 243
 244 (** val eject__o__byte_to_psd_argument :
 245     BitVector.byte Types.sig0 -> psd_argument **)
 246 let eject__o__byte_to_psd_argument x1 =
 247   psd_argument_from_byte (Types.pi1 x1)
 248
 249 type hdw_argument = I8051.register argument
 250
 251 (** val hdw_argument_from_reg : I8051.register -> hdw_argument **)
 252 let hdw_argument_from_reg x =
 253   Reg x
 254
 255 (** val dpi1__o__reg_to_hdw_argument__o__inject :
 256     (I8051.register, 'a1) Types.dPair -> hdw_argument Types.sig0 **)
 257 let dpi1__o__reg_to_hdw_argument__o__inject x2 =
 258   hdw_argument_from_reg x2.Types.dpi1
 259
 260 (** val eject__o__reg_to_hdw_argument__o__inject :
 261     I8051.register Types.sig0 -> hdw_argument Types.sig0 **)
 262 let eject__o__reg_to_hdw_argument__o__inject x2 =
 263   hdw_argument_from_reg (Types.pi1 x2)
 264
 265 (** val reg_to_hdw_argument__o__inject :
 266     I8051.register -> hdw_argument Types.sig0 **)
 267 let reg_to_hdw_argument__o__inject x1 =
 268   hdw_argument_from_reg x1
 269
 270 (** val dpi1__o__reg_to_hdw_argument :
 271     (I8051.register, 'a1) Types.dPair -> hdw_argument **)
 272 let dpi1__o__reg_to_hdw_argument x1 =
 273   hdw_argument_from_reg x1.Types.dpi1
 274
 275 (** val eject__o__reg_to_hdw_argument :
 276     I8051.register Types.sig0 -> hdw_argument **)
 277 let eject__o__reg_to_hdw_argument x1 =
 278   hdw_argument_from_reg (Types.pi1 x1)
 279
 280 (** val hdw_argument_from_byte : BitVector.byte -> hdw_argument **)
 281 let hdw_argument_from_byte x =
 282   Imm x
 283
 284 (** val dpi1__o__byte_to_hdw_argument__o__inject :
 285     (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0 **)
 286 let dpi1__o__byte_to_hdw_argument__o__inject x2 =
 287   psd_argument_from_byte x2.Types.dpi1
 288
 289 (** val eject__o__byte_to_hdw_argument__o__inject :
 290     BitVector.byte Types.sig0 -> psd_argument Types.sig0 **)
 291 let eject__o__byte_to_hdw_argument__o__inject x2 =
 292   psd_argument_from_byte (Types.pi1 x2)
 293
 294 (** val byte_to_hdw_argument__o__inject :
 295     BitVector.byte -> psd_argument Types.sig0 **)
 296 let byte_to_hdw_argument__o__inject x1 =
 297   psd_argument_from_byte x1
 298
 299 (** val dpi1__o__byte_to_hdw_argument :
 300     (BitVector.byte, 'a1) Types.dPair -> psd_argument **)
 301 let dpi1__o__byte_to_hdw_argument x1 =
 302   psd_argument_from_byte x1.Types.dpi1
 303
 304 (** val eject__o__byte_to_hdw_argument :
 305     BitVector.byte Types.sig0 -> psd_argument **)
 306 let eject__o__byte_to_hdw_argument x1 =
 307   psd_argument_from_byte (Types.pi1 x1)
 308
 309 (** val byte_of_nat : Nat.nat -> BitVector.byte **)
 310 let byte_of_nat =
 311   Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 312     (Nat.S (Nat.S Nat.O))))))))
 313
 314 (** val zero_byte : BitVector.byte **)
 315 let zero_byte =
 316   BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 317     Nat.O))))))))
 318
 319 type unserialized_params = { ext_seq_labels : (__ -> Graphs.label List.list);
 320                              has_tailcalls : Bool.bool }
 321
 322 (** val unserialized_params_rect_Type4 :
 323     (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 324     __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 325     unserialized_params -> 'a1 **)
 326 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_16928 =
 327   let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
 328     x_16928
 329   in
 330   h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
 331     ext_seq_labels0 has_tailcalls0 __
 332
 333 (** val unserialized_params_rect_Type5 :
 334     (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 335     __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 336     unserialized_params -> 'a1 **)
 337 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_16930 =
 338   let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
 339     x_16930
 340   in
 341   h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
 342     ext_seq_labels0 has_tailcalls0 __
 343
 344 (** val unserialized_params_rect_Type3 :
 345     (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 346     __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 347     unserialized_params -> 'a1 **)
 348 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_16932 =
 349   let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
 350     x_16932
 351   in
 352   h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
 353     ext_seq_labels0 has_tailcalls0 __
 354
 355 (** val unserialized_params_rect_Type2 :
 356     (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 357     __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 358     unserialized_params -> 'a1 **)
 359 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_16934 =
 360   let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
 361     x_16934
 362   in
 363   h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
 364     ext_seq_labels0 has_tailcalls0 __
 365
 366 (** val unserialized_params_rect_Type1 :
 367     (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 368     __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 369     unserialized_params -> 'a1 **)
 370 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_16936 =
 371   let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
 372     x_16936
 373   in
 374   h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
 375     ext_seq_labels0 has_tailcalls0 __
 376
 377 (** val unserialized_params_rect_Type0 :
 378     (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 379     __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
 380     unserialized_params -> 'a1 **)
 381 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_16938 =
 382   let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
 383     x_16938
 384   in
 385   h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
 386     ext_seq_labels0 has_tailcalls0 __
 387
 388 type acc_a_reg = __
 389
 390 type acc_b_reg = __
 391
 392 type acc_a_arg = __
 393
 394 type acc_b_arg = __
 395
 396 type dpl_reg = __
 397
 398 type dph_reg = __
 399
 400 type dpl_arg = __
 401
 402 type dph_arg = __
 403
 404 type snd_arg = __
 405
 406 type pair_move = __
 407
 408 type call_args = __
 409
 410 type call_dest = __
 411
 412 type ext_seq = __
 413
 414 (** val ext_seq_labels :
 415     unserialized_params -> __ -> Graphs.label List.list **)
 416 let rec ext_seq_labels xxx =
 417   xxx.ext_seq_labels
 418
 419 (** val has_tailcalls : unserialized_params -> Bool.bool **)
 420 let rec has_tailcalls xxx =
 421   xxx.has_tailcalls
 422
 423 type paramsT = __
 424
 425 (** val unserialized_params_inv_rect_Type4 :
 426     unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 427     __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
 428     -> __ -> __ -> 'a1) -> 'a1 **)
 429 let unserialized_params_inv_rect_Type4 hterm h1 =
 430   let hcut = unserialized_params_rect_Type4 h1 hterm in hcut __
 431
 432 (** val unserialized_params_inv_rect_Type3 :
 433     unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 434     __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
 435     -> __ -> __ -> 'a1) -> 'a1 **)
 436 let unserialized_params_inv_rect_Type3 hterm h1 =
 437   let hcut = unserialized_params_rect_Type3 h1 hterm in hcut __
 438
 439 (** val unserialized_params_inv_rect_Type2 :
 440     unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 441     __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
 442     -> __ -> __ -> 'a1) -> 'a1 **)
 443 let unserialized_params_inv_rect_Type2 hterm h1 =
 444   let hcut = unserialized_params_rect_Type2 h1 hterm in hcut __
 445
 446 (** val unserialized_params_inv_rect_Type1 :
 447     unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 448     __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
 449     -> __ -> __ -> 'a1) -> 'a1 **)
 450 let unserialized_params_inv_rect_Type1 hterm h1 =
 451   let hcut = unserialized_params_rect_Type1 h1 hterm in hcut __
 452
 453 (** val unserialized_params_inv_rect_Type0 :
 454     unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
 455     __ -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool
 456     -> __ -> __ -> 'a1) -> 'a1 **)
 457 let unserialized_params_inv_rect_Type0 hterm h1 =
 458   let hcut = unserialized_params_rect_Type0 h1 hterm in hcut __
 459
 460 (** val unserialized_params_jmdiscr :
 461     unserialized_params -> unserialized_params -> __ **)
 462 let unserialized_params_jmdiscr x y =
 463   Logic.eq_rect_Type2 x
 464     (let { ext_seq_labels = a13; has_tailcalls = a14 } = x in
 465     Obj.magic (fun _ dH ->
 466       dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
 467
 468 type get_pseudo_reg_functs = { acc_a_regs : (__ -> Registers.register
 469                                             List.list);
 470                                acc_b_regs : (__ -> Registers.register
 471                                             List.list);
 472                                acc_a_args : (__ -> Registers.register
 473                                             List.list);
 474                                acc_b_args : (__ -> Registers.register
 475                                             List.list);
 476                                dpl_regs : (__ -> Registers.register
 477                                           List.list);
 478                                dph_regs : (__ -> Registers.register
 479                                           List.list);
 480                                dpl_args : (__ -> Registers.register
 481                                           List.list);
 482                                dph_args : (__ -> Registers.register
 483                                           List.list);
 484                                snd_args : (__ -> Registers.register
 485                                           List.list);
 486                                pair_move_regs : (__ -> Registers.register
 487                                                 List.list);
 488                                f_call_args : (__ -> Registers.register
 489                                              List.list);
 490                                f_call_dest : (__ -> Registers.register
 491                                              List.list);
 492                                ext_seq_regs : (__ -> Registers.register
 493                                               List.list);
 494                                params_regs : (__ -> Registers.register
 495                                              List.list) }
 496
 497 (** val get_pseudo_reg_functs_rect_Type4 :
 498     unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 499     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 500     (__ -> Registers.register List.list) -> (__ -> Registers.register
 501     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 502     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 503     (__ -> Registers.register List.list) -> (__ -> Registers.register
 504     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 505     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 506     (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 507     'a1 **)
 508 let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_16955 =
 509   let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
 510     acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
 511     dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
 512     snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
 513     f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
 514     params_regs0 } = x_16955
 515   in
 516   h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
 517     dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
 518     f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
 519
 520 (** val get_pseudo_reg_functs_rect_Type5 :
 521     unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 522     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 523     (__ -> Registers.register List.list) -> (__ -> Registers.register
 524     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 525     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 526     (__ -> Registers.register List.list) -> (__ -> Registers.register
 527     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 528     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 529     (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 530     'a1 **)
 531 let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_16957 =
 532   let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
 533     acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
 534     dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
 535     snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
 536     f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
 537     params_regs0 } = x_16957
 538   in
 539   h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
 540     dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
 541     f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
 542
 543 (** val get_pseudo_reg_functs_rect_Type3 :
 544     unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 545     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 546     (__ -> Registers.register List.list) -> (__ -> Registers.register
 547     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 548     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 549     (__ -> Registers.register List.list) -> (__ -> Registers.register
 550     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 551     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 552     (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 553     'a1 **)
 554 let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_16959 =
 555   let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
 556     acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
 557     dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
 558     snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
 559     f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
 560     params_regs0 } = x_16959
 561   in
 562   h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
 563     dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
 564     f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
 565
 566 (** val get_pseudo_reg_functs_rect_Type2 :
 567     unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 568     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 569     (__ -> Registers.register List.list) -> (__ -> Registers.register
 570     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 571     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 572     (__ -> Registers.register List.list) -> (__ -> Registers.register
 573     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 574     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 575     (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 576     'a1 **)
 577 let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_16961 =
 578   let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
 579     acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
 580     dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
 581     snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
 582     f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
 583     params_regs0 } = x_16961
 584   in
 585   h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
 586     dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
 587     f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
 588
 589 (** val get_pseudo_reg_functs_rect_Type1 :
 590     unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 591     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 592     (__ -> Registers.register List.list) -> (__ -> Registers.register
 593     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 594     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 595     (__ -> Registers.register List.list) -> (__ -> Registers.register
 596     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 597     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 598     (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 599     'a1 **)
 600 let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_16963 =
 601   let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
 602     acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
 603     dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
 604     snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
 605     f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
 606     params_regs0 } = x_16963
 607   in
 608   h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
 609     dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
 610     f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
 611
 612 (** val get_pseudo_reg_functs_rect_Type0 :
 613     unserialized_params -> ((__ -> Registers.register List.list) -> (__ ->
 614     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 615     (__ -> Registers.register List.list) -> (__ -> Registers.register
 616     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 617     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 618     (__ -> Registers.register List.list) -> (__ -> Registers.register
 619     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 620     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 621     (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
 622     'a1 **)
 623 let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_16965 =
 624   let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
 625     acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
 626     dph_regs0; dpl_args = dpl_args0; dph_args = dph_args0; snd_args =
 627     snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
 628     f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
 629     params_regs0 } = x_16965
 630   in
 631   h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
 632     dpl_regs0 dph_regs0 dpl_args0 dph_args0 snd_args0 pair_move_regs0
 633     f_call_args0 f_call_dest0 ext_seq_regs0 params_regs0
 634
 635 (** val acc_a_regs :
 636     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 637     List.list **)
 638 let rec acc_a_regs p xxx =
 639   xxx.acc_a_regs
 640
 641 (** val acc_b_regs :
 642     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 643     List.list **)
 644 let rec acc_b_regs p xxx =
 645   xxx.acc_b_regs
 646
 647 (** val acc_a_args :
 648     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 649     List.list **)
 650 let rec acc_a_args p xxx =
 651   xxx.acc_a_args
 652
 653 (** val acc_b_args :
 654     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 655     List.list **)
 656 let rec acc_b_args p xxx =
 657   xxx.acc_b_args
 658
 659 (** val dpl_regs :
 660     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 661     List.list **)
 662 let rec dpl_regs p xxx =
 663   xxx.dpl_regs
 664
 665 (** val dph_regs :
 666     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 667     List.list **)
 668 let rec dph_regs p xxx =
 669   xxx.dph_regs
 670
 671 (** val dpl_args :
 672     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 673     List.list **)
 674 let rec dpl_args p xxx =
 675   xxx.dpl_args
 676
 677 (** val dph_args :
 678     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 679     List.list **)
 680 let rec dph_args p xxx =
 681   xxx.dph_args
 682
 683 (** val snd_args :
 684     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 685     List.list **)
 686 let rec snd_args p xxx =
 687   xxx.snd_args
 688
 689 (** val pair_move_regs :
 690     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 691     List.list **)
 692 let rec pair_move_regs p xxx =
 693   xxx.pair_move_regs
 694
 695 (** val f_call_args :
 696     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 697     List.list **)
 698 let rec f_call_args p xxx =
 699   xxx.f_call_args
 700
 701 (** val f_call_dest :
 702     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 703     List.list **)
 704 let rec f_call_dest p xxx =
 705   xxx.f_call_dest
 706
 707 (** val ext_seq_regs :
 708     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 709     List.list **)
 710 let rec ext_seq_regs p xxx =
 711   xxx.ext_seq_regs
 712
 713 (** val params_regs :
 714     unserialized_params -> get_pseudo_reg_functs -> __ -> Registers.register
 715     List.list **)
 716 let rec params_regs p xxx =
 717   xxx.params_regs
 718
 719 (** val get_pseudo_reg_functs_inv_rect_Type4 :
 720     unserialized_params -> get_pseudo_reg_functs -> ((__ ->
 721     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 722     (__ -> Registers.register List.list) -> (__ -> Registers.register
 723     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 724     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 725     (__ -> Registers.register List.list) -> (__ -> Registers.register
 726     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 727     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 728     (__ -> Registers.register List.list) -> (__ -> Registers.register
 729     List.list) -> __ -> 'a1) -> 'a1 **)
 730 let get_pseudo_reg_functs_inv_rect_Type4 x1 hterm h1 =
 731   let hcut = get_pseudo_reg_functs_rect_Type4 x1 h1 hterm in hcut __
 732
 733 (** val get_pseudo_reg_functs_inv_rect_Type3 :
 734     unserialized_params -> get_pseudo_reg_functs -> ((__ ->
 735     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 736     (__ -> Registers.register List.list) -> (__ -> Registers.register
 737     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 738     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 739     (__ -> Registers.register List.list) -> (__ -> Registers.register
 740     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 741     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 742     (__ -> Registers.register List.list) -> (__ -> Registers.register
 743     List.list) -> __ -> 'a1) -> 'a1 **)
 744 let get_pseudo_reg_functs_inv_rect_Type3 x1 hterm h1 =
 745   let hcut = get_pseudo_reg_functs_rect_Type3 x1 h1 hterm in hcut __
 746
 747 (** val get_pseudo_reg_functs_inv_rect_Type2 :
 748     unserialized_params -> get_pseudo_reg_functs -> ((__ ->
 749     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 750     (__ -> Registers.register List.list) -> (__ -> Registers.register
 751     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 752     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 753     (__ -> Registers.register List.list) -> (__ -> Registers.register
 754     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 755     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 756     (__ -> Registers.register List.list) -> (__ -> Registers.register
 757     List.list) -> __ -> 'a1) -> 'a1 **)
 758 let get_pseudo_reg_functs_inv_rect_Type2 x1 hterm h1 =
 759   let hcut = get_pseudo_reg_functs_rect_Type2 x1 h1 hterm in hcut __
 760
 761 (** val get_pseudo_reg_functs_inv_rect_Type1 :
 762     unserialized_params -> get_pseudo_reg_functs -> ((__ ->
 763     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 764     (__ -> Registers.register List.list) -> (__ -> Registers.register
 765     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 766     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 767     (__ -> Registers.register List.list) -> (__ -> Registers.register
 768     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 769     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 770     (__ -> Registers.register List.list) -> (__ -> Registers.register
 771     List.list) -> __ -> 'a1) -> 'a1 **)
 772 let get_pseudo_reg_functs_inv_rect_Type1 x1 hterm h1 =
 773   let hcut = get_pseudo_reg_functs_rect_Type1 x1 h1 hterm in hcut __
 774
 775 (** val get_pseudo_reg_functs_inv_rect_Type0 :
 776     unserialized_params -> get_pseudo_reg_functs -> ((__ ->
 777     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 778     (__ -> Registers.register List.list) -> (__ -> Registers.register
 779     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 780     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 781     (__ -> Registers.register List.list) -> (__ -> Registers.register
 782     List.list) -> (__ -> Registers.register List.list) -> (__ ->
 783     Registers.register List.list) -> (__ -> Registers.register List.list) ->
 784     (__ -> Registers.register List.list) -> (__ -> Registers.register
 785     List.list) -> __ -> 'a1) -> 'a1 **)
 786 let get_pseudo_reg_functs_inv_rect_Type0 x1 hterm h1 =
 787   let hcut = get_pseudo_reg_functs_rect_Type0 x1 h1 hterm in hcut __
 788
 789 (** val get_pseudo_reg_functs_jmdiscr :
 790     unserialized_params -> get_pseudo_reg_functs -> get_pseudo_reg_functs ->
 791     __ **)
 792 let get_pseudo_reg_functs_jmdiscr a1 x y =
 793   Logic.eq_rect_Type2 x
 794     (let { acc_a_regs = a0; acc_b_regs = a10; acc_a_args = a2; acc_b_args =
 795        a3; dpl_regs = a4; dph_regs = a5; dpl_args = a6; dph_args = a7;
 796        snd_args = a8; pair_move_regs = a9; f_call_args = a100; f_call_dest =
 797        a11; ext_seq_regs = a12; params_regs = a13 } = x
 798      in
 799     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
 800
 801 type uns_params = { u_pars : unserialized_params;
 802                     functs : get_pseudo_reg_functs }
 803
 804 (** val uns_params_rect_Type4 :
 805     (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
 806     'a1 **)
 807 let rec uns_params_rect_Type4 h_mk_uns_params x_16995 =
 808   let { u_pars = u_pars0; functs = functs0 } = x_16995 in
 809   h_mk_uns_params u_pars0 functs0
 810
 811 (** val uns_params_rect_Type5 :
 812     (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
 813     'a1 **)
 814 let rec uns_params_rect_Type5 h_mk_uns_params x_16997 =
 815   let { u_pars = u_pars0; functs = functs0 } = x_16997 in
 816   h_mk_uns_params u_pars0 functs0
 817
 818 (** val uns_params_rect_Type3 :
 819     (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
 820     'a1 **)
 821 let rec uns_params_rect_Type3 h_mk_uns_params x_16999 =
 822   let { u_pars = u_pars0; functs = functs0 } = x_16999 in
 823   h_mk_uns_params u_pars0 functs0
 824
 825 (** val uns_params_rect_Type2 :
 826     (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
 827     'a1 **)
 828 let rec uns_params_rect_Type2 h_mk_uns_params x_17001 =
 829   let { u_pars = u_pars0; functs = functs0 } = x_17001 in
 830   h_mk_uns_params u_pars0 functs0
 831
 832 (** val uns_params_rect_Type1 :
 833     (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
 834     'a1 **)
 835 let rec uns_params_rect_Type1 h_mk_uns_params x_17003 =
 836   let { u_pars = u_pars0; functs = functs0 } = x_17003 in
 837   h_mk_uns_params u_pars0 functs0
 838
 839 (** val uns_params_rect_Type0 :
 840     (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
 841     'a1 **)
 842 let rec uns_params_rect_Type0 h_mk_uns_params x_17005 =
 843   let { u_pars = u_pars0; functs = functs0 } = x_17005 in
 844   h_mk_uns_params u_pars0 functs0
 845
 846 (** val u_pars : uns_params -> unserialized_params **)
 847 let rec u_pars xxx =
 848   xxx.u_pars
 849
 850 (** val functs : uns_params -> get_pseudo_reg_functs **)
 851 let rec functs xxx =
 852   xxx.functs
 853
 854 (** val uns_params_inv_rect_Type4 :
 855     uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
 856     -> 'a1 **)
 857 let uns_params_inv_rect_Type4 hterm h1 =
 858   let hcut = uns_params_rect_Type4 h1 hterm in hcut __
 859
 860 (** val uns_params_inv_rect_Type3 :
 861     uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
 862     -> 'a1 **)
 863 let uns_params_inv_rect_Type3 hterm h1 =
 864   let hcut = uns_params_rect_Type3 h1 hterm in hcut __
 865
 866 (** val uns_params_inv_rect_Type2 :
 867     uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
 868     -> 'a1 **)
 869 let uns_params_inv_rect_Type2 hterm h1 =
 870   let hcut = uns_params_rect_Type2 h1 hterm in hcut __
 871
 872 (** val uns_params_inv_rect_Type1 :
 873     uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
 874     -> 'a1 **)
 875 let uns_params_inv_rect_Type1 hterm h1 =
 876   let hcut = uns_params_rect_Type1 h1 hterm in hcut __
 877
 878 (** val uns_params_inv_rect_Type0 :
 879     uns_params -> (unserialized_params -> get_pseudo_reg_functs -> __ -> 'a1)
 880     -> 'a1 **)
 881 let uns_params_inv_rect_Type0 hterm h1 =
 882   let hcut = uns_params_rect_Type0 h1 hterm in hcut __
 883
 884 (** val uns_params_jmdiscr : uns_params -> uns_params -> __ **)
 885 let uns_params_jmdiscr x y =
 886   Logic.eq_rect_Type2 x
 887     (let { u_pars = a0; functs = a1 } = x in
 888     Obj.magic (fun _ dH -> dH __ __)) y
 889
 890 type joint_seq =
 891 | COMMENT of String.string
 892 | MOVE of __
 893 | POP of __
 894 | PUSH of __
 895 | ADDRESS of AST.ident * BitVector.word * __ * __
 896 | OPACCS of BackEndOps.opAccs * __ * __ * __ * __
 897 | OP1 of BackEndOps.op1 * __ * __
 898 | OP2 of BackEndOps.op2 * __ * __ * __
 899 | CLEAR_CARRY
 900 | SET_CARRY
 901 | LOAD of __ * __ * __
 902 | STORE of __ * __ * __
 903 | Extension_seq of __
 904
 905 (** val joint_seq_rect_Type4 :
 906     unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
 907     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
 908     BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
 909     __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
 910     (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
 911     __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
 912 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
 913 | COMMENT x_17061 -> h_COMMENT x_17061
 914 | MOVE x_17062 -> h_MOVE x_17062
 915 | POP x_17063 -> h_POP x_17063
 916 | PUSH x_17064 -> h_PUSH x_17064
 917 | ADDRESS (i, x_17067, x_17066, x_17065) ->
 918   h_ADDRESS i __ x_17067 x_17066 x_17065
 919 | OPACCS (x_17073, x_17072, x_17071, x_17070, x_17069) ->
 920   h_OPACCS x_17073 x_17072 x_17071 x_17070 x_17069
 921 | OP1 (x_17076, x_17075, x_17074) -> h_OP1 x_17076 x_17075 x_17074
 922 | OP2 (x_17080, x_17079, x_17078, x_17077) ->
 923   h_OP2 x_17080 x_17079 x_17078 x_17077
 924 | CLEAR_CARRY -> h_CLEAR_CARRY
 925 | SET_CARRY -> h_SET_CARRY
 926 | LOAD (x_17083, x_17082, x_17081) -> h_LOAD x_17083 x_17082 x_17081
 927 | STORE (x_17086, x_17085, x_17084) -> h_STORE x_17086 x_17085 x_17084
 928 | Extension_seq x_17087 -> h_extension_seq x_17087
 929
 930 (** val joint_seq_rect_Type5 :
 931     unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
 932     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
 933     BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
 934     __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
 935     (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
 936     __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
 937 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
 938 | COMMENT x_17102 -> h_COMMENT x_17102
 939 | MOVE x_17103 -> h_MOVE x_17103
 940 | POP x_17104 -> h_POP x_17104
 941 | PUSH x_17105 -> h_PUSH x_17105
 942 | ADDRESS (i, x_17108, x_17107, x_17106) ->
 943   h_ADDRESS i __ x_17108 x_17107 x_17106
 944 | OPACCS (x_17114, x_17113, x_17112, x_17111, x_17110) ->
 945   h_OPACCS x_17114 x_17113 x_17112 x_17111 x_17110
 946 | OP1 (x_17117, x_17116, x_17115) -> h_OP1 x_17117 x_17116 x_17115
 947 | OP2 (x_17121, x_17120, x_17119, x_17118) ->
 948   h_OP2 x_17121 x_17120 x_17119 x_17118
 949 | CLEAR_CARRY -> h_CLEAR_CARRY
 950 | SET_CARRY -> h_SET_CARRY
 951 | LOAD (x_17124, x_17123, x_17122) -> h_LOAD x_17124 x_17123 x_17122
 952 | STORE (x_17127, x_17126, x_17125) -> h_STORE x_17127 x_17126 x_17125
 953 | Extension_seq x_17128 -> h_extension_seq x_17128
 954
 955 (** val joint_seq_rect_Type3 :
 956     unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
 957     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
 958     BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
 959     __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
 960     (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
 961     __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
 962 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
 963 | COMMENT x_17143 -> h_COMMENT x_17143
 964 | MOVE x_17144 -> h_MOVE x_17144
 965 | POP x_17145 -> h_POP x_17145
 966 | PUSH x_17146 -> h_PUSH x_17146
 967 | ADDRESS (i, x_17149, x_17148, x_17147) ->
 968   h_ADDRESS i __ x_17149 x_17148 x_17147
 969 | OPACCS (x_17155, x_17154, x_17153, x_17152, x_17151) ->
 970   h_OPACCS x_17155 x_17154 x_17153 x_17152 x_17151
 971 | OP1 (x_17158, x_17157, x_17156) -> h_OP1 x_17158 x_17157 x_17156
 972 | OP2 (x_17162, x_17161, x_17160, x_17159) ->
 973   h_OP2 x_17162 x_17161 x_17160 x_17159
 974 | CLEAR_CARRY -> h_CLEAR_CARRY
 975 | SET_CARRY -> h_SET_CARRY
 976 | LOAD (x_17165, x_17164, x_17163) -> h_LOAD x_17165 x_17164 x_17163
 977 | STORE (x_17168, x_17167, x_17166) -> h_STORE x_17168 x_17167 x_17166
 978 | Extension_seq x_17169 -> h_extension_seq x_17169
 979
 980 (** val joint_seq_rect_Type2 :
 981     unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
 982     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
 983     BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
 984     __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
 985     (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
 986     __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
 987 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
 988 | COMMENT x_17184 -> h_COMMENT x_17184
 989 | MOVE x_17185 -> h_MOVE x_17185
 990 | POP x_17186 -> h_POP x_17186
 991 | PUSH x_17187 -> h_PUSH x_17187
 992 | ADDRESS (i, x_17190, x_17189, x_17188) ->
 993   h_ADDRESS i __ x_17190 x_17189 x_17188
 994 | OPACCS (x_17196, x_17195, x_17194, x_17193, x_17192) ->
 995   h_OPACCS x_17196 x_17195 x_17194 x_17193 x_17192
 996 | OP1 (x_17199, x_17198, x_17197) -> h_OP1 x_17199 x_17198 x_17197
 997 | OP2 (x_17203, x_17202, x_17201, x_17200) ->
 998   h_OP2 x_17203 x_17202 x_17201 x_17200
 999 | CLEAR_CARRY -> h_CLEAR_CARRY
1000 | SET_CARRY -> h_SET_CARRY
1001 | LOAD (x_17206, x_17205, x_17204) -> h_LOAD x_17206 x_17205 x_17204
1002 | STORE (x_17209, x_17208, x_17207) -> h_STORE x_17209 x_17208 x_17207
1003 | Extension_seq x_17210 -> h_extension_seq x_17210
1004
1005 (** val joint_seq_rect_Type1 :
1006     unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
1007     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
1008     BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
1009     __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
1010     (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
1011     __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1012 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
1013 | COMMENT x_17225 -> h_COMMENT x_17225
1014 | MOVE x_17226 -> h_MOVE x_17226
1015 | POP x_17227 -> h_POP x_17227
1016 | PUSH x_17228 -> h_PUSH x_17228
1017 | ADDRESS (i, x_17231, x_17230, x_17229) ->
1018   h_ADDRESS i __ x_17231 x_17230 x_17229
1019 | OPACCS (x_17237, x_17236, x_17235, x_17234, x_17233) ->
1020   h_OPACCS x_17237 x_17236 x_17235 x_17234 x_17233
1021 | OP1 (x_17240, x_17239, x_17238) -> h_OP1 x_17240 x_17239 x_17238
1022 | OP2 (x_17244, x_17243, x_17242, x_17241) ->
1023   h_OP2 x_17244 x_17243 x_17242 x_17241
1024 | CLEAR_CARRY -> h_CLEAR_CARRY
1025 | SET_CARRY -> h_SET_CARRY
1026 | LOAD (x_17247, x_17246, x_17245) -> h_LOAD x_17247 x_17246 x_17245
1027 | STORE (x_17250, x_17249, x_17248) -> h_STORE x_17250 x_17249 x_17248
1028 | Extension_seq x_17251 -> h_extension_seq x_17251
1029
1030 (** val joint_seq_rect_Type0 :
1031     unserialized_params -> AST.ident List.list -> (String.string -> 'a1) ->
1032     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ ->
1033     BitVector.word -> __ -> __ -> 'a1) -> (BackEndOps.opAccs -> __ -> __ ->
1034     __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> 'a1) ->
1035     (BackEndOps.op2 -> __ -> __ -> __ -> 'a1) -> 'a1 -> 'a1 -> (__ -> __ ->
1036     __ -> 'a1) -> (__ -> __ -> __ -> 'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
1037 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
1038 | COMMENT x_17266 -> h_COMMENT x_17266
1039 | MOVE x_17267 -> h_MOVE x_17267
1040 | POP x_17268 -> h_POP x_17268
1041 | PUSH x_17269 -> h_PUSH x_17269
1042 | ADDRESS (i, x_17272, x_17271, x_17270) ->
1043   h_ADDRESS i __ x_17272 x_17271 x_17270
1044 | OPACCS (x_17278, x_17277, x_17276, x_17275, x_17274) ->
1045   h_OPACCS x_17278 x_17277 x_17276 x_17275 x_17274
1046 | OP1 (x_17281, x_17280, x_17279) -> h_OP1 x_17281 x_17280 x_17279
1047 | OP2 (x_17285, x_17284, x_17283, x_17282) ->
1048   h_OP2 x_17285 x_17284 x_17283 x_17282
1049 | CLEAR_CARRY -> h_CLEAR_CARRY
1050 | SET_CARRY -> h_SET_CARRY
1051 | LOAD (x_17288, x_17287, x_17286) -> h_LOAD x_17288 x_17287 x_17286
1052 | STORE (x_17291, x_17290, x_17289) -> h_STORE x_17291 x_17290 x_17289
1053 | Extension_seq x_17292 -> h_extension_seq x_17292
1054
1055 (** val joint_seq_inv_rect_Type4 :
1056     unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1057     -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1058     'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1059     (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1060     (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1061     -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1062     __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1063 let joint_seq_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1064   let hcut =
1065     joint_seq_rect_Type4 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1066       hterm
1067   in
1068   hcut __
1069
1070 (** val joint_seq_inv_rect_Type3 :
1071     unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1072     -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1073     'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1074     (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1075     (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1076     -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1077     __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1078 let joint_seq_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1079   let hcut =
1080     joint_seq_rect_Type3 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1081       hterm
1082   in
1083   hcut __
1084
1085 (** val joint_seq_inv_rect_Type2 :
1086     unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1087     -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1088     'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1089     (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1090     (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1091     -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1092     __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1093 let joint_seq_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1094   let hcut =
1095     joint_seq_rect_Type2 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1096       hterm
1097   in
1098   hcut __
1099
1100 (** val joint_seq_inv_rect_Type1 :
1101     unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1102     -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1103     'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1104     (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1105     (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1106     -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1107     __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1108 let joint_seq_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1109   let hcut =
1110     joint_seq_rect_Type1 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1111       hterm
1112   in
1113   hcut __
1114
1115 (** val joint_seq_inv_rect_Type0 :
1116     unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
1117     -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
1118     'a1) -> (AST.ident -> __ -> BitVector.word -> __ -> __ -> __ -> 'a1) ->
1119     (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
1120     (BackEndOps.op1 -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __
1121     -> __ -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> __ -> __ ->
1122     __ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> 'a1 **)
1123 let joint_seq_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
1124   let hcut =
1125     joint_seq_rect_Type0 x1 x2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1126       hterm
1127   in
1128   hcut __
1129
1130 (** val joint_seq_discr :
1131     unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1132     __ **)
1133 let joint_seq_discr a1 a2 x y =
1134   Logic.eq_rect_Type2 x
1135     (match x with
1136      | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1137      | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1138      | POP a0 -> Obj.magic (fun _ dH -> dH __)
1139      | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1140      | ADDRESS (a0, a20, a3, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __)
1141      | OPACCS (a0, a10, a20, a3, a4) ->
1142        Obj.magic (fun _ dH -> dH __ __ __ __ __)
1143      | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1144      | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1145      | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1146      | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1147      | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1148      | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1149      | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1150
1151 (** val joint_seq_jmdiscr :
1152     unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq ->
1153     __ **)
1154 let joint_seq_jmdiscr a1 a2 x y =
1155   Logic.eq_rect_Type2 x
1156     (match x with
1157      | COMMENT a0 -> Obj.magic (fun _ dH -> dH __)
1158      | MOVE a0 -> Obj.magic (fun _ dH -> dH __)
1159      | POP a0 -> Obj.magic (fun _ dH -> dH __)
1160      | PUSH a0 -> Obj.magic (fun _ dH -> dH __)
1161      | ADDRESS (a0, a20, a3, a4) -> Obj.magic (fun _ dH -> dH __ __ __ __ __)
1162      | OPACCS (a0, a10, a20, a3, a4) ->
1163        Obj.magic (fun _ dH -> dH __ __ __ __ __)
1164      | OP1 (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1165      | OP2 (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1166      | CLEAR_CARRY -> Obj.magic (fun _ dH -> dH)
1167      | SET_CARRY -> Obj.magic (fun _ dH -> dH)
1168      | LOAD (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1169      | STORE (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1170      | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1171
1172 (** val get_used_registers_from_seq :
1173     unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1174     joint_seq -> Registers.register List.list **)
1175 let get_used_registers_from_seq p globals functs0 = function
1176 | COMMENT x -> List.Nil
1177 | MOVE pm -> functs0.pair_move_regs pm
1178 | POP r -> functs0.acc_a_regs r
1179 | PUSH r -> functs0.acc_a_args r
1180 | ADDRESS (x, x1, r1, r2) ->
1181   List.append (functs0.dpl_regs r1) (functs0.dph_regs r2)
1182 | OPACCS (o, r1, r2, r3, r4) ->
1183   List.append (functs0.acc_a_regs r1)
1184     (List.append (functs0.acc_b_regs r2)
1185       (List.append (functs0.acc_a_args r3) (functs0.acc_b_args r4)))
1186 | OP1 (o, r1, r2) ->
1187   List.append (functs0.acc_a_regs r1) (functs0.acc_a_regs r2)
1188 | OP2 (o, r1, r2, r3) ->
1189   List.append (functs0.acc_a_regs r1)
1190     (List.append (functs0.acc_a_args r2) (functs0.snd_args r3))
1191 | CLEAR_CARRY -> List.Nil
1192 | SET_CARRY -> List.Nil
1193 | LOAD (r1, r2, r3) ->
1194   List.append (functs0.acc_a_regs r1)
1195     (List.append (functs0.dpl_args r2) (functs0.dph_args r3))
1196 | STORE (r1, r2, r3) ->
1197   List.append (functs0.dpl_args r1)
1198     (List.append (functs0.dph_args r2) (functs0.acc_a_args r3))
1199 | Extension_seq ext -> functs0.ext_seq_regs ext
1200
1201 (** val nOOP : unserialized_params -> AST.ident List.list -> joint_seq **)
1202 let nOOP p globals =
1203   COMMENT String.EmptyString
1204
1205 (** val dpi1__o__extension_seq_to_seq__o__inject :
1206     unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1207     joint_seq Types.sig0 **)
1208 let dpi1__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1209   Extension_seq x4.Types.dpi1
1210
1211 (** val eject__o__extension_seq_to_seq__o__inject :
1212     unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
1213     Types.sig0 **)
1214 let eject__o__extension_seq_to_seq__o__inject x0 x1 x4 =
1215   Extension_seq (Types.pi1 x4)
1216
1217 (** val extension_seq_to_seq__o__inject :
1218     unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0 **)
1219 let extension_seq_to_seq__o__inject x0 x1 x3 =
1220   Extension_seq x3
1221
1222 (** val dpi1__o__extension_seq_to_seq :
1223     unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1224     joint_seq **)
1225 let dpi1__o__extension_seq_to_seq x0 x1 x3 =
1226   Extension_seq x3.Types.dpi1
1227
1228 (** val eject__o__extension_seq_to_seq :
1229     unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq **)
1230 let eject__o__extension_seq_to_seq x0 x1 x3 =
1231   Extension_seq (Types.pi1 x3)
1232
1233 type joint_step =
1234 | COST_LABEL of CostLabel.costlabel
1235 | CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
1236 | COND of __ * Graphs.label
1237 | Step_seq of joint_seq
1238
1239 (** val joint_step_rect_Type4 :
1240     unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1241     'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1242     -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1243 let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1244 | COST_LABEL x_17565 -> h_COST_LABEL x_17565
1245 | CALL (x_17568, x_17567, x_17566) -> h_CALL x_17568 x_17567 x_17566
1246 | COND (x_17570, x_17569) -> h_COND x_17570 x_17569
1247 | Step_seq x_17571 -> h_step_seq x_17571
1248
1249 (** val joint_step_rect_Type5 :
1250     unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1251     'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1252     -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1253 let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1254 | COST_LABEL x_17577 -> h_COST_LABEL x_17577
1255 | CALL (x_17580, x_17579, x_17578) -> h_CALL x_17580 x_17579 x_17578
1256 | COND (x_17582, x_17581) -> h_COND x_17582 x_17581
1257 | Step_seq x_17583 -> h_step_seq x_17583
1258
1259 (** val joint_step_rect_Type3 :
1260     unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1261     'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1262     -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1263 let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1264 | COST_LABEL x_17589 -> h_COST_LABEL x_17589
1265 | CALL (x_17592, x_17591, x_17590) -> h_CALL x_17592 x_17591 x_17590
1266 | COND (x_17594, x_17593) -> h_COND x_17594 x_17593
1267 | Step_seq x_17595 -> h_step_seq x_17595
1268
1269 (** val joint_step_rect_Type2 :
1270     unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1271     'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1272     -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1273 let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1274 | COST_LABEL x_17601 -> h_COST_LABEL x_17601
1275 | CALL (x_17604, x_17603, x_17602) -> h_CALL x_17604 x_17603 x_17602
1276 | COND (x_17606, x_17605) -> h_COND x_17606 x_17605
1277 | Step_seq x_17607 -> h_step_seq x_17607
1278
1279 (** val joint_step_rect_Type1 :
1280     unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1281     'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1282     -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1283 let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1284 | COST_LABEL x_17613 -> h_COST_LABEL x_17613
1285 | CALL (x_17616, x_17615, x_17614) -> h_CALL x_17616 x_17615 x_17614
1286 | COND (x_17618, x_17617) -> h_COND x_17618 x_17617
1287 | Step_seq x_17619 -> h_step_seq x_17619
1288
1289 (** val joint_step_rect_Type0 :
1290     unserialized_params -> AST.ident List.list -> (CostLabel.costlabel ->
1291     'a1) -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1)
1292     -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
1293 let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
1294 | COST_LABEL x_17625 -> h_COST_LABEL x_17625
1295 | CALL (x_17628, x_17627, x_17626) -> h_CALL x_17628 x_17627 x_17626
1296 | COND (x_17630, x_17629) -> h_COND x_17630 x_17629
1297 | Step_seq x_17631 -> h_step_seq x_17631
1298
1299 (** val joint_step_inv_rect_Type4 :
1300     unserialized_params -> AST.ident List.list -> joint_step ->
1301     (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1302     Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1303     -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1304 let joint_step_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
1305   let hcut = joint_step_rect_Type4 x1 x2 h1 h2 h3 h4 hterm in hcut __
1306
1307 (** val joint_step_inv_rect_Type3 :
1308     unserialized_params -> AST.ident List.list -> joint_step ->
1309     (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1310     Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1311     -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1312 let joint_step_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
1313   let hcut = joint_step_rect_Type3 x1 x2 h1 h2 h3 h4 hterm in hcut __
1314
1315 (** val joint_step_inv_rect_Type2 :
1316     unserialized_params -> AST.ident List.list -> joint_step ->
1317     (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1318     Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1319     -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1320 let joint_step_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
1321   let hcut = joint_step_rect_Type2 x1 x2 h1 h2 h3 h4 hterm in hcut __
1322
1323 (** val joint_step_inv_rect_Type1 :
1324     unserialized_params -> AST.ident List.list -> joint_step ->
1325     (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1326     Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1327     -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1328 let joint_step_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
1329   let hcut = joint_step_rect_Type1 x1 x2 h1 h2 h3 h4 hterm in hcut __
1330
1331 (** val joint_step_inv_rect_Type0 :
1332     unserialized_params -> AST.ident List.list -> joint_step ->
1333     (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
1334     Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1)
1335     -> (joint_seq -> __ -> 'a1) -> 'a1 **)
1336 let joint_step_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
1337   let hcut = joint_step_rect_Type0 x1 x2 h1 h2 h3 h4 hterm in hcut __
1338
1339 (** val joint_step_discr :
1340     unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1341     __ **)
1342 let joint_step_discr a1 a2 x y =
1343   Logic.eq_rect_Type2 x
1344     (match x with
1345      | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1346      | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1347      | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1348      | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1349
1350 (** val joint_step_jmdiscr :
1351     unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
1352     __ **)
1353 let joint_step_jmdiscr a1 a2 x y =
1354   Logic.eq_rect_Type2 x
1355     (match x with
1356      | COST_LABEL a0 -> Obj.magic (fun _ dH -> dH __)
1357      | CALL (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
1358      | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1359      | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
1360
1361 (** val get_used_registers_from_step :
1362     unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
1363     joint_step -> Registers.register List.list **)
1364 let get_used_registers_from_step p globals functs0 = function
1365 | COST_LABEL c -> List.Nil
1366 | CALL (id, args, dest) ->
1367   let r_id =
1368     match id with
1369     | Types.Inl x -> List.Nil
1370     | Types.Inr ptr ->
1371       List.append (functs0.dpl_args ptr.Types.fst)
1372         (functs0.dph_args ptr.Types.snd)
1373   in
1374   List.append r_id
1375     (List.append (functs0.f_call_args args) (functs0.f_call_dest dest))
1376 | COND (r, lbl) -> functs0.acc_a_regs r
1377 | Step_seq s -> get_used_registers_from_seq p globals functs0 s
1378
1379 (** val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1380     unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1381     joint_step Types.sig0 **)
1382 let dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1383   Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x4)
1384
1385 (** val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
1386     unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
1387     Types.sig0 **)
1388 let eject__o__extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x4 =
1389   Step_seq (eject__o__extension_seq_to_seq x0 x1 x4)
1390
1391 (** val extension_seq_to_seq__o__seq_to_step__o__inject :
1392     unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0 **)
1393 let extension_seq_to_seq__o__seq_to_step__o__inject x0 x1 x2 =
1394   Step_seq (Extension_seq x2)
1395
1396 (** val dpi1__o__seq_to_step__o__inject :
1397     unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1398     Types.dPair -> joint_step Types.sig0 **)
1399 let dpi1__o__seq_to_step__o__inject x0 x1 x4 =
1400   Step_seq x4.Types.dpi1
1401
1402 (** val eject__o__seq_to_step__o__inject :
1403     unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1404     joint_step Types.sig0 **)
1405 let eject__o__seq_to_step__o__inject x0 x1 x4 =
1406   Step_seq (Types.pi1 x4)
1407
1408 (** val seq_to_step__o__inject :
1409     unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
1410     Types.sig0 **)
1411 let seq_to_step__o__inject x0 x1 x3 =
1412   Step_seq x3
1413
1414 (** val dpi1__o__extension_seq_to_seq__o__seq_to_step :
1415     unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
1416     joint_step **)
1417 let dpi1__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1418   Step_seq (dpi1__o__extension_seq_to_seq x0 x1 x3)
1419
1420 (** val eject__o__extension_seq_to_seq__o__seq_to_step :
1421     unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step **)
1422 let eject__o__extension_seq_to_seq__o__seq_to_step x0 x1 x3 =
1423   Step_seq (eject__o__extension_seq_to_seq x0 x1 x3)
1424
1425 (** val extension_seq_to_seq__o__seq_to_step :
1426     unserialized_params -> AST.ident List.list -> __ -> joint_step **)
1427 let extension_seq_to_seq__o__seq_to_step x0 x1 x2 =
1428   Step_seq (Extension_seq x2)
1429
1430 (** val dpi1__o__seq_to_step :
1431     unserialized_params -> AST.ident List.list -> (joint_seq, 'a1)
1432     Types.dPair -> joint_step **)
1433 let dpi1__o__seq_to_step x0 x1 x3 =
1434   Step_seq x3.Types.dpi1
1435
1436 (** val eject__o__seq_to_step :
1437     unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
1438     joint_step **)
1439 let eject__o__seq_to_step x0 x1 x3 =
1440   Step_seq (Types.pi1 x3)
1441
1442 (** val step_labels :
1443     unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
1444     List.list **)
1445 let step_labels p globals = function
1446 | COST_LABEL x -> List.Nil
1447 | CALL (x, x0, x1) -> List.Nil
1448 | COND (x, l) -> List.Cons (l, List.Nil)
1449 | Step_seq s0 ->
1450   (match s0 with
1451    | COMMENT x -> List.Nil
1452    | MOVE x -> List.Nil
1453    | POP x -> List.Nil
1454    | PUSH x -> List.Nil
1455    | ADDRESS (x, x1, x2, x3) -> List.Nil
1456    | OPACCS (x, x0, x1, x2, x3) -> List.Nil
1457    | OP1 (x, x0, x1) -> List.Nil
1458    | OP2 (x, x0, x1, x2) -> List.Nil
1459    | CLEAR_CARRY -> List.Nil
1460    | SET_CARRY -> List.Nil
1461    | LOAD (x, x0, x1) -> List.Nil
1462    | STORE (x, x0, x1) -> List.Nil
1463    | Extension_seq ext -> p.ext_seq_labels ext)
1464
1465 type stmt_params = { uns_pars : uns_params;
1466                      succ_label : (__ -> Graphs.label Types.option);
1467                      has_fcond : Bool.bool }
1468
1469 (** val stmt_params_rect_Type4 :
1470     (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1471     'a1) -> stmt_params -> 'a1 **)
1472 let rec stmt_params_rect_Type4 h_mk_stmt_params x_17710 =
1473   let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1474     has_fcond0 } = x_17710
1475   in
1476   h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1477
1478 (** val stmt_params_rect_Type5 :
1479     (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1480     'a1) -> stmt_params -> 'a1 **)
1481 let rec stmt_params_rect_Type5 h_mk_stmt_params x_17712 =
1482   let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1483     has_fcond0 } = x_17712
1484   in
1485   h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1486
1487 (** val stmt_params_rect_Type3 :
1488     (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1489     'a1) -> stmt_params -> 'a1 **)
1490 let rec stmt_params_rect_Type3 h_mk_stmt_params x_17714 =
1491   let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1492     has_fcond0 } = x_17714
1493   in
1494   h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1495
1496 (** val stmt_params_rect_Type2 :
1497     (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1498     'a1) -> stmt_params -> 'a1 **)
1499 let rec stmt_params_rect_Type2 h_mk_stmt_params x_17716 =
1500   let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1501     has_fcond0 } = x_17716
1502   in
1503   h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1504
1505 (** val stmt_params_rect_Type1 :
1506     (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1507     'a1) -> stmt_params -> 'a1 **)
1508 let rec stmt_params_rect_Type1 h_mk_stmt_params x_17718 =
1509   let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1510     has_fcond0 } = x_17718
1511   in
1512   h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1513
1514 (** val stmt_params_rect_Type0 :
1515     (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
1516     'a1) -> stmt_params -> 'a1 **)
1517 let rec stmt_params_rect_Type0 h_mk_stmt_params x_17720 =
1518   let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
1519     has_fcond0 } = x_17720
1520   in
1521   h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
1522
1523 (** val uns_pars : stmt_params -> uns_params **)
1524 let rec uns_pars xxx =
1525   xxx.uns_pars
1526
1527 type succ = __
1528
1529 (** val succ_label : stmt_params -> __ -> Graphs.label Types.option **)
1530 let rec succ_label xxx =
1531   xxx.succ_label
1532
1533 (** val has_fcond : stmt_params -> Bool.bool **)
1534 let rec has_fcond xxx =
1535   xxx.has_fcond
1536
1537 (** val stmt_params_inv_rect_Type4 :
1538     stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1539     Bool.bool -> __ -> 'a1) -> 'a1 **)
1540 let stmt_params_inv_rect_Type4 hterm h1 =
1541   let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
1542
1543 (** val stmt_params_inv_rect_Type3 :
1544     stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1545     Bool.bool -> __ -> 'a1) -> 'a1 **)
1546 let stmt_params_inv_rect_Type3 hterm h1 =
1547   let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
1548
1549 (** val stmt_params_inv_rect_Type2 :
1550     stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1551     Bool.bool -> __ -> 'a1) -> 'a1 **)
1552 let stmt_params_inv_rect_Type2 hterm h1 =
1553   let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
1554
1555 (** val stmt_params_inv_rect_Type1 :
1556     stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1557     Bool.bool -> __ -> 'a1) -> 'a1 **)
1558 let stmt_params_inv_rect_Type1 hterm h1 =
1559   let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
1560
1561 (** val stmt_params_inv_rect_Type0 :
1562     stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
1563     Bool.bool -> __ -> 'a1) -> 'a1 **)
1564 let stmt_params_inv_rect_Type0 hterm h1 =
1565   let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
1566
1567 (** val stmt_params_jmdiscr : stmt_params -> stmt_params -> __ **)
1568 let stmt_params_jmdiscr x y =
1569   Logic.eq_rect_Type2 x
1570     (let { uns_pars = a0; succ_label = a2; has_fcond = a3 } = x in
1571     Obj.magic (fun _ dH -> dH __ __ __ __)) y
1572
1573 (** val uns_pars__o__u_pars : stmt_params -> unserialized_params **)
1574 let uns_pars__o__u_pars x0 =
1575   x0.uns_pars.u_pars
1576
1577 type joint_fin_step =
1578 | GOTO of Graphs.label
1579 | RETURN
1580 | TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
1581
1582 (** val joint_fin_step_rect_Type4 :
1583     unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1584     (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1585 let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
1586 | GOTO x_17744 -> h_GOTO x_17744
1587 | RETURN -> h_RETURN
1588 | TAILCALL (x_17746, x_17745) -> h_TAILCALL __ x_17746 x_17745
1589
1590 (** val joint_fin_step_rect_Type5 :
1591     unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1592     (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1593 let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
1594 | GOTO x_17752 -> h_GOTO x_17752
1595 | RETURN -> h_RETURN
1596 | TAILCALL (x_17754, x_17753) -> h_TAILCALL __ x_17754 x_17753
1597
1598 (** val joint_fin_step_rect_Type3 :
1599     unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1600     (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1601 let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
1602 | GOTO x_17760 -> h_GOTO x_17760
1603 | RETURN -> h_RETURN
1604 | TAILCALL (x_17762, x_17761) -> h_TAILCALL __ x_17762 x_17761
1605
1606 (** val joint_fin_step_rect_Type2 :
1607     unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1608     (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1609 let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
1610 | GOTO x_17768 -> h_GOTO x_17768
1611 | RETURN -> h_RETURN
1612 | TAILCALL (x_17770, x_17769) -> h_TAILCALL __ x_17770 x_17769
1613
1614 (** val joint_fin_step_rect_Type1 :
1615     unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1616     (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1617 let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
1618 | GOTO x_17776 -> h_GOTO x_17776
1619 | RETURN -> h_RETURN
1620 | TAILCALL (x_17778, x_17777) -> h_TAILCALL __ x_17778 x_17777
1621
1622 (** val joint_fin_step_rect_Type0 :
1623     unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
1624     (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
1625 let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
1626 | GOTO x_17784 -> h_GOTO x_17784
1627 | RETURN -> h_RETURN
1628 | TAILCALL (x_17786, x_17785) -> h_TAILCALL __ x_17786 x_17785
1629
1630 (** val joint_fin_step_inv_rect_Type4 :
1631     unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1632     (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1633     __ -> 'a1) -> 'a1 **)
1634 let joint_fin_step_inv_rect_Type4 x1 hterm h1 h2 h3 =
1635   let hcut = joint_fin_step_rect_Type4 x1 h1 h2 h3 hterm in hcut __
1636
1637 (** val joint_fin_step_inv_rect_Type3 :
1638     unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1639     (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1640     __ -> 'a1) -> 'a1 **)
1641 let joint_fin_step_inv_rect_Type3 x1 hterm h1 h2 h3 =
1642   let hcut = joint_fin_step_rect_Type3 x1 h1 h2 h3 hterm in hcut __
1643
1644 (** val joint_fin_step_inv_rect_Type2 :
1645     unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1646     (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1647     __ -> 'a1) -> 'a1 **)
1648 let joint_fin_step_inv_rect_Type2 x1 hterm h1 h2 h3 =
1649   let hcut = joint_fin_step_rect_Type2 x1 h1 h2 h3 hterm in hcut __
1650
1651 (** val joint_fin_step_inv_rect_Type1 :
1652     unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1653     (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1654     __ -> 'a1) -> 'a1 **)
1655 let joint_fin_step_inv_rect_Type1 x1 hterm h1 h2 h3 =
1656   let hcut = joint_fin_step_rect_Type1 x1 h1 h2 h3 hterm in hcut __
1657
1658 (** val joint_fin_step_inv_rect_Type0 :
1659     unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) ->
1660     (__ -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ ->
1661     __ -> 'a1) -> 'a1 **)
1662 let joint_fin_step_inv_rect_Type0 x1 hterm h1 h2 h3 =
1663   let hcut = joint_fin_step_rect_Type0 x1 h1 h2 h3 hterm in hcut __
1664
1665 (** val joint_fin_step_discr :
1666     unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1667 let joint_fin_step_discr a1 x y =
1668   Logic.eq_rect_Type2 x
1669     (match x with
1670      | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1671      | RETURN -> Obj.magic (fun _ dH -> dH)
1672      | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1673
1674 (** val joint_fin_step_jmdiscr :
1675     unserialized_params -> joint_fin_step -> joint_fin_step -> __ **)
1676 let joint_fin_step_jmdiscr a1 x y =
1677   Logic.eq_rect_Type2 x
1678     (match x with
1679      | GOTO a0 -> Obj.magic (fun _ dH -> dH __)
1680      | RETURN -> Obj.magic (fun _ dH -> dH)
1681      | TAILCALL (a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1682
1683 (** val fin_step_labels :
1684     unserialized_params -> joint_fin_step -> Graphs.label List.list **)
1685 let fin_step_labels p = function
1686 | GOTO l -> List.Cons (l, List.Nil)
1687 | RETURN -> List.Nil
1688 | TAILCALL (x0, x1) -> List.Nil
1689
1690 type joint_statement =
1691 | Sequential of joint_step * __
1692 | Final of joint_fin_step
1693 | FCOND of __ * Graphs.label * Graphs.label
1694
1695 (** val joint_statement_rect_Type4 :
1696     stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1697     (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1698     'a1) -> joint_statement -> 'a1 **)
1699 let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
1700 | Sequential (x_17852, x_17851) -> h_sequential x_17852 x_17851
1701 | Final x_17853 -> h_final x_17853
1702 | FCOND (x_17856, x_17855, x_17854) -> h_FCOND __ x_17856 x_17855 x_17854
1703
1704 (** val joint_statement_rect_Type5 :
1705     stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1706     (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1707     'a1) -> joint_statement -> 'a1 **)
1708 let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
1709 | Sequential (x_17863, x_17862) -> h_sequential x_17863 x_17862
1710 | Final x_17864 -> h_final x_17864
1711 | FCOND (x_17867, x_17866, x_17865) -> h_FCOND __ x_17867 x_17866 x_17865
1712
1713 (** val joint_statement_rect_Type3 :
1714     stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1715     (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1716     'a1) -> joint_statement -> 'a1 **)
1717 let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
1718 | Sequential (x_17874, x_17873) -> h_sequential x_17874 x_17873
1719 | Final x_17875 -> h_final x_17875
1720 | FCOND (x_17878, x_17877, x_17876) -> h_FCOND __ x_17878 x_17877 x_17876
1721
1722 (** val joint_statement_rect_Type2 :
1723     stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1724     (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1725     'a1) -> joint_statement -> 'a1 **)
1726 let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
1727 | Sequential (x_17885, x_17884) -> h_sequential x_17885 x_17884
1728 | Final x_17886 -> h_final x_17886
1729 | FCOND (x_17889, x_17888, x_17887) -> h_FCOND __ x_17889 x_17888 x_17887
1730
1731 (** val joint_statement_rect_Type1 :
1732     stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1733     (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1734     'a1) -> joint_statement -> 'a1 **)
1735 let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
1736 | Sequential (x_17896, x_17895) -> h_sequential x_17896 x_17895
1737 | Final x_17897 -> h_final x_17897
1738 | FCOND (x_17900, x_17899, x_17898) -> h_FCOND __ x_17900 x_17899 x_17898
1739
1740 (** val joint_statement_rect_Type0 :
1741     stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
1742     (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
1743     'a1) -> joint_statement -> 'a1 **)
1744 let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
1745 | Sequential (x_17907, x_17906) -> h_sequential x_17907 x_17906
1746 | Final x_17908 -> h_final x_17908
1747 | FCOND (x_17911, x_17910, x_17909) -> h_FCOND __ x_17911 x_17910 x_17909
1748
1749 (** val joint_statement_inv_rect_Type4 :
1750     stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1751     __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1752     Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1753 let joint_statement_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
1754   let hcut = joint_statement_rect_Type4 x1 x2 h1 h2 h3 hterm in hcut __
1755
1756 (** val joint_statement_inv_rect_Type3 :
1757     stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1758     __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1759     Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1760 let joint_statement_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
1761   let hcut = joint_statement_rect_Type3 x1 x2 h1 h2 h3 hterm in hcut __
1762
1763 (** val joint_statement_inv_rect_Type2 :
1764     stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1765     __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1766     Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1767 let joint_statement_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
1768   let hcut = joint_statement_rect_Type2 x1 x2 h1 h2 h3 hterm in hcut __
1769
1770 (** val joint_statement_inv_rect_Type1 :
1771     stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1772     __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1773     Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1774 let joint_statement_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
1775   let hcut = joint_statement_rect_Type1 x1 x2 h1 h2 h3 hterm in hcut __
1776
1777 (** val joint_statement_inv_rect_Type0 :
1778     stmt_params -> AST.ident List.list -> joint_statement -> (joint_step ->
1779     __ -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ ->
1780     Graphs.label -> Graphs.label -> __ -> 'a1) -> 'a1 **)
1781 let joint_statement_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
1782   let hcut = joint_statement_rect_Type0 x1 x2 h1 h2 h3 hterm in hcut __
1783
1784 (** val joint_statement_discr :
1785     stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1786     -> __ **)
1787 let joint_statement_discr a1 a2 x y =
1788   Logic.eq_rect_Type2 x
1789     (match x with
1790      | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1791      | Final a0 -> Obj.magic (fun _ dH -> dH __)
1792      | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1793
1794 (** val joint_statement_jmdiscr :
1795     stmt_params -> AST.ident List.list -> joint_statement -> joint_statement
1796     -> __ **)
1797 let joint_statement_jmdiscr a1 a2 x y =
1798   Logic.eq_rect_Type2 x
1799     (match x with
1800      | Sequential (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
1801      | Final a0 -> Obj.magic (fun _ dH -> dH __)
1802      | FCOND (a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1803
1804 (** val dpi1__o__fin_step_to_stmt__o__inject :
1805     stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1806     -> joint_statement Types.sig0 **)
1807 let dpi1__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1808   Final x4.Types.dpi1
1809
1810 (** val eject__o__fin_step_to_stmt__o__inject :
1811     stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1812     joint_statement Types.sig0 **)
1813 let eject__o__fin_step_to_stmt__o__inject x0 x1 x4 =
1814   Final (Types.pi1 x4)
1815
1816 (** val fin_step_to_stmt__o__inject :
1817     stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
1818     Types.sig0 **)
1819 let fin_step_to_stmt__o__inject x0 x1 x3 =
1820   Final x3
1821
1822 (** val dpi1__o__fin_step_to_stmt :
1823     stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair
1824     -> joint_statement **)
1825 let dpi1__o__fin_step_to_stmt x0 x1 x3 =
1826   Final x3.Types.dpi1
1827
1828 (** val eject__o__fin_step_to_stmt :
1829     stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
1830     joint_statement **)
1831 let eject__o__fin_step_to_stmt x0 x1 x3 =
1832   Final (Types.pi1 x3)
1833
1834 type params = { stmt_pars : stmt_params;
1835                 stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
1836                           Types.option);
1837                 point_of_label : (AST.ident List.list -> __ -> Graphs.label
1838                                  -> __ Types.option);
1839                 point_of_succ : (__ -> __ -> __) }
1840
1841 (** val params_rect_Type4 :
1842     (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1843     joint_statement Types.option) -> (AST.ident List.list -> __ ->
1844     Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1845     'a1 **)
1846 let rec params_rect_Type4 h_mk_params x_17984 =
1847   let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1848     point_of_label0; point_of_succ = point_of_succ0 } = x_17984
1849   in
1850   h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1851
1852 (** val params_rect_Type5 :
1853     (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1854     joint_statement Types.option) -> (AST.ident List.list -> __ ->
1855     Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1856     'a1 **)
1857 let rec params_rect_Type5 h_mk_params x_17986 =
1858   let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1859     point_of_label0; point_of_succ = point_of_succ0 } = x_17986
1860   in
1861   h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1862
1863 (** val params_rect_Type3 :
1864     (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1865     joint_statement Types.option) -> (AST.ident List.list -> __ ->
1866     Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1867     'a1 **)
1868 let rec params_rect_Type3 h_mk_params x_17988 =
1869   let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1870     point_of_label0; point_of_succ = point_of_succ0 } = x_17988
1871   in
1872   h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1873
1874 (** val params_rect_Type2 :
1875     (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1876     joint_statement Types.option) -> (AST.ident List.list -> __ ->
1877     Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1878     'a1 **)
1879 let rec params_rect_Type2 h_mk_params x_17990 =
1880   let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1881     point_of_label0; point_of_succ = point_of_succ0 } = x_17990
1882   in
1883   h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1884
1885 (** val params_rect_Type1 :
1886     (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1887     joint_statement Types.option) -> (AST.ident List.list -> __ ->
1888     Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1889     'a1 **)
1890 let rec params_rect_Type1 h_mk_params x_17992 =
1891   let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1892     point_of_label0; point_of_succ = point_of_succ0 } = x_17992
1893   in
1894   h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1895
1896 (** val params_rect_Type0 :
1897     (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1898     joint_statement Types.option) -> (AST.ident List.list -> __ ->
1899     Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
1900     'a1 **)
1901 let rec params_rect_Type0 h_mk_params x_17994 =
1902   let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
1903     point_of_label0; point_of_succ = point_of_succ0 } = x_17994
1904   in
1905   h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
1906
1907 (** val stmt_pars : params -> stmt_params **)
1908 let rec stmt_pars xxx =
1909   xxx.stmt_pars
1910
1911 type codeT = __
1912
1913 type code_point = __
1914
1915 (** val stmt_at :
1916     params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option **)
1917 let rec stmt_at xxx =
1918   xxx.stmt_at
1919
1920 (** val point_of_label :
1921     params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option **)
1922 let rec point_of_label xxx =
1923   xxx.point_of_label
1924
1925 (** val point_of_succ : params -> __ -> __ -> __ **)
1926 let rec point_of_succ xxx =
1927   xxx.point_of_succ
1928
1929 (** val params_inv_rect_Type4 :
1930     params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1931     joint_statement Types.option) -> (AST.ident List.list -> __ ->
1932     Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1933 let params_inv_rect_Type4 hterm h1 =
1934   let hcut = params_rect_Type4 h1 hterm in hcut __
1935
1936 (** val params_inv_rect_Type3 :
1937     params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1938     joint_statement Types.option) -> (AST.ident List.list -> __ ->
1939     Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1940 let params_inv_rect_Type3 hterm h1 =
1941   let hcut = params_rect_Type3 h1 hterm in hcut __
1942
1943 (** val params_inv_rect_Type2 :
1944     params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1945     joint_statement Types.option) -> (AST.ident List.list -> __ ->
1946     Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1947 let params_inv_rect_Type2 hterm h1 =
1948   let hcut = params_rect_Type2 h1 hterm in hcut __
1949
1950 (** val params_inv_rect_Type1 :
1951     params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1952     joint_statement Types.option) -> (AST.ident List.list -> __ ->
1953     Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1954 let params_inv_rect_Type1 hterm h1 =
1955   let hcut = params_rect_Type1 h1 hterm in hcut __
1956
1957 (** val params_inv_rect_Type0 :
1958     params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
1959     joint_statement Types.option) -> (AST.ident List.list -> __ ->
1960     Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1 **)
1961 let params_inv_rect_Type0 hterm h1 =
1962   let hcut = params_rect_Type0 h1 hterm in hcut __
1963
1964 (** val params_jmdiscr : params -> params -> __ **)
1965 let params_jmdiscr x y =
1966   Logic.eq_rect_Type2 x
1967     (let { stmt_pars = a0; stmt_at = a3; point_of_label = a4; point_of_succ =
1968        a5 } = x
1969      in
1970     Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1971
1972 (** val stmt_pars__o__uns_pars : params -> uns_params **)
1973 let stmt_pars__o__uns_pars x0 =
1974   x0.stmt_pars.uns_pars
1975
1976 (** val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params **)
1977 let stmt_pars__o__uns_pars__o__u_pars x0 =
1978   uns_pars__o__u_pars x0.stmt_pars
1979
1980 (** val code_has_point :
1981     params -> AST.ident List.list -> __ -> __ -> Bool.bool **)
1982 let code_has_point p globals c pt =
1983   match p.stmt_at globals c pt with
1984   | Types.None -> Bool.False
1985   | Types.Some x -> Bool.True
1986
1987 (** val code_has_label :
1988     params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool **)
1989 let code_has_label p globals c l =
1990   match p.point_of_label globals c l with
1991   | Types.None -> Bool.False
1992   | Types.Some pt -> code_has_point p globals c pt
1993
1994 (** val stmt_explicit_labels :
1995     stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
1996     List.list **)
1997 let stmt_explicit_labels p globals = function
1998 | Sequential (c, x) -> step_labels (uns_pars__o__u_pars p) globals c
1999 | Final c -> fin_step_labels (uns_pars__o__u_pars p) c
2000 | FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
2001
2002 (** val stmt_implicit_label :
2003     stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
2004     Types.option **)
2005 let stmt_implicit_label p globals = function
2006 | Sequential (x, s0) -> p.succ_label s0
2007 | Final x -> Types.None
2008 | FCOND (x0, x1, x2) -> Types.None
2009
2010 (** val stmt_labels :
2011     stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
2012     List.list **)
2013 let stmt_labels p g stmt =
2014   List.append
2015     (match stmt_implicit_label p g stmt with
2016      | Types.None -> List.Nil
2017      | Types.Some l -> List.Cons (l, List.Nil))
2018     (stmt_explicit_labels p g stmt)
2019
2020 (** val stmt_registers :
2021     stmt_params -> AST.ident List.list -> joint_statement ->
2022     Registers.register List.list **)
2023 let stmt_registers p globals = function
2024 | Sequential (c, x) ->
2025   get_used_registers_from_step p.uns_pars.u_pars globals p.uns_pars.functs c
2026 | Final c ->
2027   (match c with
2028    | GOTO x -> List.Nil
2029    | RETURN -> List.Nil
2030    | TAILCALL (x0, r) -> p.uns_pars.functs.f_call_args r)
2031 | FCOND (r, x0, x1) -> p.uns_pars.functs.acc_a_regs r
2032
2033 type lin_params =
2034   uns_params
2035   (* singleton inductive, whose constructor was mk_lin_params *)
2036
2037 (** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2038 let rec lin_params_rect_Type4 h_mk_lin_params x_18017 =
2039   let l_u_pars = x_18017 in h_mk_lin_params l_u_pars
2040
2041 (** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2042 let rec lin_params_rect_Type5 h_mk_lin_params x_18019 =
2043   let l_u_pars = x_18019 in h_mk_lin_params l_u_pars
2044
2045 (** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2046 let rec lin_params_rect_Type3 h_mk_lin_params x_18021 =
2047   let l_u_pars = x_18021 in h_mk_lin_params l_u_pars
2048
2049 (** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2050 let rec lin_params_rect_Type2 h_mk_lin_params x_18023 =
2051   let l_u_pars = x_18023 in h_mk_lin_params l_u_pars
2052
2053 (** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2054 let rec lin_params_rect_Type1 h_mk_lin_params x_18025 =
2055   let l_u_pars = x_18025 in h_mk_lin_params l_u_pars
2056
2057 (** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
2058 let rec lin_params_rect_Type0 h_mk_lin_params x_18027 =
2059   let l_u_pars = x_18027 in h_mk_lin_params l_u_pars
2060
2061 (** val l_u_pars : lin_params -> uns_params **)
2062 let rec l_u_pars xxx =
2063   let yyy = xxx in yyy
2064
2065 (** val lin_params_inv_rect_Type4 :
2066     lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2067 let lin_params_inv_rect_Type4 hterm h1 =
2068   let hcut = lin_params_rect_Type4 h1 hterm in hcut __
2069
2070 (** val lin_params_inv_rect_Type3 :
2071     lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2072 let lin_params_inv_rect_Type3 hterm h1 =
2073   let hcut = lin_params_rect_Type3 h1 hterm in hcut __
2074
2075 (** val lin_params_inv_rect_Type2 :
2076     lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2077 let lin_params_inv_rect_Type2 hterm h1 =
2078   let hcut = lin_params_rect_Type2 h1 hterm in hcut __
2079
2080 (** val lin_params_inv_rect_Type1 :
2081     lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2082 let lin_params_inv_rect_Type1 hterm h1 =
2083   let hcut = lin_params_rect_Type1 h1 hterm in hcut __
2084
2085 (** val lin_params_inv_rect_Type0 :
2086     lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2087 let lin_params_inv_rect_Type0 hterm h1 =
2088   let hcut = lin_params_rect_Type0 h1 hterm in hcut __
2089
2090 (** val lin_params_jmdiscr : lin_params -> lin_params -> __ **)
2091 let lin_params_jmdiscr x y =
2092   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2093
2094 (** val lin_params_to_params : lin_params -> params **)
2095 let lin_params_to_params lp =
2096   { stmt_pars = { uns_pars = (l_u_pars lp); succ_label = (fun x ->
2097     Types.None); has_fcond = Bool.True }; stmt_at =
2098     (fun globals code point ->
2099     Obj.magic
2100       (Monad.m_bind0 (Monad.max_def Option.option)
2101         (Obj.magic (List.nth_opt (Obj.magic point) (Obj.magic code)))
2102         (fun ls ->
2103         Monad.m_return0 (Monad.max_def Option.option) ls.Types.snd)));
2104     point_of_label = (fun globals c lbl ->
2105     Util.if_then_else_safe
2106       (LabelledObjects.occurs_exactly_once PreIdentifiers.LabelTag lbl
2107         (Obj.magic c)) (fun _ ->
2108       Obj.magic
2109         (Monad.m_return0 (Monad.max_def Option.option)
2110           (LabelledObjects.index_of_label PreIdentifiers.LabelTag lbl
2111             (Obj.magic c)))) (fun _ -> Types.None)); point_of_succ =
2112     (fun current x -> Obj.magic (Nat.S (Obj.magic current))) }
2113
2114 (** val lp_to_p__o__stmt_pars : lin_params -> stmt_params **)
2115 let lp_to_p__o__stmt_pars x0 =
2116   (lin_params_to_params x0).stmt_pars
2117
2118 (** val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params **)
2119 let lp_to_p__o__stmt_pars__o__uns_pars x0 =
2120   stmt_pars__o__uns_pars (lin_params_to_params x0)
2121
2122 (** val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2123     lin_params -> unserialized_params **)
2124 let lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2125   stmt_pars__o__uns_pars__o__u_pars (lin_params_to_params x0)
2126
2127 type graph_params =
2128   uns_params
2129   (* singleton inductive, whose constructor was mk_graph_params *)
2130
2131 (** val graph_params_rect_Type4 :
2132     (uns_params -> 'a1) -> graph_params -> 'a1 **)
2133 let rec graph_params_rect_Type4 h_mk_graph_params x_18043 =
2134   let g_u_pars = x_18043 in h_mk_graph_params g_u_pars
2135
2136 (** val graph_params_rect_Type5 :
2137     (uns_params -> 'a1) -> graph_params -> 'a1 **)
2138 let rec graph_params_rect_Type5 h_mk_graph_params x_18045 =
2139   let g_u_pars = x_18045 in h_mk_graph_params g_u_pars
2140
2141 (** val graph_params_rect_Type3 :
2142     (uns_params -> 'a1) -> graph_params -> 'a1 **)
2143 let rec graph_params_rect_Type3 h_mk_graph_params x_18047 =
2144   let g_u_pars = x_18047 in h_mk_graph_params g_u_pars
2145
2146 (** val graph_params_rect_Type2 :
2147     (uns_params -> 'a1) -> graph_params -> 'a1 **)
2148 let rec graph_params_rect_Type2 h_mk_graph_params x_18049 =
2149   let g_u_pars = x_18049 in h_mk_graph_params g_u_pars
2150
2151 (** val graph_params_rect_Type1 :
2152     (uns_params -> 'a1) -> graph_params -> 'a1 **)
2153 let rec graph_params_rect_Type1 h_mk_graph_params x_18051 =
2154   let g_u_pars = x_18051 in h_mk_graph_params g_u_pars
2155
2156 (** val graph_params_rect_Type0 :
2157     (uns_params -> 'a1) -> graph_params -> 'a1 **)
2158 let rec graph_params_rect_Type0 h_mk_graph_params x_18053 =
2159   let g_u_pars = x_18053 in h_mk_graph_params g_u_pars
2160
2161 (** val g_u_pars : graph_params -> uns_params **)
2162 let rec g_u_pars xxx =
2163   let yyy = xxx in yyy
2164
2165 (** val graph_params_inv_rect_Type4 :
2166     graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2167 let graph_params_inv_rect_Type4 hterm h1 =
2168   let hcut = graph_params_rect_Type4 h1 hterm in hcut __
2169
2170 (** val graph_params_inv_rect_Type3 :
2171     graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2172 let graph_params_inv_rect_Type3 hterm h1 =
2173   let hcut = graph_params_rect_Type3 h1 hterm in hcut __
2174
2175 (** val graph_params_inv_rect_Type2 :
2176     graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2177 let graph_params_inv_rect_Type2 hterm h1 =
2178   let hcut = graph_params_rect_Type2 h1 hterm in hcut __
2179
2180 (** val graph_params_inv_rect_Type1 :
2181     graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2182 let graph_params_inv_rect_Type1 hterm h1 =
2183   let hcut = graph_params_rect_Type1 h1 hterm in hcut __
2184
2185 (** val graph_params_inv_rect_Type0 :
2186     graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
2187 let graph_params_inv_rect_Type0 hterm h1 =
2188   let hcut = graph_params_rect_Type0 h1 hterm in hcut __
2189
2190 (** val graph_params_jmdiscr : graph_params -> graph_params -> __ **)
2191 let graph_params_jmdiscr x y =
2192   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
2193
2194 (** val graph_params_to_params : graph_params -> params **)
2195 let graph_params_to_params gp =
2196   { stmt_pars = { uns_pars = (g_u_pars gp); succ_label =
2197     (Obj.magic (fun x -> Types.Some x)); has_fcond = Bool.False }; stmt_at =
2198     (fun globals code ->
2199     Obj.magic (Identifiers.lookup PreIdentifiers.LabelTag (Obj.magic code)));
2200     point_of_label = (fun x x0 lbl ->
2201     Obj.magic (Monad.m_return0 (Monad.max_def Option.option) lbl));
2202     point_of_succ = (fun x lbl -> lbl) }
2203
2204 (** val gp_to_p__o__stmt_pars : graph_params -> stmt_params **)
2205 let gp_to_p__o__stmt_pars x0 =
2206   (graph_params_to_params x0).stmt_pars
2207
2208 (** val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params **)
2209 let gp_to_p__o__stmt_pars__o__uns_pars x0 =
2210   stmt_pars__o__uns_pars (graph_params_to_params x0)
2211
2212 (** val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
2213     graph_params -> unserialized_params **)
2214 let gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
2215   stmt_pars__o__uns_pars__o__u_pars (graph_params_to_params x0)
2216
2217 type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
2218                                  joint_if_runiverse : Identifiers.universe;
2219                                  joint_if_result : __; joint_if_params :
2220                                  __; joint_if_stacksize : Nat.nat;
2221                                  joint_if_local_stacksize : Nat.nat;
2222                                  joint_if_code : __; joint_if_entry :
2223                                  __ }
2224
2225 (** val joint_internal_function_rect_Type4 :
2226     params -> AST.ident List.list -> (Identifiers.universe ->
2227     Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2228     'a1) -> joint_internal_function -> 'a1 **)
2229 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_18069 =
2230   let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2231     joint_if_runiverse0; joint_if_result = joint_if_result0;
2232     joint_if_params = joint_if_params0; joint_if_stacksize =
2233     joint_if_stacksize0; joint_if_local_stacksize =
2234     joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2235     joint_if_entry = joint_if_entry0 } = x_18069
2236   in
2237   h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2238     joint_if_result0 joint_if_params0 joint_if_stacksize0
2239     joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2240
2241 (** val joint_internal_function_rect_Type5 :
2242     params -> AST.ident List.list -> (Identifiers.universe ->
2243     Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2244     'a1) -> joint_internal_function -> 'a1 **)
2245 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_18071 =
2246   let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2247     joint_if_runiverse0; joint_if_result = joint_if_result0;
2248     joint_if_params = joint_if_params0; joint_if_stacksize =
2249     joint_if_stacksize0; joint_if_local_stacksize =
2250     joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2251     joint_if_entry = joint_if_entry0 } = x_18071
2252   in
2253   h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2254     joint_if_result0 joint_if_params0 joint_if_stacksize0
2255     joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2256
2257 (** val joint_internal_function_rect_Type3 :
2258     params -> AST.ident List.list -> (Identifiers.universe ->
2259     Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2260     'a1) -> joint_internal_function -> 'a1 **)
2261 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_18073 =
2262   let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2263     joint_if_runiverse0; joint_if_result = joint_if_result0;
2264     joint_if_params = joint_if_params0; joint_if_stacksize =
2265     joint_if_stacksize0; joint_if_local_stacksize =
2266     joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2267     joint_if_entry = joint_if_entry0 } = x_18073
2268   in
2269   h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2270     joint_if_result0 joint_if_params0 joint_if_stacksize0
2271     joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2272
2273 (** val joint_internal_function_rect_Type2 :
2274     params -> AST.ident List.list -> (Identifiers.universe ->
2275     Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2276     'a1) -> joint_internal_function -> 'a1 **)
2277 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_18075 =
2278   let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2279     joint_if_runiverse0; joint_if_result = joint_if_result0;
2280     joint_if_params = joint_if_params0; joint_if_stacksize =
2281     joint_if_stacksize0; joint_if_local_stacksize =
2282     joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2283     joint_if_entry = joint_if_entry0 } = x_18075
2284   in
2285   h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2286     joint_if_result0 joint_if_params0 joint_if_stacksize0
2287     joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2288
2289 (** val joint_internal_function_rect_Type1 :
2290     params -> AST.ident List.list -> (Identifiers.universe ->
2291     Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2292     'a1) -> joint_internal_function -> 'a1 **)
2293 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_18077 =
2294   let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2295     joint_if_runiverse0; joint_if_result = joint_if_result0;
2296     joint_if_params = joint_if_params0; joint_if_stacksize =
2297     joint_if_stacksize0; joint_if_local_stacksize =
2298     joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2299     joint_if_entry = joint_if_entry0 } = x_18077
2300   in
2301   h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2302     joint_if_result0 joint_if_params0 joint_if_stacksize0
2303     joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2304
2305 (** val joint_internal_function_rect_Type0 :
2306     params -> AST.ident List.list -> (Identifiers.universe ->
2307     Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
2308     'a1) -> joint_internal_function -> 'a1 **)
2309 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_18079 =
2310   let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
2311     joint_if_runiverse0; joint_if_result = joint_if_result0;
2312     joint_if_params = joint_if_params0; joint_if_stacksize =
2313     joint_if_stacksize0; joint_if_local_stacksize =
2314     joint_if_local_stacksize0; joint_if_code = joint_if_code0;
2315     joint_if_entry = joint_if_entry0 } = x_18079
2316   in
2317   h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
2318     joint_if_result0 joint_if_params0 joint_if_stacksize0
2319     joint_if_local_stacksize0 joint_if_code0 joint_if_entry0
2320
2321 (** val joint_if_luniverse :
2322     params -> AST.ident List.list -> joint_internal_function ->
2323     Identifiers.universe **)
2324 let rec joint_if_luniverse p globals xxx =
2325   xxx.joint_if_luniverse
2326
2327 (** val joint_if_runiverse :
2328     params -> AST.ident List.list -> joint_internal_function ->
2329     Identifiers.universe **)
2330 let rec joint_if_runiverse p globals xxx =
2331   xxx.joint_if_runiverse
2332
2333 (** val joint_if_result :
2334     params -> AST.ident List.list -> joint_internal_function -> __ **)
2335 let rec joint_if_result p globals xxx =
2336   xxx.joint_if_result
2337
2338 (** val joint_if_params :
2339     params -> AST.ident List.list -> joint_internal_function -> __ **)
2340 let rec joint_if_params p globals xxx =
2341   xxx.joint_if_params
2342
2343 (** val joint_if_stacksize :
2344     params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2345 let rec joint_if_stacksize p globals xxx =
2346   xxx.joint_if_stacksize
2347
2348 (** val joint_if_local_stacksize :
2349     params -> AST.ident List.list -> joint_internal_function -> Nat.nat **)
2350 let rec joint_if_local_stacksize p globals xxx =
2351   xxx.joint_if_local_stacksize
2352
2353 (** val joint_if_code :
2354     params -> AST.ident List.list -> joint_internal_function -> __ **)
2355 let rec joint_if_code p globals xxx =
2356   xxx.joint_if_code
2357
2358 (** val joint_if_entry :
2359     params -> AST.ident List.list -> joint_internal_function -> __ **)
2360 let rec joint_if_entry p globals xxx =
2361   xxx.joint_if_entry
2362
2363 (** val joint_internal_function_inv_rect_Type4 :
2364     params -> AST.ident List.list -> joint_internal_function ->
2365     (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2366     Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2367 let joint_internal_function_inv_rect_Type4 x1 x2 hterm h1 =
2368   let hcut = joint_internal_function_rect_Type4 x1 x2 h1 hterm in hcut __
2369
2370 (** val joint_internal_function_inv_rect_Type3 :
2371     params -> AST.ident List.list -> joint_internal_function ->
2372     (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2373     Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2374 let joint_internal_function_inv_rect_Type3 x1 x2 hterm h1 =
2375   let hcut = joint_internal_function_rect_Type3 x1 x2 h1 hterm in hcut __
2376
2377 (** val joint_internal_function_inv_rect_Type2 :
2378     params -> AST.ident List.list -> joint_internal_function ->
2379     (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2380     Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2381 let joint_internal_function_inv_rect_Type2 x1 x2 hterm h1 =
2382   let hcut = joint_internal_function_rect_Type2 x1 x2 h1 hterm in hcut __
2383
2384 (** val joint_internal_function_inv_rect_Type1 :
2385     params -> AST.ident List.list -> joint_internal_function ->
2386     (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2387     Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2388 let joint_internal_function_inv_rect_Type1 x1 x2 hterm h1 =
2389   let hcut = joint_internal_function_rect_Type1 x1 x2 h1 hterm in hcut __
2390
2391 (** val joint_internal_function_inv_rect_Type0 :
2392     params -> AST.ident List.list -> joint_internal_function ->
2393     (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat ->
2394     Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2395 let joint_internal_function_inv_rect_Type0 x1 x2 hterm h1 =
2396   let hcut = joint_internal_function_rect_Type0 x1 x2 h1 hterm in hcut __
2397
2398 (** val joint_internal_function_jmdiscr :
2399     params -> AST.ident List.list -> joint_internal_function ->
2400     joint_internal_function -> __ **)
2401 let joint_internal_function_jmdiscr a1 a2 x y =
2402   Logic.eq_rect_Type2 x
2403     (let { joint_if_luniverse = a0; joint_if_runiverse = a10;
2404        joint_if_result = a20; joint_if_params = a3; joint_if_stacksize = a4;
2405        joint_if_local_stacksize = a5; joint_if_code = a6; joint_if_entry =
2406        a7 } = x
2407      in
2408     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
2409
2410 (** val good_if_rect_Type4 :
2411     params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2412     __ -> __ -> __ -> 'a1) -> 'a1 **)
2413 let rec good_if_rect_Type4 p globals def h_mk_good_if =
2414   h_mk_good_if __ __ __ __ __
2415
2416 (** val good_if_rect_Type5 :
2417     params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2418     __ -> __ -> __ -> 'a1) -> 'a1 **)
2419 let rec good_if_rect_Type5 p globals def h_mk_good_if =
2420   h_mk_good_if __ __ __ __ __
2421
2422 (** val good_if_rect_Type3 :
2423     params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2424     __ -> __ -> __ -> 'a1) -> 'a1 **)
2425 let rec good_if_rect_Type3 p globals def h_mk_good_if =
2426   h_mk_good_if __ __ __ __ __
2427
2428 (** val good_if_rect_Type2 :
2429     params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2430     __ -> __ -> __ -> 'a1) -> 'a1 **)
2431 let rec good_if_rect_Type2 p globals def h_mk_good_if =
2432   h_mk_good_if __ __ __ __ __
2433
2434 (** val good_if_rect_Type1 :
2435     params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2436     __ -> __ -> __ -> 'a1) -> 'a1 **)
2437 let rec good_if_rect_Type1 p globals def h_mk_good_if =
2438   h_mk_good_if __ __ __ __ __
2439
2440 (** val good_if_rect_Type0 :
2441     params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2442     __ -> __ -> __ -> 'a1) -> 'a1 **)
2443 let rec good_if_rect_Type0 p globals def h_mk_good_if =
2444   h_mk_good_if __ __ __ __ __
2445
2446 (** val good_if_inv_rect_Type4 :
2447     params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2448     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2449 let good_if_inv_rect_Type4 x1 x2 x3 h1 =
2450   let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
2451
2452 (** val good_if_inv_rect_Type3 :
2453     params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2454     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2455 let good_if_inv_rect_Type3 x1 x2 x3 h1 =
2456   let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
2457
2458 (** val good_if_inv_rect_Type2 :
2459     params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2460     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2461 let good_if_inv_rect_Type2 x1 x2 x3 h1 =
2462   let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
2463
2464 (** val good_if_inv_rect_Type1 :
2465     params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2466     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2467 let good_if_inv_rect_Type1 x1 x2 x3 h1 =
2468   let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
2469
2470 (** val good_if_inv_rect_Type0 :
2471     params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
2472     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
2473 let good_if_inv_rect_Type0 x1 x2 x3 h1 =
2474   let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
2475
2476 (** val good_if_discr :
2477     params -> AST.ident List.list -> joint_internal_function -> __ **)
2478 let good_if_discr a1 a2 a3 =
2479   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2480
2481 (** val good_if_jmdiscr :
2482     params -> AST.ident List.list -> joint_internal_function -> __ **)
2483 let good_if_jmdiscr a1 a2 a3 =
2484   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
2485
2486 type joint_closed_internal_function = joint_internal_function Types.sig0
2487
2488 (** val set_joint_code :
2489     AST.ident List.list -> params -> joint_internal_function -> __ -> __ ->
2490     joint_internal_function **)
2491 let set_joint_code globals pars int_fun graph entry =
2492   { joint_if_luniverse = int_fun.joint_if_luniverse; joint_if_runiverse =
2493     int_fun.joint_if_runiverse; joint_if_result = int_fun.joint_if_result;
2494     joint_if_params = int_fun.joint_if_params; joint_if_stacksize =
2495     int_fun.joint_if_stacksize; joint_if_local_stacksize =
2496     int_fun.joint_if_local_stacksize; joint_if_code = graph; joint_if_entry =
2497     entry }
2498
2499 (** val set_luniverse :
2500     params -> AST.ident List.list -> joint_internal_function ->
2501     Identifiers.universe -> joint_internal_function **)
2502 let set_luniverse globals pars p luniverse =
2503   { joint_if_luniverse = luniverse; joint_if_runiverse =
2504     p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2505     joint_if_params = p.joint_if_params; joint_if_stacksize =
2506     p.joint_if_stacksize; joint_if_local_stacksize =
2507     p.joint_if_local_stacksize; joint_if_code = p.joint_if_code;
2508     joint_if_entry = p.joint_if_entry }
2509
2510 (** val set_runiverse :
2511     params -> AST.ident List.list -> joint_internal_function ->
2512     Identifiers.universe -> joint_internal_function **)
2513 let set_runiverse globals pars p runiverse =
2514   { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2515     runiverse; joint_if_result = p.joint_if_result; joint_if_params =
2516     p.joint_if_params; joint_if_stacksize = p.joint_if_stacksize;
2517     joint_if_local_stacksize = p.joint_if_local_stacksize; joint_if_code =
2518     p.joint_if_code; joint_if_entry = p.joint_if_entry }
2519
2520 (** val add_graph :
2521     graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
2522     joint_internal_function -> joint_internal_function **)
2523 let add_graph g_pars globals l stmt p =
2524   let code =
2525     Identifiers.add PreIdentifiers.LabelTag (Obj.magic p.joint_if_code) l
2526       stmt
2527   in
2528   { joint_if_luniverse = p.joint_if_luniverse; joint_if_runiverse =
2529   p.joint_if_runiverse; joint_if_result = p.joint_if_result;
2530   joint_if_params = p.joint_if_params; joint_if_stacksize =
2531   p.joint_if_stacksize; joint_if_local_stacksize =
2532   p.joint_if_local_stacksize; joint_if_code = (Obj.magic code);
2533   joint_if_entry = p.joint_if_entry }
2534
2535 type joint_function = joint_closed_internal_function AST.fundef
2536
2537 type joint_program = { jp_functions : AST.ident List.list;
2538                        joint_prog : (joint_function, AST.init_data List.list)
2539                                     AST.program;
2540                        init_cost_label : CostLabel.costlabel }
2541
2542 (** val joint_program_rect_Type4 :
2543     params -> (AST.ident List.list -> (joint_function, AST.init_data
2544     List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2545     joint_program -> 'a1 **)
2546 let rec joint_program_rect_Type4 p h_mk_joint_program x_18121 =
2547   let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2548     init_cost_label = init_cost_label0 } = x_18121
2549   in
2550   h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2551
2552 (** val joint_program_rect_Type5 :
2553     params -> (AST.ident List.list -> (joint_function, AST.init_data
2554     List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2555     joint_program -> 'a1 **)
2556 let rec joint_program_rect_Type5 p h_mk_joint_program x_18123 =
2557   let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2558     init_cost_label = init_cost_label0 } = x_18123
2559   in
2560   h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2561
2562 (** val joint_program_rect_Type3 :
2563     params -> (AST.ident List.list -> (joint_function, AST.init_data
2564     List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2565     joint_program -> 'a1 **)
2566 let rec joint_program_rect_Type3 p h_mk_joint_program x_18125 =
2567   let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2568     init_cost_label = init_cost_label0 } = x_18125
2569   in
2570   h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2571
2572 (** val joint_program_rect_Type2 :
2573     params -> (AST.ident List.list -> (joint_function, AST.init_data
2574     List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2575     joint_program -> 'a1 **)
2576 let rec joint_program_rect_Type2 p h_mk_joint_program x_18127 =
2577   let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2578     init_cost_label = init_cost_label0 } = x_18127
2579   in
2580   h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2581
2582 (** val joint_program_rect_Type1 :
2583     params -> (AST.ident List.list -> (joint_function, AST.init_data
2584     List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2585     joint_program -> 'a1 **)
2586 let rec joint_program_rect_Type1 p h_mk_joint_program x_18129 =
2587   let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2588     init_cost_label = init_cost_label0 } = x_18129
2589   in
2590   h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2591
2592 (** val joint_program_rect_Type0 :
2593     params -> (AST.ident List.list -> (joint_function, AST.init_data
2594     List.list) AST.program -> CostLabel.costlabel -> __ -> 'a1) ->
2595     joint_program -> 'a1 **)
2596 let rec joint_program_rect_Type0 p h_mk_joint_program x_18131 =
2597   let { jp_functions = jp_functions0; joint_prog = joint_prog0;
2598     init_cost_label = init_cost_label0 } = x_18131
2599   in
2600   h_mk_joint_program jp_functions0 joint_prog0 init_cost_label0 __
2601
2602 (** val jp_functions : params -> joint_program -> AST.ident List.list **)
2603 let rec jp_functions p xxx =
2604   xxx.jp_functions
2605
2606 (** val joint_prog :
2607     params -> joint_program -> (joint_function, AST.init_data List.list)
2608     AST.program **)
2609 let rec joint_prog p xxx =
2610   xxx.joint_prog
2611
2612 (** val init_cost_label : params -> joint_program -> CostLabel.costlabel **)
2613 let rec init_cost_label p xxx =
2614   xxx.init_cost_label
2615
2616 (** val joint_program_inv_rect_Type4 :
2617     params -> joint_program -> (AST.ident List.list -> (joint_function,
2618     AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2619     -> 'a1) -> 'a1 **)
2620 let joint_program_inv_rect_Type4 x1 hterm h1 =
2621   let hcut = joint_program_rect_Type4 x1 h1 hterm in hcut __
2622
2623 (** val joint_program_inv_rect_Type3 :
2624     params -> joint_program -> (AST.ident List.list -> (joint_function,
2625     AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2626     -> 'a1) -> 'a1 **)
2627 let joint_program_inv_rect_Type3 x1 hterm h1 =
2628   let hcut = joint_program_rect_Type3 x1 h1 hterm in hcut __
2629
2630 (** val joint_program_inv_rect_Type2 :
2631     params -> joint_program -> (AST.ident List.list -> (joint_function,
2632     AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2633     -> 'a1) -> 'a1 **)
2634 let joint_program_inv_rect_Type2 x1 hterm h1 =
2635   let hcut = joint_program_rect_Type2 x1 h1 hterm in hcut __
2636
2637 (** val joint_program_inv_rect_Type1 :
2638     params -> joint_program -> (AST.ident List.list -> (joint_function,
2639     AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2640     -> 'a1) -> 'a1 **)
2641 let joint_program_inv_rect_Type1 x1 hterm h1 =
2642   let hcut = joint_program_rect_Type1 x1 h1 hterm in hcut __
2643
2644 (** val joint_program_inv_rect_Type0 :
2645     params -> joint_program -> (AST.ident List.list -> (joint_function,
2646     AST.init_data List.list) AST.program -> CostLabel.costlabel -> __ -> __
2647     -> 'a1) -> 'a1 **)
2648 let joint_program_inv_rect_Type0 x1 hterm h1 =
2649   let hcut = joint_program_rect_Type0 x1 h1 hterm in hcut __
2650
2651 (** val joint_program_discr :
2652     params -> joint_program -> joint_program -> __ **)
2653 let joint_program_discr a1 x y =
2654   Logic.eq_rect_Type2 x
2655     (let { jp_functions = a0; joint_prog = a10; init_cost_label = a2 } = x in
2656     Obj.magic (fun _ dH -> dH __ __ __ __)) y
2657
2658 (** val joint_program_jmdiscr :
2659     params -> joint_program -> joint_program -> __ **)
2660 let joint_program_jmdiscr a1 x y =
2661   Logic.eq_rect_Type2 x
2662     (let { jp_functions = a0; joint_prog = a10; init_cost_label = a2 } = x in
2663     Obj.magic (fun _ dH -> dH __ __ __ __)) y
2664
2665 (** val dpi1__o__joint_prog__o__inject :
2666     params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2667     AST.init_data List.list) AST.program Types.sig0 **)
2668 let dpi1__o__joint_prog__o__inject x0 x2 =
2669   x2.Types.dpi1.joint_prog
2670
2671 (** val eject__o__joint_prog__o__inject :
2672     params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2673     List.list) AST.program Types.sig0 **)
2674 let eject__o__joint_prog__o__inject x0 x2 =
2675   (Types.pi1 x2).joint_prog
2676
2677 (** val joint_prog__o__inject :
2678     params -> joint_program -> (joint_function, AST.init_data List.list)
2679     AST.program Types.sig0 **)
2680 let joint_prog__o__inject x0 x1 =
2681   x1.joint_prog
2682
2683 (** val dpi1__o__joint_prog :
2684     params -> (joint_program, 'a1) Types.dPair -> (joint_function,
2685     AST.init_data List.list) AST.program **)
2686 let dpi1__o__joint_prog x0 x2 =
2687   x2.Types.dpi1.joint_prog
2688
2689 (** val eject__o__joint_prog :
2690     params -> joint_program Types.sig0 -> (joint_function, AST.init_data
2691     List.list) AST.program **)
2692 let eject__o__joint_prog x0 x2 =
2693   (Types.pi1 x2).joint_prog
2694
2695 (** val prog_names : params -> joint_program -> AST.ident List.list **)
2696 let prog_names pars p =
2697   List.append (AST.prog_var_names p.joint_prog) p.jp_functions
2698
2699 (** val transform_joint_program :
2700     params -> params -> (AST.ident List.list ->
2701     joint_closed_internal_function -> joint_closed_internal_function) ->
2702     joint_program -> joint_program **)
2703 let transform_joint_program src dst trans prog_in =
2704   { jp_functions = prog_in.jp_functions; joint_prog =
2705     (AST.transform_program prog_in.joint_prog (fun vars ->
2706       AST.transf_fundef (trans (List.append vars prog_in.jp_functions))));
2707     init_cost_label = prog_in.init_cost_label }
2708
2709 type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
2710
2711 (** val stack_cost : params -> joint_program -> stack_cost_model **)
2712 let stack_cost p pr =
2713   List.foldr (fun id_fun acc ->
2714     let { Types.fst = id; Types.snd = fun0 } = id_fun in
2715     (match fun0 with
2716      | AST.Internal jif ->
2717        List.Cons ({ Types.fst = id; Types.snd =
2718          (Types.pi1 jif).joint_if_stacksize }, acc)
2719      | AST.External x -> acc)) List.Nil pr.joint_prog.AST.prog_funct
2720
2721 open Extra_bool
2722
2723 open Coqlib
2724
2725 open Values
2726
2727 open FrontEndVal
2728
2729 open GenMem
2730
2731 open FrontEndMem
2732
2733 open Globalenvs
2734
2735 (** val globals_stacksize : params -> joint_program -> Nat.nat **)
2736 let globals_stacksize pars p =
2737   List.fold Nat.plus Nat.O (fun entry -> Bool.True) (fun entry ->
2738     Globalenvs.size_init_data_list entry.Types.snd)
2739     p.joint_prog.AST.prog_vars
2740