Changeset 2951 for extracted/joint.ml


Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint.ml

    r2873 r2951  
    110110    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    111111let rec argument_rect_Type4 h_Reg h_Imm = function
    112 | Reg x_19830 -> h_Reg x_19830
    113 | Imm x_19831 -> h_Imm x_19831
     112| Reg x_16908 -> h_Reg x_16908
     113| Imm x_16909 -> h_Imm x_16909
    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_19835 -> h_Reg x_19835
    119 | Imm x_19836 -> h_Imm x_19836
     118| Reg x_16913 -> h_Reg x_16913
     119| Imm x_16914 -> h_Imm x_16914
    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_19840 -> h_Reg x_19840
    125 | Imm x_19841 -> h_Imm x_19841
     124| Reg x_16918 -> h_Reg x_16918
     125| Imm x_16919 -> h_Imm x_16919
    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_19845 -> h_Reg x_19845
    131 | Imm x_19846 -> h_Imm x_19846
     130| Reg x_16923 -> h_Reg x_16923
     131| Imm x_16924 -> h_Imm x_16924
    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_19850 -> h_Reg x_19850
    137 | Imm x_19851 -> h_Imm x_19851
     136| Reg x_16928 -> h_Reg x_16928
     137| Imm x_16929 -> h_Imm x_16929
    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_19855 -> h_Reg x_19855
    143 | Imm x_19856 -> h_Imm x_19856
     142| Reg x_16933 -> h_Reg x_16933
     143| Imm x_16934 -> h_Imm x_16934
    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_19891 =
     326let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_16969 =
    327327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    328     x_19891
     328    x_16969
    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_19893 =
     337let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_16971 =
    338338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    339     x_19893
     339    x_16971
    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_19895 =
     348let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_16973 =
    349349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    350     x_19895
     350    x_16973
    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_19897 =
     359let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_16975 =
    360360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    361     x_19897
     361    x_16975
    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_19899 =
     370let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_16977 =
    371371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    372     x_19899
     372    x_16977
    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_19901 =
     381let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_16979 =
    382382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    383     x_19901
     383    x_16979
    384384  in
    385385  h_mk_unserialized_params __ __ __ __ __ __ __ __ __ __ __ __ __
     
    506506    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    507507    'a1 **)
    508 let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_19918 =
     508let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_16996 =
    509509  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    510510    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    512512    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    513513    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    514     params_regs0 } = x_19918
     514    params_regs0 } = x_16996
    515515  in
    516516  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    529529    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    530530    'a1 **)
    531 let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_19920 =
     531let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_16998 =
    532532  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    533533    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    535535    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    536536    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    537     params_regs0 } = x_19920
     537    params_regs0 } = x_16998
    538538  in
    539539  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    552552    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    553553    'a1 **)
    554 let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_19922 =
     554let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_17000 =
    555555  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    556556    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    558558    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    559559    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    560     params_regs0 } = x_19922
     560    params_regs0 } = x_17000
    561561  in
    562562  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    575575    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    576576    'a1 **)
    577 let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_19924 =
     577let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_17002 =
    578578  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    579579    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    581581    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    582582    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    583     params_regs0 } = x_19924
     583    params_regs0 } = x_17002
    584584  in
    585585  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    598598    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    599599    'a1 **)
    600 let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_19926 =
     600let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_17004 =
    601601  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    602602    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    604604    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    605605    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    606     params_regs0 } = x_19926
     606    params_regs0 } = x_17004
    607607  in
    608608  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    621621    (__ -> Registers.register List.list) -> 'a1) -> get_pseudo_reg_functs ->
    622622    'a1 **)
    623 let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_19928 =
     623let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_17006 =
    624624  let { acc_a_regs = acc_a_regs0; acc_b_regs = acc_b_regs0; acc_a_args =
    625625    acc_a_args0; acc_b_args = acc_b_args0; dpl_regs = dpl_regs0; dph_regs =
     
    627627    snd_args0; pair_move_regs = pair_move_regs0; f_call_args = f_call_args0;
    628628    f_call_dest = f_call_dest0; ext_seq_regs = ext_seq_regs0; params_regs =
    629     params_regs0 } = x_19928
     629    params_regs0 } = x_17006
    630630  in
    631631  h_mk_get_pseudo_reg_functs acc_a_regs0 acc_b_regs0 acc_a_args0 acc_b_args0
     
    805805    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    806806    'a1 **)
    807 let rec uns_params_rect_Type4 h_mk_uns_params x_19958 =
    808   let { u_pars = u_pars0; functs = functs0 } = x_19958 in
     807let rec uns_params_rect_Type4 h_mk_uns_params x_17036 =
     808  let { u_pars = u_pars0; functs = functs0 } = x_17036 in
    809809  h_mk_uns_params u_pars0 functs0
    810810
     
    812812    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    813813    'a1 **)
    814 let rec uns_params_rect_Type5 h_mk_uns_params x_19960 =
    815   let { u_pars = u_pars0; functs = functs0 } = x_19960 in
     814let rec uns_params_rect_Type5 h_mk_uns_params x_17038 =
     815  let { u_pars = u_pars0; functs = functs0 } = x_17038 in
    816816  h_mk_uns_params u_pars0 functs0
    817817
     
    819819    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    820820    'a1 **)
    821 let rec uns_params_rect_Type3 h_mk_uns_params x_19962 =
    822   let { u_pars = u_pars0; functs = functs0 } = x_19962 in
     821let rec uns_params_rect_Type3 h_mk_uns_params x_17040 =
     822  let { u_pars = u_pars0; functs = functs0 } = x_17040 in
    823823  h_mk_uns_params u_pars0 functs0
    824824
     
    826826    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    827827    'a1 **)
    828 let rec uns_params_rect_Type2 h_mk_uns_params x_19964 =
    829   let { u_pars = u_pars0; functs = functs0 } = x_19964 in
     828let rec uns_params_rect_Type2 h_mk_uns_params x_17042 =
     829  let { u_pars = u_pars0; functs = functs0 } = x_17042 in
    830830  h_mk_uns_params u_pars0 functs0
    831831
     
    833833    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    834834    'a1 **)
    835 let rec uns_params_rect_Type1 h_mk_uns_params x_19966 =
    836   let { u_pars = u_pars0; functs = functs0 } = x_19966 in
     835let rec uns_params_rect_Type1 h_mk_uns_params x_17044 =
     836  let { u_pars = u_pars0; functs = functs0 } = x_17044 in
    837837  h_mk_uns_params u_pars0 functs0
    838838
     
    840840    (unserialized_params -> get_pseudo_reg_functs -> 'a1) -> uns_params ->
    841841    'a1 **)
    842 let rec uns_params_rect_Type0 h_mk_uns_params x_19968 =
    843   let { u_pars = u_pars0; functs = functs0 } = x_19968 in
     842let rec uns_params_rect_Type0 h_mk_uns_params x_17046 =
     843  let { u_pars = u_pars0; functs = functs0 } = x_17046 in
    844844  h_mk_uns_params u_pars0 functs0
    845845
     
    911911    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    912912let 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_20023 -> h_COMMENT x_20023
    914 | MOVE x_20024 -> h_MOVE x_20024
    915 | POP x_20025 -> h_POP x_20025
    916 | PUSH x_20026 -> h_PUSH x_20026
    917 | ADDRESS (i, x_20028, x_20027) -> h_ADDRESS i __ x_20028 x_20027
    918 | OPACCS (x_20034, x_20033, x_20032, x_20031, x_20030) ->
    919   h_OPACCS x_20034 x_20033 x_20032 x_20031 x_20030
    920 | OP1 (x_20037, x_20036, x_20035) -> h_OP1 x_20037 x_20036 x_20035
    921 | OP2 (x_20041, x_20040, x_20039, x_20038) ->
    922   h_OP2 x_20041 x_20040 x_20039 x_20038
     913| COMMENT x_17101 -> h_COMMENT x_17101
     914| MOVE x_17102 -> h_MOVE x_17102
     915| POP x_17103 -> h_POP x_17103
     916| PUSH x_17104 -> h_PUSH x_17104
     917| ADDRESS (i, x_17106, x_17105) -> h_ADDRESS i __ x_17106 x_17105
     918| OPACCS (x_17112, x_17111, x_17110, x_17109, x_17108) ->
     919  h_OPACCS x_17112 x_17111 x_17110 x_17109 x_17108
     920| OP1 (x_17115, x_17114, x_17113) -> h_OP1 x_17115 x_17114 x_17113
     921| OP2 (x_17119, x_17118, x_17117, x_17116) ->
     922  h_OP2 x_17119 x_17118 x_17117 x_17116
    923923| CLEAR_CARRY -> h_CLEAR_CARRY
    924924| SET_CARRY -> h_SET_CARRY
    925 | LOAD (x_20044, x_20043, x_20042) -> h_LOAD x_20044 x_20043 x_20042
    926 | STORE (x_20047, x_20046, x_20045) -> h_STORE x_20047 x_20046 x_20045
    927 | Extension_seq x_20048 -> h_extension_seq x_20048
     925| LOAD (x_17122, x_17121, x_17120) -> h_LOAD x_17122 x_17121 x_17120
     926| STORE (x_17125, x_17124, x_17123) -> h_STORE x_17125 x_17124 x_17123
     927| Extension_seq x_17126 -> h_extension_seq x_17126
    928928
    929929(** val joint_seq_rect_Type5 :
     
    935935    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    936936let 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
    937 | COMMENT x_20063 -> h_COMMENT x_20063
    938 | MOVE x_20064 -> h_MOVE x_20064
    939 | POP x_20065 -> h_POP x_20065
    940 | PUSH x_20066 -> h_PUSH x_20066
    941 | ADDRESS (i, x_20068, x_20067) -> h_ADDRESS i __ x_20068 x_20067
    942 | OPACCS (x_20074, x_20073, x_20072, x_20071, x_20070) ->
    943   h_OPACCS x_20074 x_20073 x_20072 x_20071 x_20070
    944 | OP1 (x_20077, x_20076, x_20075) -> h_OP1 x_20077 x_20076 x_20075
    945 | OP2 (x_20081, x_20080, x_20079, x_20078) ->
    946   h_OP2 x_20081 x_20080 x_20079 x_20078
     937| COMMENT x_17141 -> h_COMMENT x_17141
     938| MOVE x_17142 -> h_MOVE x_17142
     939| POP x_17143 -> h_POP x_17143
     940| PUSH x_17144 -> h_PUSH x_17144
     941| ADDRESS (i, x_17146, x_17145) -> h_ADDRESS i __ x_17146 x_17145
     942| OPACCS (x_17152, x_17151, x_17150, x_17149, x_17148) ->
     943  h_OPACCS x_17152 x_17151 x_17150 x_17149 x_17148
     944| OP1 (x_17155, x_17154, x_17153) -> h_OP1 x_17155 x_17154 x_17153
     945| OP2 (x_17159, x_17158, x_17157, x_17156) ->
     946  h_OP2 x_17159 x_17158 x_17157 x_17156
    947947| CLEAR_CARRY -> h_CLEAR_CARRY
    948948| SET_CARRY -> h_SET_CARRY
    949 | LOAD (x_20084, x_20083, x_20082) -> h_LOAD x_20084 x_20083 x_20082
    950 | STORE (x_20087, x_20086, x_20085) -> h_STORE x_20087 x_20086 x_20085
    951 | Extension_seq x_20088 -> h_extension_seq x_20088
     949| LOAD (x_17162, x_17161, x_17160) -> h_LOAD x_17162 x_17161 x_17160
     950| STORE (x_17165, x_17164, x_17163) -> h_STORE x_17165 x_17164 x_17163
     951| Extension_seq x_17166 -> h_extension_seq x_17166
    952952
    953953(** val joint_seq_rect_Type3 :
     
    959959    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    960960let 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
    961 | COMMENT x_20103 -> h_COMMENT x_20103
    962 | MOVE x_20104 -> h_MOVE x_20104
    963 | POP x_20105 -> h_POP x_20105
    964 | PUSH x_20106 -> h_PUSH x_20106
    965 | ADDRESS (i, x_20108, x_20107) -> h_ADDRESS i __ x_20108 x_20107
    966 | OPACCS (x_20114, x_20113, x_20112, x_20111, x_20110) ->
    967   h_OPACCS x_20114 x_20113 x_20112 x_20111 x_20110
    968 | OP1 (x_20117, x_20116, x_20115) -> h_OP1 x_20117 x_20116 x_20115
    969 | OP2 (x_20121, x_20120, x_20119, x_20118) ->
    970   h_OP2 x_20121 x_20120 x_20119 x_20118
     961| COMMENT x_17181 -> h_COMMENT x_17181
     962| MOVE x_17182 -> h_MOVE x_17182
     963| POP x_17183 -> h_POP x_17183
     964| PUSH x_17184 -> h_PUSH x_17184
     965| ADDRESS (i, x_17186, x_17185) -> h_ADDRESS i __ x_17186 x_17185
     966| OPACCS (x_17192, x_17191, x_17190, x_17189, x_17188) ->
     967  h_OPACCS x_17192 x_17191 x_17190 x_17189 x_17188
     968| OP1 (x_17195, x_17194, x_17193) -> h_OP1 x_17195 x_17194 x_17193
     969| OP2 (x_17199, x_17198, x_17197, x_17196) ->
     970  h_OP2 x_17199 x_17198 x_17197 x_17196
    971971| CLEAR_CARRY -> h_CLEAR_CARRY
    972972| SET_CARRY -> h_SET_CARRY
    973 | LOAD (x_20124, x_20123, x_20122) -> h_LOAD x_20124 x_20123 x_20122
    974 | STORE (x_20127, x_20126, x_20125) -> h_STORE x_20127 x_20126 x_20125
    975 | Extension_seq x_20128 -> h_extension_seq x_20128
     973| LOAD (x_17202, x_17201, x_17200) -> h_LOAD x_17202 x_17201 x_17200
     974| STORE (x_17205, x_17204, x_17203) -> h_STORE x_17205 x_17204 x_17203
     975| Extension_seq x_17206 -> h_extension_seq x_17206
    976976
    977977(** val joint_seq_rect_Type2 :
     
    983983    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    984984let 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
    985 | COMMENT x_20143 -> h_COMMENT x_20143
    986 | MOVE x_20144 -> h_MOVE x_20144
    987 | POP x_20145 -> h_POP x_20145
    988 | PUSH x_20146 -> h_PUSH x_20146
    989 | ADDRESS (i, x_20148, x_20147) -> h_ADDRESS i __ x_20148 x_20147
    990 | OPACCS (x_20154, x_20153, x_20152, x_20151, x_20150) ->
    991   h_OPACCS x_20154 x_20153 x_20152 x_20151 x_20150
    992 | OP1 (x_20157, x_20156, x_20155) -> h_OP1 x_20157 x_20156 x_20155
    993 | OP2 (x_20161, x_20160, x_20159, x_20158) ->
    994   h_OP2 x_20161 x_20160 x_20159 x_20158
     985| COMMENT x_17221 -> h_COMMENT x_17221
     986| MOVE x_17222 -> h_MOVE x_17222
     987| POP x_17223 -> h_POP x_17223
     988| PUSH x_17224 -> h_PUSH x_17224
     989| ADDRESS (i, x_17226, x_17225) -> h_ADDRESS i __ x_17226 x_17225
     990| OPACCS (x_17232, x_17231, x_17230, x_17229, x_17228) ->
     991  h_OPACCS x_17232 x_17231 x_17230 x_17229 x_17228
     992| OP1 (x_17235, x_17234, x_17233) -> h_OP1 x_17235 x_17234 x_17233
     993| OP2 (x_17239, x_17238, x_17237, x_17236) ->
     994  h_OP2 x_17239 x_17238 x_17237 x_17236
    995995| CLEAR_CARRY -> h_CLEAR_CARRY
    996996| SET_CARRY -> h_SET_CARRY
    997 | LOAD (x_20164, x_20163, x_20162) -> h_LOAD x_20164 x_20163 x_20162
    998 | STORE (x_20167, x_20166, x_20165) -> h_STORE x_20167 x_20166 x_20165
    999 | Extension_seq x_20168 -> h_extension_seq x_20168
     997| LOAD (x_17242, x_17241, x_17240) -> h_LOAD x_17242 x_17241 x_17240
     998| STORE (x_17245, x_17244, x_17243) -> h_STORE x_17245 x_17244 x_17243
     999| Extension_seq x_17246 -> h_extension_seq x_17246
    10001000
    10011001(** val joint_seq_rect_Type1 :
     
    10071007    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    10081008let 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
    1009 | COMMENT x_20183 -> h_COMMENT x_20183
    1010 | MOVE x_20184 -> h_MOVE x_20184
    1011 | POP x_20185 -> h_POP x_20185
    1012 | PUSH x_20186 -> h_PUSH x_20186
    1013 | ADDRESS (i, x_20188, x_20187) -> h_ADDRESS i __ x_20188 x_20187
    1014 | OPACCS (x_20194, x_20193, x_20192, x_20191, x_20190) ->
    1015   h_OPACCS x_20194 x_20193 x_20192 x_20191 x_20190
    1016 | OP1 (x_20197, x_20196, x_20195) -> h_OP1 x_20197 x_20196 x_20195
    1017 | OP2 (x_20201, x_20200, x_20199, x_20198) ->
    1018   h_OP2 x_20201 x_20200 x_20199 x_20198
     1009| COMMENT x_17261 -> h_COMMENT x_17261
     1010| MOVE x_17262 -> h_MOVE x_17262
     1011| POP x_17263 -> h_POP x_17263
     1012| PUSH x_17264 -> h_PUSH x_17264
     1013| ADDRESS (i, x_17266, x_17265) -> h_ADDRESS i __ x_17266 x_17265
     1014| OPACCS (x_17272, x_17271, x_17270, x_17269, x_17268) ->
     1015  h_OPACCS x_17272 x_17271 x_17270 x_17269 x_17268
     1016| OP1 (x_17275, x_17274, x_17273) -> h_OP1 x_17275 x_17274 x_17273
     1017| OP2 (x_17279, x_17278, x_17277, x_17276) ->
     1018  h_OP2 x_17279 x_17278 x_17277 x_17276
    10191019| CLEAR_CARRY -> h_CLEAR_CARRY
    10201020| SET_CARRY -> h_SET_CARRY
    1021 | LOAD (x_20204, x_20203, x_20202) -> h_LOAD x_20204 x_20203 x_20202
    1022 | STORE (x_20207, x_20206, x_20205) -> h_STORE x_20207 x_20206 x_20205
    1023 | Extension_seq x_20208 -> h_extension_seq x_20208
     1021| LOAD (x_17282, x_17281, x_17280) -> h_LOAD x_17282 x_17281 x_17280
     1022| STORE (x_17285, x_17284, x_17283) -> h_STORE x_17285 x_17284 x_17283
     1023| Extension_seq x_17286 -> h_extension_seq x_17286
    10241024
    10251025(** val joint_seq_rect_Type0 :
     
    10311031    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    10321032let 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
    1033 | COMMENT x_20223 -> h_COMMENT x_20223
    1034 | MOVE x_20224 -> h_MOVE x_20224
    1035 | POP x_20225 -> h_POP x_20225
    1036 | PUSH x_20226 -> h_PUSH x_20226
    1037 | ADDRESS (i, x_20228, x_20227) -> h_ADDRESS i __ x_20228 x_20227
    1038 | OPACCS (x_20234, x_20233, x_20232, x_20231, x_20230) ->
    1039   h_OPACCS x_20234 x_20233 x_20232 x_20231 x_20230
    1040 | OP1 (x_20237, x_20236, x_20235) -> h_OP1 x_20237 x_20236 x_20235
    1041 | OP2 (x_20241, x_20240, x_20239, x_20238) ->
    1042   h_OP2 x_20241 x_20240 x_20239 x_20238
     1033| COMMENT x_17301 -> h_COMMENT x_17301
     1034| MOVE x_17302 -> h_MOVE x_17302
     1035| POP x_17303 -> h_POP x_17303
     1036| PUSH x_17304 -> h_PUSH x_17304
     1037| ADDRESS (i, x_17306, x_17305) -> h_ADDRESS i __ x_17306 x_17305
     1038| OPACCS (x_17312, x_17311, x_17310, x_17309, x_17308) ->
     1039  h_OPACCS x_17312 x_17311 x_17310 x_17309 x_17308
     1040| OP1 (x_17315, x_17314, x_17313) -> h_OP1 x_17315 x_17314 x_17313
     1041| OP2 (x_17319, x_17318, x_17317, x_17316) ->
     1042  h_OP2 x_17319 x_17318 x_17317 x_17316
    10431043| CLEAR_CARRY -> h_CLEAR_CARRY
    10441044| SET_CARRY -> h_SET_CARRY
    1045 | LOAD (x_20244, x_20243, x_20242) -> h_LOAD x_20244 x_20243 x_20242
    1046 | STORE (x_20247, x_20246, x_20245) -> h_STORE x_20247 x_20246 x_20245
    1047 | Extension_seq x_20248 -> h_extension_seq x_20248
     1045| LOAD (x_17322, x_17321, x_17320) -> h_LOAD x_17322 x_17321 x_17320
     1046| STORE (x_17325, x_17324, x_17323) -> h_STORE x_17325 x_17324 x_17323
     1047| Extension_seq x_17326 -> h_extension_seq x_17326
    10481048
    10491049(** val joint_seq_inv_rect_Type4 :
     
    12361236    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12371237let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1238 | COST_LABEL x_20515 -> h_COST_LABEL x_20515
    1239 | CALL (x_20518, x_20517, x_20516) -> h_CALL x_20518 x_20517 x_20516
    1240 | COND (x_20520, x_20519) -> h_COND x_20520 x_20519
    1241 | Step_seq x_20521 -> h_step_seq x_20521
     1238| COST_LABEL x_17593 -> h_COST_LABEL x_17593
     1239| CALL (x_17596, x_17595, x_17594) -> h_CALL x_17596 x_17595 x_17594
     1240| COND (x_17598, x_17597) -> h_COND x_17598 x_17597
     1241| Step_seq x_17599 -> h_step_seq x_17599
    12421242
    12431243(** val joint_step_rect_Type5 :
     
    12461246    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12471247let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1248 | COST_LABEL x_20527 -> h_COST_LABEL x_20527
    1249 | CALL (x_20530, x_20529, x_20528) -> h_CALL x_20530 x_20529 x_20528
    1250 | COND (x_20532, x_20531) -> h_COND x_20532 x_20531
    1251 | Step_seq x_20533 -> h_step_seq x_20533
     1248| COST_LABEL x_17605 -> h_COST_LABEL x_17605
     1249| CALL (x_17608, x_17607, x_17606) -> h_CALL x_17608 x_17607 x_17606
     1250| COND (x_17610, x_17609) -> h_COND x_17610 x_17609
     1251| Step_seq x_17611 -> h_step_seq x_17611
    12521252
    12531253(** val joint_step_rect_Type3 :
     
    12561256    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12571257let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1258 | COST_LABEL x_20539 -> h_COST_LABEL x_20539
    1259 | CALL (x_20542, x_20541, x_20540) -> h_CALL x_20542 x_20541 x_20540
    1260 | COND (x_20544, x_20543) -> h_COND x_20544 x_20543
    1261 | Step_seq x_20545 -> h_step_seq x_20545
     1258| COST_LABEL x_17617 -> h_COST_LABEL x_17617
     1259| CALL (x_17620, x_17619, x_17618) -> h_CALL x_17620 x_17619 x_17618
     1260| COND (x_17622, x_17621) -> h_COND x_17622 x_17621
     1261| Step_seq x_17623 -> h_step_seq x_17623
    12621262
    12631263(** val joint_step_rect_Type2 :
     
    12661266    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12671267let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1268 | COST_LABEL x_20551 -> h_COST_LABEL x_20551
    1269 | CALL (x_20554, x_20553, x_20552) -> h_CALL x_20554 x_20553 x_20552
    1270 | COND (x_20556, x_20555) -> h_COND x_20556 x_20555
    1271 | Step_seq x_20557 -> h_step_seq x_20557
     1268| COST_LABEL x_17629 -> h_COST_LABEL x_17629
     1269| CALL (x_17632, x_17631, x_17630) -> h_CALL x_17632 x_17631 x_17630
     1270| COND (x_17634, x_17633) -> h_COND x_17634 x_17633
     1271| Step_seq x_17635 -> h_step_seq x_17635
    12721272
    12731273(** val joint_step_rect_Type1 :
     
    12761276    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12771277let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1278 | COST_LABEL x_20563 -> h_COST_LABEL x_20563
    1279 | CALL (x_20566, x_20565, x_20564) -> h_CALL x_20566 x_20565 x_20564
    1280 | COND (x_20568, x_20567) -> h_COND x_20568 x_20567
    1281 | Step_seq x_20569 -> h_step_seq x_20569
     1278| COST_LABEL x_17641 -> h_COST_LABEL x_17641
     1279| CALL (x_17644, x_17643, x_17642) -> h_CALL x_17644 x_17643 x_17642
     1280| COND (x_17646, x_17645) -> h_COND x_17646 x_17645
     1281| Step_seq x_17647 -> h_step_seq x_17647
    12821282
    12831283(** val joint_step_rect_Type0 :
     
    12861286    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12871287let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1288 | COST_LABEL x_20575 -> h_COST_LABEL x_20575
    1289 | CALL (x_20578, x_20577, x_20576) -> h_CALL x_20578 x_20577 x_20576
    1290 | COND (x_20580, x_20579) -> h_COND x_20580 x_20579
    1291 | Step_seq x_20581 -> h_step_seq x_20581
     1288| COST_LABEL x_17653 -> h_COST_LABEL x_17653
     1289| CALL (x_17656, x_17655, x_17654) -> h_CALL x_17656 x_17655 x_17654
     1290| COND (x_17658, x_17657) -> h_COND x_17658 x_17657
     1291| Step_seq x_17659 -> h_step_seq x_17659
    12921292
    12931293(** val joint_step_inv_rect_Type4 :
     
    14641464    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14651465    'a1) -> stmt_params -> 'a1 **)
    1466 let rec stmt_params_rect_Type4 h_mk_stmt_params x_20660 =
     1466let rec stmt_params_rect_Type4 h_mk_stmt_params x_17738 =
    14671467  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1468     has_fcond0 } = x_20660
     1468    has_fcond0 } = x_17738
    14691469  in
    14701470  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14731473    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14741474    'a1) -> stmt_params -> 'a1 **)
    1475 let rec stmt_params_rect_Type5 h_mk_stmt_params x_20662 =
     1475let rec stmt_params_rect_Type5 h_mk_stmt_params x_17740 =
    14761476  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1477     has_fcond0 } = x_20662
     1477    has_fcond0 } = x_17740
    14781478  in
    14791479  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14821482    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14831483    'a1) -> stmt_params -> 'a1 **)
    1484 let rec stmt_params_rect_Type3 h_mk_stmt_params x_20664 =
     1484let rec stmt_params_rect_Type3 h_mk_stmt_params x_17742 =
    14851485  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1486     has_fcond0 } = x_20664
     1486    has_fcond0 } = x_17742
    14871487  in
    14881488  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14911491    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14921492    'a1) -> stmt_params -> 'a1 **)
    1493 let rec stmt_params_rect_Type2 h_mk_stmt_params x_20666 =
     1493let rec stmt_params_rect_Type2 h_mk_stmt_params x_17744 =
    14941494  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1495     has_fcond0 } = x_20666
     1495    has_fcond0 } = x_17744
    14961496  in
    14971497  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15001500    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    15011501    'a1) -> stmt_params -> 'a1 **)
    1502 let rec stmt_params_rect_Type1 h_mk_stmt_params x_20668 =
     1502let rec stmt_params_rect_Type1 h_mk_stmt_params x_17746 =
    15031503  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1504     has_fcond0 } = x_20668
     1504    has_fcond0 } = x_17746
    15051505  in
    15061506  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15091509    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    15101510    'a1) -> stmt_params -> 'a1 **)
    1511 let rec stmt_params_rect_Type0 h_mk_stmt_params x_20670 =
     1511let rec stmt_params_rect_Type0 h_mk_stmt_params x_17748 =
    15121512  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1513     has_fcond0 } = x_20670
     1513    has_fcond0 } = x_17748
    15141514  in
    15151515  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15781578    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15791579let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
    1580 | GOTO x_20694 -> h_GOTO x_20694
     1580| GOTO x_17772 -> h_GOTO x_17772
    15811581| RETURN -> h_RETURN
    1582 | TAILCALL (x_20696, x_20695) -> h_TAILCALL __ x_20696 x_20695
     1582| TAILCALL (x_17774, x_17773) -> h_TAILCALL __ x_17774 x_17773
    15831583
    15841584(** val joint_fin_step_rect_Type5 :
     
    15861586    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15871587let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
    1588 | GOTO x_20702 -> h_GOTO x_20702
     1588| GOTO x_17780 -> h_GOTO x_17780
    15891589| RETURN -> h_RETURN
    1590 | TAILCALL (x_20704, x_20703) -> h_TAILCALL __ x_20704 x_20703
     1590| TAILCALL (x_17782, x_17781) -> h_TAILCALL __ x_17782 x_17781
    15911591
    15921592(** val joint_fin_step_rect_Type3 :
     
    15941594    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15951595let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
    1596 | GOTO x_20710 -> h_GOTO x_20710
     1596| GOTO x_17788 -> h_GOTO x_17788
    15971597| RETURN -> h_RETURN
    1598 | TAILCALL (x_20712, x_20711) -> h_TAILCALL __ x_20712 x_20711
     1598| TAILCALL (x_17790, x_17789) -> h_TAILCALL __ x_17790 x_17789
    15991599
    16001600(** val joint_fin_step_rect_Type2 :
     
    16021602    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16031603let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
    1604 | GOTO x_20718 -> h_GOTO x_20718
     1604| GOTO x_17796 -> h_GOTO x_17796
    16051605| RETURN -> h_RETURN
    1606 | TAILCALL (x_20720, x_20719) -> h_TAILCALL __ x_20720 x_20719
     1606| TAILCALL (x_17798, x_17797) -> h_TAILCALL __ x_17798 x_17797
    16071607
    16081608(** val joint_fin_step_rect_Type1 :
     
    16101610    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16111611let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
    1612 | GOTO x_20726 -> h_GOTO x_20726
     1612| GOTO x_17804 -> h_GOTO x_17804
    16131613| RETURN -> h_RETURN
    1614 | TAILCALL (x_20728, x_20727) -> h_TAILCALL __ x_20728 x_20727
     1614| TAILCALL (x_17806, x_17805) -> h_TAILCALL __ x_17806 x_17805
    16151615
    16161616(** val joint_fin_step_rect_Type0 :
     
    16181618    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16191619let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
    1620 | GOTO x_20734 -> h_GOTO x_20734
     1620| GOTO x_17812 -> h_GOTO x_17812
    16211621| RETURN -> h_RETURN
    1622 | TAILCALL (x_20736, x_20735) -> h_TAILCALL __ x_20736 x_20735
     1622| TAILCALL (x_17814, x_17813) -> h_TAILCALL __ x_17814 x_17813
    16231623
    16241624(** val joint_fin_step_inv_rect_Type4 :
     
    16921692    'a1) -> joint_statement -> 'a1 **)
    16931693let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
    1694 | Sequential (x_20802, x_20801) -> h_sequential x_20802 x_20801
    1695 | Final x_20803 -> h_final x_20803
    1696 | FCOND (x_20806, x_20805, x_20804) -> h_FCOND __ x_20806 x_20805 x_20804
     1694| Sequential (x_17880, x_17879) -> h_sequential x_17880 x_17879
     1695| Final x_17881 -> h_final x_17881
     1696| FCOND (x_17884, x_17883, x_17882) -> h_FCOND __ x_17884 x_17883 x_17882
    16971697
    16981698(** val joint_statement_rect_Type5 :
     
    17011701    'a1) -> joint_statement -> 'a1 **)
    17021702let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
    1703 | Sequential (x_20813, x_20812) -> h_sequential x_20813 x_20812
    1704 | Final x_20814 -> h_final x_20814
    1705 | FCOND (x_20817, x_20816, x_20815) -> h_FCOND __ x_20817 x_20816 x_20815
     1703| Sequential (x_17891, x_17890) -> h_sequential x_17891 x_17890
     1704| Final x_17892 -> h_final x_17892
     1705| FCOND (x_17895, x_17894, x_17893) -> h_FCOND __ x_17895 x_17894 x_17893
    17061706
    17071707(** val joint_statement_rect_Type3 :
     
    17101710    'a1) -> joint_statement -> 'a1 **)
    17111711let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
    1712 | Sequential (x_20824, x_20823) -> h_sequential x_20824 x_20823
    1713 | Final x_20825 -> h_final x_20825
    1714 | FCOND (x_20828, x_20827, x_20826) -> h_FCOND __ x_20828 x_20827 x_20826
     1712| Sequential (x_17902, x_17901) -> h_sequential x_17902 x_17901
     1713| Final x_17903 -> h_final x_17903
     1714| FCOND (x_17906, x_17905, x_17904) -> h_FCOND __ x_17906 x_17905 x_17904
    17151715
    17161716(** val joint_statement_rect_Type2 :
     
    17191719    'a1) -> joint_statement -> 'a1 **)
    17201720let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
    1721 | Sequential (x_20835, x_20834) -> h_sequential x_20835 x_20834
    1722 | Final x_20836 -> h_final x_20836
    1723 | FCOND (x_20839, x_20838, x_20837) -> h_FCOND __ x_20839 x_20838 x_20837
     1721| Sequential (x_17913, x_17912) -> h_sequential x_17913 x_17912
     1722| Final x_17914 -> h_final x_17914
     1723| FCOND (x_17917, x_17916, x_17915) -> h_FCOND __ x_17917 x_17916 x_17915
    17241724
    17251725(** val joint_statement_rect_Type1 :
     
    17281728    'a1) -> joint_statement -> 'a1 **)
    17291729let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
    1730 | Sequential (x_20846, x_20845) -> h_sequential x_20846 x_20845
    1731 | Final x_20847 -> h_final x_20847
    1732 | FCOND (x_20850, x_20849, x_20848) -> h_FCOND __ x_20850 x_20849 x_20848
     1730| Sequential (x_17924, x_17923) -> h_sequential x_17924 x_17923
     1731| Final x_17925 -> h_final x_17925
     1732| FCOND (x_17928, x_17927, x_17926) -> h_FCOND __ x_17928 x_17927 x_17926
    17331733
    17341734(** val joint_statement_rect_Type0 :
     
    17371737    'a1) -> joint_statement -> 'a1 **)
    17381738let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
    1739 | Sequential (x_20857, x_20856) -> h_sequential x_20857 x_20856
    1740 | Final x_20858 -> h_final x_20858
    1741 | FCOND (x_20861, x_20860, x_20859) -> h_FCOND __ x_20861 x_20860 x_20859
     1739| Sequential (x_17935, x_17934) -> h_sequential x_17935 x_17934
     1740| Final x_17936 -> h_final x_17936
     1741| FCOND (x_17939, x_17938, x_17937) -> h_FCOND __ x_17939 x_17938 x_17937
    17421742
    17431743(** val joint_statement_inv_rect_Type4 :
     
    18381838    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18391839    'a1 **)
    1840 let rec params_rect_Type4 h_mk_params x_20934 =
     1840let rec params_rect_Type4 h_mk_params x_18012 =
    18411841  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1842     point_of_label0; point_of_succ = point_of_succ0 } = x_20934
     1842    point_of_label0; point_of_succ = point_of_succ0 } = x_18012
    18431843  in
    18441844  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18491849    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18501850    'a1 **)
    1851 let rec params_rect_Type5 h_mk_params x_20936 =
     1851let rec params_rect_Type5 h_mk_params x_18014 =
    18521852  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1853     point_of_label0; point_of_succ = point_of_succ0 } = x_20936
     1853    point_of_label0; point_of_succ = point_of_succ0 } = x_18014
    18541854  in
    18551855  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18601860    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18611861    'a1 **)
    1862 let rec params_rect_Type3 h_mk_params x_20938 =
     1862let rec params_rect_Type3 h_mk_params x_18016 =
    18631863  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1864     point_of_label0; point_of_succ = point_of_succ0 } = x_20938
     1864    point_of_label0; point_of_succ = point_of_succ0 } = x_18016
    18651865  in
    18661866  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18711871    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18721872    'a1 **)
    1873 let rec params_rect_Type2 h_mk_params x_20940 =
     1873let rec params_rect_Type2 h_mk_params x_18018 =
    18741874  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1875     point_of_label0; point_of_succ = point_of_succ0 } = x_20940
     1875    point_of_label0; point_of_succ = point_of_succ0 } = x_18018
    18761876  in
    18771877  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18821882    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18831883    'a1 **)
    1884 let rec params_rect_Type1 h_mk_params x_20942 =
     1884let rec params_rect_Type1 h_mk_params x_18020 =
    18851885  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1886     point_of_label0; point_of_succ = point_of_succ0 } = x_20942
     1886    point_of_label0; point_of_succ = point_of_succ0 } = x_18020
    18871887  in
    18881888  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18931893    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18941894    'a1 **)
    1895 let rec params_rect_Type0 h_mk_params x_20944 =
     1895let rec params_rect_Type0 h_mk_params x_18022 =
    18961896  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1897     point_of_label0; point_of_succ = point_of_succ0 } = x_20944
     1897    point_of_label0; point_of_succ = point_of_succ0 } = x_18022
    18981898  in
    18991899  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    20302030
    20312031(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2032 let rec lin_params_rect_Type4 h_mk_lin_params x_20967 =
    2033   let l_u_pars = x_20967 in h_mk_lin_params l_u_pars
     2032let rec lin_params_rect_Type4 h_mk_lin_params x_18045 =
     2033  let l_u_pars = x_18045 in h_mk_lin_params l_u_pars
    20342034
    20352035(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2036 let rec lin_params_rect_Type5 h_mk_lin_params x_20969 =
    2037   let l_u_pars = x_20969 in h_mk_lin_params l_u_pars
     2036let rec lin_params_rect_Type5 h_mk_lin_params x_18047 =
     2037  let l_u_pars = x_18047 in h_mk_lin_params l_u_pars
    20382038
    20392039(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2040 let rec lin_params_rect_Type3 h_mk_lin_params x_20971 =
    2041   let l_u_pars = x_20971 in h_mk_lin_params l_u_pars
     2040let rec lin_params_rect_Type3 h_mk_lin_params x_18049 =
     2041  let l_u_pars = x_18049 in h_mk_lin_params l_u_pars
    20422042
    20432043(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2044 let rec lin_params_rect_Type2 h_mk_lin_params x_20973 =
    2045   let l_u_pars = x_20973 in h_mk_lin_params l_u_pars
     2044let rec lin_params_rect_Type2 h_mk_lin_params x_18051 =
     2045  let l_u_pars = x_18051 in h_mk_lin_params l_u_pars
    20462046
    20472047(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2048 let rec lin_params_rect_Type1 h_mk_lin_params x_20975 =
    2049   let l_u_pars = x_20975 in h_mk_lin_params l_u_pars
     2048let rec lin_params_rect_Type1 h_mk_lin_params x_18053 =
     2049  let l_u_pars = x_18053 in h_mk_lin_params l_u_pars
    20502050
    20512051(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2052 let rec lin_params_rect_Type0 h_mk_lin_params x_20977 =
    2053   let l_u_pars = x_20977 in h_mk_lin_params l_u_pars
     2052let rec lin_params_rect_Type0 h_mk_lin_params x_18055 =
     2053  let l_u_pars = x_18055 in h_mk_lin_params l_u_pars
    20542054
    20552055(** val l_u_pars : lin_params -> uns_params **)
     
    21252125(** val graph_params_rect_Type4 :
    21262126    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2127 let rec graph_params_rect_Type4 h_mk_graph_params x_20993 =
    2128   let g_u_pars = x_20993 in h_mk_graph_params g_u_pars
     2127let rec graph_params_rect_Type4 h_mk_graph_params x_18071 =
     2128  let g_u_pars = x_18071 in h_mk_graph_params g_u_pars
    21292129
    21302130(** val graph_params_rect_Type5 :
    21312131    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2132 let rec graph_params_rect_Type5 h_mk_graph_params x_20995 =
    2133   let g_u_pars = x_20995 in h_mk_graph_params g_u_pars
     2132let rec graph_params_rect_Type5 h_mk_graph_params x_18073 =
     2133  let g_u_pars = x_18073 in h_mk_graph_params g_u_pars
    21342134
    21352135(** val graph_params_rect_Type3 :
    21362136    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2137 let rec graph_params_rect_Type3 h_mk_graph_params x_20997 =
    2138   let g_u_pars = x_20997 in h_mk_graph_params g_u_pars
     2137let rec graph_params_rect_Type3 h_mk_graph_params x_18075 =
     2138  let g_u_pars = x_18075 in h_mk_graph_params g_u_pars
    21392139
    21402140(** val graph_params_rect_Type2 :
    21412141    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2142 let rec graph_params_rect_Type2 h_mk_graph_params x_20999 =
    2143   let g_u_pars = x_20999 in h_mk_graph_params g_u_pars
     2142let rec graph_params_rect_Type2 h_mk_graph_params x_18077 =
     2143  let g_u_pars = x_18077 in h_mk_graph_params g_u_pars
    21442144
    21452145(** val graph_params_rect_Type1 :
    21462146    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2147 let rec graph_params_rect_Type1 h_mk_graph_params x_21001 =
    2148   let g_u_pars = x_21001 in h_mk_graph_params g_u_pars
     2147let rec graph_params_rect_Type1 h_mk_graph_params x_18079 =
     2148  let g_u_pars = x_18079 in h_mk_graph_params g_u_pars
    21492149
    21502150(** val graph_params_rect_Type0 :
    21512151    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2152 let rec graph_params_rect_Type0 h_mk_graph_params x_21003 =
    2153   let g_u_pars = x_21003 in h_mk_graph_params g_u_pars
     2152let rec graph_params_rect_Type0 h_mk_graph_params x_18081 =
     2153  let g_u_pars = x_18081 in h_mk_graph_params g_u_pars
    21542154
    21552155(** val g_u_pars : graph_params -> uns_params **)
     
    22212221    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22222222    'a1) -> joint_internal_function -> 'a1 **)
    2223 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_21019 =
     2223let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_18097 =
    22242224  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22252225    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22272227    joint_if_stacksize0; joint_if_local_stacksize =
    22282228    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2229     joint_if_entry = joint_if_entry0 } = x_21019
     2229    joint_if_entry = joint_if_entry0 } = x_18097
    22302230  in
    22312231  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22372237    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22382238    'a1) -> joint_internal_function -> 'a1 **)
    2239 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_21021 =
     2239let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_18099 =
    22402240  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22412241    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22432243    joint_if_stacksize0; joint_if_local_stacksize =
    22442244    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2245     joint_if_entry = joint_if_entry0 } = x_21021
     2245    joint_if_entry = joint_if_entry0 } = x_18099
    22462246  in
    22472247  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22532253    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22542254    'a1) -> joint_internal_function -> 'a1 **)
    2255 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_21023 =
     2255let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_18101 =
    22562256  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22572257    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22592259    joint_if_stacksize0; joint_if_local_stacksize =
    22602260    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2261     joint_if_entry = joint_if_entry0 } = x_21023
     2261    joint_if_entry = joint_if_entry0 } = x_18101
    22622262  in
    22632263  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22692269    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22702270    'a1) -> joint_internal_function -> 'a1 **)
    2271 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_21025 =
     2271let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_18103 =
    22722272  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22732273    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22752275    joint_if_stacksize0; joint_if_local_stacksize =
    22762276    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2277     joint_if_entry = joint_if_entry0 } = x_21025
     2277    joint_if_entry = joint_if_entry0 } = x_18103
    22782278  in
    22792279  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22852285    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22862286    'a1) -> joint_internal_function -> 'a1 **)
    2287 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_21027 =
     2287let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_18105 =
    22882288  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22892289    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22912291    joint_if_stacksize0; joint_if_local_stacksize =
    22922292    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2293     joint_if_entry = joint_if_entry0 } = x_21027
     2293    joint_if_entry = joint_if_entry0 } = x_18105
    22942294  in
    22952295  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    23012301    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    23022302    'a1) -> joint_internal_function -> 'a1 **)
    2303 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_21029 =
     2303let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_18107 =
    23042304  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    23052305    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    23072307    joint_if_stacksize0; joint_if_local_stacksize =
    23082308    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2309     joint_if_entry = joint_if_entry0 } = x_21029
     2309    joint_if_entry = joint_if_entry0 } = x_18107
    23102310  in
    23112311  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    24042404(** val good_if_rect_Type4 :
    24052405    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2406     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2406    __ -> __ -> __ -> 'a1) -> 'a1 **)
    24072407let rec good_if_rect_Type4 p globals def h_mk_good_if =
    2408   h_mk_good_if __ __ __ __ __ __
     2408  h_mk_good_if __ __ __ __ __
    24092409
    24102410(** val good_if_rect_Type5 :
    24112411    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2412     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2412    __ -> __ -> __ -> 'a1) -> 'a1 **)
    24132413let rec good_if_rect_Type5 p globals def h_mk_good_if =
    2414   h_mk_good_if __ __ __ __ __ __
     2414  h_mk_good_if __ __ __ __ __
    24152415
    24162416(** val good_if_rect_Type3 :
    24172417    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2418     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2418    __ -> __ -> __ -> 'a1) -> 'a1 **)
    24192419let rec good_if_rect_Type3 p globals def h_mk_good_if =
    2420   h_mk_good_if __ __ __ __ __ __
     2420  h_mk_good_if __ __ __ __ __
    24212421
    24222422(** val good_if_rect_Type2 :
    24232423    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2424     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2424    __ -> __ -> __ -> 'a1) -> 'a1 **)
    24252425let rec good_if_rect_Type2 p globals def h_mk_good_if =
    2426   h_mk_good_if __ __ __ __ __ __
     2426  h_mk_good_if __ __ __ __ __
    24272427
    24282428(** val good_if_rect_Type1 :
    24292429    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2430     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2430    __ -> __ -> __ -> 'a1) -> 'a1 **)
    24312431let rec good_if_rect_Type1 p globals def h_mk_good_if =
    2432   h_mk_good_if __ __ __ __ __ __
     2432  h_mk_good_if __ __ __ __ __
    24332433
    24342434(** val good_if_rect_Type0 :
    24352435    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2436     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2436    __ -> __ -> __ -> 'a1) -> 'a1 **)
    24372437let rec good_if_rect_Type0 p globals def h_mk_good_if =
    2438   h_mk_good_if __ __ __ __ __ __
     2438  h_mk_good_if __ __ __ __ __
    24392439
    24402440(** val good_if_inv_rect_Type4 :
    24412441    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2442     __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2442    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24432443let good_if_inv_rect_Type4 x1 x2 x3 h1 =
    24442444  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
     
    24462446(** val good_if_inv_rect_Type3 :
    24472447    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2448     __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2448    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24492449let good_if_inv_rect_Type3 x1 x2 x3 h1 =
    24502450  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
     
    24522452(** val good_if_inv_rect_Type2 :
    24532453    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2454     __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2454    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24552455let good_if_inv_rect_Type2 x1 x2 x3 h1 =
    24562456  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
     
    24582458(** val good_if_inv_rect_Type1 :
    24592459    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2460     __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2460    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24612461let good_if_inv_rect_Type1 x1 x2 x3 h1 =
    24622462  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
     
    24642464(** val good_if_inv_rect_Type0 :
    24652465    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2466     __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2466    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24672467let good_if_inv_rect_Type0 x1 x2 x3 h1 =
    24682468  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
     2469
     2470(** val good_if_discr :
     2471    params -> AST.ident List.list -> joint_internal_function -> __ **)
     2472let good_if_discr a1 a2 a3 =
     2473  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
    24692474
    24702475(** val good_if_jmdiscr :
    24712476    params -> AST.ident List.list -> joint_internal_function -> __ **)
    24722477let good_if_jmdiscr a1 a2 a3 =
    2473   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) __
     2478  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
    24742479
    24752480type joint_closed_internal_function = joint_internal_function Types.sig0
     
    25242529type joint_function = joint_closed_internal_function AST.fundef
    25252530
    2526 type joint_program = (joint_function, Nat.nat) AST.program
     2531type joint_program = { joint_prog : (joint_function, AST.init_data List.list)
     2532                                    AST.program;
     2533                       init_cost_label : CostLabel.costlabel }
     2534
     2535(** val joint_program_rect_Type4 :
     2536    params -> ((joint_function, AST.init_data List.list) AST.program ->
     2537    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
     2538let rec joint_program_rect_Type4 p h_mk_joint_program x_18149 =
     2539  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
     2540    x_18149
     2541  in
     2542  h_mk_joint_program joint_prog0 init_cost_label0
     2543
     2544(** val joint_program_rect_Type5 :
     2545    params -> ((joint_function, AST.init_data List.list) AST.program ->
     2546    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
     2547let rec joint_program_rect_Type5 p h_mk_joint_program x_18151 =
     2548  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
     2549    x_18151
     2550  in
     2551  h_mk_joint_program joint_prog0 init_cost_label0
     2552
     2553(** val joint_program_rect_Type3 :
     2554    params -> ((joint_function, AST.init_data List.list) AST.program ->
     2555    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
     2556let rec joint_program_rect_Type3 p h_mk_joint_program x_18153 =
     2557  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
     2558    x_18153
     2559  in
     2560  h_mk_joint_program joint_prog0 init_cost_label0
     2561
     2562(** val joint_program_rect_Type2 :
     2563    params -> ((joint_function, AST.init_data List.list) AST.program ->
     2564    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
     2565let rec joint_program_rect_Type2 p h_mk_joint_program x_18155 =
     2566  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
     2567    x_18155
     2568  in
     2569  h_mk_joint_program joint_prog0 init_cost_label0
     2570
     2571(** val joint_program_rect_Type1 :
     2572    params -> ((joint_function, AST.init_data List.list) AST.program ->
     2573    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
     2574let rec joint_program_rect_Type1 p h_mk_joint_program x_18157 =
     2575  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
     2576    x_18157
     2577  in
     2578  h_mk_joint_program joint_prog0 init_cost_label0
     2579
     2580(** val joint_program_rect_Type0 :
     2581    params -> ((joint_function, AST.init_data List.list) AST.program ->
     2582    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
     2583let rec joint_program_rect_Type0 p h_mk_joint_program x_18159 =
     2584  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
     2585    x_18159
     2586  in
     2587  h_mk_joint_program joint_prog0 init_cost_label0
     2588
     2589(** val joint_prog :
     2590    params -> joint_program -> (joint_function, AST.init_data List.list)
     2591    AST.program **)
     2592let rec joint_prog p xxx =
     2593  xxx.joint_prog
     2594
     2595(** val init_cost_label : params -> joint_program -> CostLabel.costlabel **)
     2596let rec init_cost_label p xxx =
     2597  xxx.init_cost_label
     2598
     2599(** val joint_program_inv_rect_Type4 :
     2600    params -> joint_program -> ((joint_function, AST.init_data List.list)
     2601    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
     2602let joint_program_inv_rect_Type4 x1 hterm h1 =
     2603  let hcut = joint_program_rect_Type4 x1 h1 hterm in hcut __
     2604
     2605(** val joint_program_inv_rect_Type3 :
     2606    params -> joint_program -> ((joint_function, AST.init_data List.list)
     2607    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
     2608let joint_program_inv_rect_Type3 x1 hterm h1 =
     2609  let hcut = joint_program_rect_Type3 x1 h1 hterm in hcut __
     2610
     2611(** val joint_program_inv_rect_Type2 :
     2612    params -> joint_program -> ((joint_function, AST.init_data List.list)
     2613    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
     2614let joint_program_inv_rect_Type2 x1 hterm h1 =
     2615  let hcut = joint_program_rect_Type2 x1 h1 hterm in hcut __
     2616
     2617(** val joint_program_inv_rect_Type1 :
     2618    params -> joint_program -> ((joint_function, AST.init_data List.list)
     2619    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
     2620let joint_program_inv_rect_Type1 x1 hterm h1 =
     2621  let hcut = joint_program_rect_Type1 x1 h1 hterm in hcut __
     2622
     2623(** val joint_program_inv_rect_Type0 :
     2624    params -> joint_program -> ((joint_function, AST.init_data List.list)
     2625    AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1 **)
     2626let joint_program_inv_rect_Type0 x1 hterm h1 =
     2627  let hcut = joint_program_rect_Type0 x1 h1 hterm in hcut __
     2628
     2629(** val joint_program_discr :
     2630    params -> joint_program -> joint_program -> __ **)
     2631let joint_program_discr a1 x y =
     2632  Logic.eq_rect_Type2 x
     2633    (let { joint_prog = a0; init_cost_label = a10 } = x in
     2634    Obj.magic (fun _ dH -> dH __ __)) y
     2635
     2636(** val joint_program_jmdiscr :
     2637    params -> joint_program -> joint_program -> __ **)
     2638let joint_program_jmdiscr a1 x y =
     2639  Logic.eq_rect_Type2 x
     2640    (let { joint_prog = a0; init_cost_label = a10 } = x in
     2641    Obj.magic (fun _ dH -> dH __ __)) y
     2642
     2643(** val dpi1__o__joint_prog__o__inject :
     2644    params -> (joint_program, 'a1) Types.dPair -> (joint_function,
     2645    AST.init_data List.list) AST.program Types.sig0 **)
     2646let dpi1__o__joint_prog__o__inject x0 x3 =
     2647  x3.Types.dpi1.joint_prog
     2648
     2649(** val eject__o__joint_prog__o__inject :
     2650    params -> joint_program Types.sig0 -> (joint_function, AST.init_data
     2651    List.list) AST.program Types.sig0 **)
     2652let eject__o__joint_prog__o__inject x0 x3 =
     2653  (Types.pi1 x3).joint_prog
     2654
     2655(** val joint_prog__o__inject :
     2656    params -> joint_program -> (joint_function, AST.init_data List.list)
     2657    AST.program Types.sig0 **)
     2658let joint_prog__o__inject x0 x2 =
     2659  x2.joint_prog
     2660
     2661(** val dpi1__o__joint_prog :
     2662    params -> (joint_program, 'a1) Types.dPair -> (joint_function,
     2663    AST.init_data List.list) AST.program **)
     2664let dpi1__o__joint_prog x0 x2 =
     2665  x2.Types.dpi1.joint_prog
     2666
     2667(** val eject__o__joint_prog :
     2668    params -> joint_program Types.sig0 -> (joint_function, AST.init_data
     2669    List.list) AST.program **)
     2670let eject__o__joint_prog x0 x2 =
     2671  (Types.pi1 x2).joint_prog
    25272672
    25282673type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
     
    25362681       List.Cons ({ Types.fst = id; Types.snd =
    25372682         (Types.pi1 jif).joint_if_stacksize }, acc)
    2538      | AST.External x -> acc)) List.Nil pr.AST.prog_funct
     2683     | AST.External x -> acc)) List.Nil pr.joint_prog.AST.prog_funct
     2684
     2685open Extra_bool
     2686
     2687open Coqlib
     2688
     2689open Values
     2690
     2691open FrontEndVal
     2692
     2693open GenMem
     2694
     2695open FrontEndMem
     2696
     2697open Globalenvs
    25392698
    25402699(** val globals_stacksize : params -> joint_program -> Nat.nat **)
    25412700let globals_stacksize pars p =
    25422701  List.fold Nat.plus Nat.O (fun entry -> Bool.True) (fun entry ->
    2543     entry.Types.snd) p.AST.prog_vars
    2544 
     2702    Globalenvs.size_init_data_list entry.Types.snd)
     2703    p.joint_prog.AST.prog_vars
     2704
Note: See TracChangeset for help on using the changeset viewer.