Changeset 2854 for extracted/joint.ml


Ignore:
Timestamp:
Mar 12, 2013, 5:53:56 PM (7 years ago)
Author:
sacerdot
Message:

Pretty printing of the LTL program.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint.ml

    r2827 r2854  
    110110    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    111111let rec argument_rect_Type4 h_Reg h_Imm = function
    112 | Reg x_19661 -> h_Reg x_19661
    113 | Imm x_19662 -> h_Imm x_19662
     112| Reg x_7 -> h_Reg x_7
     113| Imm x_8 -> h_Imm x_8
    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_19666 -> h_Reg x_19666
    119 | Imm x_19667 -> h_Imm x_19667
     118| Reg x_12 -> h_Reg x_12
     119| Imm x_13 -> h_Imm x_13
    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_19671 -> h_Reg x_19671
    125 | Imm x_19672 -> h_Imm x_19672
     124| Reg x_17 -> h_Reg x_17
     125| Imm x_18 -> h_Imm x_18
    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_19676 -> h_Reg x_19676
    131 | Imm x_19677 -> h_Imm x_19677
     130| Reg x_22 -> h_Reg x_22
     131| Imm x_23 -> h_Imm x_23
    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_19681 -> h_Reg x_19681
    137 | Imm x_19682 -> h_Imm x_19682
     136| Reg x_27 -> h_Reg x_27
     137| Imm x_28 -> h_Imm x_28
    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_19686 -> h_Reg x_19686
    143 | Imm x_19687 -> h_Imm x_19687
     142| Reg x_32 -> h_Reg x_32
     143| Imm x_33 -> h_Imm x_33
    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_19722 =
     326let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_68 =
    327327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    328     x_19722
     328    x_68
    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_19724 =
     337let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_70 =
    338338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    339     x_19724
     339    x_70
    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_19726 =
     348let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_72 =
    349349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    350     x_19726
     350    x_72
    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_19728 =
     359let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_74 =
    360360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    361     x_19728
     361    x_74
    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_19730 =
     370let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_76 =
    371371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    372     x_19730
     372    x_76
    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_19732 =
     381let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_78 =
    382382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    383     x_19732
     383    x_78
    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_19749 =
     508let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_95 =
    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_19749
     514    params_regs0 } = x_95
    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_19751 =
     531let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_97 =
    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_19751
     537    params_regs0 } = x_97
    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_19753 =
     554let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_99 =
    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_19753
     560    params_regs0 } = x_99
    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_19755 =
     577let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_101 =
    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_19755
     583    params_regs0 } = x_101
    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_19757 =
     600let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_103 =
    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_19757
     606    params_regs0 } = x_103
    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_19759 =
     623let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_105 =
    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_19759
     629    params_regs0 } = x_105
    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_19789 =
    808   let { u_pars = u_pars0; functs = functs0 } = x_19789 in
     807let rec uns_params_rect_Type4 h_mk_uns_params x_135 =
     808  let { u_pars = u_pars0; functs = functs0 } = x_135 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_19791 =
    815   let { u_pars = u_pars0; functs = functs0 } = x_19791 in
     814let rec uns_params_rect_Type5 h_mk_uns_params x_137 =
     815  let { u_pars = u_pars0; functs = functs0 } = x_137 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_19793 =
    822   let { u_pars = u_pars0; functs = functs0 } = x_19793 in
     821let rec uns_params_rect_Type3 h_mk_uns_params x_139 =
     822  let { u_pars = u_pars0; functs = functs0 } = x_139 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_19795 =
    829   let { u_pars = u_pars0; functs = functs0 } = x_19795 in
     828let rec uns_params_rect_Type2 h_mk_uns_params x_141 =
     829  let { u_pars = u_pars0; functs = functs0 } = x_141 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_19797 =
    836   let { u_pars = u_pars0; functs = functs0 } = x_19797 in
     835let rec uns_params_rect_Type1 h_mk_uns_params x_143 =
     836  let { u_pars = u_pars0; functs = functs0 } = x_143 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_19799 =
    843   let { u_pars = u_pars0; functs = functs0 } = x_19799 in
     842let rec uns_params_rect_Type0 h_mk_uns_params x_145 =
     843  let { u_pars = u_pars0; functs = functs0 } = x_145 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_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
     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
    923922| CLEAR_CARRY -> h_CLEAR_CARRY
    924923| SET_CARRY -> h_SET_CARRY
    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
     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
    928927
    929928(** val joint_seq_rect_Type5 :
     
    935934    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    936935let 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_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
     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
    947945| CLEAR_CARRY -> h_CLEAR_CARRY
    948946| SET_CARRY -> h_SET_CARRY
    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
     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
    952950
    953951(** val joint_seq_rect_Type3 :
     
    959957    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    960958let 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_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
     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
    971968| CLEAR_CARRY -> h_CLEAR_CARRY
    972969| SET_CARRY -> h_SET_CARRY
    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
     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
    976973
    977974(** val joint_seq_rect_Type2 :
     
    983980    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    984981let 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_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
     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
    995991| CLEAR_CARRY -> h_CLEAR_CARRY
    996992| SET_CARRY -> h_SET_CARRY
    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
     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
    1000996
    1001997(** val joint_seq_rect_Type1 :
     
    10071003    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    10081004let 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_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
     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
    10191014| CLEAR_CARRY -> h_CLEAR_CARRY
    10201015| SET_CARRY -> h_SET_CARRY
    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
     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
    10241019
    10251020(** val joint_seq_rect_Type0 :
     
    10311026    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    10321027let 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_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
     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
    10431037| CLEAR_CARRY -> h_CLEAR_CARRY
    10441038| SET_CARRY -> h_SET_CARRY
    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
     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
    10481042
    10491043(** val joint_seq_inv_rect_Type4 :
     
    12361230    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12371231let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     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
    12421236
    12431237(** val joint_step_rect_Type5 :
     
    12461240    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12471241let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     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
    12521246
    12531247(** val joint_step_rect_Type3 :
     
    12561250    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12571251let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     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
    12621256
    12631257(** val joint_step_rect_Type2 :
     
    12661260    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12671261let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     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
    12721266
    12731267(** val joint_step_rect_Type1 :
     
    12761270    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12771271let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     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
    12821276
    12831277(** val joint_step_rect_Type0 :
     
    12861280    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12871281let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    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
     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
    12921286
    12931287(** val joint_step_inv_rect_Type4 :
     
    13591353| COST_LABEL c -> List.Nil
    13601354| CALL (id, args, dest) ->
    1361   List.append (functs0.f_call_args args) (functs0.f_call_dest dest)
     1355  let r_id =
     1356    match id with
     1357    | Types.Inl x -> List.Nil
     1358    | Types.Inr ptr ->
     1359      List.append (functs0.dpl_args ptr.Types.fst)
     1360        (functs0.dph_args ptr.Types.snd)
     1361  in
     1362  List.append r_id
     1363    (List.append (functs0.f_call_args args) (functs0.f_call_dest dest))
    13621364| COND (r, lbl) -> functs0.acc_a_regs r
    13631365| Step_seq s -> get_used_registers_from_seq p globals functs0 s
     
    14561458    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14571459    'a1) -> stmt_params -> 'a1 **)
    1458 let rec stmt_params_rect_Type4 h_mk_stmt_params x_20491 =
     1460let rec stmt_params_rect_Type4 h_mk_stmt_params x_837 =
    14591461  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1460     has_fcond0 } = x_20491
     1462    has_fcond0 } = x_837
    14611463  in
    14621464  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14651467    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14661468    'a1) -> stmt_params -> 'a1 **)
    1467 let rec stmt_params_rect_Type5 h_mk_stmt_params x_20493 =
     1469let rec stmt_params_rect_Type5 h_mk_stmt_params x_839 =
    14681470  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1469     has_fcond0 } = x_20493
     1471    has_fcond0 } = x_839
    14701472  in
    14711473  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14741476    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14751477    'a1) -> stmt_params -> 'a1 **)
    1476 let rec stmt_params_rect_Type3 h_mk_stmt_params x_20495 =
     1478let rec stmt_params_rect_Type3 h_mk_stmt_params x_841 =
    14771479  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1478     has_fcond0 } = x_20495
     1480    has_fcond0 } = x_841
    14791481  in
    14801482  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14831485    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14841486    'a1) -> stmt_params -> 'a1 **)
    1485 let rec stmt_params_rect_Type2 h_mk_stmt_params x_20497 =
     1487let rec stmt_params_rect_Type2 h_mk_stmt_params x_843 =
    14861488  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1487     has_fcond0 } = x_20497
     1489    has_fcond0 } = x_843
    14881490  in
    14891491  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14921494    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14931495    'a1) -> stmt_params -> 'a1 **)
    1494 let rec stmt_params_rect_Type1 h_mk_stmt_params x_20499 =
     1496let rec stmt_params_rect_Type1 h_mk_stmt_params x_845 =
    14951497  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1496     has_fcond0 } = x_20499
     1498    has_fcond0 } = x_845
    14971499  in
    14981500  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15011503    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    15021504    'a1) -> stmt_params -> 'a1 **)
    1503 let rec stmt_params_rect_Type0 h_mk_stmt_params x_20501 =
     1505let rec stmt_params_rect_Type0 h_mk_stmt_params x_847 =
    15041506  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1505     has_fcond0 } = x_20501
     1507    has_fcond0 } = x_847
    15061508  in
    15071509  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15701572    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15711573let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
    1572 | GOTO x_20525 -> h_GOTO x_20525
     1574| GOTO x_871 -> h_GOTO x_871
    15731575| RETURN -> h_RETURN
    1574 | TAILCALL (x_20527, x_20526) -> h_TAILCALL __ x_20527 x_20526
     1576| TAILCALL (x_873, x_872) -> h_TAILCALL __ x_873 x_872
    15751577
    15761578(** val joint_fin_step_rect_Type5 :
     
    15781580    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15791581let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
    1580 | GOTO x_20533 -> h_GOTO x_20533
     1582| GOTO x_879 -> h_GOTO x_879
    15811583| RETURN -> h_RETURN
    1582 | TAILCALL (x_20535, x_20534) -> h_TAILCALL __ x_20535 x_20534
     1584| TAILCALL (x_881, x_880) -> h_TAILCALL __ x_881 x_880
    15831585
    15841586(** val joint_fin_step_rect_Type3 :
     
    15861588    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15871589let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
    1588 | GOTO x_20541 -> h_GOTO x_20541
     1590| GOTO x_887 -> h_GOTO x_887
    15891591| RETURN -> h_RETURN
    1590 | TAILCALL (x_20543, x_20542) -> h_TAILCALL __ x_20543 x_20542
     1592| TAILCALL (x_889, x_888) -> h_TAILCALL __ x_889 x_888
    15911593
    15921594(** val joint_fin_step_rect_Type2 :
     
    15941596    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15951597let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
    1596 | GOTO x_20549 -> h_GOTO x_20549
     1598| GOTO x_895 -> h_GOTO x_895
    15971599| RETURN -> h_RETURN
    1598 | TAILCALL (x_20551, x_20550) -> h_TAILCALL __ x_20551 x_20550
     1600| TAILCALL (x_897, x_896) -> h_TAILCALL __ x_897 x_896
    15991601
    16001602(** val joint_fin_step_rect_Type1 :
     
    16021604    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16031605let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
    1604 | GOTO x_20557 -> h_GOTO x_20557
     1606| GOTO x_903 -> h_GOTO x_903
    16051607| RETURN -> h_RETURN
    1606 | TAILCALL (x_20559, x_20558) -> h_TAILCALL __ x_20559 x_20558
     1608| TAILCALL (x_905, x_904) -> h_TAILCALL __ x_905 x_904
    16071609
    16081610(** val joint_fin_step_rect_Type0 :
     
    16101612    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16111613let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
    1612 | GOTO x_20565 -> h_GOTO x_20565
     1614| GOTO x_911 -> h_GOTO x_911
    16131615| RETURN -> h_RETURN
    1614 | TAILCALL (x_20567, x_20566) -> h_TAILCALL __ x_20567 x_20566
     1616| TAILCALL (x_913, x_912) -> h_TAILCALL __ x_913 x_912
    16151617
    16161618(** val joint_fin_step_inv_rect_Type4 :
     
    16841686    'a1) -> joint_statement -> 'a1 **)
    16851687let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
    1686 | Sequential (x_20633, x_20632) -> h_sequential x_20633 x_20632
    1687 | Final x_20634 -> h_final x_20634
    1688 | FCOND (x_20637, x_20636, x_20635) -> h_FCOND __ x_20637 x_20636 x_20635
     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
    16891691
    16901692(** val joint_statement_rect_Type5 :
     
    16931695    'a1) -> joint_statement -> 'a1 **)
    16941696let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
    1695 | Sequential (x_20644, x_20643) -> h_sequential x_20644 x_20643
    1696 | Final x_20645 -> h_final x_20645
    1697 | FCOND (x_20648, x_20647, x_20646) -> h_FCOND __ x_20648 x_20647 x_20646
     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
    16981700
    16991701(** val joint_statement_rect_Type3 :
     
    17021704    'a1) -> joint_statement -> 'a1 **)
    17031705let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
    1704 | Sequential (x_20655, x_20654) -> h_sequential x_20655 x_20654
    1705 | Final x_20656 -> h_final x_20656
    1706 | FCOND (x_20659, x_20658, x_20657) -> h_FCOND __ x_20659 x_20658 x_20657
     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
    17071709
    17081710(** val joint_statement_rect_Type2 :
     
    17111713    'a1) -> joint_statement -> 'a1 **)
    17121714let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
    1713 | Sequential (x_20666, x_20665) -> h_sequential x_20666 x_20665
    1714 | Final x_20667 -> h_final x_20667
    1715 | FCOND (x_20670, x_20669, x_20668) -> h_FCOND __ x_20670 x_20669 x_20668
     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
    17161718
    17171719(** val joint_statement_rect_Type1 :
     
    17201722    'a1) -> joint_statement -> 'a1 **)
    17211723let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
    1722 | Sequential (x_20677, x_20676) -> h_sequential x_20677 x_20676
    1723 | Final x_20678 -> h_final x_20678
    1724 | FCOND (x_20681, x_20680, x_20679) -> h_FCOND __ x_20681 x_20680 x_20679
     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
    17251727
    17261728(** val joint_statement_rect_Type0 :
     
    17291731    'a1) -> joint_statement -> 'a1 **)
    17301732let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
    1731 | Sequential (x_20688, x_20687) -> h_sequential x_20688 x_20687
    1732 | Final x_20689 -> h_final x_20689
    1733 | FCOND (x_20692, x_20691, x_20690) -> h_FCOND __ x_20692 x_20691 x_20690
     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
    17341736
    17351737(** val joint_statement_inv_rect_Type4 :
     
    18301832    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18311833    'a1 **)
    1832 let rec params_rect_Type4 h_mk_params x_20765 =
     1834let rec params_rect_Type4 h_mk_params x_1111 =
    18331835  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1834     point_of_label0; point_of_succ = point_of_succ0 } = x_20765
     1836    point_of_label0; point_of_succ = point_of_succ0 } = x_1111
    18351837  in
    18361838  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18411843    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18421844    'a1 **)
    1843 let rec params_rect_Type5 h_mk_params x_20767 =
     1845let rec params_rect_Type5 h_mk_params x_1113 =
    18441846  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1845     point_of_label0; point_of_succ = point_of_succ0 } = x_20767
     1847    point_of_label0; point_of_succ = point_of_succ0 } = x_1113
    18461848  in
    18471849  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18521854    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18531855    'a1 **)
    1854 let rec params_rect_Type3 h_mk_params x_20769 =
     1856let rec params_rect_Type3 h_mk_params x_1115 =
    18551857  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1856     point_of_label0; point_of_succ = point_of_succ0 } = x_20769
     1858    point_of_label0; point_of_succ = point_of_succ0 } = x_1115
    18571859  in
    18581860  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18631865    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18641866    'a1 **)
    1865 let rec params_rect_Type2 h_mk_params x_20771 =
     1867let rec params_rect_Type2 h_mk_params x_1117 =
    18661868  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1867     point_of_label0; point_of_succ = point_of_succ0 } = x_20771
     1869    point_of_label0; point_of_succ = point_of_succ0 } = x_1117
    18681870  in
    18691871  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18741876    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18751877    'a1 **)
    1876 let rec params_rect_Type1 h_mk_params x_20773 =
     1878let rec params_rect_Type1 h_mk_params x_1119 =
    18771879  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1878     point_of_label0; point_of_succ = point_of_succ0 } = x_20773
     1880    point_of_label0; point_of_succ = point_of_succ0 } = x_1119
    18791881  in
    18801882  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18851887    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18861888    'a1 **)
    1887 let rec params_rect_Type0 h_mk_params x_20775 =
     1889let rec params_rect_Type0 h_mk_params x_1121 =
    18881890  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1889     point_of_label0; point_of_succ = point_of_succ0 } = x_20775
     1891    point_of_label0; point_of_succ = point_of_succ0 } = x_1121
    18901892  in
    18911893  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    20222024
    20232025(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2024 let rec lin_params_rect_Type4 h_mk_lin_params x_20798 =
    2025   let l_u_pars = x_20798 in h_mk_lin_params l_u_pars
     2026let 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
    20262028
    20272029(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2028 let rec lin_params_rect_Type5 h_mk_lin_params x_20800 =
    2029   let l_u_pars = x_20800 in h_mk_lin_params l_u_pars
     2030let 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
    20302032
    20312033(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2032 let rec lin_params_rect_Type3 h_mk_lin_params x_20802 =
    2033   let l_u_pars = x_20802 in h_mk_lin_params l_u_pars
     2034let 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
    20342036
    20352037(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2036 let rec lin_params_rect_Type2 h_mk_lin_params x_20804 =
    2037   let l_u_pars = x_20804 in h_mk_lin_params l_u_pars
     2038let 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
    20382040
    20392041(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2040 let rec lin_params_rect_Type1 h_mk_lin_params x_20806 =
    2041   let l_u_pars = x_20806 in h_mk_lin_params l_u_pars
     2042let 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
    20422044
    20432045(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2044 let rec lin_params_rect_Type0 h_mk_lin_params x_20808 =
    2045   let l_u_pars = x_20808 in h_mk_lin_params l_u_pars
     2046let 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
    20462048
    20472049(** val l_u_pars : lin_params -> uns_params **)
     
    21172119(** val graph_params_rect_Type4 :
    21182120    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2119 let rec graph_params_rect_Type4 h_mk_graph_params x_20824 =
    2120   let g_u_pars = x_20824 in h_mk_graph_params g_u_pars
     2121let 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
    21212123
    21222124(** val graph_params_rect_Type5 :
    21232125    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2124 let rec graph_params_rect_Type5 h_mk_graph_params x_20826 =
    2125   let g_u_pars = x_20826 in h_mk_graph_params g_u_pars
     2126let 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
    21262128
    21272129(** val graph_params_rect_Type3 :
    21282130    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2129 let rec graph_params_rect_Type3 h_mk_graph_params x_20828 =
    2130   let g_u_pars = x_20828 in h_mk_graph_params g_u_pars
     2131let 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
    21312133
    21322134(** val graph_params_rect_Type2 :
    21332135    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2134 let rec graph_params_rect_Type2 h_mk_graph_params x_20830 =
    2135   let g_u_pars = x_20830 in h_mk_graph_params g_u_pars
     2136let 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
    21362138
    21372139(** val graph_params_rect_Type1 :
    21382140    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2139 let rec graph_params_rect_Type1 h_mk_graph_params x_20832 =
    2140   let g_u_pars = x_20832 in h_mk_graph_params g_u_pars
     2141let 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
    21412143
    21422144(** val graph_params_rect_Type0 :
    21432145    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2144 let rec graph_params_rect_Type0 h_mk_graph_params x_20834 =
    2145   let g_u_pars = x_20834 in h_mk_graph_params g_u_pars
     2146let 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
    21462148
    21472149(** val g_u_pars : graph_params -> uns_params **)
     
    22132215    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22142216    'a1) -> joint_internal_function -> 'a1 **)
    2215 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20850 =
     2217let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_1196 =
    22162218  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22172219    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22192221    joint_if_stacksize0; joint_if_local_stacksize =
    22202222    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2221     joint_if_entry = joint_if_entry0 } = x_20850
     2223    joint_if_entry = joint_if_entry0 } = x_1196
    22222224  in
    22232225  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22292231    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22302232    'a1) -> joint_internal_function -> 'a1 **)
    2231 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20852 =
     2233let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_1198 =
    22322234  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22332235    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22352237    joint_if_stacksize0; joint_if_local_stacksize =
    22362238    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2237     joint_if_entry = joint_if_entry0 } = x_20852
     2239    joint_if_entry = joint_if_entry0 } = x_1198
    22382240  in
    22392241  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22452247    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22462248    'a1) -> joint_internal_function -> 'a1 **)
    2247 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20854 =
     2249let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_1200 =
    22482250  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22492251    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22512253    joint_if_stacksize0; joint_if_local_stacksize =
    22522254    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2253     joint_if_entry = joint_if_entry0 } = x_20854
     2255    joint_if_entry = joint_if_entry0 } = x_1200
    22542256  in
    22552257  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22612263    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22622264    'a1) -> joint_internal_function -> 'a1 **)
    2263 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20856 =
     2265let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_1202 =
    22642266  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22652267    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22672269    joint_if_stacksize0; joint_if_local_stacksize =
    22682270    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2269     joint_if_entry = joint_if_entry0 } = x_20856
     2271    joint_if_entry = joint_if_entry0 } = x_1202
    22702272  in
    22712273  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22772279    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22782280    'a1) -> joint_internal_function -> 'a1 **)
    2279 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20858 =
     2281let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_1204 =
    22802282  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22812283    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22832285    joint_if_stacksize0; joint_if_local_stacksize =
    22842286    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2285     joint_if_entry = joint_if_entry0 } = x_20858
     2287    joint_if_entry = joint_if_entry0 } = x_1204
    22862288  in
    22872289  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22932295    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22942296    'a1) -> joint_internal_function -> 'a1 **)
    2295 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20860 =
     2297let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_1206 =
    22962298  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22972299    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22992301    joint_if_stacksize0; joint_if_local_stacksize =
    23002302    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2301     joint_if_entry = joint_if_entry0 } = x_20860
     2303    joint_if_entry = joint_if_entry0 } = x_1206
    23022304  in
    23032305  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
Note: See TracChangeset for help on using the changeset viewer.