Changeset 2997 for extracted/joint.ml


Ignore:
Timestamp:
Mar 28, 2013, 10:27:41 AM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint.ml

    r2951 r2997  
    110110    ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2 **)
    111111let rec argument_rect_Type4 h_Reg h_Imm = function
    112 | Reg x_16908 -> h_Reg x_16908
    113 | Imm x_16909 -> h_Imm x_16909
     112| Reg x_224 -> h_Reg x_224
     113| Imm x_225 -> h_Imm x_225
    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_16913 -> h_Reg x_16913
    119 | Imm x_16914 -> h_Imm x_16914
     118| Reg x_229 -> h_Reg x_229
     119| Imm x_230 -> h_Imm x_230
    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_16918 -> h_Reg x_16918
    125 | Imm x_16919 -> h_Imm x_16919
     124| Reg x_234 -> h_Reg x_234
     125| Imm x_235 -> h_Imm x_235
    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_16923 -> h_Reg x_16923
    131 | Imm x_16924 -> h_Imm x_16924
     130| Reg x_239 -> h_Reg x_239
     131| Imm x_240 -> h_Imm x_240
    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_16928 -> h_Reg x_16928
    137 | Imm x_16929 -> h_Imm x_16929
     136| Reg x_244 -> h_Reg x_244
     137| Imm x_245 -> h_Imm x_245
    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_16933 -> h_Reg x_16933
    143 | Imm x_16934 -> h_Imm x_16934
     142| Reg x_249 -> h_Reg x_249
     143| Imm x_250 -> h_Imm x_250
    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_16969 =
     326let rec unserialized_params_rect_Type4 h_mk_unserialized_params x_285 =
    327327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    328     x_16969
     328    x_285
    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_16971 =
     337let rec unserialized_params_rect_Type5 h_mk_unserialized_params x_287 =
    338338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    339     x_16971
     339    x_287
    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_16973 =
     348let rec unserialized_params_rect_Type3 h_mk_unserialized_params x_289 =
    349349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    350     x_16973
     350    x_289
    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_16975 =
     359let rec unserialized_params_rect_Type2 h_mk_unserialized_params x_291 =
    360360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    361     x_16975
     361    x_291
    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_16977 =
     370let rec unserialized_params_rect_Type1 h_mk_unserialized_params x_293 =
    371371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    372     x_16977
     372    x_293
    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_16979 =
     381let rec unserialized_params_rect_Type0 h_mk_unserialized_params x_295 =
    382382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    383     x_16979
     383    x_295
    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_16996 =
     508let rec get_pseudo_reg_functs_rect_Type4 p h_mk_get_pseudo_reg_functs x_312 =
    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_16996
     514    params_regs0 } = x_312
    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_16998 =
     531let rec get_pseudo_reg_functs_rect_Type5 p h_mk_get_pseudo_reg_functs x_314 =
    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_16998
     537    params_regs0 } = x_314
    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_17000 =
     554let rec get_pseudo_reg_functs_rect_Type3 p h_mk_get_pseudo_reg_functs x_316 =
    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_17000
     560    params_regs0 } = x_316
    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_17002 =
     577let rec get_pseudo_reg_functs_rect_Type2 p h_mk_get_pseudo_reg_functs x_318 =
    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_17002
     583    params_regs0 } = x_318
    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_17004 =
     600let rec get_pseudo_reg_functs_rect_Type1 p h_mk_get_pseudo_reg_functs x_320 =
    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_17004
     606    params_regs0 } = x_320
    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_17006 =
     623let rec get_pseudo_reg_functs_rect_Type0 p h_mk_get_pseudo_reg_functs x_322 =
    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_17006
     629    params_regs0 } = x_322
    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_17036 =
    808   let { u_pars = u_pars0; functs = functs0 } = x_17036 in
     807let rec uns_params_rect_Type4 h_mk_uns_params x_352 =
     808  let { u_pars = u_pars0; functs = functs0 } = x_352 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_17038 =
    815   let { u_pars = u_pars0; functs = functs0 } = x_17038 in
     814let rec uns_params_rect_Type5 h_mk_uns_params x_354 =
     815  let { u_pars = u_pars0; functs = functs0 } = x_354 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_17040 =
    822   let { u_pars = u_pars0; functs = functs0 } = x_17040 in
     821let rec uns_params_rect_Type3 h_mk_uns_params x_356 =
     822  let { u_pars = u_pars0; functs = functs0 } = x_356 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_17042 =
    829   let { u_pars = u_pars0; functs = functs0 } = x_17042 in
     828let rec uns_params_rect_Type2 h_mk_uns_params x_358 =
     829  let { u_pars = u_pars0; functs = functs0 } = x_358 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_17044 =
    836   let { u_pars = u_pars0; functs = functs0 } = x_17044 in
     835let rec uns_params_rect_Type1 h_mk_uns_params x_360 =
     836  let { u_pars = u_pars0; functs = functs0 } = x_360 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_17046 =
    843   let { u_pars = u_pars0; functs = functs0 } = x_17046 in
     842let rec uns_params_rect_Type0 h_mk_uns_params x_362 =
     843  let { u_pars = u_pars0; functs = functs0 } = x_362 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_17101 -> h_COMMENT x_17101
    914 | MOVE x_17102 -> h_MOVE x_17102
    915 | POP x_17103 -> h_POP x_17103
    916 | PUSH x_17104 -> h_PUSH x_17104
    917 | ADDRESS (i, x_17106, x_17105) -> h_ADDRESS i __ x_17106 x_17105
    918 | OPACCS (x_17112, x_17111, x_17110, x_17109, x_17108) ->
    919   h_OPACCS x_17112 x_17111 x_17110 x_17109 x_17108
    920 | OP1 (x_17115, x_17114, x_17113) -> h_OP1 x_17115 x_17114 x_17113
    921 | OP2 (x_17119, x_17118, x_17117, x_17116) ->
    922   h_OP2 x_17119 x_17118 x_17117 x_17116
     913| COMMENT x_417 -> h_COMMENT x_417
     914| MOVE x_418 -> h_MOVE x_418
     915| POP x_419 -> h_POP x_419
     916| PUSH x_420 -> h_PUSH x_420
     917| ADDRESS (i, x_422, x_421) -> h_ADDRESS i __ x_422 x_421
     918| OPACCS (x_428, x_427, x_426, x_425, x_424) ->
     919  h_OPACCS x_428 x_427 x_426 x_425 x_424
     920| OP1 (x_431, x_430, x_429) -> h_OP1 x_431 x_430 x_429
     921| OP2 (x_435, x_434, x_433, x_432) -> h_OP2 x_435 x_434 x_433 x_432
    923922| CLEAR_CARRY -> h_CLEAR_CARRY
    924923| SET_CARRY -> h_SET_CARRY
    925 | LOAD (x_17122, x_17121, x_17120) -> h_LOAD x_17122 x_17121 x_17120
    926 | STORE (x_17125, x_17124, x_17123) -> h_STORE x_17125 x_17124 x_17123
    927 | Extension_seq x_17126 -> h_extension_seq x_17126
     924| LOAD (x_438, x_437, x_436) -> h_LOAD x_438 x_437 x_436
     925| STORE (x_441, x_440, x_439) -> h_STORE x_441 x_440 x_439
     926| Extension_seq x_442 -> h_extension_seq x_442
    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_17141 -> h_COMMENT x_17141
    938 | MOVE x_17142 -> h_MOVE x_17142
    939 | POP x_17143 -> h_POP x_17143
    940 | PUSH x_17144 -> h_PUSH x_17144
    941 | ADDRESS (i, x_17146, x_17145) -> h_ADDRESS i __ x_17146 x_17145
    942 | OPACCS (x_17152, x_17151, x_17150, x_17149, x_17148) ->
    943   h_OPACCS x_17152 x_17151 x_17150 x_17149 x_17148
    944 | OP1 (x_17155, x_17154, x_17153) -> h_OP1 x_17155 x_17154 x_17153
    945 | OP2 (x_17159, x_17158, x_17157, x_17156) ->
    946   h_OP2 x_17159 x_17158 x_17157 x_17156
     936| COMMENT x_457 -> h_COMMENT x_457
     937| MOVE x_458 -> h_MOVE x_458
     938| POP x_459 -> h_POP x_459
     939| PUSH x_460 -> h_PUSH x_460
     940| ADDRESS (i, x_462, x_461) -> h_ADDRESS i __ x_462 x_461
     941| OPACCS (x_468, x_467, x_466, x_465, x_464) ->
     942  h_OPACCS x_468 x_467 x_466 x_465 x_464
     943| OP1 (x_471, x_470, x_469) -> h_OP1 x_471 x_470 x_469
     944| OP2 (x_475, x_474, x_473, x_472) -> h_OP2 x_475 x_474 x_473 x_472
    947945| CLEAR_CARRY -> h_CLEAR_CARRY
    948946| SET_CARRY -> h_SET_CARRY
    949 | LOAD (x_17162, x_17161, x_17160) -> h_LOAD x_17162 x_17161 x_17160
    950 | STORE (x_17165, x_17164, x_17163) -> h_STORE x_17165 x_17164 x_17163
    951 | Extension_seq x_17166 -> h_extension_seq x_17166
     947| LOAD (x_478, x_477, x_476) -> h_LOAD x_478 x_477 x_476
     948| STORE (x_481, x_480, x_479) -> h_STORE x_481 x_480 x_479
     949| Extension_seq x_482 -> h_extension_seq x_482
    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_17181 -> h_COMMENT x_17181
    962 | MOVE x_17182 -> h_MOVE x_17182
    963 | POP x_17183 -> h_POP x_17183
    964 | PUSH x_17184 -> h_PUSH x_17184
    965 | ADDRESS (i, x_17186, x_17185) -> h_ADDRESS i __ x_17186 x_17185
    966 | OPACCS (x_17192, x_17191, x_17190, x_17189, x_17188) ->
    967   h_OPACCS x_17192 x_17191 x_17190 x_17189 x_17188
    968 | OP1 (x_17195, x_17194, x_17193) -> h_OP1 x_17195 x_17194 x_17193
    969 | OP2 (x_17199, x_17198, x_17197, x_17196) ->
    970   h_OP2 x_17199 x_17198 x_17197 x_17196
     959| COMMENT x_497 -> h_COMMENT x_497
     960| MOVE x_498 -> h_MOVE x_498
     961| POP x_499 -> h_POP x_499
     962| PUSH x_500 -> h_PUSH x_500
     963| ADDRESS (i, x_502, x_501) -> h_ADDRESS i __ x_502 x_501
     964| OPACCS (x_508, x_507, x_506, x_505, x_504) ->
     965  h_OPACCS x_508 x_507 x_506 x_505 x_504
     966| OP1 (x_511, x_510, x_509) -> h_OP1 x_511 x_510 x_509
     967| OP2 (x_515, x_514, x_513, x_512) -> h_OP2 x_515 x_514 x_513 x_512
    971968| CLEAR_CARRY -> h_CLEAR_CARRY
    972969| SET_CARRY -> h_SET_CARRY
    973 | LOAD (x_17202, x_17201, x_17200) -> h_LOAD x_17202 x_17201 x_17200
    974 | STORE (x_17205, x_17204, x_17203) -> h_STORE x_17205 x_17204 x_17203
    975 | Extension_seq x_17206 -> h_extension_seq x_17206
     970| LOAD (x_518, x_517, x_516) -> h_LOAD x_518 x_517 x_516
     971| STORE (x_521, x_520, x_519) -> h_STORE x_521 x_520 x_519
     972| Extension_seq x_522 -> h_extension_seq x_522
    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_17221 -> h_COMMENT x_17221
    986 | MOVE x_17222 -> h_MOVE x_17222
    987 | POP x_17223 -> h_POP x_17223
    988 | PUSH x_17224 -> h_PUSH x_17224
    989 | ADDRESS (i, x_17226, x_17225) -> h_ADDRESS i __ x_17226 x_17225
    990 | OPACCS (x_17232, x_17231, x_17230, x_17229, x_17228) ->
    991   h_OPACCS x_17232 x_17231 x_17230 x_17229 x_17228
    992 | OP1 (x_17235, x_17234, x_17233) -> h_OP1 x_17235 x_17234 x_17233
    993 | OP2 (x_17239, x_17238, x_17237, x_17236) ->
    994   h_OP2 x_17239 x_17238 x_17237 x_17236
     982| COMMENT x_537 -> h_COMMENT x_537
     983| MOVE x_538 -> h_MOVE x_538
     984| POP x_539 -> h_POP x_539
     985| PUSH x_540 -> h_PUSH x_540
     986| ADDRESS (i, x_542, x_541) -> h_ADDRESS i __ x_542 x_541
     987| OPACCS (x_548, x_547, x_546, x_545, x_544) ->
     988  h_OPACCS x_548 x_547 x_546 x_545 x_544
     989| OP1 (x_551, x_550, x_549) -> h_OP1 x_551 x_550 x_549
     990| OP2 (x_555, x_554, x_553, x_552) -> h_OP2 x_555 x_554 x_553 x_552
    995991| CLEAR_CARRY -> h_CLEAR_CARRY
    996992| SET_CARRY -> h_SET_CARRY
    997 | LOAD (x_17242, x_17241, x_17240) -> h_LOAD x_17242 x_17241 x_17240
    998 | STORE (x_17245, x_17244, x_17243) -> h_STORE x_17245 x_17244 x_17243
    999 | Extension_seq x_17246 -> h_extension_seq x_17246
     993| LOAD (x_558, x_557, x_556) -> h_LOAD x_558 x_557 x_556
     994| STORE (x_561, x_560, x_559) -> h_STORE x_561 x_560 x_559
     995| Extension_seq x_562 -> h_extension_seq x_562
    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_17261 -> h_COMMENT x_17261
    1010 | MOVE x_17262 -> h_MOVE x_17262
    1011 | POP x_17263 -> h_POP x_17263
    1012 | PUSH x_17264 -> h_PUSH x_17264
    1013 | ADDRESS (i, x_17266, x_17265) -> h_ADDRESS i __ x_17266 x_17265
    1014 | OPACCS (x_17272, x_17271, x_17270, x_17269, x_17268) ->
    1015   h_OPACCS x_17272 x_17271 x_17270 x_17269 x_17268
    1016 | OP1 (x_17275, x_17274, x_17273) -> h_OP1 x_17275 x_17274 x_17273
    1017 | OP2 (x_17279, x_17278, x_17277, x_17276) ->
    1018   h_OP2 x_17279 x_17278 x_17277 x_17276
     1005| COMMENT x_577 -> h_COMMENT x_577
     1006| MOVE x_578 -> h_MOVE x_578
     1007| POP x_579 -> h_POP x_579
     1008| PUSH x_580 -> h_PUSH x_580
     1009| ADDRESS (i, x_582, x_581) -> h_ADDRESS i __ x_582 x_581
     1010| OPACCS (x_588, x_587, x_586, x_585, x_584) ->
     1011  h_OPACCS x_588 x_587 x_586 x_585 x_584
     1012| OP1 (x_591, x_590, x_589) -> h_OP1 x_591 x_590 x_589
     1013| OP2 (x_595, x_594, x_593, x_592) -> h_OP2 x_595 x_594 x_593 x_592
    10191014| CLEAR_CARRY -> h_CLEAR_CARRY
    10201015| SET_CARRY -> h_SET_CARRY
    1021 | LOAD (x_17282, x_17281, x_17280) -> h_LOAD x_17282 x_17281 x_17280
    1022 | STORE (x_17285, x_17284, x_17283) -> h_STORE x_17285 x_17284 x_17283
    1023 | Extension_seq x_17286 -> h_extension_seq x_17286
     1016| LOAD (x_598, x_597, x_596) -> h_LOAD x_598 x_597 x_596
     1017| STORE (x_601, x_600, x_599) -> h_STORE x_601 x_600 x_599
     1018| Extension_seq x_602 -> h_extension_seq x_602
    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_17301 -> h_COMMENT x_17301
    1034 | MOVE x_17302 -> h_MOVE x_17302
    1035 | POP x_17303 -> h_POP x_17303
    1036 | PUSH x_17304 -> h_PUSH x_17304
    1037 | ADDRESS (i, x_17306, x_17305) -> h_ADDRESS i __ x_17306 x_17305
    1038 | OPACCS (x_17312, x_17311, x_17310, x_17309, x_17308) ->
    1039   h_OPACCS x_17312 x_17311 x_17310 x_17309 x_17308
    1040 | OP1 (x_17315, x_17314, x_17313) -> h_OP1 x_17315 x_17314 x_17313
    1041 | OP2 (x_17319, x_17318, x_17317, x_17316) ->
    1042   h_OP2 x_17319 x_17318 x_17317 x_17316
     1028| COMMENT x_617 -> h_COMMENT x_617
     1029| MOVE x_618 -> h_MOVE x_618
     1030| POP x_619 -> h_POP x_619
     1031| PUSH x_620 -> h_PUSH x_620
     1032| ADDRESS (i, x_622, x_621) -> h_ADDRESS i __ x_622 x_621
     1033| OPACCS (x_628, x_627, x_626, x_625, x_624) ->
     1034  h_OPACCS x_628 x_627 x_626 x_625 x_624
     1035| OP1 (x_631, x_630, x_629) -> h_OP1 x_631 x_630 x_629
     1036| OP2 (x_635, x_634, x_633, x_632) -> h_OP2 x_635 x_634 x_633 x_632
    10431037| CLEAR_CARRY -> h_CLEAR_CARRY
    10441038| SET_CARRY -> h_SET_CARRY
    1045 | LOAD (x_17322, x_17321, x_17320) -> h_LOAD x_17322 x_17321 x_17320
    1046 | STORE (x_17325, x_17324, x_17323) -> h_STORE x_17325 x_17324 x_17323
    1047 | Extension_seq x_17326 -> h_extension_seq x_17326
     1039| LOAD (x_638, x_637, x_636) -> h_LOAD x_638 x_637 x_636
     1040| STORE (x_641, x_640, x_639) -> h_STORE x_641 x_640 x_639
     1041| Extension_seq x_642 -> h_extension_seq x_642
    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_17593 -> h_COST_LABEL x_17593
    1239 | CALL (x_17596, x_17595, x_17594) -> h_CALL x_17596 x_17595 x_17594
    1240 | COND (x_17598, x_17597) -> h_COND x_17598 x_17597
    1241 | Step_seq x_17599 -> h_step_seq x_17599
     1232| COST_LABEL x_909 -> h_COST_LABEL x_909
     1233| CALL (x_912, x_911, x_910) -> h_CALL x_912 x_911 x_910
     1234| COND (x_914, x_913) -> h_COND x_914 x_913
     1235| Step_seq x_915 -> h_step_seq x_915
    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_17605 -> h_COST_LABEL x_17605
    1249 | CALL (x_17608, x_17607, x_17606) -> h_CALL x_17608 x_17607 x_17606
    1250 | COND (x_17610, x_17609) -> h_COND x_17610 x_17609
    1251 | Step_seq x_17611 -> h_step_seq x_17611
     1242| COST_LABEL x_921 -> h_COST_LABEL x_921
     1243| CALL (x_924, x_923, x_922) -> h_CALL x_924 x_923 x_922
     1244| COND (x_926, x_925) -> h_COND x_926 x_925
     1245| Step_seq x_927 -> h_step_seq x_927
    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_17617 -> h_COST_LABEL x_17617
    1259 | CALL (x_17620, x_17619, x_17618) -> h_CALL x_17620 x_17619 x_17618
    1260 | COND (x_17622, x_17621) -> h_COND x_17622 x_17621
    1261 | Step_seq x_17623 -> h_step_seq x_17623
     1252| COST_LABEL x_933 -> h_COST_LABEL x_933
     1253| CALL (x_936, x_935, x_934) -> h_CALL x_936 x_935 x_934
     1254| COND (x_938, x_937) -> h_COND x_938 x_937
     1255| Step_seq x_939 -> h_step_seq x_939
    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_17629 -> h_COST_LABEL x_17629
    1269 | CALL (x_17632, x_17631, x_17630) -> h_CALL x_17632 x_17631 x_17630
    1270 | COND (x_17634, x_17633) -> h_COND x_17634 x_17633
    1271 | Step_seq x_17635 -> h_step_seq x_17635
     1262| COST_LABEL x_945 -> h_COST_LABEL x_945
     1263| CALL (x_948, x_947, x_946) -> h_CALL x_948 x_947 x_946
     1264| COND (x_950, x_949) -> h_COND x_950 x_949
     1265| Step_seq x_951 -> h_step_seq x_951
    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_17641 -> h_COST_LABEL x_17641
    1279 | CALL (x_17644, x_17643, x_17642) -> h_CALL x_17644 x_17643 x_17642
    1280 | COND (x_17646, x_17645) -> h_COND x_17646 x_17645
    1281 | Step_seq x_17647 -> h_step_seq x_17647
     1272| COST_LABEL x_957 -> h_COST_LABEL x_957
     1273| CALL (x_960, x_959, x_958) -> h_CALL x_960 x_959 x_958
     1274| COND (x_962, x_961) -> h_COND x_962 x_961
     1275| Step_seq x_963 -> h_step_seq x_963
    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_17653 -> h_COST_LABEL x_17653
    1289 | CALL (x_17656, x_17655, x_17654) -> h_CALL x_17656 x_17655 x_17654
    1290 | COND (x_17658, x_17657) -> h_COND x_17658 x_17657
    1291 | Step_seq x_17659 -> h_step_seq x_17659
     1282| COST_LABEL x_969 -> h_COST_LABEL x_969
     1283| CALL (x_972, x_971, x_970) -> h_CALL x_972 x_971 x_970
     1284| COND (x_974, x_973) -> h_COND x_974 x_973
     1285| Step_seq x_975 -> h_step_seq x_975
    12921286
    12931287(** val joint_step_inv_rect_Type4 :
     
    14641458    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14651459    'a1) -> stmt_params -> 'a1 **)
    1466 let rec stmt_params_rect_Type4 h_mk_stmt_params x_17738 =
     1460let rec stmt_params_rect_Type4 h_mk_stmt_params x_1054 =
    14671461  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1468     has_fcond0 } = x_17738
     1462    has_fcond0 } = x_1054
    14691463  in
    14701464  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14731467    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14741468    'a1) -> stmt_params -> 'a1 **)
    1475 let rec stmt_params_rect_Type5 h_mk_stmt_params x_17740 =
     1469let rec stmt_params_rect_Type5 h_mk_stmt_params x_1056 =
    14761470  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1477     has_fcond0 } = x_17740
     1471    has_fcond0 } = x_1056
    14781472  in
    14791473  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14821476    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14831477    'a1) -> stmt_params -> 'a1 **)
    1484 let rec stmt_params_rect_Type3 h_mk_stmt_params x_17742 =
     1478let rec stmt_params_rect_Type3 h_mk_stmt_params x_1058 =
    14851479  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1486     has_fcond0 } = x_17742
     1480    has_fcond0 } = x_1058
    14871481  in
    14881482  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14911485    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14921486    'a1) -> stmt_params -> 'a1 **)
    1493 let rec stmt_params_rect_Type2 h_mk_stmt_params x_17744 =
     1487let rec stmt_params_rect_Type2 h_mk_stmt_params x_1060 =
    14941488  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1495     has_fcond0 } = x_17744
     1489    has_fcond0 } = x_1060
    14961490  in
    14971491  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15001494    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    15011495    'a1) -> stmt_params -> 'a1 **)
    1502 let rec stmt_params_rect_Type1 h_mk_stmt_params x_17746 =
     1496let rec stmt_params_rect_Type1 h_mk_stmt_params x_1062 =
    15031497  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1504     has_fcond0 } = x_17746
     1498    has_fcond0 } = x_1062
    15051499  in
    15061500  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15091503    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    15101504    'a1) -> stmt_params -> 'a1 **)
    1511 let rec stmt_params_rect_Type0 h_mk_stmt_params x_17748 =
     1505let rec stmt_params_rect_Type0 h_mk_stmt_params x_1064 =
    15121506  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1513     has_fcond0 } = x_17748
     1507    has_fcond0 } = x_1064
    15141508  in
    15151509  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15781572    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15791573let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
    1580 | GOTO x_17772 -> h_GOTO x_17772
     1574| GOTO x_1088 -> h_GOTO x_1088
    15811575| RETURN -> h_RETURN
    1582 | TAILCALL (x_17774, x_17773) -> h_TAILCALL __ x_17774 x_17773
     1576| TAILCALL (x_1090, x_1089) -> h_TAILCALL __ x_1090 x_1089
    15831577
    15841578(** val joint_fin_step_rect_Type5 :
     
    15861580    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15871581let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
    1588 | GOTO x_17780 -> h_GOTO x_17780
     1582| GOTO x_1096 -> h_GOTO x_1096
    15891583| RETURN -> h_RETURN
    1590 | TAILCALL (x_17782, x_17781) -> h_TAILCALL __ x_17782 x_17781
     1584| TAILCALL (x_1098, x_1097) -> h_TAILCALL __ x_1098 x_1097
    15911585
    15921586(** val joint_fin_step_rect_Type3 :
     
    15941588    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15951589let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
    1596 | GOTO x_17788 -> h_GOTO x_17788
     1590| GOTO x_1104 -> h_GOTO x_1104
    15971591| RETURN -> h_RETURN
    1598 | TAILCALL (x_17790, x_17789) -> h_TAILCALL __ x_17790 x_17789
     1592| TAILCALL (x_1106, x_1105) -> h_TAILCALL __ x_1106 x_1105
    15991593
    16001594(** val joint_fin_step_rect_Type2 :
     
    16021596    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16031597let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
    1604 | GOTO x_17796 -> h_GOTO x_17796
     1598| GOTO x_1112 -> h_GOTO x_1112
    16051599| RETURN -> h_RETURN
    1606 | TAILCALL (x_17798, x_17797) -> h_TAILCALL __ x_17798 x_17797
     1600| TAILCALL (x_1114, x_1113) -> h_TAILCALL __ x_1114 x_1113
    16071601
    16081602(** val joint_fin_step_rect_Type1 :
     
    16101604    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16111605let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
    1612 | GOTO x_17804 -> h_GOTO x_17804
     1606| GOTO x_1120 -> h_GOTO x_1120
    16131607| RETURN -> h_RETURN
    1614 | TAILCALL (x_17806, x_17805) -> h_TAILCALL __ x_17806 x_17805
     1608| TAILCALL (x_1122, x_1121) -> h_TAILCALL __ x_1122 x_1121
    16151609
    16161610(** val joint_fin_step_rect_Type0 :
     
    16181612    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16191613let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
    1620 | GOTO x_17812 -> h_GOTO x_17812
     1614| GOTO x_1128 -> h_GOTO x_1128
    16211615| RETURN -> h_RETURN
    1622 | TAILCALL (x_17814, x_17813) -> h_TAILCALL __ x_17814 x_17813
     1616| TAILCALL (x_1130, x_1129) -> h_TAILCALL __ x_1130 x_1129
    16231617
    16241618(** val joint_fin_step_inv_rect_Type4 :
     
    16921686    'a1) -> joint_statement -> 'a1 **)
    16931687let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
    1694 | Sequential (x_17880, x_17879) -> h_sequential x_17880 x_17879
    1695 | Final x_17881 -> h_final x_17881
    1696 | FCOND (x_17884, x_17883, x_17882) -> h_FCOND __ x_17884 x_17883 x_17882
     1688| Sequential (x_1196, x_1195) -> h_sequential x_1196 x_1195
     1689| Final x_1197 -> h_final x_1197
     1690| FCOND (x_1200, x_1199, x_1198) -> h_FCOND __ x_1200 x_1199 x_1198
    16971691
    16981692(** val joint_statement_rect_Type5 :
     
    17011695    'a1) -> joint_statement -> 'a1 **)
    17021696let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
    1703 | Sequential (x_17891, x_17890) -> h_sequential x_17891 x_17890
    1704 | Final x_17892 -> h_final x_17892
    1705 | FCOND (x_17895, x_17894, x_17893) -> h_FCOND __ x_17895 x_17894 x_17893
     1697| Sequential (x_1207, x_1206) -> h_sequential x_1207 x_1206
     1698| Final x_1208 -> h_final x_1208
     1699| FCOND (x_1211, x_1210, x_1209) -> h_FCOND __ x_1211 x_1210 x_1209
    17061700
    17071701(** val joint_statement_rect_Type3 :
     
    17101704    'a1) -> joint_statement -> 'a1 **)
    17111705let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
    1712 | Sequential (x_17902, x_17901) -> h_sequential x_17902 x_17901
    1713 | Final x_17903 -> h_final x_17903
    1714 | FCOND (x_17906, x_17905, x_17904) -> h_FCOND __ x_17906 x_17905 x_17904
     1706| Sequential (x_1218, x_1217) -> h_sequential x_1218 x_1217
     1707| Final x_1219 -> h_final x_1219
     1708| FCOND (x_1222, x_1221, x_1220) -> h_FCOND __ x_1222 x_1221 x_1220
    17151709
    17161710(** val joint_statement_rect_Type2 :
     
    17191713    'a1) -> joint_statement -> 'a1 **)
    17201714let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
    1721 | Sequential (x_17913, x_17912) -> h_sequential x_17913 x_17912
    1722 | Final x_17914 -> h_final x_17914
    1723 | FCOND (x_17917, x_17916, x_17915) -> h_FCOND __ x_17917 x_17916 x_17915
     1715| Sequential (x_1229, x_1228) -> h_sequential x_1229 x_1228
     1716| Final x_1230 -> h_final x_1230
     1717| FCOND (x_1233, x_1232, x_1231) -> h_FCOND __ x_1233 x_1232 x_1231
    17241718
    17251719(** val joint_statement_rect_Type1 :
     
    17281722    'a1) -> joint_statement -> 'a1 **)
    17291723let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
    1730 | Sequential (x_17924, x_17923) -> h_sequential x_17924 x_17923
    1731 | Final x_17925 -> h_final x_17925
    1732 | FCOND (x_17928, x_17927, x_17926) -> h_FCOND __ x_17928 x_17927 x_17926
     1724| Sequential (x_1240, x_1239) -> h_sequential x_1240 x_1239
     1725| Final x_1241 -> h_final x_1241
     1726| FCOND (x_1244, x_1243, x_1242) -> h_FCOND __ x_1244 x_1243 x_1242
    17331727
    17341728(** val joint_statement_rect_Type0 :
     
    17371731    'a1) -> joint_statement -> 'a1 **)
    17381732let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
    1739 | Sequential (x_17935, x_17934) -> h_sequential x_17935 x_17934
    1740 | Final x_17936 -> h_final x_17936
    1741 | FCOND (x_17939, x_17938, x_17937) -> h_FCOND __ x_17939 x_17938 x_17937
     1733| Sequential (x_1251, x_1250) -> h_sequential x_1251 x_1250
     1734| Final x_1252 -> h_final x_1252
     1735| FCOND (x_1255, x_1254, x_1253) -> h_FCOND __ x_1255 x_1254 x_1253
    17421736
    17431737(** val joint_statement_inv_rect_Type4 :
     
    18381832    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18391833    'a1 **)
    1840 let rec params_rect_Type4 h_mk_params x_18012 =
     1834let rec params_rect_Type4 h_mk_params x_1328 =
    18411835  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1842     point_of_label0; point_of_succ = point_of_succ0 } = x_18012
     1836    point_of_label0; point_of_succ = point_of_succ0 } = x_1328
    18431837  in
    18441838  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18491843    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18501844    'a1 **)
    1851 let rec params_rect_Type5 h_mk_params x_18014 =
     1845let rec params_rect_Type5 h_mk_params x_1330 =
    18521846  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1853     point_of_label0; point_of_succ = point_of_succ0 } = x_18014
     1847    point_of_label0; point_of_succ = point_of_succ0 } = x_1330
    18541848  in
    18551849  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18601854    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18611855    'a1 **)
    1862 let rec params_rect_Type3 h_mk_params x_18016 =
     1856let rec params_rect_Type3 h_mk_params x_1332 =
    18631857  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1864     point_of_label0; point_of_succ = point_of_succ0 } = x_18016
     1858    point_of_label0; point_of_succ = point_of_succ0 } = x_1332
    18651859  in
    18661860  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18711865    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18721866    'a1 **)
    1873 let rec params_rect_Type2 h_mk_params x_18018 =
     1867let rec params_rect_Type2 h_mk_params x_1334 =
    18741868  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1875     point_of_label0; point_of_succ = point_of_succ0 } = x_18018
     1869    point_of_label0; point_of_succ = point_of_succ0 } = x_1334
    18761870  in
    18771871  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18821876    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18831877    'a1 **)
    1884 let rec params_rect_Type1 h_mk_params x_18020 =
     1878let rec params_rect_Type1 h_mk_params x_1336 =
    18851879  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1886     point_of_label0; point_of_succ = point_of_succ0 } = x_18020
     1880    point_of_label0; point_of_succ = point_of_succ0 } = x_1336
    18871881  in
    18881882  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18931887    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18941888    'a1 **)
    1895 let rec params_rect_Type0 h_mk_params x_18022 =
     1889let rec params_rect_Type0 h_mk_params x_1338 =
    18961890  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1897     point_of_label0; point_of_succ = point_of_succ0 } = x_18022
     1891    point_of_label0; point_of_succ = point_of_succ0 } = x_1338
    18981892  in
    18991893  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    20302024
    20312025(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2032 let rec lin_params_rect_Type4 h_mk_lin_params x_18045 =
    2033   let l_u_pars = x_18045 in h_mk_lin_params l_u_pars
     2026let rec lin_params_rect_Type4 h_mk_lin_params x_1361 =
     2027  let l_u_pars = x_1361 in h_mk_lin_params l_u_pars
    20342028
    20352029(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2036 let rec lin_params_rect_Type5 h_mk_lin_params x_18047 =
    2037   let l_u_pars = x_18047 in h_mk_lin_params l_u_pars
     2030let rec lin_params_rect_Type5 h_mk_lin_params x_1363 =
     2031  let l_u_pars = x_1363 in h_mk_lin_params l_u_pars
    20382032
    20392033(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2040 let rec lin_params_rect_Type3 h_mk_lin_params x_18049 =
    2041   let l_u_pars = x_18049 in h_mk_lin_params l_u_pars
     2034let rec lin_params_rect_Type3 h_mk_lin_params x_1365 =
     2035  let l_u_pars = x_1365 in h_mk_lin_params l_u_pars
    20422036
    20432037(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2044 let rec lin_params_rect_Type2 h_mk_lin_params x_18051 =
    2045   let l_u_pars = x_18051 in h_mk_lin_params l_u_pars
     2038let rec lin_params_rect_Type2 h_mk_lin_params x_1367 =
     2039  let l_u_pars = x_1367 in h_mk_lin_params l_u_pars
    20462040
    20472041(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2048 let rec lin_params_rect_Type1 h_mk_lin_params x_18053 =
    2049   let l_u_pars = x_18053 in h_mk_lin_params l_u_pars
     2042let rec lin_params_rect_Type1 h_mk_lin_params x_1369 =
     2043  let l_u_pars = x_1369 in h_mk_lin_params l_u_pars
    20502044
    20512045(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2052 let rec lin_params_rect_Type0 h_mk_lin_params x_18055 =
    2053   let l_u_pars = x_18055 in h_mk_lin_params l_u_pars
     2046let rec lin_params_rect_Type0 h_mk_lin_params x_1371 =
     2047  let l_u_pars = x_1371 in h_mk_lin_params l_u_pars
    20542048
    20552049(** val l_u_pars : lin_params -> uns_params **)
     
    21252119(** val graph_params_rect_Type4 :
    21262120    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2127 let rec graph_params_rect_Type4 h_mk_graph_params x_18071 =
    2128   let g_u_pars = x_18071 in h_mk_graph_params g_u_pars
     2121let rec graph_params_rect_Type4 h_mk_graph_params x_1387 =
     2122  let g_u_pars = x_1387 in h_mk_graph_params g_u_pars
    21292123
    21302124(** val graph_params_rect_Type5 :
    21312125    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2132 let rec graph_params_rect_Type5 h_mk_graph_params x_18073 =
    2133   let g_u_pars = x_18073 in h_mk_graph_params g_u_pars
     2126let rec graph_params_rect_Type5 h_mk_graph_params x_1389 =
     2127  let g_u_pars = x_1389 in h_mk_graph_params g_u_pars
    21342128
    21352129(** val graph_params_rect_Type3 :
    21362130    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2137 let rec graph_params_rect_Type3 h_mk_graph_params x_18075 =
    2138   let g_u_pars = x_18075 in h_mk_graph_params g_u_pars
     2131let rec graph_params_rect_Type3 h_mk_graph_params x_1391 =
     2132  let g_u_pars = x_1391 in h_mk_graph_params g_u_pars
    21392133
    21402134(** val graph_params_rect_Type2 :
    21412135    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2142 let rec graph_params_rect_Type2 h_mk_graph_params x_18077 =
    2143   let g_u_pars = x_18077 in h_mk_graph_params g_u_pars
     2136let rec graph_params_rect_Type2 h_mk_graph_params x_1393 =
     2137  let g_u_pars = x_1393 in h_mk_graph_params g_u_pars
    21442138
    21452139(** val graph_params_rect_Type1 :
    21462140    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2147 let rec graph_params_rect_Type1 h_mk_graph_params x_18079 =
    2148   let g_u_pars = x_18079 in h_mk_graph_params g_u_pars
     2141let rec graph_params_rect_Type1 h_mk_graph_params x_1395 =
     2142  let g_u_pars = x_1395 in h_mk_graph_params g_u_pars
    21492143
    21502144(** val graph_params_rect_Type0 :
    21512145    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2152 let rec graph_params_rect_Type0 h_mk_graph_params x_18081 =
    2153   let g_u_pars = x_18081 in h_mk_graph_params g_u_pars
     2146let rec graph_params_rect_Type0 h_mk_graph_params x_1397 =
     2147  let g_u_pars = x_1397 in h_mk_graph_params g_u_pars
    21542148
    21552149(** val g_u_pars : graph_params -> uns_params **)
     
    22212215    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22222216    'a1) -> joint_internal_function -> 'a1 **)
    2223 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_18097 =
     2217let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_1413 =
    22242218  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22252219    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22272221    joint_if_stacksize0; joint_if_local_stacksize =
    22282222    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2229     joint_if_entry = joint_if_entry0 } = x_18097
     2223    joint_if_entry = joint_if_entry0 } = x_1413
    22302224  in
    22312225  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22372231    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22382232    'a1) -> joint_internal_function -> 'a1 **)
    2239 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_18099 =
     2233let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_1415 =
    22402234  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22412235    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22432237    joint_if_stacksize0; joint_if_local_stacksize =
    22442238    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2245     joint_if_entry = joint_if_entry0 } = x_18099
     2239    joint_if_entry = joint_if_entry0 } = x_1415
    22462240  in
    22472241  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22532247    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22542248    'a1) -> joint_internal_function -> 'a1 **)
    2255 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_18101 =
     2249let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_1417 =
    22562250  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22572251    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22592253    joint_if_stacksize0; joint_if_local_stacksize =
    22602254    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2261     joint_if_entry = joint_if_entry0 } = x_18101
     2255    joint_if_entry = joint_if_entry0 } = x_1417
    22622256  in
    22632257  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22692263    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22702264    'a1) -> joint_internal_function -> 'a1 **)
    2271 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_18103 =
     2265let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_1419 =
    22722266  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22732267    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22752269    joint_if_stacksize0; joint_if_local_stacksize =
    22762270    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2277     joint_if_entry = joint_if_entry0 } = x_18103
     2271    joint_if_entry = joint_if_entry0 } = x_1419
    22782272  in
    22792273  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22852279    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22862280    'a1) -> joint_internal_function -> 'a1 **)
    2287 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_18105 =
     2281let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_1421 =
    22882282  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22892283    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22912285    joint_if_stacksize0; joint_if_local_stacksize =
    22922286    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2293     joint_if_entry = joint_if_entry0 } = x_18105
     2287    joint_if_entry = joint_if_entry0 } = x_1421
    22942288  in
    22952289  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    23012295    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    23022296    'a1) -> joint_internal_function -> 'a1 **)
    2303 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_18107 =
     2297let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_1423 =
    23042298  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    23052299    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    23072301    joint_if_stacksize0; joint_if_local_stacksize =
    23082302    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2309     joint_if_entry = joint_if_entry0 } = x_18107
     2303    joint_if_entry = joint_if_entry0 } = x_1423
    23102304  in
    23112305  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    25362530    params -> ((joint_function, AST.init_data List.list) AST.program ->
    25372531    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
    2538 let rec joint_program_rect_Type4 p h_mk_joint_program x_18149 =
     2532let rec joint_program_rect_Type4 p h_mk_joint_program x_1465 =
    25392533  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
    2540     x_18149
     2534    x_1465
    25412535  in
    25422536  h_mk_joint_program joint_prog0 init_cost_label0
     
    25452539    params -> ((joint_function, AST.init_data List.list) AST.program ->
    25462540    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
    2547 let rec joint_program_rect_Type5 p h_mk_joint_program x_18151 =
     2541let rec joint_program_rect_Type5 p h_mk_joint_program x_1467 =
    25482542  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
    2549     x_18151
     2543    x_1467
    25502544  in
    25512545  h_mk_joint_program joint_prog0 init_cost_label0
     
    25542548    params -> ((joint_function, AST.init_data List.list) AST.program ->
    25552549    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
    2556 let rec joint_program_rect_Type3 p h_mk_joint_program x_18153 =
     2550let rec joint_program_rect_Type3 p h_mk_joint_program x_1469 =
    25572551  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
    2558     x_18153
     2552    x_1469
    25592553  in
    25602554  h_mk_joint_program joint_prog0 init_cost_label0
     
    25632557    params -> ((joint_function, AST.init_data List.list) AST.program ->
    25642558    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
    2565 let rec joint_program_rect_Type2 p h_mk_joint_program x_18155 =
     2559let rec joint_program_rect_Type2 p h_mk_joint_program x_1471 =
    25662560  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
    2567     x_18155
     2561    x_1471
    25682562  in
    25692563  h_mk_joint_program joint_prog0 init_cost_label0
     
    25722566    params -> ((joint_function, AST.init_data List.list) AST.program ->
    25732567    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
    2574 let rec joint_program_rect_Type1 p h_mk_joint_program x_18157 =
     2568let rec joint_program_rect_Type1 p h_mk_joint_program x_1473 =
    25752569  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
    2576     x_18157
     2570    x_1473
    25772571  in
    25782572  h_mk_joint_program joint_prog0 init_cost_label0
     
    25812575    params -> ((joint_function, AST.init_data List.list) AST.program ->
    25822576    CostLabel.costlabel -> 'a1) -> joint_program -> 'a1 **)
    2583 let rec joint_program_rect_Type0 p h_mk_joint_program x_18159 =
     2577let rec joint_program_rect_Type0 p h_mk_joint_program x_1475 =
    25842578  let { joint_prog = joint_prog0; init_cost_label = init_cost_label0 } =
    2585     x_18159
     2579    x_1475
    25862580  in
    25872581  h_mk_joint_program joint_prog0 init_cost_label0
Note: See TracChangeset for help on using the changeset viewer.