Changeset 2867 for extracted/joint.ml


Ignore:
Timestamp:
Mar 13, 2013, 11:12:29 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after indianess bug fixes by Paolo.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint.ml

    r2854 r2867  
    110110    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    111111let rec argument_rect_Type4 h_Reg h_Imm = function
    112 | Reg x_7 -> h_Reg x_7
    113 | Imm x_8 -> h_Imm x_8
     112| Reg x_19661 -> h_Reg x_19661
     113| Imm x_19662 -> h_Imm x_19662
    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_12 -> h_Reg x_12
    119 | Imm x_13 -> h_Imm x_13
     118| Reg x_19666 -> h_Reg x_19666
     119| Imm x_19667 -> h_Imm x_19667
    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_17 -> h_Reg x_17
    125 | Imm x_18 -> h_Imm x_18
     124| Reg x_19671 -> h_Reg x_19671
     125| Imm x_19672 -> h_Imm x_19672
    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_22 -> h_Reg x_22
    131 | Imm x_23 -> h_Imm x_23
     130| Reg x_19676 -> h_Reg x_19676
     131| Imm x_19677 -> h_Imm x_19677
    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_27 -> h_Reg x_27
    137 | Imm x_28 -> h_Imm x_28
     136| Reg x_19681 -> h_Reg x_19681
     137| Imm x_19682 -> h_Imm x_19682
    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_32 -> h_Reg x_32
    143 | Imm x_33 -> h_Imm x_33
     142| Reg x_19686 -> h_Reg x_19686
     143| Imm x_19687 -> h_Imm x_19687
    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_68 =
     326let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_19722 =
    327327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    328     x_68
     328    x_19722
    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_70 =
     337let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_19724 =
    338338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    339     x_70
     339    x_19724
    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_72 =
     348let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_19726 =
    349349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    350     x_72
     350    x_19726
    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_74 =
     359let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_19728 =
    360360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    361     x_74
     361    x_19728
    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_76 =
     370let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_19730 =
    371371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    372     x_76
     372    x_19730
    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_78 =
     381let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_19732 =
    382382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    383     x_78
     383    x_19732
    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_95 =
     508let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_19749 =
    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_95
     514    params_regs0 } = x_19749
    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_97 =
     531let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_19751 =
    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_97
     537    params_regs0 } = x_19751
    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_99 =
     554let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_19753 =
    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_99
     560    params_regs0 } = x_19753
    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_101 =
     577let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_19755 =
    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_101
     583    params_regs0 } = x_19755
    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_103 =
     600let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_19757 =
    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_103
     606    params_regs0 } = x_19757
    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_105 =
     623let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_19759 =
    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_105
     629    params_regs0 } = x_19759
    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_135 =
    808   let { u_pars = u_pars0; functs = functs0 } = x_135 in
     807let rec uns_params_rect_Type4 h_mk_uns_params x_19789 =
     808  let { u_pars = u_pars0; functs = functs0 } = x_19789 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_137 =
    815   let { u_pars = u_pars0; functs = functs0 } = x_137 in
     814let rec uns_params_rect_Type5 h_mk_uns_params x_19791 =
     815  let { u_pars = u_pars0; functs = functs0 } = x_19791 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_139 =
    822   let { u_pars = u_pars0; functs = functs0 } = x_139 in
     821let rec uns_params_rect_Type3 h_mk_uns_params x_19793 =
     822  let { u_pars = u_pars0; functs = functs0 } = x_19793 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_141 =
    829   let { u_pars = u_pars0; functs = functs0 } = x_141 in
     828let rec uns_params_rect_Type2 h_mk_uns_params x_19795 =
     829  let { u_pars = u_pars0; functs = functs0 } = x_19795 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_143 =
    836   let { u_pars = u_pars0; functs = functs0 } = x_143 in
     835let rec uns_params_rect_Type1 h_mk_uns_params x_19797 =
     836  let { u_pars = u_pars0; functs = functs0 } = x_19797 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_145 =
    843   let { u_pars = u_pars0; functs = functs0 } = x_145 in
     842let rec uns_params_rect_Type0 h_mk_uns_params x_19799 =
     843  let { u_pars = u_pars0; functs = functs0 } = x_19799 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_200 -> h_COMMENT x_200
    914 | MOVE x_201 -> h_MOVE x_201
    915 | POP x_202 -> h_POP x_202
    916 | PUSH x_203 -> h_PUSH x_203
    917 | ADDRESS (i, x_205, x_204) -> h_ADDRESS i __ x_205 x_204
    918 | OPACCS (x_211, x_210, x_209, x_208, x_207) ->
    919   h_OPACCS x_211 x_210 x_209 x_208 x_207
    920 | OP1 (x_214, x_213, x_212) -> h_OP1 x_214 x_213 x_212
    921 | OP2 (x_218, x_217, x_216, x_215) -> h_OP2 x_218 x_217 x_216 x_215
     913| COMMENT x_19854 -> h_COMMENT x_19854
     914| MOVE x_19855 -> h_MOVE x_19855
     915| POP x_19856 -> h_POP x_19856
     916| PUSH x_19857 -> h_PUSH x_19857
     917| ADDRESS (i, x_19859, x_19858) -> h_ADDRESS i __ x_19859 x_19858
     918| OPACCS (x_19865, x_19864, x_19863, x_19862, x_19861) ->
     919  h_OPACCS x_19865 x_19864 x_19863 x_19862 x_19861
     920| OP1 (x_19868, x_19867, x_19866) -> h_OP1 x_19868 x_19867 x_19866
     921| OP2 (x_19872, x_19871, x_19870, x_19869) ->
     922  h_OP2 x_19872 x_19871 x_19870 x_19869
    922923| CLEAR_CARRY -> h_CLEAR_CARRY
    923924| SET_CARRY -> h_SET_CARRY
    924 | LOAD (x_221, x_220, x_219) -> h_LOAD x_221 x_220 x_219
    925 | STORE (x_224, x_223, x_222) -> h_STORE x_224 x_223 x_222
    926 | Extension_seq x_225 -> h_extension_seq x_225
     925| LOAD (x_19875, x_19874, x_19873) -> h_LOAD x_19875 x_19874 x_19873
     926| STORE (x_19878, x_19877, x_19876) -> h_STORE x_19878 x_19877 x_19876
     927| Extension_seq x_19879 -> h_extension_seq x_19879
    927928
    928929(** val joint_seq_rect_Type5 :
     
    934935    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    935936let 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
    936 | COMMENT x_240 -> h_COMMENT x_240
    937 | MOVE x_241 -> h_MOVE x_241
    938 | POP x_242 -> h_POP x_242
    939 | PUSH x_243 -> h_PUSH x_243
    940 | ADDRESS (i, x_245, x_244) -> h_ADDRESS i __ x_245 x_244
    941 | OPACCS (x_251, x_250, x_249, x_248, x_247) ->
    942   h_OPACCS x_251 x_250 x_249 x_248 x_247
    943 | OP1 (x_254, x_253, x_252) -> h_OP1 x_254 x_253 x_252
    944 | OP2 (x_258, x_257, x_256, x_255) -> h_OP2 x_258 x_257 x_256 x_255
     937| COMMENT x_19894 -> h_COMMENT x_19894
     938| MOVE x_19895 -> h_MOVE x_19895
     939| POP x_19896 -> h_POP x_19896
     940| PUSH x_19897 -> h_PUSH x_19897
     941| ADDRESS (i, x_19899, x_19898) -> h_ADDRESS i __ x_19899 x_19898
     942| OPACCS (x_19905, x_19904, x_19903, x_19902, x_19901) ->
     943  h_OPACCS x_19905 x_19904 x_19903 x_19902 x_19901
     944| OP1 (x_19908, x_19907, x_19906) -> h_OP1 x_19908 x_19907 x_19906
     945| OP2 (x_19912, x_19911, x_19910, x_19909) ->
     946  h_OP2 x_19912 x_19911 x_19910 x_19909
    945947| CLEAR_CARRY -> h_CLEAR_CARRY
    946948| SET_CARRY -> h_SET_CARRY
    947 | LOAD (x_261, x_260, x_259) -> h_LOAD x_261 x_260 x_259
    948 | STORE (x_264, x_263, x_262) -> h_STORE x_264 x_263 x_262
    949 | Extension_seq x_265 -> h_extension_seq x_265
     949| LOAD (x_19915, x_19914, x_19913) -> h_LOAD x_19915 x_19914 x_19913
     950| STORE (x_19918, x_19917, x_19916) -> h_STORE x_19918 x_19917 x_19916
     951| Extension_seq x_19919 -> h_extension_seq x_19919
    950952
    951953(** val joint_seq_rect_Type3 :
     
    957959    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    958960let 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
    959 | COMMENT x_280 -> h_COMMENT x_280
    960 | MOVE x_281 -> h_MOVE x_281
    961 | POP x_282 -> h_POP x_282
    962 | PUSH x_283 -> h_PUSH x_283
    963 | ADDRESS (i, x_285, x_284) -> h_ADDRESS i __ x_285 x_284
    964 | OPACCS (x_291, x_290, x_289, x_288, x_287) ->
    965   h_OPACCS x_291 x_290 x_289 x_288 x_287
    966 | OP1 (x_294, x_293, x_292) -> h_OP1 x_294 x_293 x_292
    967 | OP2 (x_298, x_297, x_296, x_295) -> h_OP2 x_298 x_297 x_296 x_295
     961| COMMENT x_19934 -> h_COMMENT x_19934
     962| MOVE x_19935 -> h_MOVE x_19935
     963| POP x_19936 -> h_POP x_19936
     964| PUSH x_19937 -> h_PUSH x_19937
     965| ADDRESS (i, x_19939, x_19938) -> h_ADDRESS i __ x_19939 x_19938
     966| OPACCS (x_19945, x_19944, x_19943, x_19942, x_19941) ->
     967  h_OPACCS x_19945 x_19944 x_19943 x_19942 x_19941
     968| OP1 (x_19948, x_19947, x_19946) -> h_OP1 x_19948 x_19947 x_19946
     969| OP2 (x_19952, x_19951, x_19950, x_19949) ->
     970  h_OP2 x_19952 x_19951 x_19950 x_19949
    968971| CLEAR_CARRY -> h_CLEAR_CARRY
    969972| SET_CARRY -> h_SET_CARRY
    970 | LOAD (x_301, x_300, x_299) -> h_LOAD x_301 x_300 x_299
    971 | STORE (x_304, x_303, x_302) -> h_STORE x_304 x_303 x_302
    972 | Extension_seq x_305 -> h_extension_seq x_305
     973| LOAD (x_19955, x_19954, x_19953) -> h_LOAD x_19955 x_19954 x_19953
     974| STORE (x_19958, x_19957, x_19956) -> h_STORE x_19958 x_19957 x_19956
     975| Extension_seq x_19959 -> h_extension_seq x_19959
    973976
    974977(** val joint_seq_rect_Type2 :
     
    980983    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    981984let 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
    982 | COMMENT x_320 -> h_COMMENT x_320
    983 | MOVE x_321 -> h_MOVE x_321
    984 | POP x_322 -> h_POP x_322
    985 | PUSH x_323 -> h_PUSH x_323
    986 | ADDRESS (i, x_325, x_324) -> h_ADDRESS i __ x_325 x_324
    987 | OPACCS (x_331, x_330, x_329, x_328, x_327) ->
    988   h_OPACCS x_331 x_330 x_329 x_328 x_327
    989 | OP1 (x_334, x_333, x_332) -> h_OP1 x_334 x_333 x_332
    990 | OP2 (x_338, x_337, x_336, x_335) -> h_OP2 x_338 x_337 x_336 x_335
     985| COMMENT x_19974 -> h_COMMENT x_19974
     986| MOVE x_19975 -> h_MOVE x_19975
     987| POP x_19976 -> h_POP x_19976
     988| PUSH x_19977 -> h_PUSH x_19977
     989| ADDRESS (i, x_19979, x_19978) -> h_ADDRESS i __ x_19979 x_19978
     990| OPACCS (x_19985, x_19984, x_19983, x_19982, x_19981) ->
     991  h_OPACCS x_19985 x_19984 x_19983 x_19982 x_19981
     992| OP1 (x_19988, x_19987, x_19986) -> h_OP1 x_19988 x_19987 x_19986
     993| OP2 (x_19992, x_19991, x_19990, x_19989) ->
     994  h_OP2 x_19992 x_19991 x_19990 x_19989
    991995| CLEAR_CARRY -> h_CLEAR_CARRY
    992996| SET_CARRY -> h_SET_CARRY
    993 | LOAD (x_341, x_340, x_339) -> h_LOAD x_341 x_340 x_339
    994 | STORE (x_344, x_343, x_342) -> h_STORE x_344 x_343 x_342
    995 | Extension_seq x_345 -> h_extension_seq x_345
     997| LOAD (x_19995, x_19994, x_19993) -> h_LOAD x_19995 x_19994 x_19993
     998| STORE (x_19998, x_19997, x_19996) -> h_STORE x_19998 x_19997 x_19996
     999| Extension_seq x_19999 -> h_extension_seq x_19999
    9961000
    9971001(** val joint_seq_rect_Type1 :
     
    10031007    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    10041008let 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
    1005 | COMMENT x_360 -> h_COMMENT x_360
    1006 | MOVE x_361 -> h_MOVE x_361
    1007 | POP x_362 -> h_POP x_362
    1008 | PUSH x_363 -> h_PUSH x_363
    1009 | ADDRESS (i, x_365, x_364) -> h_ADDRESS i __ x_365 x_364
    1010 | OPACCS (x_371, x_370, x_369, x_368, x_367) ->
    1011   h_OPACCS x_371 x_370 x_369 x_368 x_367
    1012 | OP1 (x_374, x_373, x_372) -> h_OP1 x_374 x_373 x_372
    1013 | OP2 (x_378, x_377, x_376, x_375) -> h_OP2 x_378 x_377 x_376 x_375
     1009| COMMENT x_20014 -> h_COMMENT x_20014
     1010| MOVE x_20015 -> h_MOVE x_20015
     1011| POP x_20016 -> h_POP x_20016
     1012| PUSH x_20017 -> h_PUSH x_20017
     1013| ADDRESS (i, x_20019, x_20018) -> h_ADDRESS i __ x_20019 x_20018
     1014| OPACCS (x_20025, x_20024, x_20023, x_20022, x_20021) ->
     1015  h_OPACCS x_20025 x_20024 x_20023 x_20022 x_20021
     1016| OP1 (x_20028, x_20027, x_20026) -> h_OP1 x_20028 x_20027 x_20026
     1017| OP2 (x_20032, x_20031, x_20030, x_20029) ->
     1018  h_OP2 x_20032 x_20031 x_20030 x_20029
    10141019| CLEAR_CARRY -> h_CLEAR_CARRY
    10151020| SET_CARRY -> h_SET_CARRY
    1016 | LOAD (x_381, x_380, x_379) -> h_LOAD x_381 x_380 x_379
    1017 | STORE (x_384, x_383, x_382) -> h_STORE x_384 x_383 x_382
    1018 | Extension_seq x_385 -> h_extension_seq x_385
     1021| LOAD (x_20035, x_20034, x_20033) -> h_LOAD x_20035 x_20034 x_20033
     1022| STORE (x_20038, x_20037, x_20036) -> h_STORE x_20038 x_20037 x_20036
     1023| Extension_seq x_20039 -> h_extension_seq x_20039
    10191024
    10201025(** val joint_seq_rect_Type0 :
     
    10261031    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    10271032let 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
    1028 | COMMENT x_400 -> h_COMMENT x_400
    1029 | MOVE x_401 -> h_MOVE x_401
    1030 | POP x_402 -> h_POP x_402
    1031 | PUSH x_403 -> h_PUSH x_403
    1032 | ADDRESS (i, x_405, x_404) -> h_ADDRESS i __ x_405 x_404
    1033 | OPACCS (x_411, x_410, x_409, x_408, x_407) ->
    1034   h_OPACCS x_411 x_410 x_409 x_408 x_407
    1035 | OP1 (x_414, x_413, x_412) -> h_OP1 x_414 x_413 x_412
    1036 | OP2 (x_418, x_417, x_416, x_415) -> h_OP2 x_418 x_417 x_416 x_415
     1033| COMMENT x_20054 -> h_COMMENT x_20054
     1034| MOVE x_20055 -> h_MOVE x_20055
     1035| POP x_20056 -> h_POP x_20056
     1036| PUSH x_20057 -> h_PUSH x_20057
     1037| ADDRESS (i, x_20059, x_20058) -> h_ADDRESS i __ x_20059 x_20058
     1038| OPACCS (x_20065, x_20064, x_20063, x_20062, x_20061) ->
     1039  h_OPACCS x_20065 x_20064 x_20063 x_20062 x_20061
     1040| OP1 (x_20068, x_20067, x_20066) -> h_OP1 x_20068 x_20067 x_20066
     1041| OP2 (x_20072, x_20071, x_20070, x_20069) ->
     1042  h_OP2 x_20072 x_20071 x_20070 x_20069
    10371043| CLEAR_CARRY -> h_CLEAR_CARRY
    10381044| SET_CARRY -> h_SET_CARRY
    1039 | LOAD (x_421, x_420, x_419) -> h_LOAD x_421 x_420 x_419
    1040 | STORE (x_424, x_423, x_422) -> h_STORE x_424 x_423 x_422
    1041 | Extension_seq x_425 -> h_extension_seq x_425
     1045| LOAD (x_20075, x_20074, x_20073) -> h_LOAD x_20075 x_20074 x_20073
     1046| STORE (x_20078, x_20077, x_20076) -> h_STORE x_20078 x_20077 x_20076
     1047| Extension_seq x_20079 -> h_extension_seq x_20079
    10421048
    10431049(** val joint_seq_inv_rect_Type4 :
     
    12301236    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12311237let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1232 | COST_LABEL x_692 -> h_COST_LABEL x_692
    1233 | CALL (x_695, x_694, x_693) -> h_CALL x_695 x_694 x_693
    1234 | COND (x_697, x_696) -> h_COND x_697 x_696
    1235 | Step_seq x_698 -> h_step_seq x_698
     1238| COST_LABEL x_20346 -> h_COST_LABEL x_20346
     1239| CALL (x_20349, x_20348, x_20347) -> h_CALL x_20349 x_20348 x_20347
     1240| COND (x_20351, x_20350) -> h_COND x_20351 x_20350
     1241| Step_seq x_20352 -> h_step_seq x_20352
    12361242
    12371243(** val joint_step_rect_Type5 :
     
    12401246    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12411247let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1242 | COST_LABEL x_704 -> h_COST_LABEL x_704
    1243 | CALL (x_707, x_706, x_705) -> h_CALL x_707 x_706 x_705
    1244 | COND (x_709, x_708) -> h_COND x_709 x_708
    1245 | Step_seq x_710 -> h_step_seq x_710
     1248| COST_LABEL x_20358 -> h_COST_LABEL x_20358
     1249| CALL (x_20361, x_20360, x_20359) -> h_CALL x_20361 x_20360 x_20359
     1250| COND (x_20363, x_20362) -> h_COND x_20363 x_20362
     1251| Step_seq x_20364 -> h_step_seq x_20364
    12461252
    12471253(** val joint_step_rect_Type3 :
     
    12501256    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12511257let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1252 | COST_LABEL x_716 -> h_COST_LABEL x_716
    1253 | CALL (x_719, x_718, x_717) -> h_CALL x_719 x_718 x_717
    1254 | COND (x_721, x_720) -> h_COND x_721 x_720
    1255 | Step_seq x_722 -> h_step_seq x_722
     1258| COST_LABEL x_20370 -> h_COST_LABEL x_20370
     1259| CALL (x_20373, x_20372, x_20371) -> h_CALL x_20373 x_20372 x_20371
     1260| COND (x_20375, x_20374) -> h_COND x_20375 x_20374
     1261| Step_seq x_20376 -> h_step_seq x_20376
    12561262
    12571263(** val joint_step_rect_Type2 :
     
    12601266    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12611267let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1262 | COST_LABEL x_728 -> h_COST_LABEL x_728
    1263 | CALL (x_731, x_730, x_729) -> h_CALL x_731 x_730 x_729
    1264 | COND (x_733, x_732) -> h_COND x_733 x_732
    1265 | Step_seq x_734 -> h_step_seq x_734
     1268| COST_LABEL x_20382 -> h_COST_LABEL x_20382
     1269| CALL (x_20385, x_20384, x_20383) -> h_CALL x_20385 x_20384 x_20383
     1270| COND (x_20387, x_20386) -> h_COND x_20387 x_20386
     1271| Step_seq x_20388 -> h_step_seq x_20388
    12661272
    12671273(** val joint_step_rect_Type1 :
     
    12701276    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12711277let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1272 | COST_LABEL x_740 -> h_COST_LABEL x_740
    1273 | CALL (x_743, x_742, x_741) -> h_CALL x_743 x_742 x_741
    1274 | COND (x_745, x_744) -> h_COND x_745 x_744
    1275 | Step_seq x_746 -> h_step_seq x_746
     1278| COST_LABEL x_20394 -> h_COST_LABEL x_20394
     1279| CALL (x_20397, x_20396, x_20395) -> h_CALL x_20397 x_20396 x_20395
     1280| COND (x_20399, x_20398) -> h_COND x_20399 x_20398
     1281| Step_seq x_20400 -> h_step_seq x_20400
    12761282
    12771283(** val joint_step_rect_Type0 :
     
    12801286    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12811287let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1282 | COST_LABEL x_752 -> h_COST_LABEL x_752
    1283 | CALL (x_755, x_754, x_753) -> h_CALL x_755 x_754 x_753
    1284 | COND (x_757, x_756) -> h_COND x_757 x_756
    1285 | Step_seq x_758 -> h_step_seq x_758
     1288| COST_LABEL x_20406 -> h_COST_LABEL x_20406
     1289| CALL (x_20409, x_20408, x_20407) -> h_CALL x_20409 x_20408 x_20407
     1290| COND (x_20411, x_20410) -> h_COND x_20411 x_20410
     1291| Step_seq x_20412 -> h_step_seq x_20412
    12861292
    12871293(** val joint_step_inv_rect_Type4 :
     
    14581464    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14591465    'a1) -> stmt_params -> 'a1 **)
    1460 let rec stmt_params_rect_Type4 h_mk_stmt_params x_837 =
     1466let rec stmt_params_rect_Type4 h_mk_stmt_params x_20491 =
    14611467  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1462     has_fcond0 } = x_837
     1468    has_fcond0 } = x_20491
    14631469  in
    14641470  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14671473    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14681474    'a1) -> stmt_params -> 'a1 **)
    1469 let rec stmt_params_rect_Type5 h_mk_stmt_params x_839 =
     1475let rec stmt_params_rect_Type5 h_mk_stmt_params x_20493 =
    14701476  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1471     has_fcond0 } = x_839
     1477    has_fcond0 } = x_20493
    14721478  in
    14731479  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14761482    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14771483    'a1) -> stmt_params -> 'a1 **)
    1478 let rec stmt_params_rect_Type3 h_mk_stmt_params x_841 =
     1484let rec stmt_params_rect_Type3 h_mk_stmt_params x_20495 =
    14791485  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1480     has_fcond0 } = x_841
     1486    has_fcond0 } = x_20495
    14811487  in
    14821488  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14851491    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14861492    'a1) -> stmt_params -> 'a1 **)
    1487 let rec stmt_params_rect_Type2 h_mk_stmt_params x_843 =
     1493let rec stmt_params_rect_Type2 h_mk_stmt_params x_20497 =
    14881494  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1489     has_fcond0 } = x_843
     1495    has_fcond0 } = x_20497
    14901496  in
    14911497  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14941500    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14951501    'a1) -> stmt_params -> 'a1 **)
    1496 let rec stmt_params_rect_Type1 h_mk_stmt_params x_845 =
     1502let rec stmt_params_rect_Type1 h_mk_stmt_params x_20499 =
    14971503  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1498     has_fcond0 } = x_845
     1504    has_fcond0 } = x_20499
    14991505  in
    15001506  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15031509    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    15041510    'a1) -> stmt_params -> 'a1 **)
    1505 let rec stmt_params_rect_Type0 h_mk_stmt_params x_847 =
     1511let rec stmt_params_rect_Type0 h_mk_stmt_params x_20501 =
    15061512  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1507     has_fcond0 } = x_847
     1513    has_fcond0 } = x_20501
    15081514  in
    15091515  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15721578    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15731579let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
    1574 | GOTO x_871 -> h_GOTO x_871
     1580| GOTO x_20525 -> h_GOTO x_20525
    15751581| RETURN -> h_RETURN
    1576 | TAILCALL (x_873, x_872) -> h_TAILCALL __ x_873 x_872
     1582| TAILCALL (x_20527, x_20526) -> h_TAILCALL __ x_20527 x_20526
    15771583
    15781584(** val joint_fin_step_rect_Type5 :
     
    15801586    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15811587let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
    1582 | GOTO x_879 -> h_GOTO x_879
     1588| GOTO x_20533 -> h_GOTO x_20533
    15831589| RETURN -> h_RETURN
    1584 | TAILCALL (x_881, x_880) -> h_TAILCALL __ x_881 x_880
     1590| TAILCALL (x_20535, x_20534) -> h_TAILCALL __ x_20535 x_20534
    15851591
    15861592(** val joint_fin_step_rect_Type3 :
     
    15881594    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15891595let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
    1590 | GOTO x_887 -> h_GOTO x_887
     1596| GOTO x_20541 -> h_GOTO x_20541
    15911597| RETURN -> h_RETURN
    1592 | TAILCALL (x_889, x_888) -> h_TAILCALL __ x_889 x_888
     1598| TAILCALL (x_20543, x_20542) -> h_TAILCALL __ x_20543 x_20542
    15931599
    15941600(** val joint_fin_step_rect_Type2 :
     
    15961602    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15971603let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
    1598 | GOTO x_895 -> h_GOTO x_895
     1604| GOTO x_20549 -> h_GOTO x_20549
    15991605| RETURN -> h_RETURN
    1600 | TAILCALL (x_897, x_896) -> h_TAILCALL __ x_897 x_896
     1606| TAILCALL (x_20551, x_20550) -> h_TAILCALL __ x_20551 x_20550
    16011607
    16021608(** val joint_fin_step_rect_Type1 :
     
    16041610    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16051611let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
    1606 | GOTO x_903 -> h_GOTO x_903
     1612| GOTO x_20557 -> h_GOTO x_20557
    16071613| RETURN -> h_RETURN
    1608 | TAILCALL (x_905, x_904) -> h_TAILCALL __ x_905 x_904
     1614| TAILCALL (x_20559, x_20558) -> h_TAILCALL __ x_20559 x_20558
    16091615
    16101616(** val joint_fin_step_rect_Type0 :
     
    16121618    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16131619let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
    1614 | GOTO x_911 -> h_GOTO x_911
     1620| GOTO x_20565 -> h_GOTO x_20565
    16151621| RETURN -> h_RETURN
    1616 | TAILCALL (x_913, x_912) -> h_TAILCALL __ x_913 x_912
     1622| TAILCALL (x_20567, x_20566) -> h_TAILCALL __ x_20567 x_20566
    16171623
    16181624(** val joint_fin_step_inv_rect_Type4 :
     
    16861692    'a1) -> joint_statement -> 'a1 **)
    16871693let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
    1688 | Sequential (x_979, x_978) -> h_sequential x_979 x_978
    1689 | Final x_980 -> h_final x_980
    1690 | FCOND (x_983, x_982, x_981) -> h_FCOND __ x_983 x_982 x_981
     1694| Sequential (x_20633, x_20632) -> h_sequential x_20633 x_20632
     1695| Final x_20634 -> h_final x_20634
     1696| FCOND (x_20637, x_20636, x_20635) -> h_FCOND __ x_20637 x_20636 x_20635
    16911697
    16921698(** val joint_statement_rect_Type5 :
     
    16951701    'a1) -> joint_statement -> 'a1 **)
    16961702let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
    1697 | Sequential (x_990, x_989) -> h_sequential x_990 x_989
    1698 | Final x_991 -> h_final x_991
    1699 | FCOND (x_994, x_993, x_992) -> h_FCOND __ x_994 x_993 x_992
     1703| Sequential (x_20644, x_20643) -> h_sequential x_20644 x_20643
     1704| Final x_20645 -> h_final x_20645
     1705| FCOND (x_20648, x_20647, x_20646) -> h_FCOND __ x_20648 x_20647 x_20646
    17001706
    17011707(** val joint_statement_rect_Type3 :
     
    17041710    'a1) -> joint_statement -> 'a1 **)
    17051711let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
    1706 | Sequential (x_1001, x_1000) -> h_sequential x_1001 x_1000
    1707 | Final x_1002 -> h_final x_1002
    1708 | FCOND (x_1005, x_1004, x_1003) -> h_FCOND __ x_1005 x_1004 x_1003
     1712| Sequential (x_20655, x_20654) -> h_sequential x_20655 x_20654
     1713| Final x_20656 -> h_final x_20656
     1714| FCOND (x_20659, x_20658, x_20657) -> h_FCOND __ x_20659 x_20658 x_20657
    17091715
    17101716(** val joint_statement_rect_Type2 :
     
    17131719    'a1) -> joint_statement -> 'a1 **)
    17141720let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
    1715 | Sequential (x_1012, x_1011) -> h_sequential x_1012 x_1011
    1716 | Final x_1013 -> h_final x_1013
    1717 | FCOND (x_1016, x_1015, x_1014) -> h_FCOND __ x_1016 x_1015 x_1014
     1721| Sequential (x_20666, x_20665) -> h_sequential x_20666 x_20665
     1722| Final x_20667 -> h_final x_20667
     1723| FCOND (x_20670, x_20669, x_20668) -> h_FCOND __ x_20670 x_20669 x_20668
    17181724
    17191725(** val joint_statement_rect_Type1 :
     
    17221728    'a1) -> joint_statement -> 'a1 **)
    17231729let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
    1724 | Sequential (x_1023, x_1022) -> h_sequential x_1023 x_1022
    1725 | Final x_1024 -> h_final x_1024
    1726 | FCOND (x_1027, x_1026, x_1025) -> h_FCOND __ x_1027 x_1026 x_1025
     1730| Sequential (x_20677, x_20676) -> h_sequential x_20677 x_20676
     1731| Final x_20678 -> h_final x_20678
     1732| FCOND (x_20681, x_20680, x_20679) -> h_FCOND __ x_20681 x_20680 x_20679
    17271733
    17281734(** val joint_statement_rect_Type0 :
     
    17311737    'a1) -> joint_statement -> 'a1 **)
    17321738let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
    1733 | Sequential (x_1034, x_1033) -> h_sequential x_1034 x_1033
    1734 | Final x_1035 -> h_final x_1035
    1735 | FCOND (x_1038, x_1037, x_1036) -> h_FCOND __ x_1038 x_1037 x_1036
     1739| Sequential (x_20688, x_20687) -> h_sequential x_20688 x_20687
     1740| Final x_20689 -> h_final x_20689
     1741| FCOND (x_20692, x_20691, x_20690) -> h_FCOND __ x_20692 x_20691 x_20690
    17361742
    17371743(** val joint_statement_inv_rect_Type4 :
     
    18321838    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18331839    'a1 **)
    1834 let rec params_rect_Type4 h_mk_params x_1111 =
     1840let rec params_rect_Type4 h_mk_params x_20765 =
    18351841  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1836     point_of_label0; point_of_succ = point_of_succ0 } = x_1111
     1842    point_of_label0; point_of_succ = point_of_succ0 } = x_20765
    18371843  in
    18381844  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18431849    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18441850    'a1 **)
    1845 let rec params_rect_Type5 h_mk_params x_1113 =
     1851let rec params_rect_Type5 h_mk_params x_20767 =
    18461852  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1847     point_of_label0; point_of_succ = point_of_succ0 } = x_1113
     1853    point_of_label0; point_of_succ = point_of_succ0 } = x_20767
    18481854  in
    18491855  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18541860    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18551861    'a1 **)
    1856 let rec params_rect_Type3 h_mk_params x_1115 =
     1862let rec params_rect_Type3 h_mk_params x_20769 =
    18571863  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1858     point_of_label0; point_of_succ = point_of_succ0 } = x_1115
     1864    point_of_label0; point_of_succ = point_of_succ0 } = x_20769
    18591865  in
    18601866  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18651871    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18661872    'a1 **)
    1867 let rec params_rect_Type2 h_mk_params x_1117 =
     1873let rec params_rect_Type2 h_mk_params x_20771 =
    18681874  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1869     point_of_label0; point_of_succ = point_of_succ0 } = x_1117
     1875    point_of_label0; point_of_succ = point_of_succ0 } = x_20771
    18701876  in
    18711877  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18761882    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18771883    'a1 **)
    1878 let rec params_rect_Type1 h_mk_params x_1119 =
     1884let rec params_rect_Type1 h_mk_params x_20773 =
    18791885  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1880     point_of_label0; point_of_succ = point_of_succ0 } = x_1119
     1886    point_of_label0; point_of_succ = point_of_succ0 } = x_20773
    18811887  in
    18821888  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18871893    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18881894    'a1 **)
    1889 let rec params_rect_Type0 h_mk_params x_1121 =
     1895let rec params_rect_Type0 h_mk_params x_20775 =
    18901896  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1891     point_of_label0; point_of_succ = point_of_succ0 } = x_1121
     1897    point_of_label0; point_of_succ = point_of_succ0 } = x_20775
    18921898  in
    18931899  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    20242030
    20252031(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2026 let rec lin_params_rect_Type4 h_mk_lin_params x_1144 =
    2027   let l_u_pars = x_1144 in h_mk_lin_params l_u_pars
     2032let rec lin_params_rect_Type4 h_mk_lin_params x_20798 =
     2033  let l_u_pars = x_20798 in h_mk_lin_params l_u_pars
    20282034
    20292035(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2030 let rec lin_params_rect_Type5 h_mk_lin_params x_1146 =
    2031   let l_u_pars = x_1146 in h_mk_lin_params l_u_pars
     2036let rec lin_params_rect_Type5 h_mk_lin_params x_20800 =
     2037  let l_u_pars = x_20800 in h_mk_lin_params l_u_pars
    20322038
    20332039(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2034 let rec lin_params_rect_Type3 h_mk_lin_params x_1148 =
    2035   let l_u_pars = x_1148 in h_mk_lin_params l_u_pars
     2040let rec lin_params_rect_Type3 h_mk_lin_params x_20802 =
     2041  let l_u_pars = x_20802 in h_mk_lin_params l_u_pars
    20362042
    20372043(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2038 let rec lin_params_rect_Type2 h_mk_lin_params x_1150 =
    2039   let l_u_pars = x_1150 in h_mk_lin_params l_u_pars
     2044let rec lin_params_rect_Type2 h_mk_lin_params x_20804 =
     2045  let l_u_pars = x_20804 in h_mk_lin_params l_u_pars
    20402046
    20412047(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2042 let rec lin_params_rect_Type1 h_mk_lin_params x_1152 =
    2043   let l_u_pars = x_1152 in h_mk_lin_params l_u_pars
     2048let rec lin_params_rect_Type1 h_mk_lin_params x_20806 =
     2049  let l_u_pars = x_20806 in h_mk_lin_params l_u_pars
    20442050
    20452051(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2046 let rec lin_params_rect_Type0 h_mk_lin_params x_1154 =
    2047   let l_u_pars = x_1154 in h_mk_lin_params l_u_pars
     2052let rec lin_params_rect_Type0 h_mk_lin_params x_20808 =
     2053  let l_u_pars = x_20808 in h_mk_lin_params l_u_pars
    20482054
    20492055(** val l_u_pars : lin_params -> uns_params **)
     
    21192125(** val graph_params_rect_Type4 :
    21202126    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2121 let rec graph_params_rect_Type4 h_mk_graph_params x_1170 =
    2122   let g_u_pars = x_1170 in h_mk_graph_params g_u_pars
     2127let rec graph_params_rect_Type4 h_mk_graph_params x_20824 =
     2128  let g_u_pars = x_20824 in h_mk_graph_params g_u_pars
    21232129
    21242130(** val graph_params_rect_Type5 :
    21252131    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2126 let rec graph_params_rect_Type5 h_mk_graph_params x_1172 =
    2127   let g_u_pars = x_1172 in h_mk_graph_params g_u_pars
     2132let rec graph_params_rect_Type5 h_mk_graph_params x_20826 =
     2133  let g_u_pars = x_20826 in h_mk_graph_params g_u_pars
    21282134
    21292135(** val graph_params_rect_Type3 :
    21302136    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2131 let rec graph_params_rect_Type3 h_mk_graph_params x_1174 =
    2132   let g_u_pars = x_1174 in h_mk_graph_params g_u_pars
     2137let rec graph_params_rect_Type3 h_mk_graph_params x_20828 =
     2138  let g_u_pars = x_20828 in h_mk_graph_params g_u_pars
    21332139
    21342140(** val graph_params_rect_Type2 :
    21352141    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2136 let rec graph_params_rect_Type2 h_mk_graph_params x_1176 =
    2137   let g_u_pars = x_1176 in h_mk_graph_params g_u_pars
     2142let rec graph_params_rect_Type2 h_mk_graph_params x_20830 =
     2143  let g_u_pars = x_20830 in h_mk_graph_params g_u_pars
    21382144
    21392145(** val graph_params_rect_Type1 :
    21402146    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2141 let rec graph_params_rect_Type1 h_mk_graph_params x_1178 =
    2142   let g_u_pars = x_1178 in h_mk_graph_params g_u_pars
     2147let rec graph_params_rect_Type1 h_mk_graph_params x_20832 =
     2148  let g_u_pars = x_20832 in h_mk_graph_params g_u_pars
    21432149
    21442150(** val graph_params_rect_Type0 :
    21452151    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2146 let rec graph_params_rect_Type0 h_mk_graph_params x_1180 =
    2147   let g_u_pars = x_1180 in h_mk_graph_params g_u_pars
     2152let rec graph_params_rect_Type0 h_mk_graph_params x_20834 =
     2153  let g_u_pars = x_20834 in h_mk_graph_params g_u_pars
    21482154
    21492155(** val g_u_pars : graph_params -> uns_params **)
     
    22152221    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22162222    'a1) -> joint_internal_function -> 'a1 **)
    2217 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_1196 =
     2223let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20850 =
    22182224  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22192225    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22212227    joint_if_stacksize0; joint_if_local_stacksize =
    22222228    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2223     joint_if_entry = joint_if_entry0 } = x_1196
     2229    joint_if_entry = joint_if_entry0 } = x_20850
    22242230  in
    22252231  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22312237    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22322238    'a1) -> joint_internal_function -> 'a1 **)
    2233 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_1198 =
     2239let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20852 =
    22342240  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22352241    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22372243    joint_if_stacksize0; joint_if_local_stacksize =
    22382244    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2239     joint_if_entry = joint_if_entry0 } = x_1198
     2245    joint_if_entry = joint_if_entry0 } = x_20852
    22402246  in
    22412247  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22472253    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22482254    'a1) -> joint_internal_function -> 'a1 **)
    2249 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_1200 =
     2255let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20854 =
    22502256  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22512257    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22532259    joint_if_stacksize0; joint_if_local_stacksize =
    22542260    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2255     joint_if_entry = joint_if_entry0 } = x_1200
     2261    joint_if_entry = joint_if_entry0 } = x_20854
    22562262  in
    22572263  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22632269    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22642270    'a1) -> joint_internal_function -> 'a1 **)
    2265 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_1202 =
     2271let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20856 =
    22662272  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22672273    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22692275    joint_if_stacksize0; joint_if_local_stacksize =
    22702276    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2271     joint_if_entry = joint_if_entry0 } = x_1202
     2277    joint_if_entry = joint_if_entry0 } = x_20856
    22722278  in
    22732279  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22792285    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22802286    'a1) -> joint_internal_function -> 'a1 **)
    2281 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_1204 =
     2287let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20858 =
    22822288  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22832289    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22852291    joint_if_stacksize0; joint_if_local_stacksize =
    22862292    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2287     joint_if_entry = joint_if_entry0 } = x_1204
     2293    joint_if_entry = joint_if_entry0 } = x_20858
    22882294  in
    22892295  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22952301    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22962302    'a1) -> joint_internal_function -> 'a1 **)
    2297 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_1206 =
     2303let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20860 =
    22982304  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22992305    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    23012307    joint_if_stacksize0; joint_if_local_stacksize =
    23022308    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2303     joint_if_entry = joint_if_entry0 } = x_1206
     2309    joint_if_entry = joint_if_entry0 } = x_20860
    23042310  in
    23052311  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    23982404(** val good_if_rect_Type4 :
    23992405    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2400     __ -> __ -> __ -> 'a1) -> 'a1 **)
     2406    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24012407let rec good_if_rect_Type4 p globals def h_mk_good_if =
    2402   h_mk_good_if __ __ __ __ __
     2408  h_mk_good_if __ __ __ __ __ __
    24032409
    24042410(** val good_if_rect_Type5 :
    24052411    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2406     __ -> __ -> __ -> 'a1) -> 'a1 **)
     2412    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24072413let rec good_if_rect_Type5 p globals def h_mk_good_if =
    2408   h_mk_good_if __ __ __ __ __
     2414  h_mk_good_if __ __ __ __ __ __
    24092415
    24102416(** val good_if_rect_Type3 :
    24112417    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2412     __ -> __ -> __ -> 'a1) -> 'a1 **)
     2418    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24132419let rec good_if_rect_Type3 p globals def h_mk_good_if =
    2414   h_mk_good_if __ __ __ __ __
     2420  h_mk_good_if __ __ __ __ __ __
    24152421
    24162422(** val good_if_rect_Type2 :
    24172423    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2418     __ -> __ -> __ -> 'a1) -> 'a1 **)
     2424    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24192425let rec good_if_rect_Type2 p globals def h_mk_good_if =
    2420   h_mk_good_if __ __ __ __ __
     2426  h_mk_good_if __ __ __ __ __ __
    24212427
    24222428(** val good_if_rect_Type1 :
    24232429    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2424     __ -> __ -> __ -> 'a1) -> 'a1 **)
     2430    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24252431let rec good_if_rect_Type1 p globals def h_mk_good_if =
    2426   h_mk_good_if __ __ __ __ __
     2432  h_mk_good_if __ __ __ __ __ __
    24272433
    24282434(** val good_if_rect_Type0 :
    24292435    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2430     __ -> __ -> __ -> 'a1) -> 'a1 **)
     2436    __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24312437let rec good_if_rect_Type0 p globals def h_mk_good_if =
    2432   h_mk_good_if __ __ __ __ __
     2438  h_mk_good_if __ __ __ __ __ __
    24332439
    24342440(** val good_if_inv_rect_Type4 :
    24352441    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2436     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2442    __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24372443let good_if_inv_rect_Type4 x1 x2 x3 h1 =
    24382444  let hcut = good_if_rect_Type4 x1 x2 x3 h1 in hcut __
     
    24402446(** val good_if_inv_rect_Type3 :
    24412447    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2442     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2448    __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24432449let good_if_inv_rect_Type3 x1 x2 x3 h1 =
    24442450  let hcut = good_if_rect_Type3 x1 x2 x3 h1 in hcut __
     
    24462452(** val good_if_inv_rect_Type2 :
    24472453    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2448     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2454    __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24492455let good_if_inv_rect_Type2 x1 x2 x3 h1 =
    24502456  let hcut = good_if_rect_Type2 x1 x2 x3 h1 in hcut __
     
    24522458(** val good_if_inv_rect_Type1 :
    24532459    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2454     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2460    __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24552461let good_if_inv_rect_Type1 x1 x2 x3 h1 =
    24562462  let hcut = good_if_rect_Type1 x1 x2 x3 h1 in hcut __
     
    24582464(** val good_if_inv_rect_Type0 :
    24592465    params -> AST.ident List.list -> joint_internal_function -> (__ -> __ ->
    2460     __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
     2466    __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    24612467let good_if_inv_rect_Type0 x1 x2 x3 h1 =
    24622468  let hcut = good_if_rect_Type0 x1 x2 x3 h1 in hcut __
    2463 
    2464 (** val good_if_discr :
    2465     params -> AST.ident List.list -> joint_internal_function -> __ **)
    2466 let good_if_discr a1 a2 a3 =
    2467   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
    24682469
    24692470(** val good_if_jmdiscr :
    24702471    params -> AST.ident List.list -> joint_internal_function -> __ **)
    24712472let good_if_jmdiscr a1 a2 a3 =
    2472   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __)) __
     2473  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) __
    24732474
    24742475type joint_closed_internal_function = joint_internal_function Types.sig0
Note: See TracChangeset for help on using the changeset viewer.