Changeset 2797 for extracted/joint.ml


Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint.ml

    r2775 r2797  
    110110    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    111111let rec argument_rect_Type4 h_Reg h_Imm = function
    112 | Reg x_19531 -> h_Reg x_19531
    113 | Imm x_19532 -> h_Imm x_19532
     112| Reg x_19544 -> h_Reg x_19544
     113| Imm x_19545 -> h_Imm x_19545
    114114
    115115(** val argument_rect_Type5 :
    116116    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    117117let rec argument_rect_Type5 h_Reg h_Imm = function
    118 | Reg x_19536 -> h_Reg x_19536
    119 | Imm x_19537 -> h_Imm x_19537
     118| Reg x_19549 -> h_Reg x_19549
     119| Imm x_19550 -> h_Imm x_19550
    120120
    121121(** val argument_rect_Type3 :
    122122    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    123123let rec argument_rect_Type3 h_Reg h_Imm = function
    124 | Reg x_19541 -> h_Reg x_19541
    125 | Imm x_19542 -> h_Imm x_19542
     124| Reg x_19554 -> h_Reg x_19554
     125| Imm x_19555 -> h_Imm x_19555
    126126
    127127(** val argument_rect_Type2 :
    128128    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    129129let rec argument_rect_Type2 h_Reg h_Imm = function
    130 | Reg x_19546 -> h_Reg x_19546
    131 | Imm x_19547 -> h_Imm x_19547
     130| Reg x_19559 -> h_Reg x_19559
     131| Imm x_19560 -> h_Imm x_19560
    132132
    133133(** val argument_rect_Type1 :
    134134    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    135135let rec argument_rect_Type1 h_Reg h_Imm = function
    136 | Reg x_19551 -> h_Reg x_19551
    137 | Imm x_19552 -> h_Imm x_19552
     136| Reg x_19564 -> h_Reg x_19564
     137| Imm x_19565 -> h_Imm x_19565
    138138
    139139(** val argument_rect_Type0 :
    140140    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    141141let rec argument_rect_Type0 h_Reg h_Imm = function
    142 | Reg x_19556 -> h_Reg x_19556
    143 | Imm x_19557 -> h_Imm x_19557
     142| Reg x_19569 -> h_Reg x_19569
     143| Imm x_19570 -> h_Imm x_19570
    144144
    145145(** val argument_inv_rect_Type4 :
     
    324324    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    325325    unserialized_params -> 'a1 **)
    326 let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_19592 =
     326let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_19605 =
    327327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    328     x_19592
     328    x_19605
    329329  in
    330330  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    335335    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    336336    unserialized_params -> 'a1 **)
    337 let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_19594 =
     337let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_19607 =
    338338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    339     x_19594
     339    x_19607
    340340  in
    341341  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    346346    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    347347    unserialized_params -> 'a1 **)
    348 let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_19596 =
     348let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_19609 =
    349349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    350     x_19596
     350    x_19609
    351351  in
    352352  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    357357    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    358358    unserialized_params -> 'a1 **)
    359 let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_19598 =
     359let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_19611 =
    360360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    361     x_19598
     361    x_19611
    362362  in
    363363  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    368368    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    369369    unserialized_params -> 'a1 **)
    370 let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_19600 =
     370let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_19613 =
    371371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    372     x_19600
     372    x_19613
    373373  in
    374374  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    379379    __ -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
    380380    unserialized_params -> 'a1 **)
    381 let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_19602 =
     381let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_19615 =
    382382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    383     x_19602
     383    x_19615
    384384  in
    385385  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    465465    Obj.magic (fun _ dH ->
    466466      dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y
     467
     468type 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 **)
     508let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_19632 =
     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_19632
     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 **)
     531let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_19634 =
     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_19634
     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 **)
     554let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_19636 =
     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_19636
     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 **)
     577let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_19638 =
     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_19638
     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 **)
     600let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_19640 =
     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_19640
     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 **)
     623let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_19642 =
     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_19642
     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 **)
     638let 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 **)
     644let 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 **)
     650let 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 **)
     656let 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 **)
     662let 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 **)
     668let 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 **)
     674let 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 **)
     680let 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 **)
     686let 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 **)
     692let 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 **)
     698let 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 **)
     704let 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 **)
     710let 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 **)
     716let 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 **)
     730let 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 **)
     744let 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 **)
     758let 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 **)
     772let 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 **)
     786let 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    __ **)
     792let 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
     801type 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 **)
     807let rec uns_params_rect_Type4 h_mk_uns_params x_19672 =
     808  let { u_pars = u_pars0; functs = functs0 } = x_19672 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 **)
     814let rec uns_params_rect_Type5 h_mk_uns_params x_19674 =
     815  let { u_pars = u_pars0; functs = functs0 } = x_19674 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 **)
     821let rec uns_params_rect_Type3 h_mk_uns_params x_19676 =
     822  let { u_pars = u_pars0; functs = functs0 } = x_19676 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 **)
     828let rec uns_params_rect_Type2 h_mk_uns_params x_19678 =
     829  let { u_pars = u_pars0; functs = functs0 } = x_19678 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 **)
     835let rec uns_params_rect_Type1 h_mk_uns_params x_19680 =
     836  let { u_pars = u_pars0; functs = functs0 } = x_19680 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 **)
     842let rec uns_params_rect_Type0 h_mk_uns_params x_19682 =
     843  let { u_pars = u_pars0; functs = functs0 } = x_19682 in
     844  h_mk_uns_params u_pars0 functs0
     845
     846(** val u_pars : uns_params -> unserialized_params **)
     847let rec u_pars xxx =
     848  xxx.u_pars
     849
     850(** val functs : uns_params -> get_pseudo_reg_functs **)
     851let 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 **)
     857let 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 **)
     863let 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 **)
     869let 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 **)
     875let 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 **)
     881let 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 -> __ **)
     885let 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
    467889
    468890type joint_seq =
     
    489911    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    490912let 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
    491 | COMMENT x_19658 -> h_COMMENT x_19658
    492 | MOVE x_19659 -> h_MOVE x_19659
    493 | POP x_19660 -> h_POP x_19660
    494 | PUSH x_19661 -> h_PUSH x_19661
    495 | ADDRESS (i, x_19663, x_19662) -> h_ADDRESS i __ x_19663 x_19662
    496 | OPACCS (x_19669, x_19668, x_19667, x_19666, x_19665) ->
    497   h_OPACCS x_19669 x_19668 x_19667 x_19666 x_19665
    498 | OP1 (x_19672, x_19671, x_19670) -> h_OP1 x_19672 x_19671 x_19670
    499 | OP2 (x_19676, x_19675, x_19674, x_19673) ->
    500   h_OP2 x_19676 x_19675 x_19674 x_19673
     913| COMMENT x_19737 -> h_COMMENT x_19737
     914| MOVE x_19738 -> h_MOVE x_19738
     915| POP x_19739 -> h_POP x_19739
     916| PUSH x_19740 -> h_PUSH x_19740
     917| ADDRESS (i, x_19742, x_19741) -> h_ADDRESS i __ x_19742 x_19741
     918| OPACCS (x_19748, x_19747, x_19746, x_19745, x_19744) ->
     919  h_OPACCS x_19748 x_19747 x_19746 x_19745 x_19744
     920| OP1 (x_19751, x_19750, x_19749) -> h_OP1 x_19751 x_19750 x_19749
     921| OP2 (x_19755, x_19754, x_19753, x_19752) ->
     922  h_OP2 x_19755 x_19754 x_19753 x_19752
    501923| CLEAR_CARRY -> h_CLEAR_CARRY
    502924| SET_CARRY -> h_SET_CARRY
    503 | LOAD (x_19679, x_19678, x_19677) -> h_LOAD x_19679 x_19678 x_19677
    504 | STORE (x_19682, x_19681, x_19680) -> h_STORE x_19682 x_19681 x_19680
    505 | Extension_seq x_19683 -> h_extension_seq x_19683
     925| LOAD (x_19758, x_19757, x_19756) -> h_LOAD x_19758 x_19757 x_19756
     926| STORE (x_19761, x_19760, x_19759) -> h_STORE x_19761 x_19760 x_19759
     927| Extension_seq x_19762 -> h_extension_seq x_19762
    506928
    507929(** val joint_seq_rect_Type5 :
     
    513935    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    514936let 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
    515 | COMMENT x_19698 -> h_COMMENT x_19698
    516 | MOVE x_19699 -> h_MOVE x_19699
    517 | POP x_19700 -> h_POP x_19700
    518 | PUSH x_19701 -> h_PUSH x_19701
    519 | ADDRESS (i, x_19703, x_19702) -> h_ADDRESS i __ x_19703 x_19702
    520 | OPACCS (x_19709, x_19708, x_19707, x_19706, x_19705) ->
    521   h_OPACCS x_19709 x_19708 x_19707 x_19706 x_19705
    522 | OP1 (x_19712, x_19711, x_19710) -> h_OP1 x_19712 x_19711 x_19710
    523 | OP2 (x_19716, x_19715, x_19714, x_19713) ->
    524   h_OP2 x_19716 x_19715 x_19714 x_19713
     937| COMMENT x_19777 -> h_COMMENT x_19777
     938| MOVE x_19778 -> h_MOVE x_19778
     939| POP x_19779 -> h_POP x_19779
     940| PUSH x_19780 -> h_PUSH x_19780
     941| ADDRESS (i, x_19782, x_19781) -> h_ADDRESS i __ x_19782 x_19781
     942| OPACCS (x_19788, x_19787, x_19786, x_19785, x_19784) ->
     943  h_OPACCS x_19788 x_19787 x_19786 x_19785 x_19784
     944| OP1 (x_19791, x_19790, x_19789) -> h_OP1 x_19791 x_19790 x_19789
     945| OP2 (x_19795, x_19794, x_19793, x_19792) ->
     946  h_OP2 x_19795 x_19794 x_19793 x_19792
    525947| CLEAR_CARRY -> h_CLEAR_CARRY
    526948| SET_CARRY -> h_SET_CARRY
    527 | LOAD (x_19719, x_19718, x_19717) -> h_LOAD x_19719 x_19718 x_19717
    528 | STORE (x_19722, x_19721, x_19720) -> h_STORE x_19722 x_19721 x_19720
    529 | Extension_seq x_19723 -> h_extension_seq x_19723
     949| LOAD (x_19798, x_19797, x_19796) -> h_LOAD x_19798 x_19797 x_19796
     950| STORE (x_19801, x_19800, x_19799) -> h_STORE x_19801 x_19800 x_19799
     951| Extension_seq x_19802 -> h_extension_seq x_19802
    530952
    531953(** val joint_seq_rect_Type3 :
     
    537959    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    538960let 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
    539 | COMMENT x_19738 -> h_COMMENT x_19738
    540 | MOVE x_19739 -> h_MOVE x_19739
    541 | POP x_19740 -> h_POP x_19740
    542 | PUSH x_19741 -> h_PUSH x_19741
    543 | ADDRESS (i, x_19743, x_19742) -> h_ADDRESS i __ x_19743 x_19742
    544 | OPACCS (x_19749, x_19748, x_19747, x_19746, x_19745) ->
    545   h_OPACCS x_19749 x_19748 x_19747 x_19746 x_19745
    546 | OP1 (x_19752, x_19751, x_19750) -> h_OP1 x_19752 x_19751 x_19750
    547 | OP2 (x_19756, x_19755, x_19754, x_19753) ->
    548   h_OP2 x_19756 x_19755 x_19754 x_19753
     961| COMMENT x_19817 -> h_COMMENT x_19817
     962| MOVE x_19818 -> h_MOVE x_19818
     963| POP x_19819 -> h_POP x_19819
     964| PUSH x_19820 -> h_PUSH x_19820
     965| ADDRESS (i, x_19822, x_19821) -> h_ADDRESS i __ x_19822 x_19821
     966| OPACCS (x_19828, x_19827, x_19826, x_19825, x_19824) ->
     967  h_OPACCS x_19828 x_19827 x_19826 x_19825 x_19824
     968| OP1 (x_19831, x_19830, x_19829) -> h_OP1 x_19831 x_19830 x_19829
     969| OP2 (x_19835, x_19834, x_19833, x_19832) ->
     970  h_OP2 x_19835 x_19834 x_19833 x_19832
    549971| CLEAR_CARRY -> h_CLEAR_CARRY
    550972| SET_CARRY -> h_SET_CARRY
    551 | LOAD (x_19759, x_19758, x_19757) -> h_LOAD x_19759 x_19758 x_19757
    552 | STORE (x_19762, x_19761, x_19760) -> h_STORE x_19762 x_19761 x_19760
    553 | Extension_seq x_19763 -> h_extension_seq x_19763
     973| LOAD (x_19838, x_19837, x_19836) -> h_LOAD x_19838 x_19837 x_19836
     974| STORE (x_19841, x_19840, x_19839) -> h_STORE x_19841 x_19840 x_19839
     975| Extension_seq x_19842 -> h_extension_seq x_19842
    554976
    555977(** val joint_seq_rect_Type2 :
     
    561983    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    562984let 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
    563 | COMMENT x_19778 -> h_COMMENT x_19778
    564 | MOVE x_19779 -> h_MOVE x_19779
    565 | POP x_19780 -> h_POP x_19780
    566 | PUSH x_19781 -> h_PUSH x_19781
    567 | ADDRESS (i, x_19783, x_19782) -> h_ADDRESS i __ x_19783 x_19782
    568 | OPACCS (x_19789, x_19788, x_19787, x_19786, x_19785) ->
    569   h_OPACCS x_19789 x_19788 x_19787 x_19786 x_19785
    570 | OP1 (x_19792, x_19791, x_19790) -> h_OP1 x_19792 x_19791 x_19790
    571 | OP2 (x_19796, x_19795, x_19794, x_19793) ->
    572   h_OP2 x_19796 x_19795 x_19794 x_19793
     985| COMMENT x_19857 -> h_COMMENT x_19857
     986| MOVE x_19858 -> h_MOVE x_19858
     987| POP x_19859 -> h_POP x_19859
     988| PUSH x_19860 -> h_PUSH x_19860
     989| ADDRESS (i, x_19862, x_19861) -> h_ADDRESS i __ x_19862 x_19861
     990| OPACCS (x_19868, x_19867, x_19866, x_19865, x_19864) ->
     991  h_OPACCS x_19868 x_19867 x_19866 x_19865 x_19864
     992| OP1 (x_19871, x_19870, x_19869) -> h_OP1 x_19871 x_19870 x_19869
     993| OP2 (x_19875, x_19874, x_19873, x_19872) ->
     994  h_OP2 x_19875 x_19874 x_19873 x_19872
    573995| CLEAR_CARRY -> h_CLEAR_CARRY
    574996| SET_CARRY -> h_SET_CARRY
    575 | LOAD (x_19799, x_19798, x_19797) -> h_LOAD x_19799 x_19798 x_19797
    576 | STORE (x_19802, x_19801, x_19800) -> h_STORE x_19802 x_19801 x_19800
    577 | Extension_seq x_19803 -> h_extension_seq x_19803
     997| LOAD (x_19878, x_19877, x_19876) -> h_LOAD x_19878 x_19877 x_19876
     998| STORE (x_19881, x_19880, x_19879) -> h_STORE x_19881 x_19880 x_19879
     999| Extension_seq x_19882 -> h_extension_seq x_19882
    5781000
    5791001(** val joint_seq_rect_Type1 :
     
    5851007    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    5861008let 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
    587 | COMMENT x_19818 -> h_COMMENT x_19818
    588 | MOVE x_19819 -> h_MOVE x_19819
    589 | POP x_19820 -> h_POP x_19820
    590 | PUSH x_19821 -> h_PUSH x_19821
    591 | ADDRESS (i, x_19823, x_19822) -> h_ADDRESS i __ x_19823 x_19822
    592 | OPACCS (x_19829, x_19828, x_19827, x_19826, x_19825) ->
    593   h_OPACCS x_19829 x_19828 x_19827 x_19826 x_19825
    594 | OP1 (x_19832, x_19831, x_19830) -> h_OP1 x_19832 x_19831 x_19830
    595 | OP2 (x_19836, x_19835, x_19834, x_19833) ->
    596   h_OP2 x_19836 x_19835 x_19834 x_19833
     1009| COMMENT x_19897 -> h_COMMENT x_19897
     1010| MOVE x_19898 -> h_MOVE x_19898
     1011| POP x_19899 -> h_POP x_19899
     1012| PUSH x_19900 -> h_PUSH x_19900
     1013| ADDRESS (i, x_19902, x_19901) -> h_ADDRESS i __ x_19902 x_19901
     1014| OPACCS (x_19908, x_19907, x_19906, x_19905, x_19904) ->
     1015  h_OPACCS x_19908 x_19907 x_19906 x_19905 x_19904
     1016| OP1 (x_19911, x_19910, x_19909) -> h_OP1 x_19911 x_19910 x_19909
     1017| OP2 (x_19915, x_19914, x_19913, x_19912) ->
     1018  h_OP2 x_19915 x_19914 x_19913 x_19912
    5971019| CLEAR_CARRY -> h_CLEAR_CARRY
    5981020| SET_CARRY -> h_SET_CARRY
    599 | LOAD (x_19839, x_19838, x_19837) -> h_LOAD x_19839 x_19838 x_19837
    600 | STORE (x_19842, x_19841, x_19840) -> h_STORE x_19842 x_19841 x_19840
    601 | Extension_seq x_19843 -> h_extension_seq x_19843
     1021| LOAD (x_19918, x_19917, x_19916) -> h_LOAD x_19918 x_19917 x_19916
     1022| STORE (x_19921, x_19920, x_19919) -> h_STORE x_19921 x_19920 x_19919
     1023| Extension_seq x_19922 -> h_extension_seq x_19922
    6021024
    6031025(** val joint_seq_rect_Type0 :
     
    6091031    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    6101032let 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
    611 | COMMENT x_19858 -> h_COMMENT x_19858
    612 | MOVE x_19859 -> h_MOVE x_19859
    613 | POP x_19860 -> h_POP x_19860
    614 | PUSH x_19861 -> h_PUSH x_19861
    615 | ADDRESS (i, x_19863, x_19862) -> h_ADDRESS i __ x_19863 x_19862
    616 | OPACCS (x_19869, x_19868, x_19867, x_19866, x_19865) ->
    617   h_OPACCS x_19869 x_19868 x_19867 x_19866 x_19865
    618 | OP1 (x_19872, x_19871, x_19870) -> h_OP1 x_19872 x_19871 x_19870
    619 | OP2 (x_19876, x_19875, x_19874, x_19873) ->
    620   h_OP2 x_19876 x_19875 x_19874 x_19873
     1033| COMMENT x_19937 -> h_COMMENT x_19937
     1034| MOVE x_19938 -> h_MOVE x_19938
     1035| POP x_19939 -> h_POP x_19939
     1036| PUSH x_19940 -> h_PUSH x_19940
     1037| ADDRESS (i, x_19942, x_19941) -> h_ADDRESS i __ x_19942 x_19941
     1038| OPACCS (x_19948, x_19947, x_19946, x_19945, x_19944) ->
     1039  h_OPACCS x_19948 x_19947 x_19946 x_19945 x_19944
     1040| OP1 (x_19951, x_19950, x_19949) -> h_OP1 x_19951 x_19950 x_19949
     1041| OP2 (x_19955, x_19954, x_19953, x_19952) ->
     1042  h_OP2 x_19955 x_19954 x_19953 x_19952
    6211043| CLEAR_CARRY -> h_CLEAR_CARRY
    6221044| SET_CARRY -> h_SET_CARRY
    623 | LOAD (x_19879, x_19878, x_19877) -> h_LOAD x_19879 x_19878 x_19877
    624 | STORE (x_19882, x_19881, x_19880) -> h_STORE x_19882 x_19881 x_19880
    625 | Extension_seq x_19883 -> h_extension_seq x_19883
     1045| LOAD (x_19958, x_19957, x_19956) -> h_LOAD x_19958 x_19957 x_19956
     1046| STORE (x_19961, x_19960, x_19959) -> h_STORE x_19961 x_19960 x_19959
     1047| Extension_seq x_19962 -> h_extension_seq x_19962
    6261048
    6271049(** val joint_seq_inv_rect_Type4 :
     
    7421164     | Extension_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
    7431165
     1166(** val get_used_registers_from_seq :
     1167    unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
     1168    joint_seq -> Registers.register List.list **)
     1169let get_used_registers_from_seq p globals functs0 = function
     1170| COMMENT x -> List.Nil
     1171| MOVE pm -> functs0.pair_move_regs pm
     1172| POP r -> functs0.acc_a_regs r
     1173| PUSH r -> functs0.acc_a_args r
     1174| ADDRESS (i, r1, r2) ->
     1175  List.append (functs0.dpl_regs r1) (functs0.dph_regs r2)
     1176| OPACCS (o, r1, r2, r3, r4) ->
     1177  List.append (functs0.acc_a_regs r1)
     1178    (List.append (functs0.acc_b_regs r2)
     1179      (List.append (functs0.acc_a_args r3) (functs0.acc_b_args r4)))
     1180| OP1 (o, r1, r2) ->
     1181  List.append (functs0.acc_a_regs r1) (functs0.acc_a_regs r2)
     1182| OP2 (o, r1, r2, r3) ->
     1183  List.append (functs0.acc_a_regs r1)
     1184    (List.append (functs0.acc_a_args r2) (functs0.snd_args r3))
     1185| CLEAR_CARRY -> List.Nil
     1186| SET_CARRY -> List.Nil
     1187| LOAD (r1, r2, r3) ->
     1188  List.append (functs0.acc_a_regs r1)
     1189    (List.append (functs0.dpl_args r2) (functs0.dph_args r3))
     1190| STORE (r1, r2, r3) ->
     1191  List.append (functs0.dpl_args r1)
     1192    (List.append (functs0.dph_args r2) (functs0.acc_a_args r3))
     1193| Extension_seq ext -> functs0.ext_seq_regs ext
     1194
    7441195(** val nOOP : unserialized_params -> AST.ident List.list -> joint_seq **)
    7451196let nOOP p globals =
     
    7851236    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    7861237let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    787 | COST_LABEL x_20150 -> h_COST_LABEL x_20150
    788 | CALL (x_20153, x_20152, x_20151) -> h_CALL x_20153 x_20152 x_20151
    789 | COND (x_20155, x_20154) -> h_COND x_20155 x_20154
    790 | Step_seq x_20156 -> h_step_seq x_20156
     1238| COST_LABEL x_20229 -> h_COST_LABEL x_20229
     1239| CALL (x_20232, x_20231, x_20230) -> h_CALL x_20232 x_20231 x_20230
     1240| COND (x_20234, x_20233) -> h_COND x_20234 x_20233
     1241| Step_seq x_20235 -> h_step_seq x_20235
    7911242
    7921243(** val joint_step_rect_Type5 :
     
    7951246    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    7961247let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    797 | COST_LABEL x_20162 -> h_COST_LABEL x_20162
    798 | CALL (x_20165, x_20164, x_20163) -> h_CALL x_20165 x_20164 x_20163
    799 | COND (x_20167, x_20166) -> h_COND x_20167 x_20166
    800 | Step_seq x_20168 -> h_step_seq x_20168
     1248| COST_LABEL x_20241 -> h_COST_LABEL x_20241
     1249| CALL (x_20244, x_20243, x_20242) -> h_CALL x_20244 x_20243 x_20242
     1250| COND (x_20246, x_20245) -> h_COND x_20246 x_20245
     1251| Step_seq x_20247 -> h_step_seq x_20247
    8011252
    8021253(** val joint_step_rect_Type3 :
     
    8051256    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    8061257let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    807 | COST_LABEL x_20174 -> h_COST_LABEL x_20174
    808 | CALL (x_20177, x_20176, x_20175) -> h_CALL x_20177 x_20176 x_20175
    809 | COND (x_20179, x_20178) -> h_COND x_20179 x_20178
    810 | Step_seq x_20180 -> h_step_seq x_20180
     1258| COST_LABEL x_20253 -> h_COST_LABEL x_20253
     1259| CALL (x_20256, x_20255, x_20254) -> h_CALL x_20256 x_20255 x_20254
     1260| COND (x_20258, x_20257) -> h_COND x_20258 x_20257
     1261| Step_seq x_20259 -> h_step_seq x_20259
    8111262
    8121263(** val joint_step_rect_Type2 :
     
    8151266    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    8161267let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    817 | COST_LABEL x_20186 -> h_COST_LABEL x_20186
    818 | CALL (x_20189, x_20188, x_20187) -> h_CALL x_20189 x_20188 x_20187
    819 | COND (x_20191, x_20190) -> h_COND x_20191 x_20190
    820 | Step_seq x_20192 -> h_step_seq x_20192
     1268| COST_LABEL x_20265 -> h_COST_LABEL x_20265
     1269| CALL (x_20268, x_20267, x_20266) -> h_CALL x_20268 x_20267 x_20266
     1270| COND (x_20270, x_20269) -> h_COND x_20270 x_20269
     1271| Step_seq x_20271 -> h_step_seq x_20271
    8211272
    8221273(** val joint_step_rect_Type1 :
     
    8251276    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    8261277let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    827 | COST_LABEL x_20198 -> h_COST_LABEL x_20198
    828 | CALL (x_20201, x_20200, x_20199) -> h_CALL x_20201 x_20200 x_20199
    829 | COND (x_20203, x_20202) -> h_COND x_20203 x_20202
    830 | Step_seq x_20204 -> h_step_seq x_20204
     1278| COST_LABEL x_20277 -> h_COST_LABEL x_20277
     1279| CALL (x_20280, x_20279, x_20278) -> h_CALL x_20280 x_20279 x_20278
     1280| COND (x_20282, x_20281) -> h_COND x_20282 x_20281
     1281| Step_seq x_20283 -> h_step_seq x_20283
    8311282
    8321283(** val joint_step_rect_Type0 :
     
    8351286    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    8361287let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    837 | COST_LABEL x_20210 -> h_COST_LABEL x_20210
    838 | CALL (x_20213, x_20212, x_20211) -> h_CALL x_20213 x_20212 x_20211
    839 | COND (x_20215, x_20214) -> h_COND x_20215 x_20214
    840 | Step_seq x_20216 -> h_step_seq x_20216
     1288| COST_LABEL x_20289 -> h_COST_LABEL x_20289
     1289| CALL (x_20292, x_20291, x_20290) -> h_CALL x_20292 x_20291 x_20290
     1290| COND (x_20294, x_20293) -> h_COND x_20294 x_20293
     1291| Step_seq x_20295 -> h_step_seq x_20295
    8411292
    8421293(** val joint_step_inv_rect_Type4 :
     
    9011352     | COND (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
    9021353     | Step_seq a0 -> Obj.magic (fun _ dH -> dH __)) y
     1354
     1355(** val get_used_registers_from_step :
     1356    unserialized_params -> AST.ident List.list -> get_pseudo_reg_functs ->
     1357    joint_step -> Registers.register List.list **)
     1358let get_used_registers_from_step p globals functs0 = function
     1359| COST_LABEL c -> List.Nil
     1360| CALL (id, args, dest) ->
     1361  List.append (functs0.f_call_args args) (functs0.f_call_dest dest)
     1362| COND (r, lbl) -> functs0.acc_a_regs r
     1363| Step_seq s -> get_used_registers_from_seq p globals functs0 s
    9031364
    9041365(** val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
     
    9881449   | Extension_seq ext -> p.ext_seq_labels ext)
    9891450
    990 type stmt_params = { uns_pars : unserialized_params;
     1451type stmt_params = { uns_pars : uns_params;
    9911452                     succ_label : (__ -> Graphs.label Types.option);
    9921453                     has_fcond : Bool.bool }
    9931454
    9941455(** val stmt_params_rect_Type4 :
    995     (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    996     Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    997 let rec stmt_params_rect_Type4 h_mk_stmt_params x_20295 =
     1456    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
     1457    'a1) -> stmt_params -> 'a1 **)
     1458let rec stmt_params_rect_Type4 h_mk_stmt_params x_20374 =
    9981459  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    999     has_fcond0 } = x_20295
     1460    has_fcond0 } = x_20374
    10001461  in
    10011462  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
    10021463
    10031464(** val stmt_params_rect_Type5 :
    1004     (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    1005     Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    1006 let rec stmt_params_rect_Type5 h_mk_stmt_params x_20297 =
     1465    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
     1466    'a1) -> stmt_params -> 'a1 **)
     1467let rec stmt_params_rect_Type5 h_mk_stmt_params x_20376 =
    10071468  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1008     has_fcond0 } = x_20297
     1469    has_fcond0 } = x_20376
    10091470  in
    10101471  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
    10111472
    10121473(** val stmt_params_rect_Type3 :
    1013     (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    1014     Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    1015 let rec stmt_params_rect_Type3 h_mk_stmt_params x_20299 =
     1474    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
     1475    'a1) -> stmt_params -> 'a1 **)
     1476let rec stmt_params_rect_Type3 h_mk_stmt_params x_20378 =
    10161477  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1017     has_fcond0 } = x_20299
     1478    has_fcond0 } = x_20378
    10181479  in
    10191480  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
    10201481
    10211482(** val stmt_params_rect_Type2 :
    1022     (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    1023     Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    1024 let rec stmt_params_rect_Type2 h_mk_stmt_params x_20301 =
     1483    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
     1484    'a1) -> stmt_params -> 'a1 **)
     1485let rec stmt_params_rect_Type2 h_mk_stmt_params x_20380 =
    10251486  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1026     has_fcond0 } = x_20301
     1487    has_fcond0 } = x_20380
    10271488  in
    10281489  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
    10291490
    10301491(** val stmt_params_rect_Type1 :
    1031     (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    1032     Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    1033 let rec stmt_params_rect_Type1 h_mk_stmt_params x_20303 =
     1492    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
     1493    'a1) -> stmt_params -> 'a1 **)
     1494let rec stmt_params_rect_Type1 h_mk_stmt_params x_20382 =
    10341495  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1035     has_fcond0 } = x_20303
     1496    has_fcond0 } = x_20382
    10361497  in
    10371498  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
    10381499
    10391500(** val stmt_params_rect_Type0 :
    1040     (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
    1041     Bool.bool -> 'a1) -> stmt_params -> 'a1 **)
    1042 let rec stmt_params_rect_Type0 h_mk_stmt_params x_20305 =
     1501    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
     1502    'a1) -> stmt_params -> 'a1 **)
     1503let rec stmt_params_rect_Type0 h_mk_stmt_params x_20384 =
    10431504  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1044     has_fcond0 } = x_20305
     1505    has_fcond0 } = x_20384
    10451506  in
    10461507  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
    10471508
    1048 (** val uns_pars : stmt_params -> unserialized_params **)
     1509(** val uns_pars : stmt_params -> uns_params **)
    10491510let rec uns_pars xxx =
    10501511  xxx.uns_pars
     
    10611522
    10621523(** val stmt_params_inv_rect_Type4 :
    1063     stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
    1064     Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
     1524    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
     1525    Bool.bool -> __ -> 'a1) -> 'a1 **)
    10651526let stmt_params_inv_rect_Type4 hterm h1 =
    10661527  let hcut = stmt_params_rect_Type4 h1 hterm in hcut __
    10671528
    10681529(** val stmt_params_inv_rect_Type3 :
    1069     stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
    1070     Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
     1530    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
     1531    Bool.bool -> __ -> 'a1) -> 'a1 **)
    10711532let stmt_params_inv_rect_Type3 hterm h1 =
    10721533  let hcut = stmt_params_rect_Type3 h1 hterm in hcut __
    10731534
    10741535(** val stmt_params_inv_rect_Type2 :
    1075     stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
    1076     Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
     1536    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
     1537    Bool.bool -> __ -> 'a1) -> 'a1 **)
    10771538let stmt_params_inv_rect_Type2 hterm h1 =
    10781539  let hcut = stmt_params_rect_Type2 h1 hterm in hcut __
    10791540
    10801541(** val stmt_params_inv_rect_Type1 :
    1081     stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
    1082     Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
     1542    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
     1543    Bool.bool -> __ -> 'a1) -> 'a1 **)
    10831544let stmt_params_inv_rect_Type1 hterm h1 =
    10841545  let hcut = stmt_params_rect_Type1 h1 hterm in hcut __
    10851546
    10861547(** val stmt_params_inv_rect_Type0 :
    1087     stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
    1088     Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1 **)
     1548    stmt_params -> (uns_params -> __ -> (__ -> Graphs.label Types.option) ->
     1549    Bool.bool -> __ -> 'a1) -> 'a1 **)
    10891550let stmt_params_inv_rect_Type0 hterm h1 =
    10901551  let hcut = stmt_params_rect_Type0 h1 hterm in hcut __
     
    10961557    Obj.magic (fun _ dH -> dH __ __ __ __)) y
    10971558
     1559(** val uns_pars__o__u_pars : stmt_params -> unserialized_params **)
     1560let uns_pars__o__u_pars x0 =
     1561  x0.uns_pars.u_pars
     1562
    10981563type joint_fin_step =
    10991564| GOTO of Graphs.label
     
    11051570    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11061571let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
    1107 | GOTO x_20329 -> h_GOTO x_20329
     1572| GOTO x_20408 -> h_GOTO x_20408
    11081573| RETURN -> h_RETURN
    1109 | TAILCALL (x_20331, x_20330) -> h_TAILCALL __ x_20331 x_20330
     1574| TAILCALL (x_20410, x_20409) -> h_TAILCALL __ x_20410 x_20409
    11101575
    11111576(** val joint_fin_step_rect_Type5 :
     
    11131578    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11141579let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
    1115 | GOTO x_20337 -> h_GOTO x_20337
     1580| GOTO x_20416 -> h_GOTO x_20416
    11161581| RETURN -> h_RETURN
    1117 | TAILCALL (x_20339, x_20338) -> h_TAILCALL __ x_20339 x_20338
     1582| TAILCALL (x_20418, x_20417) -> h_TAILCALL __ x_20418 x_20417
    11181583
    11191584(** val joint_fin_step_rect_Type3 :
     
    11211586    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11221587let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
    1123 | GOTO x_20345 -> h_GOTO x_20345
     1588| GOTO x_20424 -> h_GOTO x_20424
    11241589| RETURN -> h_RETURN
    1125 | TAILCALL (x_20347, x_20346) -> h_TAILCALL __ x_20347 x_20346
     1590| TAILCALL (x_20426, x_20425) -> h_TAILCALL __ x_20426 x_20425
    11261591
    11271592(** val joint_fin_step_rect_Type2 :
     
    11291594    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11301595let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
    1131 | GOTO x_20353 -> h_GOTO x_20353
     1596| GOTO x_20432 -> h_GOTO x_20432
    11321597| RETURN -> h_RETURN
    1133 | TAILCALL (x_20355, x_20354) -> h_TAILCALL __ x_20355 x_20354
     1598| TAILCALL (x_20434, x_20433) -> h_TAILCALL __ x_20434 x_20433
    11341599
    11351600(** val joint_fin_step_rect_Type1 :
     
    11371602    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11381603let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
    1139 | GOTO x_20361 -> h_GOTO x_20361
     1604| GOTO x_20440 -> h_GOTO x_20440
    11401605| RETURN -> h_RETURN
    1141 | TAILCALL (x_20363, x_20362) -> h_TAILCALL __ x_20363 x_20362
     1606| TAILCALL (x_20442, x_20441) -> h_TAILCALL __ x_20442 x_20441
    11421607
    11431608(** val joint_fin_step_rect_Type0 :
     
    11451610    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    11461611let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
    1147 | GOTO x_20369 -> h_GOTO x_20369
     1612| GOTO x_20448 -> h_GOTO x_20448
    11481613| RETURN -> h_RETURN
    1149 | TAILCALL (x_20371, x_20370) -> h_TAILCALL __ x_20371 x_20370
     1614| TAILCALL (x_20450, x_20449) -> h_TAILCALL __ x_20450 x_20449
    11501615
    11511616(** val joint_fin_step_inv_rect_Type4 :
     
    12191684    'a1) -> joint_statement -> 'a1 **)
    12201685let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
    1221 | Sequential (x_20437, x_20436) -> h_sequential x_20437 x_20436
    1222 | Final x_20438 -> h_final x_20438
    1223 | FCOND (x_20441, x_20440, x_20439) -> h_FCOND __ x_20441 x_20440 x_20439
     1686| Sequential (x_20516, x_20515) -> h_sequential x_20516 x_20515
     1687| Final x_20517 -> h_final x_20517
     1688| FCOND (x_20520, x_20519, x_20518) -> h_FCOND __ x_20520 x_20519 x_20518
    12241689
    12251690(** val joint_statement_rect_Type5 :
     
    12281693    'a1) -> joint_statement -> 'a1 **)
    12291694let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
    1230 | Sequential (x_20448, x_20447) -> h_sequential x_20448 x_20447
    1231 | Final x_20449 -> h_final x_20449
    1232 | FCOND (x_20452, x_20451, x_20450) -> h_FCOND __ x_20452 x_20451 x_20450
     1695| Sequential (x_20527, x_20526) -> h_sequential x_20527 x_20526
     1696| Final x_20528 -> h_final x_20528
     1697| FCOND (x_20531, x_20530, x_20529) -> h_FCOND __ x_20531 x_20530 x_20529
    12331698
    12341699(** val joint_statement_rect_Type3 :
     
    12371702    'a1) -> joint_statement -> 'a1 **)
    12381703let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
    1239 | Sequential (x_20459, x_20458) -> h_sequential x_20459 x_20458
    1240 | Final x_20460 -> h_final x_20460
    1241 | FCOND (x_20463, x_20462, x_20461) -> h_FCOND __ x_20463 x_20462 x_20461
     1704| Sequential (x_20538, x_20537) -> h_sequential x_20538 x_20537
     1705| Final x_20539 -> h_final x_20539
     1706| FCOND (x_20542, x_20541, x_20540) -> h_FCOND __ x_20542 x_20541 x_20540
    12421707
    12431708(** val joint_statement_rect_Type2 :
     
    12461711    'a1) -> joint_statement -> 'a1 **)
    12471712let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
    1248 | Sequential (x_20470, x_20469) -> h_sequential x_20470 x_20469
    1249 | Final x_20471 -> h_final x_20471
    1250 | FCOND (x_20474, x_20473, x_20472) -> h_FCOND __ x_20474 x_20473 x_20472
     1713| Sequential (x_20549, x_20548) -> h_sequential x_20549 x_20548
     1714| Final x_20550 -> h_final x_20550
     1715| FCOND (x_20553, x_20552, x_20551) -> h_FCOND __ x_20553 x_20552 x_20551
    12511716
    12521717(** val joint_statement_rect_Type1 :
     
    12551720    'a1) -> joint_statement -> 'a1 **)
    12561721let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
    1257 | Sequential (x_20481, x_20480) -> h_sequential x_20481 x_20480
    1258 | Final x_20482 -> h_final x_20482
    1259 | FCOND (x_20485, x_20484, x_20483) -> h_FCOND __ x_20485 x_20484 x_20483
     1722| Sequential (x_20560, x_20559) -> h_sequential x_20560 x_20559
     1723| Final x_20561 -> h_final x_20561
     1724| FCOND (x_20564, x_20563, x_20562) -> h_FCOND __ x_20564 x_20563 x_20562
    12601725
    12611726(** val joint_statement_rect_Type0 :
     
    12641729    'a1) -> joint_statement -> 'a1 **)
    12651730let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
    1266 | Sequential (x_20492, x_20491) -> h_sequential x_20492 x_20491
    1267 | Final x_20493 -> h_final x_20493
    1268 | FCOND (x_20496, x_20495, x_20494) -> h_FCOND __ x_20496 x_20495 x_20494
     1731| Sequential (x_20571, x_20570) -> h_sequential x_20571 x_20570
     1732| Final x_20572 -> h_final x_20572
     1733| FCOND (x_20575, x_20574, x_20573) -> h_FCOND __ x_20575 x_20574 x_20573
    12691734
    12701735(** val joint_statement_inv_rect_Type4 :
     
    13651830    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    13661831    'a1 **)
    1367 let rec params_rect_Type4 h_mk_params x_20569 =
     1832let rec params_rect_Type4 h_mk_params x_20648 =
    13681833  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1369     point_of_label0; point_of_succ = point_of_succ0 } = x_20569
     1834    point_of_label0; point_of_succ = point_of_succ0 } = x_20648
    13701835  in
    13711836  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    13761841    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    13771842    'a1 **)
    1378 let rec params_rect_Type5 h_mk_params x_20571 =
     1843let rec params_rect_Type5 h_mk_params x_20650 =
    13791844  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1380     point_of_label0; point_of_succ = point_of_succ0 } = x_20571
     1845    point_of_label0; point_of_succ = point_of_succ0 } = x_20650
    13811846  in
    13821847  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    13871852    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    13881853    'a1 **)
    1389 let rec params_rect_Type3 h_mk_params x_20573 =
     1854let rec params_rect_Type3 h_mk_params x_20652 =
    13901855  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1391     point_of_label0; point_of_succ = point_of_succ0 } = x_20573
     1856    point_of_label0; point_of_succ = point_of_succ0 } = x_20652
    13921857  in
    13931858  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    13981863    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    13991864    'a1 **)
    1400 let rec params_rect_Type2 h_mk_params x_20575 =
     1865let rec params_rect_Type2 h_mk_params x_20654 =
    14011866  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1402     point_of_label0; point_of_succ = point_of_succ0 } = x_20575
     1867    point_of_label0; point_of_succ = point_of_succ0 } = x_20654
    14031868  in
    14041869  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    14091874    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    14101875    'a1 **)
    1411 let rec params_rect_Type1 h_mk_params x_20577 =
     1876let rec params_rect_Type1 h_mk_params x_20656 =
    14121877  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1413     point_of_label0; point_of_succ = point_of_succ0 } = x_20577
     1878    point_of_label0; point_of_succ = point_of_succ0 } = x_20656
    14141879  in
    14151880  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    14201885    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    14211886    'a1 **)
    1422 let rec params_rect_Type0 h_mk_params x_20579 =
     1887let rec params_rect_Type0 h_mk_params x_20658 =
    14231888  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1424     point_of_label0; point_of_succ = point_of_succ0 } = x_20579
     1889    point_of_label0; point_of_succ = point_of_succ0 } = x_20658
    14251890  in
    14261891  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    14911956    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
    14921957
    1493 (** val stmt_pars__o__uns_pars : params -> unserialized_params **)
     1958(** val stmt_pars__o__uns_pars : params -> uns_params **)
    14941959let stmt_pars__o__uns_pars x0 =
    14951960  x0.stmt_pars.uns_pars
     1961
     1962(** val stmt_pars__o__uns_pars__o__u_pars : params -> unserialized_params **)
     1963let stmt_pars__o__uns_pars__o__u_pars x0 =
     1964  uns_pars__o__u_pars x0.stmt_pars
    14961965
    14971966(** val code_has_point :
     
    15131982    List.list **)
    15141983let stmt_explicit_labels p globals = function
    1515 | Sequential (c, x) -> step_labels p.uns_pars globals c
    1516 | Final c -> fin_step_labels p.uns_pars c
     1984| Sequential (c, x) -> step_labels (uns_pars__o__u_pars p) globals c
     1985| Final c -> fin_step_labels (uns_pars__o__u_pars p) c
    15171986| FCOND (x0, l1, l2) -> List.Cons (l1, (List.Cons (l2, List.Nil)))
    15181987
     
    15352004    (stmt_explicit_labels p g stmt)
    15362005
     2006(** val stmt_registers :
     2007    stmt_params -> AST.ident List.list -> joint_statement ->
     2008    Registers.register List.list **)
     2009let stmt_registers p globals = function
     2010| Sequential (c, x) ->
     2011  get_used_registers_from_step p.uns_pars.u_pars globals p.uns_pars.functs c
     2012| Final c ->
     2013  (match c with
     2014   | GOTO x -> List.Nil
     2015   | RETURN -> List.Nil
     2016   | TAILCALL (x0, r) -> p.uns_pars.functs.f_call_args r)
     2017| FCOND (r, x0, x1) -> p.uns_pars.functs.acc_a_regs r
     2018
    15372019type lin_params =
    1538   unserialized_params
     2020  uns_params
    15392021  (* singleton inductive, whose constructor was mk_lin_params *)
    15402022
    1541 (** val lin_params_rect_Type4 :
    1542     (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1543 let rec lin_params_rect_Type4 h_mk_lin_params x_20602 =
    1544   let l_u_pars = x_20602 in h_mk_lin_params l_u_pars
    1545 
    1546 (** val lin_params_rect_Type5 :
    1547     (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1548 let rec lin_params_rect_Type5 h_mk_lin_params x_20604 =
    1549   let l_u_pars = x_20604 in h_mk_lin_params l_u_pars
    1550 
    1551 (** val lin_params_rect_Type3 :
    1552     (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1553 let rec lin_params_rect_Type3 h_mk_lin_params x_20606 =
    1554   let l_u_pars = x_20606 in h_mk_lin_params l_u_pars
    1555 
    1556 (** val lin_params_rect_Type2 :
    1557     (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1558 let rec lin_params_rect_Type2 h_mk_lin_params x_20608 =
    1559   let l_u_pars = x_20608 in h_mk_lin_params l_u_pars
    1560 
    1561 (** val lin_params_rect_Type1 :
    1562     (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1563 let rec lin_params_rect_Type1 h_mk_lin_params x_20610 =
    1564   let l_u_pars = x_20610 in h_mk_lin_params l_u_pars
    1565 
    1566 (** val lin_params_rect_Type0 :
    1567     (unserialized_params -> 'a1) -> lin_params -> 'a1 **)
    1568 let rec lin_params_rect_Type0 h_mk_lin_params x_20612 =
    1569   let l_u_pars = x_20612 in h_mk_lin_params l_u_pars
    1570 
    1571 (** val l_u_pars : lin_params -> unserialized_params **)
     2023(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
     2024let rec lin_params_rect_Type4 h_mk_lin_params x_20681 =
     2025  let l_u_pars = x_20681 in h_mk_lin_params l_u_pars
     2026
     2027(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
     2028let rec lin_params_rect_Type5 h_mk_lin_params x_20683 =
     2029  let l_u_pars = x_20683 in h_mk_lin_params l_u_pars
     2030
     2031(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
     2032let rec lin_params_rect_Type3 h_mk_lin_params x_20685 =
     2033  let l_u_pars = x_20685 in h_mk_lin_params l_u_pars
     2034
     2035(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
     2036let rec lin_params_rect_Type2 h_mk_lin_params x_20687 =
     2037  let l_u_pars = x_20687 in h_mk_lin_params l_u_pars
     2038
     2039(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
     2040let rec lin_params_rect_Type1 h_mk_lin_params x_20689 =
     2041  let l_u_pars = x_20689 in h_mk_lin_params l_u_pars
     2042
     2043(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
     2044let rec lin_params_rect_Type0 h_mk_lin_params x_20691 =
     2045  let l_u_pars = x_20691 in h_mk_lin_params l_u_pars
     2046
     2047(** val l_u_pars : lin_params -> uns_params **)
    15722048let rec l_u_pars xxx =
    15732049  let yyy = xxx in yyy
    15742050
    15752051(** val lin_params_inv_rect_Type4 :
    1576     lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
     2052    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
    15772053let lin_params_inv_rect_Type4 hterm h1 =
    15782054  let hcut = lin_params_rect_Type4 h1 hterm in hcut __
    15792055
    15802056(** val lin_params_inv_rect_Type3 :
    1581     lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
     2057    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
    15822058let lin_params_inv_rect_Type3 hterm h1 =
    15832059  let hcut = lin_params_rect_Type3 h1 hterm in hcut __
    15842060
    15852061(** val lin_params_inv_rect_Type2 :
    1586     lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
     2062    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
    15872063let lin_params_inv_rect_Type2 hterm h1 =
    15882064  let hcut = lin_params_rect_Type2 h1 hterm in hcut __
    15892065
    15902066(** val lin_params_inv_rect_Type1 :
    1591     lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
     2067    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
    15922068let lin_params_inv_rect_Type1 hterm h1 =
    15932069  let hcut = lin_params_rect_Type1 h1 hterm in hcut __
    15942070
    15952071(** val lin_params_inv_rect_Type0 :
    1596     lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
     2072    lin_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
    15972073let lin_params_inv_rect_Type0 hterm h1 =
    15982074  let hcut = lin_params_rect_Type0 h1 hterm in hcut __
     
    16262102  (lin_params_to_params x0).stmt_pars
    16272103
    1628 (** val lp_to_p__o__stmt_pars__o__uns_pars :
    1629     lin_params -> unserialized_params **)
     2104(** val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> uns_params **)
    16302105let lp_to_p__o__stmt_pars__o__uns_pars x0 =
    16312106  stmt_pars__o__uns_pars (lin_params_to_params x0)
    16322107
     2108(** val lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
     2109    lin_params -> unserialized_params **)
     2110let lp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
     2111  stmt_pars__o__uns_pars__o__u_pars (lin_params_to_params x0)
     2112
    16332113type graph_params =
    1634   unserialized_params
     2114  uns_params
    16352115  (* singleton inductive, whose constructor was mk_graph_params *)
    16362116
    16372117(** val graph_params_rect_Type4 :
    1638     (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1639 let rec graph_params_rect_Type4 h_mk_graph_params x_20628 =
    1640   let g_u_pars = x_20628 in h_mk_graph_params g_u_pars
     2118    (uns_params -> 'a1) -> graph_params -> 'a1 **)
     2119let rec graph_params_rect_Type4 h_mk_graph_params x_20707 =
     2120  let g_u_pars = x_20707 in h_mk_graph_params g_u_pars
    16412121
    16422122(** val graph_params_rect_Type5 :
    1643     (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1644 let rec graph_params_rect_Type5 h_mk_graph_params x_20630 =
    1645   let g_u_pars = x_20630 in h_mk_graph_params g_u_pars
     2123    (uns_params -> 'a1) -> graph_params -> 'a1 **)
     2124let rec graph_params_rect_Type5 h_mk_graph_params x_20709 =
     2125  let g_u_pars = x_20709 in h_mk_graph_params g_u_pars
    16462126
    16472127(** val graph_params_rect_Type3 :
    1648     (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1649 let rec graph_params_rect_Type3 h_mk_graph_params x_20632 =
    1650   let g_u_pars = x_20632 in h_mk_graph_params g_u_pars
     2128    (uns_params -> 'a1) -> graph_params -> 'a1 **)
     2129let rec graph_params_rect_Type3 h_mk_graph_params x_20711 =
     2130  let g_u_pars = x_20711 in h_mk_graph_params g_u_pars
    16512131
    16522132(** val graph_params_rect_Type2 :
    1653     (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1654 let rec graph_params_rect_Type2 h_mk_graph_params x_20634 =
    1655   let g_u_pars = x_20634 in h_mk_graph_params g_u_pars
     2133    (uns_params -> 'a1) -> graph_params -> 'a1 **)
     2134let rec graph_params_rect_Type2 h_mk_graph_params x_20713 =
     2135  let g_u_pars = x_20713 in h_mk_graph_params g_u_pars
    16562136
    16572137(** val graph_params_rect_Type1 :
    1658     (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1659 let rec graph_params_rect_Type1 h_mk_graph_params x_20636 =
    1660   let g_u_pars = x_20636 in h_mk_graph_params g_u_pars
     2138    (uns_params -> 'a1) -> graph_params -> 'a1 **)
     2139let rec graph_params_rect_Type1 h_mk_graph_params x_20715 =
     2140  let g_u_pars = x_20715 in h_mk_graph_params g_u_pars
    16612141
    16622142(** val graph_params_rect_Type0 :
    1663     (unserialized_params -> 'a1) -> graph_params -> 'a1 **)
    1664 let rec graph_params_rect_Type0 h_mk_graph_params x_20638 =
    1665   let g_u_pars = x_20638 in h_mk_graph_params g_u_pars
    1666 
    1667 (** val g_u_pars : graph_params -> unserialized_params **)
     2143    (uns_params -> 'a1) -> graph_params -> 'a1 **)
     2144let rec graph_params_rect_Type0 h_mk_graph_params x_20717 =
     2145  let g_u_pars = x_20717 in h_mk_graph_params g_u_pars
     2146
     2147(** val g_u_pars : graph_params -> uns_params **)
    16682148let rec g_u_pars xxx =
    16692149  let yyy = xxx in yyy
    16702150
    16712151(** val graph_params_inv_rect_Type4 :
    1672     graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
     2152    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
    16732153let graph_params_inv_rect_Type4 hterm h1 =
    16742154  let hcut = graph_params_rect_Type4 h1 hterm in hcut __
    16752155
    16762156(** val graph_params_inv_rect_Type3 :
    1677     graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
     2157    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
    16782158let graph_params_inv_rect_Type3 hterm h1 =
    16792159  let hcut = graph_params_rect_Type3 h1 hterm in hcut __
    16802160
    16812161(** val graph_params_inv_rect_Type2 :
    1682     graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
     2162    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
    16832163let graph_params_inv_rect_Type2 hterm h1 =
    16842164  let hcut = graph_params_rect_Type2 h1 hterm in hcut __
    16852165
    16862166(** val graph_params_inv_rect_Type1 :
    1687     graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
     2167    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
    16882168let graph_params_inv_rect_Type1 hterm h1 =
    16892169  let hcut = graph_params_rect_Type1 h1 hterm in hcut __
    16902170
    16912171(** val graph_params_inv_rect_Type0 :
    1692     graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1 **)
     2172    graph_params -> (uns_params -> __ -> 'a1) -> 'a1 **)
    16932173let graph_params_inv_rect_Type0 hterm h1 =
    16942174  let hcut = graph_params_rect_Type0 h1 hterm in hcut __
     
    17122192  (graph_params_to_params x0).stmt_pars
    17132193
    1714 (** val gp_to_p__o__stmt_pars__o__uns_pars :
    1715     graph_params -> unserialized_params **)
     2194(** val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> uns_params **)
    17162195let gp_to_p__o__stmt_pars__o__uns_pars x0 =
    17172196  stmt_pars__o__uns_pars (graph_params_to_params x0)
     2197
     2198(** val gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars :
     2199    graph_params -> unserialized_params **)
     2200let gp_to_p__o__stmt_pars__o__uns_pars__o__u_pars x0 =
     2201  stmt_pars__o__uns_pars__o__u_pars (graph_params_to_params x0)
    17182202
    17192203type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
     
    17282212    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    17292213    'a1) -> joint_internal_function -> 'a1 **)
    1730 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20654 =
     2214let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20733 =
    17312215  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    17322216    joint_if_runiverse0; joint_if_result = joint_if_result0;
    17332217    joint_if_params = joint_if_params0; joint_if_stacksize =
    17342218    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1735     joint_if_entry0 } = x_20654
     2219    joint_if_entry0 } = x_20733
    17362220  in
    17372221  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    17432227    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    17442228    'a1) -> joint_internal_function -> 'a1 **)
    1745 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20656 =
     2229let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20735 =
    17462230  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    17472231    joint_if_runiverse0; joint_if_result = joint_if_result0;
    17482232    joint_if_params = joint_if_params0; joint_if_stacksize =
    17492233    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1750     joint_if_entry0 } = x_20656
     2234    joint_if_entry0 } = x_20735
    17512235  in
    17522236  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    17582242    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    17592243    'a1) -> joint_internal_function -> 'a1 **)
    1760 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20658 =
     2244let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20737 =
    17612245  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    17622246    joint_if_runiverse0; joint_if_result = joint_if_result0;
    17632247    joint_if_params = joint_if_params0; joint_if_stacksize =
    17642248    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1765     joint_if_entry0 } = x_20658
     2249    joint_if_entry0 } = x_20737
    17662250  in
    17672251  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    17732257    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    17742258    'a1) -> joint_internal_function -> 'a1 **)
    1775 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20660 =
     2259let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20739 =
    17762260  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    17772261    joint_if_runiverse0; joint_if_result = joint_if_result0;
    17782262    joint_if_params = joint_if_params0; joint_if_stacksize =
    17792263    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1780     joint_if_entry0 } = x_20660
     2264    joint_if_entry0 } = x_20739
    17812265  in
    17822266  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    17882272    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    17892273    'a1) -> joint_internal_function -> 'a1 **)
    1790 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20662 =
     2274let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20741 =
    17912275  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    17922276    joint_if_runiverse0; joint_if_result = joint_if_result0;
    17932277    joint_if_params = joint_if_params0; joint_if_stacksize =
    17942278    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1795     joint_if_entry0 } = x_20662
     2279    joint_if_entry0 } = x_20741
    17962280  in
    17972281  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    18032287    Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 ->
    18042288    'a1) -> joint_internal_function -> 'a1 **)
    1805 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20664 =
     2289let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20743 =
    18062290  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    18072291    joint_if_runiverse0; joint_if_result = joint_if_result0;
    18082292    joint_if_params = joint_if_params0; joint_if_stacksize =
    18092293    joint_if_stacksize0; joint_if_code = joint_if_code0; joint_if_entry =
    1810     joint_if_entry0 } = x_20664
     2294    joint_if_entry0 } = x_20743
    18112295  in
    18122296  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    18992383(** val good_if_rect_Type4 :
    19002384    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    1901     __ -> __ -> 'a1) -> 'a1 **)
     2385    __ -> __ -> __ -> 'a1) -> 'a1 **)
    19022386let rec good_if_rect_Type4 p globals def h_mk_good_if =
    1903   h_mk_good_if __ __ __ __
     2387  h_mk_good_if __ __ __ __ __
    19042388
    19052389(** val good_if_rect_Type5 :
    19062390    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    1907     __ -> __ -> 'a1) -> 'a1 **)
     2391    __ -> __ -> __ -> 'a1) -> 'a1 **)
    19082392let rec good_if_rect_Type5 p globals def h_mk_good_if =
    1909   h_mk_good_if __ __ __ __
     2393  h_mk_good_if __ __ __ __ __
    19102394
    19112395(** val good_if_rect_Type3 :
    19122396    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    1913     __ -> __ -> 'a1) -> 'a1 **)
     2397    __ -> __ -> __ -> 'a1) -> 'a1 **)
    19142398let rec good_if_rect_Type3 p globals def h_mk_good_if =
    1915   h_mk_good_if __ __ __ __
     2399  h_mk_good_if __ __ __ __ __
    19162400
    19172401(** val good_if_rect_Type2 :
    19182402    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    1919     __ -> __ -> 'a1) -> 'a1 **)
     2403    __ -> __ -> __ -> 'a1) -> 'a1 **)
    19202404let rec good_if_rect_Type2 p globals def h_mk_good_if =
    1921   h_mk_good_if __ __ __ __
     2405  h_mk_good_if __ __ __ __ __
    19222406
    19232407(** val good_if_rect_Type1 :
    19242408    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    1925     __ -> __ -> 'a1) -> 'a1 **)
     2409    __ -> __ -> __ -> 'a1) -> 'a1 **)
    19262410let rec good_if_rect_Type1 p globals def h_mk_good_if =
    1927   h_mk_good_if __ __ __ __
     2411  h_mk_good_if __ __ __ __ __
    19282412
    19292413(** val good_if_rect_Type0 :
    19302414    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    1931     __ -> __ -> 'a1) -> 'a1 **)
     2415    __ -> __ -> __ -> 'a1) -> 'a1 **)
    19322416let rec good_if_rect_Type0 p globals def h_mk_good_if =
    1933   h_mk_good_if __ __ __ __
     2417  h_mk_good_if __ __ __ __ __
    19342418
    19352419(** val good_if_inv_rect_Type4 :
    19362420    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    1937     __ -> __ -> __ -> 'a1) -> 'a1 **)
     2421    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    19382422let good_if_inv_rect_Type4 x1 x2 x3 h1 =
    19392423  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
     
    19412425(** val good_if_inv_rect_Type3 :
    19422426    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    1943     __ -> __ -> __ -> 'a1) -> 'a1 **)
     2427    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    19442428let good_if_inv_rect_Type3 x1 x2 x3 h1 =
    19452429  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
     
    19472431(** val good_if_inv_rect_Type2 :
    19482432    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    1949     __ -> __ -> __ -> 'a1) -> 'a1 **)
     2433    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    19502434let good_if_inv_rect_Type2 x1 x2 x3 h1 =
    19512435  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
     
    19532437(** val good_if_inv_rect_Type1 :
    19542438    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    1955     __ -> __ -> __ -> 'a1) -> 'a1 **)
     2439    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    19562440let good_if_inv_rect_Type1 x1 x2 x3 h1 =
    19572441  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
     
    19592443(** val good_if_inv_rect_Type0 :
    19602444    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    1961     __ -> __ -> __ -> 'a1) -> 'a1 **)
     2445    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    19622446let good_if_inv_rect_Type0 x1 x2 x3 h1 =
    19632447  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
     
    19662450    params -> AST.ident List.list -> joint_internal_function -> __ **)
    19672451let good_if_discr a1 a2 a3 =
    1968   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
     2452  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
    19692453
    19702454(** val good_if_jmdiscr :
    19712455    params -> AST.ident List.list -> joint_internal_function -> __ **)
    19722456let good_if_jmdiscr a1 a2 a3 =
    1973   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
     2457  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
    19742458
    19752459type joint_closed_internal_function = joint_internal_function Types.sig0
Note: See TracChangeset for help on using the changeset viewer.