Changeset 2873 for extracted/joint.ml


Ignore:
Timestamp:
Mar 14, 2013, 10:37:39 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint.ml

    r2867 r2873  
    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_19830 -> h_Reg x_19830
     113| Imm x_19831 -> h_Imm x_19831
    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_19835 -> h_Reg x_19835
     119| Imm x_19836 -> h_Imm x_19836
    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_19840 -> h_Reg x_19840
     125| Imm x_19841 -> h_Imm x_19841
    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_19845 -> h_Reg x_19845
     131| Imm x_19846 -> h_Imm x_19846
    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_19850 -> h_Reg x_19850
     137| Imm x_19851 -> h_Imm x_19851
    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_19855 -> h_Reg x_19855
     143| Imm x_19856 -> h_Imm x_19856
    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_19891 =
    327327  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    328     x_19722
     328    x_19891
    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_19893 =
    338338  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    339     x_19724
     339    x_19893
    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_19895 =
    349349  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    350     x_19726
     350    x_19895
    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_19897 =
    360360  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    361     x_19728
     361    x_19897
    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_19899 =
    371371  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    372     x_19730
     372    x_19899
    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_19901 =
    382382  let { ext_seq_labels = ext_seq_labels0; has_tailcalls = has_tailcalls0 } =
    383     x_19732
     383    x_19901
    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_19918 =
    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_19918
    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_19920 =
    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_19920
    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_19922 =
    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_19922
    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_19924 =
    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_19924
    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_19926 =
    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_19926
    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_19928 =
    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_19928
    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_19958 =
     808  let { u_pars = u_pars0; functs = functs0 } = x_19958 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_19960 =
     815  let { u_pars = u_pars0; functs = functs0 } = x_19960 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_19962 =
     822  let { u_pars = u_pars0; functs = functs0 } = x_19962 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_19964 =
     829  let { u_pars = u_pars0; functs = functs0 } = x_19964 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_19966 =
     836  let { u_pars = u_pars0; functs = functs0 } = x_19966 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_19968 =
     843  let { u_pars = u_pars0; functs = functs0 } = x_19968 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_20023 -> h_COMMENT x_20023
     914| MOVE x_20024 -> h_MOVE x_20024
     915| POP x_20025 -> h_POP x_20025
     916| PUSH x_20026 -> h_PUSH x_20026
     917| ADDRESS (i, x_20028, x_20027) -> h_ADDRESS i __ x_20028 x_20027
     918| OPACCS (x_20034, x_20033, x_20032, x_20031, x_20030) ->
     919  h_OPACCS x_20034 x_20033 x_20032 x_20031 x_20030
     920| OP1 (x_20037, x_20036, x_20035) -> h_OP1 x_20037 x_20036 x_20035
     921| OP2 (x_20041, x_20040, x_20039, x_20038) ->
     922  h_OP2 x_20041 x_20040 x_20039 x_20038
    923923| CLEAR_CARRY -> h_CLEAR_CARRY
    924924| 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
     925| LOAD (x_20044, x_20043, x_20042) -> h_LOAD x_20044 x_20043 x_20042
     926| STORE (x_20047, x_20046, x_20045) -> h_STORE x_20047 x_20046 x_20045
     927| Extension_seq x_20048 -> h_extension_seq x_20048
    928928
    929929(** val joint_seq_rect_Type5 :
     
    935935    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    936936let rec joint_seq_rect_Type5 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    937 | COMMENT x_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
     937| COMMENT x_20063 -> h_COMMENT x_20063
     938| MOVE x_20064 -> h_MOVE x_20064
     939| POP x_20065 -> h_POP x_20065
     940| PUSH x_20066 -> h_PUSH x_20066
     941| ADDRESS (i, x_20068, x_20067) -> h_ADDRESS i __ x_20068 x_20067
     942| OPACCS (x_20074, x_20073, x_20072, x_20071, x_20070) ->
     943  h_OPACCS x_20074 x_20073 x_20072 x_20071 x_20070
     944| OP1 (x_20077, x_20076, x_20075) -> h_OP1 x_20077 x_20076 x_20075
     945| OP2 (x_20081, x_20080, x_20079, x_20078) ->
     946  h_OP2 x_20081 x_20080 x_20079 x_20078
    947947| CLEAR_CARRY -> h_CLEAR_CARRY
    948948| 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
     949| LOAD (x_20084, x_20083, x_20082) -> h_LOAD x_20084 x_20083 x_20082
     950| STORE (x_20087, x_20086, x_20085) -> h_STORE x_20087 x_20086 x_20085
     951| Extension_seq x_20088 -> h_extension_seq x_20088
    952952
    953953(** val joint_seq_rect_Type3 :
     
    959959    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    960960let rec joint_seq_rect_Type3 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    961 | COMMENT x_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
     961| COMMENT x_20103 -> h_COMMENT x_20103
     962| MOVE x_20104 -> h_MOVE x_20104
     963| POP x_20105 -> h_POP x_20105
     964| PUSH x_20106 -> h_PUSH x_20106
     965| ADDRESS (i, x_20108, x_20107) -> h_ADDRESS i __ x_20108 x_20107
     966| OPACCS (x_20114, x_20113, x_20112, x_20111, x_20110) ->
     967  h_OPACCS x_20114 x_20113 x_20112 x_20111 x_20110
     968| OP1 (x_20117, x_20116, x_20115) -> h_OP1 x_20117 x_20116 x_20115
     969| OP2 (x_20121, x_20120, x_20119, x_20118) ->
     970  h_OP2 x_20121 x_20120 x_20119 x_20118
    971971| CLEAR_CARRY -> h_CLEAR_CARRY
    972972| 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
     973| LOAD (x_20124, x_20123, x_20122) -> h_LOAD x_20124 x_20123 x_20122
     974| STORE (x_20127, x_20126, x_20125) -> h_STORE x_20127 x_20126 x_20125
     975| Extension_seq x_20128 -> h_extension_seq x_20128
    976976
    977977(** val joint_seq_rect_Type2 :
     
    983983    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    984984let rec joint_seq_rect_Type2 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    985 | COMMENT x_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
     985| COMMENT x_20143 -> h_COMMENT x_20143
     986| MOVE x_20144 -> h_MOVE x_20144
     987| POP x_20145 -> h_POP x_20145
     988| PUSH x_20146 -> h_PUSH x_20146
     989| ADDRESS (i, x_20148, x_20147) -> h_ADDRESS i __ x_20148 x_20147
     990| OPACCS (x_20154, x_20153, x_20152, x_20151, x_20150) ->
     991  h_OPACCS x_20154 x_20153 x_20152 x_20151 x_20150
     992| OP1 (x_20157, x_20156, x_20155) -> h_OP1 x_20157 x_20156 x_20155
     993| OP2 (x_20161, x_20160, x_20159, x_20158) ->
     994  h_OP2 x_20161 x_20160 x_20159 x_20158
    995995| CLEAR_CARRY -> h_CLEAR_CARRY
    996996| 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
     997| LOAD (x_20164, x_20163, x_20162) -> h_LOAD x_20164 x_20163 x_20162
     998| STORE (x_20167, x_20166, x_20165) -> h_STORE x_20167 x_20166 x_20165
     999| Extension_seq x_20168 -> h_extension_seq x_20168
    10001000
    10011001(** val joint_seq_rect_Type1 :
     
    10071007    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    10081008let rec joint_seq_rect_Type1 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    1009 | COMMENT x_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
     1009| COMMENT x_20183 -> h_COMMENT x_20183
     1010| MOVE x_20184 -> h_MOVE x_20184
     1011| POP x_20185 -> h_POP x_20185
     1012| PUSH x_20186 -> h_PUSH x_20186
     1013| ADDRESS (i, x_20188, x_20187) -> h_ADDRESS i __ x_20188 x_20187
     1014| OPACCS (x_20194, x_20193, x_20192, x_20191, x_20190) ->
     1015  h_OPACCS x_20194 x_20193 x_20192 x_20191 x_20190
     1016| OP1 (x_20197, x_20196, x_20195) -> h_OP1 x_20197 x_20196 x_20195
     1017| OP2 (x_20201, x_20200, x_20199, x_20198) ->
     1018  h_OP2 x_20201 x_20200 x_20199 x_20198
    10191019| CLEAR_CARRY -> h_CLEAR_CARRY
    10201020| 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
     1021| LOAD (x_20204, x_20203, x_20202) -> h_LOAD x_20204 x_20203 x_20202
     1022| STORE (x_20207, x_20206, x_20205) -> h_STORE x_20207 x_20206 x_20205
     1023| Extension_seq x_20208 -> h_extension_seq x_20208
    10241024
    10251025(** val joint_seq_rect_Type0 :
     
    10311031    'a1) -> (__ -> 'a1) -> joint_seq -> 'a1 **)
    10321032let rec joint_seq_rect_Type0 p globals h_COMMENT h_MOVE h_POP h_PUSH h_ADDRESS h_OPACCS h_OP1 h_OP2 h_CLEAR_CARRY h_SET_CARRY h_LOAD h_STORE h_extension_seq = function
    1033 | COMMENT x_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
     1033| COMMENT x_20223 -> h_COMMENT x_20223
     1034| MOVE x_20224 -> h_MOVE x_20224
     1035| POP x_20225 -> h_POP x_20225
     1036| PUSH x_20226 -> h_PUSH x_20226
     1037| ADDRESS (i, x_20228, x_20227) -> h_ADDRESS i __ x_20228 x_20227
     1038| OPACCS (x_20234, x_20233, x_20232, x_20231, x_20230) ->
     1039  h_OPACCS x_20234 x_20233 x_20232 x_20231 x_20230
     1040| OP1 (x_20237, x_20236, x_20235) -> h_OP1 x_20237 x_20236 x_20235
     1041| OP2 (x_20241, x_20240, x_20239, x_20238) ->
     1042  h_OP2 x_20241 x_20240 x_20239 x_20238
    10431043| CLEAR_CARRY -> h_CLEAR_CARRY
    10441044| 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
     1045| LOAD (x_20244, x_20243, x_20242) -> h_LOAD x_20244 x_20243 x_20242
     1046| STORE (x_20247, x_20246, x_20245) -> h_STORE x_20247 x_20246 x_20245
     1047| Extension_seq x_20248 -> h_extension_seq x_20248
    10481048
    10491049(** val joint_seq_inv_rect_Type4 :
     
    12361236    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12371237let rec joint_step_rect_Type4 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1238 | COST_LABEL x_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
     1238| COST_LABEL x_20515 -> h_COST_LABEL x_20515
     1239| CALL (x_20518, x_20517, x_20516) -> h_CALL x_20518 x_20517 x_20516
     1240| COND (x_20520, x_20519) -> h_COND x_20520 x_20519
     1241| Step_seq x_20521 -> h_step_seq x_20521
    12421242
    12431243(** val joint_step_rect_Type5 :
     
    12461246    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12471247let rec joint_step_rect_Type5 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1248 | COST_LABEL x_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
     1248| COST_LABEL x_20527 -> h_COST_LABEL x_20527
     1249| CALL (x_20530, x_20529, x_20528) -> h_CALL x_20530 x_20529 x_20528
     1250| COND (x_20532, x_20531) -> h_COND x_20532 x_20531
     1251| Step_seq x_20533 -> h_step_seq x_20533
    12521252
    12531253(** val joint_step_rect_Type3 :
     
    12561256    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12571257let rec joint_step_rect_Type3 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1258 | COST_LABEL x_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
     1258| COST_LABEL x_20539 -> h_COST_LABEL x_20539
     1259| CALL (x_20542, x_20541, x_20540) -> h_CALL x_20542 x_20541 x_20540
     1260| COND (x_20544, x_20543) -> h_COND x_20544 x_20543
     1261| Step_seq x_20545 -> h_step_seq x_20545
    12621262
    12631263(** val joint_step_rect_Type2 :
     
    12661266    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12671267let rec joint_step_rect_Type2 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1268 | COST_LABEL x_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
     1268| COST_LABEL x_20551 -> h_COST_LABEL x_20551
     1269| CALL (x_20554, x_20553, x_20552) -> h_CALL x_20554 x_20553 x_20552
     1270| COND (x_20556, x_20555) -> h_COND x_20556 x_20555
     1271| Step_seq x_20557 -> h_step_seq x_20557
    12721272
    12731273(** val joint_step_rect_Type1 :
     
    12761276    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12771277let rec joint_step_rect_Type1 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1278 | COST_LABEL x_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
     1278| COST_LABEL x_20563 -> h_COST_LABEL x_20563
     1279| CALL (x_20566, x_20565, x_20564) -> h_CALL x_20566 x_20565 x_20564
     1280| COND (x_20568, x_20567) -> h_COND x_20568 x_20567
     1281| Step_seq x_20569 -> h_step_seq x_20569
    12821282
    12831283(** val joint_step_rect_Type0 :
     
    12861286    -> (__ -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1 **)
    12871287let rec joint_step_rect_Type0 p globals h_COST_LABEL h_CALL h_COND h_step_seq = function
    1288 | COST_LABEL x_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
     1288| COST_LABEL x_20575 -> h_COST_LABEL x_20575
     1289| CALL (x_20578, x_20577, x_20576) -> h_CALL x_20578 x_20577 x_20576
     1290| COND (x_20580, x_20579) -> h_COND x_20580 x_20579
     1291| Step_seq x_20581 -> h_step_seq x_20581
    12921292
    12931293(** val joint_step_inv_rect_Type4 :
     
    14641464    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14651465    'a1) -> stmt_params -> 'a1 **)
    1466 let rec stmt_params_rect_Type4 h_mk_stmt_params x_20491 =
     1466let rec stmt_params_rect_Type4 h_mk_stmt_params x_20660 =
    14671467  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1468     has_fcond0 } = x_20491
     1468    has_fcond0 } = x_20660
    14691469  in
    14701470  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14731473    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14741474    'a1) -> stmt_params -> 'a1 **)
    1475 let rec stmt_params_rect_Type5 h_mk_stmt_params x_20493 =
     1475let rec stmt_params_rect_Type5 h_mk_stmt_params x_20662 =
    14761476  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1477     has_fcond0 } = x_20493
     1477    has_fcond0 } = x_20662
    14781478  in
    14791479  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14821482    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14831483    'a1) -> stmt_params -> 'a1 **)
    1484 let rec stmt_params_rect_Type3 h_mk_stmt_params x_20495 =
     1484let rec stmt_params_rect_Type3 h_mk_stmt_params x_20664 =
    14851485  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1486     has_fcond0 } = x_20495
     1486    has_fcond0 } = x_20664
    14871487  in
    14881488  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    14911491    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    14921492    'a1) -> stmt_params -> 'a1 **)
    1493 let rec stmt_params_rect_Type2 h_mk_stmt_params x_20497 =
     1493let rec stmt_params_rect_Type2 h_mk_stmt_params x_20666 =
    14941494  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1495     has_fcond0 } = x_20497
     1495    has_fcond0 } = x_20666
    14961496  in
    14971497  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15001500    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    15011501    'a1) -> stmt_params -> 'a1 **)
    1502 let rec stmt_params_rect_Type1 h_mk_stmt_params x_20499 =
     1502let rec stmt_params_rect_Type1 h_mk_stmt_params x_20668 =
    15031503  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1504     has_fcond0 } = x_20499
     1504    has_fcond0 } = x_20668
    15051505  in
    15061506  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15091509    (uns_params -> __ -> (__ -> Graphs.label Types.option) -> Bool.bool ->
    15101510    'a1) -> stmt_params -> 'a1 **)
    1511 let rec stmt_params_rect_Type0 h_mk_stmt_params x_20501 =
     1511let rec stmt_params_rect_Type0 h_mk_stmt_params x_20670 =
    15121512  let { uns_pars = uns_pars0; succ_label = succ_label0; has_fcond =
    1513     has_fcond0 } = x_20501
     1513    has_fcond0 } = x_20670
    15141514  in
    15151515  h_mk_stmt_params uns_pars0 __ succ_label0 has_fcond0
     
    15781578    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15791579let rec joint_fin_step_rect_Type4 p h_GOTO h_RETURN h_TAILCALL = function
    1580 | GOTO x_20525 -> h_GOTO x_20525
     1580| GOTO x_20694 -> h_GOTO x_20694
    15811581| RETURN -> h_RETURN
    1582 | TAILCALL (x_20527, x_20526) -> h_TAILCALL __ x_20527 x_20526
     1582| TAILCALL (x_20696, x_20695) -> h_TAILCALL __ x_20696 x_20695
    15831583
    15841584(** val joint_fin_step_rect_Type5 :
     
    15861586    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15871587let rec joint_fin_step_rect_Type5 p h_GOTO h_RETURN h_TAILCALL = function
    1588 | GOTO x_20533 -> h_GOTO x_20533
     1588| GOTO x_20702 -> h_GOTO x_20702
    15891589| RETURN -> h_RETURN
    1590 | TAILCALL (x_20535, x_20534) -> h_TAILCALL __ x_20535 x_20534
     1590| TAILCALL (x_20704, x_20703) -> h_TAILCALL __ x_20704 x_20703
    15911591
    15921592(** val joint_fin_step_rect_Type3 :
     
    15941594    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    15951595let rec joint_fin_step_rect_Type3 p h_GOTO h_RETURN h_TAILCALL = function
    1596 | GOTO x_20541 -> h_GOTO x_20541
     1596| GOTO x_20710 -> h_GOTO x_20710
    15971597| RETURN -> h_RETURN
    1598 | TAILCALL (x_20543, x_20542) -> h_TAILCALL __ x_20543 x_20542
     1598| TAILCALL (x_20712, x_20711) -> h_TAILCALL __ x_20712 x_20711
    15991599
    16001600(** val joint_fin_step_rect_Type2 :
     
    16021602    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16031603let rec joint_fin_step_rect_Type2 p h_GOTO h_RETURN h_TAILCALL = function
    1604 | GOTO x_20549 -> h_GOTO x_20549
     1604| GOTO x_20718 -> h_GOTO x_20718
    16051605| RETURN -> h_RETURN
    1606 | TAILCALL (x_20551, x_20550) -> h_TAILCALL __ x_20551 x_20550
     1606| TAILCALL (x_20720, x_20719) -> h_TAILCALL __ x_20720 x_20719
    16071607
    16081608(** val joint_fin_step_rect_Type1 :
     
    16101610    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16111611let rec joint_fin_step_rect_Type1 p h_GOTO h_RETURN h_TAILCALL = function
    1612 | GOTO x_20557 -> h_GOTO x_20557
     1612| GOTO x_20726 -> h_GOTO x_20726
    16131613| RETURN -> h_RETURN
    1614 | TAILCALL (x_20559, x_20558) -> h_TAILCALL __ x_20559 x_20558
     1614| TAILCALL (x_20728, x_20727) -> h_TAILCALL __ x_20728 x_20727
    16151615
    16161616(** val joint_fin_step_rect_Type0 :
     
    16181618    (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1 **)
    16191619let rec joint_fin_step_rect_Type0 p h_GOTO h_RETURN h_TAILCALL = function
    1620 | GOTO x_20565 -> h_GOTO x_20565
     1620| GOTO x_20734 -> h_GOTO x_20734
    16211621| RETURN -> h_RETURN
    1622 | TAILCALL (x_20567, x_20566) -> h_TAILCALL __ x_20567 x_20566
     1622| TAILCALL (x_20736, x_20735) -> h_TAILCALL __ x_20736 x_20735
    16231623
    16241624(** val joint_fin_step_inv_rect_Type4 :
     
    16921692    'a1) -> joint_statement -> 'a1 **)
    16931693let rec joint_statement_rect_Type4 p globals h_sequential h_final h_FCOND = function
    1694 | Sequential (x_20633, x_20632) -> h_sequential x_20633 x_20632
    1695 | Final x_20634 -> h_final x_20634
    1696 | FCOND (x_20637, x_20636, x_20635) -> h_FCOND __ x_20637 x_20636 x_20635
     1694| Sequential (x_20802, x_20801) -> h_sequential x_20802 x_20801
     1695| Final x_20803 -> h_final x_20803
     1696| FCOND (x_20806, x_20805, x_20804) -> h_FCOND __ x_20806 x_20805 x_20804
    16971697
    16981698(** val joint_statement_rect_Type5 :
     
    17011701    'a1) -> joint_statement -> 'a1 **)
    17021702let rec joint_statement_rect_Type5 p globals h_sequential h_final h_FCOND = function
    1703 | Sequential (x_20644, x_20643) -> h_sequential x_20644 x_20643
    1704 | Final x_20645 -> h_final x_20645
    1705 | FCOND (x_20648, x_20647, x_20646) -> h_FCOND __ x_20648 x_20647 x_20646
     1703| Sequential (x_20813, x_20812) -> h_sequential x_20813 x_20812
     1704| Final x_20814 -> h_final x_20814
     1705| FCOND (x_20817, x_20816, x_20815) -> h_FCOND __ x_20817 x_20816 x_20815
    17061706
    17071707(** val joint_statement_rect_Type3 :
     
    17101710    'a1) -> joint_statement -> 'a1 **)
    17111711let rec joint_statement_rect_Type3 p globals h_sequential h_final h_FCOND = function
    1712 | Sequential (x_20655, x_20654) -> h_sequential x_20655 x_20654
    1713 | Final x_20656 -> h_final x_20656
    1714 | FCOND (x_20659, x_20658, x_20657) -> h_FCOND __ x_20659 x_20658 x_20657
     1712| Sequential (x_20824, x_20823) -> h_sequential x_20824 x_20823
     1713| Final x_20825 -> h_final x_20825
     1714| FCOND (x_20828, x_20827, x_20826) -> h_FCOND __ x_20828 x_20827 x_20826
    17151715
    17161716(** val joint_statement_rect_Type2 :
     
    17191719    'a1) -> joint_statement -> 'a1 **)
    17201720let rec joint_statement_rect_Type2 p globals h_sequential h_final h_FCOND = function
    1721 | Sequential (x_20666, x_20665) -> h_sequential x_20666 x_20665
    1722 | Final x_20667 -> h_final x_20667
    1723 | FCOND (x_20670, x_20669, x_20668) -> h_FCOND __ x_20670 x_20669 x_20668
     1721| Sequential (x_20835, x_20834) -> h_sequential x_20835 x_20834
     1722| Final x_20836 -> h_final x_20836
     1723| FCOND (x_20839, x_20838, x_20837) -> h_FCOND __ x_20839 x_20838 x_20837
    17241724
    17251725(** val joint_statement_rect_Type1 :
     
    17281728    'a1) -> joint_statement -> 'a1 **)
    17291729let rec joint_statement_rect_Type1 p globals h_sequential h_final h_FCOND = function
    1730 | Sequential (x_20677, x_20676) -> h_sequential x_20677 x_20676
    1731 | Final x_20678 -> h_final x_20678
    1732 | FCOND (x_20681, x_20680, x_20679) -> h_FCOND __ x_20681 x_20680 x_20679
     1730| Sequential (x_20846, x_20845) -> h_sequential x_20846 x_20845
     1731| Final x_20847 -> h_final x_20847
     1732| FCOND (x_20850, x_20849, x_20848) -> h_FCOND __ x_20850 x_20849 x_20848
    17331733
    17341734(** val joint_statement_rect_Type0 :
     
    17371737    'a1) -> joint_statement -> 'a1 **)
    17381738let rec joint_statement_rect_Type0 p globals h_sequential h_final h_FCOND = function
    1739 | Sequential (x_20688, x_20687) -> h_sequential x_20688 x_20687
    1740 | Final x_20689 -> h_final x_20689
    1741 | FCOND (x_20692, x_20691, x_20690) -> h_FCOND __ x_20692 x_20691 x_20690
     1739| Sequential (x_20857, x_20856) -> h_sequential x_20857 x_20856
     1740| Final x_20858 -> h_final x_20858
     1741| FCOND (x_20861, x_20860, x_20859) -> h_FCOND __ x_20861 x_20860 x_20859
    17421742
    17431743(** val joint_statement_inv_rect_Type4 :
     
    18381838    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18391839    'a1 **)
    1840 let rec params_rect_Type4 h_mk_params x_20765 =
     1840let rec params_rect_Type4 h_mk_params x_20934 =
    18411841  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1842     point_of_label0; point_of_succ = point_of_succ0 } = x_20765
     1842    point_of_label0; point_of_succ = point_of_succ0 } = x_20934
    18431843  in
    18441844  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18491849    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18501850    'a1 **)
    1851 let rec params_rect_Type5 h_mk_params x_20767 =
     1851let rec params_rect_Type5 h_mk_params x_20936 =
    18521852  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1853     point_of_label0; point_of_succ = point_of_succ0 } = x_20767
     1853    point_of_label0; point_of_succ = point_of_succ0 } = x_20936
    18541854  in
    18551855  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18601860    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18611861    'a1 **)
    1862 let rec params_rect_Type3 h_mk_params x_20769 =
     1862let rec params_rect_Type3 h_mk_params x_20938 =
    18631863  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1864     point_of_label0; point_of_succ = point_of_succ0 } = x_20769
     1864    point_of_label0; point_of_succ = point_of_succ0 } = x_20938
    18651865  in
    18661866  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18711871    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18721872    'a1 **)
    1873 let rec params_rect_Type2 h_mk_params x_20771 =
     1873let rec params_rect_Type2 h_mk_params x_20940 =
    18741874  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1875     point_of_label0; point_of_succ = point_of_succ0 } = x_20771
     1875    point_of_label0; point_of_succ = point_of_succ0 } = x_20940
    18761876  in
    18771877  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18821882    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18831883    'a1 **)
    1884 let rec params_rect_Type1 h_mk_params x_20773 =
     1884let rec params_rect_Type1 h_mk_params x_20942 =
    18851885  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1886     point_of_label0; point_of_succ = point_of_succ0 } = x_20773
     1886    point_of_label0; point_of_succ = point_of_succ0 } = x_20942
    18871887  in
    18881888  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    18931893    Graphs.label -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params ->
    18941894    'a1 **)
    1895 let rec params_rect_Type0 h_mk_params x_20775 =
     1895let rec params_rect_Type0 h_mk_params x_20944 =
    18961896  let { stmt_pars = stmt_pars0; stmt_at = stmt_at0; point_of_label =
    1897     point_of_label0; point_of_succ = point_of_succ0 } = x_20775
     1897    point_of_label0; point_of_succ = point_of_succ0 } = x_20944
    18981898  in
    18991899  h_mk_params stmt_pars0 __ __ stmt_at0 point_of_label0 point_of_succ0
     
    20302030
    20312031(** val lin_params_rect_Type4 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2032 let rec lin_params_rect_Type4 h_mk_lin_params x_20798 =
    2033   let l_u_pars = x_20798 in h_mk_lin_params l_u_pars
     2032let rec lin_params_rect_Type4 h_mk_lin_params x_20967 =
     2033  let l_u_pars = x_20967 in h_mk_lin_params l_u_pars
    20342034
    20352035(** val lin_params_rect_Type5 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2036 let rec lin_params_rect_Type5 h_mk_lin_params x_20800 =
    2037   let l_u_pars = x_20800 in h_mk_lin_params l_u_pars
     2036let rec lin_params_rect_Type5 h_mk_lin_params x_20969 =
     2037  let l_u_pars = x_20969 in h_mk_lin_params l_u_pars
    20382038
    20392039(** val lin_params_rect_Type3 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2040 let rec lin_params_rect_Type3 h_mk_lin_params x_20802 =
    2041   let l_u_pars = x_20802 in h_mk_lin_params l_u_pars
     2040let rec lin_params_rect_Type3 h_mk_lin_params x_20971 =
     2041  let l_u_pars = x_20971 in h_mk_lin_params l_u_pars
    20422042
    20432043(** val lin_params_rect_Type2 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2044 let rec lin_params_rect_Type2 h_mk_lin_params x_20804 =
    2045   let l_u_pars = x_20804 in h_mk_lin_params l_u_pars
     2044let rec lin_params_rect_Type2 h_mk_lin_params x_20973 =
     2045  let l_u_pars = x_20973 in h_mk_lin_params l_u_pars
    20462046
    20472047(** val lin_params_rect_Type1 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2048 let rec lin_params_rect_Type1 h_mk_lin_params x_20806 =
    2049   let l_u_pars = x_20806 in h_mk_lin_params l_u_pars
     2048let rec lin_params_rect_Type1 h_mk_lin_params x_20975 =
     2049  let l_u_pars = x_20975 in h_mk_lin_params l_u_pars
    20502050
    20512051(** val lin_params_rect_Type0 : (uns_params -> 'a1) -> lin_params -> 'a1 **)
    2052 let rec lin_params_rect_Type0 h_mk_lin_params x_20808 =
    2053   let l_u_pars = x_20808 in h_mk_lin_params l_u_pars
     2052let rec lin_params_rect_Type0 h_mk_lin_params x_20977 =
     2053  let l_u_pars = x_20977 in h_mk_lin_params l_u_pars
    20542054
    20552055(** val l_u_pars : lin_params -> uns_params **)
     
    21252125(** val graph_params_rect_Type4 :
    21262126    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2127 let rec graph_params_rect_Type4 h_mk_graph_params x_20824 =
    2128   let g_u_pars = x_20824 in h_mk_graph_params g_u_pars
     2127let rec graph_params_rect_Type4 h_mk_graph_params x_20993 =
     2128  let g_u_pars = x_20993 in h_mk_graph_params g_u_pars
    21292129
    21302130(** val graph_params_rect_Type5 :
    21312131    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2132 let rec graph_params_rect_Type5 h_mk_graph_params x_20826 =
    2133   let g_u_pars = x_20826 in h_mk_graph_params g_u_pars
     2132let rec graph_params_rect_Type5 h_mk_graph_params x_20995 =
     2133  let g_u_pars = x_20995 in h_mk_graph_params g_u_pars
    21342134
    21352135(** val graph_params_rect_Type3 :
    21362136    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2137 let rec graph_params_rect_Type3 h_mk_graph_params x_20828 =
    2138   let g_u_pars = x_20828 in h_mk_graph_params g_u_pars
     2137let rec graph_params_rect_Type3 h_mk_graph_params x_20997 =
     2138  let g_u_pars = x_20997 in h_mk_graph_params g_u_pars
    21392139
    21402140(** val graph_params_rect_Type2 :
    21412141    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2142 let rec graph_params_rect_Type2 h_mk_graph_params x_20830 =
    2143   let g_u_pars = x_20830 in h_mk_graph_params g_u_pars
     2142let rec graph_params_rect_Type2 h_mk_graph_params x_20999 =
     2143  let g_u_pars = x_20999 in h_mk_graph_params g_u_pars
    21442144
    21452145(** val graph_params_rect_Type1 :
    21462146    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2147 let rec graph_params_rect_Type1 h_mk_graph_params x_20832 =
    2148   let g_u_pars = x_20832 in h_mk_graph_params g_u_pars
     2147let rec graph_params_rect_Type1 h_mk_graph_params x_21001 =
     2148  let g_u_pars = x_21001 in h_mk_graph_params g_u_pars
    21492149
    21502150(** val graph_params_rect_Type0 :
    21512151    (uns_params -> 'a1) -> graph_params -> 'a1 **)
    2152 let rec graph_params_rect_Type0 h_mk_graph_params x_20834 =
    2153   let g_u_pars = x_20834 in h_mk_graph_params g_u_pars
     2152let rec graph_params_rect_Type0 h_mk_graph_params x_21003 =
     2153  let g_u_pars = x_21003 in h_mk_graph_params g_u_pars
    21542154
    21552155(** val g_u_pars : graph_params -> uns_params **)
     
    22212221    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22222222    'a1) -> joint_internal_function -> 'a1 **)
    2223 let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_20850 =
     2223let rec joint_internal_function_rect_Type4 p globals h_mk_joint_internal_function x_21019 =
    22242224  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22252225    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22272227    joint_if_stacksize0; joint_if_local_stacksize =
    22282228    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2229     joint_if_entry = joint_if_entry0 } = x_20850
     2229    joint_if_entry = joint_if_entry0 } = x_21019
    22302230  in
    22312231  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22372237    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22382238    'a1) -> joint_internal_function -> 'a1 **)
    2239 let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_20852 =
     2239let rec joint_internal_function_rect_Type5 p globals h_mk_joint_internal_function x_21021 =
    22402240  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22412241    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22432243    joint_if_stacksize0; joint_if_local_stacksize =
    22442244    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2245     joint_if_entry = joint_if_entry0 } = x_20852
     2245    joint_if_entry = joint_if_entry0 } = x_21021
    22462246  in
    22472247  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22532253    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22542254    'a1) -> joint_internal_function -> 'a1 **)
    2255 let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_20854 =
     2255let rec joint_internal_function_rect_Type3 p globals h_mk_joint_internal_function x_21023 =
    22562256  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22572257    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22592259    joint_if_stacksize0; joint_if_local_stacksize =
    22602260    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2261     joint_if_entry = joint_if_entry0 } = x_20854
     2261    joint_if_entry = joint_if_entry0 } = x_21023
    22622262  in
    22632263  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22692269    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22702270    'a1) -> joint_internal_function -> 'a1 **)
    2271 let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_20856 =
     2271let rec joint_internal_function_rect_Type2 p globals h_mk_joint_internal_function x_21025 =
    22722272  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22732273    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22752275    joint_if_stacksize0; joint_if_local_stacksize =
    22762276    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2277     joint_if_entry = joint_if_entry0 } = x_20856
     2277    joint_if_entry = joint_if_entry0 } = x_21025
    22782278  in
    22792279  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    22852285    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    22862286    'a1) -> joint_internal_function -> 'a1 **)
    2287 let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_20858 =
     2287let rec joint_internal_function_rect_Type1 p globals h_mk_joint_internal_function x_21027 =
    22882288  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    22892289    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    22912291    joint_if_stacksize0; joint_if_local_stacksize =
    22922292    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2293     joint_if_entry = joint_if_entry0 } = x_20858
     2293    joint_if_entry = joint_if_entry0 } = x_21027
    22942294  in
    22952295  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
     
    23012301    Identifiers.universe -> __ -> __ -> Nat.nat -> Nat.nat -> __ -> __ ->
    23022302    'a1) -> joint_internal_function -> 'a1 **)
    2303 let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_20860 =
     2303let rec joint_internal_function_rect_Type0 p globals h_mk_joint_internal_function x_21029 =
    23042304  let { joint_if_luniverse = joint_if_luniverse0; joint_if_runiverse =
    23052305    joint_if_runiverse0; joint_if_result = joint_if_result0;
     
    23072307    joint_if_stacksize0; joint_if_local_stacksize =
    23082308    joint_if_local_stacksize0; joint_if_code = joint_if_code0;
    2309     joint_if_entry = joint_if_entry0 } = x_20860
     2309    joint_if_entry = joint_if_entry0 } = x_21029
    23102310  in
    23112311  h_mk_joint_internal_function joint_if_luniverse0 joint_if_runiverse0
Note: See TracChangeset for help on using the changeset viewer.