Changeset 2743 for extracted/aSM.ml


Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSM.ml

    r2730 r2743  
    113113    -> 'a1) -> addressing_mode -> 'a1 **)
    114114let rec addressing_mode_rect_Type4 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    115 | DIRECT x_2727 -> h_DIRECT x_2727
    116 | INDIRECT x_2728 -> h_INDIRECT x_2728
    117 | EXT_INDIRECT x_2729 -> h_EXT_INDIRECT x_2729
    118 | REGISTER x_2730 -> h_REGISTER x_2730
     115| DIRECT x_21796 -> h_DIRECT x_21796
     116| INDIRECT x_21797 -> h_INDIRECT x_21797
     117| EXT_INDIRECT x_21798 -> h_EXT_INDIRECT x_21798
     118| REGISTER x_21799 -> h_REGISTER x_21799
    119119| ACC_A -> h_ACC_A
    120120| ACC_B -> h_ACC_B
    121121| DPTR -> h_DPTR
    122 | DATA x_2731 -> h_DATA x_2731
    123 | DATA16 x_2732 -> h_DATA16 x_2732
     122| DATA x_21800 -> h_DATA x_21800
     123| DATA16 x_21801 -> h_DATA16 x_21801
    124124| ACC_DPTR -> h_ACC_DPTR
    125125| ACC_PC -> h_ACC_PC
     
    127127| INDIRECT_DPTR -> h_INDIRECT_DPTR
    128128| CARRY -> h_CARRY
    129 | BIT_ADDR x_2733 -> h_BIT_ADDR x_2733
    130 | N_BIT_ADDR x_2734 -> h_N_BIT_ADDR x_2734
    131 | RELATIVE x_2735 -> h_RELATIVE x_2735
    132 | ADDR11 x_2736 -> h_ADDR11 x_2736
    133 | ADDR16 x_2737 -> h_ADDR16 x_2737
     129| BIT_ADDR x_21802 -> h_BIT_ADDR x_21802
     130| N_BIT_ADDR x_21803 -> h_N_BIT_ADDR x_21803
     131| RELATIVE x_21804 -> h_RELATIVE x_21804
     132| ADDR11 x_21805 -> h_ADDR11 x_21805
     133| ADDR16 x_21806 -> h_ADDR16 x_21806
    134134
    135135(** val addressing_mode_rect_Type5 :
     
    141141    -> 'a1) -> addressing_mode -> 'a1 **)
    142142let rec addressing_mode_rect_Type5 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    143 | DIRECT x_2758 -> h_DIRECT x_2758
    144 | INDIRECT x_2759 -> h_INDIRECT x_2759
    145 | EXT_INDIRECT x_2760 -> h_EXT_INDIRECT x_2760
    146 | REGISTER x_2761 -> h_REGISTER x_2761
     143| DIRECT x_21827 -> h_DIRECT x_21827
     144| INDIRECT x_21828 -> h_INDIRECT x_21828
     145| EXT_INDIRECT x_21829 -> h_EXT_INDIRECT x_21829
     146| REGISTER x_21830 -> h_REGISTER x_21830
    147147| ACC_A -> h_ACC_A
    148148| ACC_B -> h_ACC_B
    149149| DPTR -> h_DPTR
    150 | DATA x_2762 -> h_DATA x_2762
    151 | DATA16 x_2763 -> h_DATA16 x_2763
     150| DATA x_21831 -> h_DATA x_21831
     151| DATA16 x_21832 -> h_DATA16 x_21832
    152152| ACC_DPTR -> h_ACC_DPTR
    153153| ACC_PC -> h_ACC_PC
     
    155155| INDIRECT_DPTR -> h_INDIRECT_DPTR
    156156| CARRY -> h_CARRY
    157 | BIT_ADDR x_2764 -> h_BIT_ADDR x_2764
    158 | N_BIT_ADDR x_2765 -> h_N_BIT_ADDR x_2765
    159 | RELATIVE x_2766 -> h_RELATIVE x_2766
    160 | ADDR11 x_2767 -> h_ADDR11 x_2767
    161 | ADDR16 x_2768 -> h_ADDR16 x_2768
     157| BIT_ADDR x_21833 -> h_BIT_ADDR x_21833
     158| N_BIT_ADDR x_21834 -> h_N_BIT_ADDR x_21834
     159| RELATIVE x_21835 -> h_RELATIVE x_21835
     160| ADDR11 x_21836 -> h_ADDR11 x_21836
     161| ADDR16 x_21837 -> h_ADDR16 x_21837
    162162
    163163(** val addressing_mode_rect_Type3 :
     
    169169    -> 'a1) -> addressing_mode -> 'a1 **)
    170170let rec addressing_mode_rect_Type3 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    171 | DIRECT x_2789 -> h_DIRECT x_2789
    172 | INDIRECT x_2790 -> h_INDIRECT x_2790
    173 | EXT_INDIRECT x_2791 -> h_EXT_INDIRECT x_2791
    174 | REGISTER x_2792 -> h_REGISTER x_2792
     171| DIRECT x_21858 -> h_DIRECT x_21858
     172| INDIRECT x_21859 -> h_INDIRECT x_21859
     173| EXT_INDIRECT x_21860 -> h_EXT_INDIRECT x_21860
     174| REGISTER x_21861 -> h_REGISTER x_21861
    175175| ACC_A -> h_ACC_A
    176176| ACC_B -> h_ACC_B
    177177| DPTR -> h_DPTR
    178 | DATA x_2793 -> h_DATA x_2793
    179 | DATA16 x_2794 -> h_DATA16 x_2794
     178| DATA x_21862 -> h_DATA x_21862
     179| DATA16 x_21863 -> h_DATA16 x_21863
    180180| ACC_DPTR -> h_ACC_DPTR
    181181| ACC_PC -> h_ACC_PC
     
    183183| INDIRECT_DPTR -> h_INDIRECT_DPTR
    184184| CARRY -> h_CARRY
    185 | BIT_ADDR x_2795 -> h_BIT_ADDR x_2795
    186 | N_BIT_ADDR x_2796 -> h_N_BIT_ADDR x_2796
    187 | RELATIVE x_2797 -> h_RELATIVE x_2797
    188 | ADDR11 x_2798 -> h_ADDR11 x_2798
    189 | ADDR16 x_2799 -> h_ADDR16 x_2799
     185| BIT_ADDR x_21864 -> h_BIT_ADDR x_21864
     186| N_BIT_ADDR x_21865 -> h_N_BIT_ADDR x_21865
     187| RELATIVE x_21866 -> h_RELATIVE x_21866
     188| ADDR11 x_21867 -> h_ADDR11 x_21867
     189| ADDR16 x_21868 -> h_ADDR16 x_21868
    190190
    191191(** val addressing_mode_rect_Type2 :
     
    197197    -> 'a1) -> addressing_mode -> 'a1 **)
    198198let rec addressing_mode_rect_Type2 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    199 | DIRECT x_2820 -> h_DIRECT x_2820
    200 | INDIRECT x_2821 -> h_INDIRECT x_2821
    201 | EXT_INDIRECT x_2822 -> h_EXT_INDIRECT x_2822
    202 | REGISTER x_2823 -> h_REGISTER x_2823
     199| DIRECT x_21889 -> h_DIRECT x_21889
     200| INDIRECT x_21890 -> h_INDIRECT x_21890
     201| EXT_INDIRECT x_21891 -> h_EXT_INDIRECT x_21891
     202| REGISTER x_21892 -> h_REGISTER x_21892
    203203| ACC_A -> h_ACC_A
    204204| ACC_B -> h_ACC_B
    205205| DPTR -> h_DPTR
    206 | DATA x_2824 -> h_DATA x_2824
    207 | DATA16 x_2825 -> h_DATA16 x_2825
     206| DATA x_21893 -> h_DATA x_21893
     207| DATA16 x_21894 -> h_DATA16 x_21894
    208208| ACC_DPTR -> h_ACC_DPTR
    209209| ACC_PC -> h_ACC_PC
     
    211211| INDIRECT_DPTR -> h_INDIRECT_DPTR
    212212| CARRY -> h_CARRY
    213 | BIT_ADDR x_2826 -> h_BIT_ADDR x_2826
    214 | N_BIT_ADDR x_2827 -> h_N_BIT_ADDR x_2827
    215 | RELATIVE x_2828 -> h_RELATIVE x_2828
    216 | ADDR11 x_2829 -> h_ADDR11 x_2829
    217 | ADDR16 x_2830 -> h_ADDR16 x_2830
     213| BIT_ADDR x_21895 -> h_BIT_ADDR x_21895
     214| N_BIT_ADDR x_21896 -> h_N_BIT_ADDR x_21896
     215| RELATIVE x_21897 -> h_RELATIVE x_21897
     216| ADDR11 x_21898 -> h_ADDR11 x_21898
     217| ADDR16 x_21899 -> h_ADDR16 x_21899
    218218
    219219(** val addressing_mode_rect_Type1 :
     
    225225    -> 'a1) -> addressing_mode -> 'a1 **)
    226226let rec addressing_mode_rect_Type1 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    227 | DIRECT x_2851 -> h_DIRECT x_2851
    228 | INDIRECT x_2852 -> h_INDIRECT x_2852
    229 | EXT_INDIRECT x_2853 -> h_EXT_INDIRECT x_2853
    230 | REGISTER x_2854 -> h_REGISTER x_2854
     227| DIRECT x_21920 -> h_DIRECT x_21920
     228| INDIRECT x_21921 -> h_INDIRECT x_21921
     229| EXT_INDIRECT x_21922 -> h_EXT_INDIRECT x_21922
     230| REGISTER x_21923 -> h_REGISTER x_21923
    231231| ACC_A -> h_ACC_A
    232232| ACC_B -> h_ACC_B
    233233| DPTR -> h_DPTR
    234 | DATA x_2855 -> h_DATA x_2855
    235 | DATA16 x_2856 -> h_DATA16 x_2856
     234| DATA x_21924 -> h_DATA x_21924
     235| DATA16 x_21925 -> h_DATA16 x_21925
    236236| ACC_DPTR -> h_ACC_DPTR
    237237| ACC_PC -> h_ACC_PC
     
    239239| INDIRECT_DPTR -> h_INDIRECT_DPTR
    240240| CARRY -> h_CARRY
    241 | BIT_ADDR x_2857 -> h_BIT_ADDR x_2857
    242 | N_BIT_ADDR x_2858 -> h_N_BIT_ADDR x_2858
    243 | RELATIVE x_2859 -> h_RELATIVE x_2859
    244 | ADDR11 x_2860 -> h_ADDR11 x_2860
    245 | ADDR16 x_2861 -> h_ADDR16 x_2861
     241| BIT_ADDR x_21926 -> h_BIT_ADDR x_21926
     242| N_BIT_ADDR x_21927 -> h_N_BIT_ADDR x_21927
     243| RELATIVE x_21928 -> h_RELATIVE x_21928
     244| ADDR11 x_21929 -> h_ADDR11 x_21929
     245| ADDR16 x_21930 -> h_ADDR16 x_21930
    246246
    247247(** val addressing_mode_rect_Type0 :
     
    253253    -> 'a1) -> addressing_mode -> 'a1 **)
    254254let rec addressing_mode_rect_Type0 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function
    255 | DIRECT x_2882 -> h_DIRECT x_2882
    256 | INDIRECT x_2883 -> h_INDIRECT x_2883
    257 | EXT_INDIRECT x_2884 -> h_EXT_INDIRECT x_2884
    258 | REGISTER x_2885 -> h_REGISTER x_2885
     255| DIRECT x_21951 -> h_DIRECT x_21951
     256| INDIRECT x_21952 -> h_INDIRECT x_21952
     257| EXT_INDIRECT x_21953 -> h_EXT_INDIRECT x_21953
     258| REGISTER x_21954 -> h_REGISTER x_21954
    259259| ACC_A -> h_ACC_A
    260260| ACC_B -> h_ACC_B
    261261| DPTR -> h_DPTR
    262 | DATA x_2886 -> h_DATA x_2886
    263 | DATA16 x_2887 -> h_DATA16 x_2887
     262| DATA x_21955 -> h_DATA x_21955
     263| DATA16 x_21956 -> h_DATA16 x_21956
    264264| ACC_DPTR -> h_ACC_DPTR
    265265| ACC_PC -> h_ACC_PC
     
    267267| INDIRECT_DPTR -> h_INDIRECT_DPTR
    268268| CARRY -> h_CARRY
    269 | BIT_ADDR x_2888 -> h_BIT_ADDR x_2888
    270 | N_BIT_ADDR x_2889 -> h_N_BIT_ADDR x_2889
    271 | RELATIVE x_2890 -> h_RELATIVE x_2890
    272 | ADDR11 x_2891 -> h_ADDR11 x_2891
    273 | ADDR16 x_2892 -> h_ADDR16 x_2892
     269| BIT_ADDR x_21957 -> h_BIT_ADDR x_21957
     270| N_BIT_ADDR x_21958 -> h_N_BIT_ADDR x_21958
     271| RELATIVE x_21959 -> h_RELATIVE x_21959
     272| ADDR11 x_21960 -> h_ADDR11 x_21960
     273| ADDR16 x_21961 -> h_ADDR16 x_21961
    274274
    275275(** val addressing_mode_inv_rect_Type4 :
     
    19281928    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19291929    'a1) -> subaddressing_mode -> 'a1 **)
    1930 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_3360 =
    1931   let subaddressing_modeel = x_3360 in
     1930let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_22429 =
     1931  let subaddressing_modeel = x_22429 in
    19321932  h_mk_subaddressing_mode subaddressing_modeel __
    19331933
     
    19351935    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19361936    'a1) -> subaddressing_mode -> 'a1 **)
    1937 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_3362 =
    1938   let subaddressing_modeel = x_3362 in
     1937let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_22431 =
     1938  let subaddressing_modeel = x_22431 in
    19391939  h_mk_subaddressing_mode subaddressing_modeel __
    19401940
     
    19421942    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19431943    'a1) -> subaddressing_mode -> 'a1 **)
    1944 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_3364 =
    1945   let subaddressing_modeel = x_3364 in
     1944let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_22433 =
     1945  let subaddressing_modeel = x_22433 in
    19461946  h_mk_subaddressing_mode subaddressing_modeel __
    19471947
     
    19491949    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19501950    'a1) -> subaddressing_mode -> 'a1 **)
    1951 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_3366 =
    1952   let subaddressing_modeel = x_3366 in
     1951let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_22435 =
     1952  let subaddressing_modeel = x_22435 in
    19531953  h_mk_subaddressing_mode subaddressing_modeel __
    19541954
     
    19561956    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19571957    'a1) -> subaddressing_mode -> 'a1 **)
    1958 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_3368 =
    1959   let subaddressing_modeel = x_3368 in
     1958let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_22437 =
     1959  let subaddressing_modeel = x_22437 in
    19601960  h_mk_subaddressing_mode subaddressing_modeel __
    19611961
     
    19631963    Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ ->
    19641964    'a1) -> subaddressing_mode -> 'a1 **)
    1965 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_3370 =
    1966   let subaddressing_modeel = x_3370 in
     1965let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_22439 =
     1966  let subaddressing_modeel = x_22439 in
    19671967  h_mk_subaddressing_mode subaddressing_modeel __
    19681968
     
    20442044let eject__o__subaddressing_modeel x0 x1 x3 =
    20452045  subaddressing_modeel x0 x1 (Types.pi1 x3)
     2046
     2047type 'x1 dpi1__o__subaddressing_mode = subaddressing_mode
     2048
     2049type eject__o__subaddressing_mode = subaddressing_mode
     2050
     2051(** val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
     2052    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2053    addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
     2054    Types.dPair -> subaddressing_mode Types.sig0 **)
     2055let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject x0 x1 x2 x3 x6 =
     2056  dpi1__o__subaddressing_modeel x0 x2 x6
     2057
     2058(** val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     2059    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2060    addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
     2061    Types.dPair -> addressing_mode Types.sig0 **)
     2062let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x0 x2 x3 x4 x6 =
     2063  subaddressing_modeel__o__inject x2 x4
     2064    (dpi1__o__subaddressing_modeel x0 x3 x6)
     2065
     2066(** val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
     2067    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2068    addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
     2069    Types.dPair -> addressing_mode **)
     2070let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 x3 x5 =
     2071  subaddressing_modeel x1 x3 (dpi1__o__subaddressing_modeel x0 x2 x5)
     2072
     2073(** val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
     2074    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2075    addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
     2076    subaddressing_mode Types.sig0 **)
     2077let eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject x0 x1 x2 x3 x6 =
     2078  eject__o__subaddressing_modeel x0 x2 x6
     2079
     2080(** val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     2081    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2082    addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
     2083    addressing_mode Types.sig0 **)
     2084let eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x0 x2 x3 x4 x6 =
     2085  subaddressing_modeel__o__inject x2 x4
     2086    (eject__o__subaddressing_modeel x0 x3 x6)
     2087
     2088(** val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
     2089    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2090    addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
     2091    addressing_mode **)
     2092let eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 x3 x5 =
     2093  subaddressing_modeel x1 x3 (eject__o__subaddressing_modeel x0 x2 x5)
     2094
     2095(** val subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
     2096    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2097    addressing_mode_tag Vector.vector -> subaddressing_mode ->
     2098    subaddressing_mode Types.sig0 **)
     2099let subaddressing_modeel__o__mk_subaddressing_mode__o__inject x0 x1 x2 x3 x4 =
     2100  subaddressing_modeel x0 x2 x4
     2101
     2102(** val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     2103    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2104    addressing_mode_tag Vector.vector -> subaddressing_mode ->
     2105    addressing_mode Types.sig0 **)
     2106let subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x0 x2 x3 x4 x5 =
     2107  subaddressing_modeel__o__inject x2 x4 (subaddressing_modeel x0 x3 x5)
     2108
     2109(** val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
     2110    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2111    addressing_mode_tag Vector.vector -> subaddressing_mode ->
     2112    addressing_mode **)
     2113let subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 x3 x4 =
     2114  subaddressing_modeel x1 x3 (subaddressing_modeel x0 x2 x4)
     2115
     2116(** val dpi1__o__mk_subaddressing_mode__o__inject :
     2117    Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
     2118    Vector.vector -> subaddressing_mode Types.sig0 **)
     2119let dpi1__o__mk_subaddressing_mode__o__inject x1 x2 x3 =
     2120  x2.Types.dpi1
     2121
     2122(** val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     2123    Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
     2124    Vector.vector -> addressing_mode Types.sig0 **)
     2125let dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x2 x3 x4 =
     2126  subaddressing_modeel__o__inject x2 x4 x3.Types.dpi1
     2127
     2128(** val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel :
     2129    Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
     2130    Vector.vector -> addressing_mode **)
     2131let dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel x1 x2 x3 =
     2132  subaddressing_modeel x1 x3 x2.Types.dpi1
     2133
     2134(** val eject__o__mk_subaddressing_mode__o__inject :
     2135    Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag
     2136    Vector.vector -> subaddressing_mode Types.sig0 **)
     2137let eject__o__mk_subaddressing_mode__o__inject x1 x2 x3 =
     2138  Types.pi1 x2
     2139
     2140(** val eject__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     2141    Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag
     2142    Vector.vector -> addressing_mode Types.sig0 **)
     2143let eject__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x2 x3 x4 =
     2144  subaddressing_modeel__o__inject x2 x4 (Types.pi1 x3)
     2145
     2146(** val eject__o__mk_subaddressing_mode__o__subaddressing_modeel :
     2147    Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag
     2148    Vector.vector -> addressing_mode **)
     2149let eject__o__mk_subaddressing_mode__o__subaddressing_modeel x1 x2 x3 =
     2150  subaddressing_modeel x1 x3 (Types.pi1 x2)
     2151
     2152(** val mk_subaddressing_mode__o__subaddressing_modeel :
     2153    Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
     2154    addressing_mode **)
     2155let mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 =
     2156  subaddressing_modeel x0 x2 x1
     2157
     2158(** val mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     2159    Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
     2160    addressing_mode Types.sig0 **)
     2161let mk_subaddressing_mode__o__subaddressing_modeel__o__inject x1 x2 x3 =
     2162  subaddressing_modeel__o__inject x1 x3 x2
     2163
     2164(** val mk_subaddressing_mode__o__inject :
     2165    Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
     2166    subaddressing_mode Types.sig0 **)
     2167let mk_subaddressing_mode__o__inject x0 x1 x2 =
     2168  x1
     2169
     2170(** val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode :
     2171    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2172    addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1)
     2173    Types.dPair -> subaddressing_mode **)
     2174let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode x0 x1 x2 x3 x5 =
     2175  dpi1__o__subaddressing_modeel x0 x2 x5
     2176
     2177(** val eject__o__subaddressing_modeel__o__mk_subaddressing_mode :
     2178    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2179    addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
     2180    subaddressing_mode **)
     2181let eject__o__subaddressing_modeel__o__mk_subaddressing_mode x0 x1 x2 x3 x5 =
     2182  eject__o__subaddressing_modeel x0 x2 x5
     2183
     2184(** val subaddressing_modeel__o__mk_subaddressing_mode :
     2185    Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     2186    addressing_mode_tag Vector.vector -> subaddressing_mode ->
     2187    subaddressing_mode **)
     2188let subaddressing_modeel__o__mk_subaddressing_mode x0 x1 x2 x3 x4 =
     2189  subaddressing_modeel x0 x2 x4
     2190
     2191(** val dpi1__o__mk_subaddressing_mode :
     2192    Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
     2193    Vector.vector -> subaddressing_mode **)
     2194let dpi1__o__mk_subaddressing_mode x1 x2 x3 =
     2195  x2.Types.dpi1
     2196
     2197(** val eject__o__mk_subaddressing_mode :
     2198    Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag
     2199    Vector.vector -> subaddressing_mode **)
     2200let eject__o__mk_subaddressing_mode x1 x2 x3 =
     2201  Types.pi1 x2
    20462202
    20472203type subaddressing_mode_elim_type = __
     
    21362292    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    21372293let rec preinstruction_rect_Type4 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2138 | ADD (x_3472, x_3471) -> h_ADD x_3472 x_3471
    2139 | ADDC (x_3474, x_3473) -> h_ADDC x_3474 x_3473
    2140 | SUBB (x_3476, x_3475) -> h_SUBB x_3476 x_3475
    2141 | INC x_3477 -> h_INC x_3477
    2142 | DEC x_3478 -> h_DEC x_3478
    2143 | MUL (x_3480, x_3479) -> h_MUL x_3480 x_3479
    2144 | DIV (x_3482, x_3481) -> h_DIV x_3482 x_3481
    2145 | DA x_3483 -> h_DA x_3483
    2146 | JC x_3484 -> h_JC x_3484
    2147 | JNC x_3485 -> h_JNC x_3485
    2148 | JB (x_3487, x_3486) -> h_JB x_3487 x_3486
    2149 | JNB (x_3489, x_3488) -> h_JNB x_3489 x_3488
    2150 | JBC (x_3491, x_3490) -> h_JBC x_3491 x_3490
    2151 | JZ x_3492 -> h_JZ x_3492
    2152 | JNZ x_3493 -> h_JNZ x_3493
    2153 | CJNE (x_3495, x_3494) -> h_CJNE x_3495 x_3494
    2154 | DJNZ (x_3497, x_3496) -> h_DJNZ x_3497 x_3496
    2155 | ANL x_3498 -> h_ANL x_3498
    2156 | ORL x_3499 -> h_ORL x_3499
    2157 | XRL x_3500 -> h_XRL x_3500
    2158 | CLR x_3501 -> h_CLR x_3501
    2159 | CPL x_3502 -> h_CPL x_3502
    2160 | RL x_3503 -> h_RL x_3503
    2161 | RLC x_3504 -> h_RLC x_3504
    2162 | RR x_3505 -> h_RR x_3505
    2163 | RRC x_3506 -> h_RRC x_3506
    2164 | SWAP x_3507 -> h_SWAP x_3507
    2165 | MOV x_3508 -> h_MOV x_3508
    2166 | MOVX x_3509 -> h_MOVX x_3509
    2167 | SETB x_3510 -> h_SETB x_3510
    2168 | PUSH x_3511 -> h_PUSH x_3511
    2169 | POP x_3512 -> h_POP x_3512
    2170 | XCH (x_3514, x_3513) -> h_XCH x_3514 x_3513
    2171 | XCHD (x_3516, x_3515) -> h_XCHD x_3516 x_3515
     2294| ADD (x_22541, x_22540) -> h_ADD x_22541 x_22540
     2295| ADDC (x_22543, x_22542) -> h_ADDC x_22543 x_22542
     2296| SUBB (x_22545, x_22544) -> h_SUBB x_22545 x_22544
     2297| INC x_22546 -> h_INC x_22546
     2298| DEC x_22547 -> h_DEC x_22547
     2299| MUL (x_22549, x_22548) -> h_MUL x_22549 x_22548
     2300| DIV (x_22551, x_22550) -> h_DIV x_22551 x_22550
     2301| DA x_22552 -> h_DA x_22552
     2302| JC x_22553 -> h_JC x_22553
     2303| JNC x_22554 -> h_JNC x_22554
     2304| JB (x_22556, x_22555) -> h_JB x_22556 x_22555
     2305| JNB (x_22558, x_22557) -> h_JNB x_22558 x_22557
     2306| JBC (x_22560, x_22559) -> h_JBC x_22560 x_22559
     2307| JZ x_22561 -> h_JZ x_22561
     2308| JNZ x_22562 -> h_JNZ x_22562
     2309| CJNE (x_22564, x_22563) -> h_CJNE x_22564 x_22563
     2310| DJNZ (x_22566, x_22565) -> h_DJNZ x_22566 x_22565
     2311| ANL x_22567 -> h_ANL x_22567
     2312| ORL x_22568 -> h_ORL x_22568
     2313| XRL x_22569 -> h_XRL x_22569
     2314| CLR x_22570 -> h_CLR x_22570
     2315| CPL x_22571 -> h_CPL x_22571
     2316| RL x_22572 -> h_RL x_22572
     2317| RLC x_22573 -> h_RLC x_22573
     2318| RR x_22574 -> h_RR x_22574
     2319| RRC x_22575 -> h_RRC x_22575
     2320| SWAP x_22576 -> h_SWAP x_22576
     2321| MOV x_22577 -> h_MOV x_22577
     2322| MOVX x_22578 -> h_MOVX x_22578
     2323| SETB x_22579 -> h_SETB x_22579
     2324| PUSH x_22580 -> h_PUSH x_22580
     2325| POP x_22581 -> h_POP x_22581
     2326| XCH (x_22583, x_22582) -> h_XCH x_22583 x_22582
     2327| XCHD (x_22585, x_22584) -> h_XCHD x_22585 x_22584
    21722328| RET -> h_RET
    21732329| RETI -> h_RETI
    21742330| NOP -> h_NOP
    2175 | JMP x_3517 -> h_JMP x_3517
     2331| JMP x_22586 -> h_JMP x_22586
    21762332
    21772333(** val preinstruction_rect_Type5 :
     
    22112367    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    22122368let rec preinstruction_rect_Type5 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2213 | ADD (x_3558, x_3557) -> h_ADD x_3558 x_3557
    2214 | ADDC (x_3560, x_3559) -> h_ADDC x_3560 x_3559
    2215 | SUBB (x_3562, x_3561) -> h_SUBB x_3562 x_3561
    2216 | INC x_3563 -> h_INC x_3563
    2217 | DEC x_3564 -> h_DEC x_3564
    2218 | MUL (x_3566, x_3565) -> h_MUL x_3566 x_3565
    2219 | DIV (x_3568, x_3567) -> h_DIV x_3568 x_3567
    2220 | DA x_3569 -> h_DA x_3569
    2221 | JC x_3570 -> h_JC x_3570
    2222 | JNC x_3571 -> h_JNC x_3571
    2223 | JB (x_3573, x_3572) -> h_JB x_3573 x_3572
    2224 | JNB (x_3575, x_3574) -> h_JNB x_3575 x_3574
    2225 | JBC (x_3577, x_3576) -> h_JBC x_3577 x_3576
    2226 | JZ x_3578 -> h_JZ x_3578
    2227 | JNZ x_3579 -> h_JNZ x_3579
    2228 | CJNE (x_3581, x_3580) -> h_CJNE x_3581 x_3580
    2229 | DJNZ (x_3583, x_3582) -> h_DJNZ x_3583 x_3582
    2230 | ANL x_3584 -> h_ANL x_3584
    2231 | ORL x_3585 -> h_ORL x_3585
    2232 | XRL x_3586 -> h_XRL x_3586
    2233 | CLR x_3587 -> h_CLR x_3587
    2234 | CPL x_3588 -> h_CPL x_3588
    2235 | RL x_3589 -> h_RL x_3589
    2236 | RLC x_3590 -> h_RLC x_3590
    2237 | RR x_3591 -> h_RR x_3591
    2238 | RRC x_3592 -> h_RRC x_3592
    2239 | SWAP x_3593 -> h_SWAP x_3593
    2240 | MOV x_3594 -> h_MOV x_3594
    2241 | MOVX x_3595 -> h_MOVX x_3595
    2242 | SETB x_3596 -> h_SETB x_3596
    2243 | PUSH x_3597 -> h_PUSH x_3597
    2244 | POP x_3598 -> h_POP x_3598
    2245 | XCH (x_3600, x_3599) -> h_XCH x_3600 x_3599
    2246 | XCHD (x_3602, x_3601) -> h_XCHD x_3602 x_3601
     2369| ADD (x_22627, x_22626) -> h_ADD x_22627 x_22626
     2370| ADDC (x_22629, x_22628) -> h_ADDC x_22629 x_22628
     2371| SUBB (x_22631, x_22630) -> h_SUBB x_22631 x_22630
     2372| INC x_22632 -> h_INC x_22632
     2373| DEC x_22633 -> h_DEC x_22633
     2374| MUL (x_22635, x_22634) -> h_MUL x_22635 x_22634
     2375| DIV (x_22637, x_22636) -> h_DIV x_22637 x_22636
     2376| DA x_22638 -> h_DA x_22638
     2377| JC x_22639 -> h_JC x_22639
     2378| JNC x_22640 -> h_JNC x_22640
     2379| JB (x_22642, x_22641) -> h_JB x_22642 x_22641
     2380| JNB (x_22644, x_22643) -> h_JNB x_22644 x_22643
     2381| JBC (x_22646, x_22645) -> h_JBC x_22646 x_22645
     2382| JZ x_22647 -> h_JZ x_22647
     2383| JNZ x_22648 -> h_JNZ x_22648
     2384| CJNE (x_22650, x_22649) -> h_CJNE x_22650 x_22649
     2385| DJNZ (x_22652, x_22651) -> h_DJNZ x_22652 x_22651
     2386| ANL x_22653 -> h_ANL x_22653
     2387| ORL x_22654 -> h_ORL x_22654
     2388| XRL x_22655 -> h_XRL x_22655
     2389| CLR x_22656 -> h_CLR x_22656
     2390| CPL x_22657 -> h_CPL x_22657
     2391| RL x_22658 -> h_RL x_22658
     2392| RLC x_22659 -> h_RLC x_22659
     2393| RR x_22660 -> h_RR x_22660
     2394| RRC x_22661 -> h_RRC x_22661
     2395| SWAP x_22662 -> h_SWAP x_22662
     2396| MOV x_22663 -> h_MOV x_22663
     2397| MOVX x_22664 -> h_MOVX x_22664
     2398| SETB x_22665 -> h_SETB x_22665
     2399| PUSH x_22666 -> h_PUSH x_22666
     2400| POP x_22667 -> h_POP x_22667
     2401| XCH (x_22669, x_22668) -> h_XCH x_22669 x_22668
     2402| XCHD (x_22671, x_22670) -> h_XCHD x_22671 x_22670
    22472403| RET -> h_RET
    22482404| RETI -> h_RETI
    22492405| NOP -> h_NOP
    2250 | JMP x_3603 -> h_JMP x_3603
     2406| JMP x_22672 -> h_JMP x_22672
    22512407
    22522408(** val preinstruction_rect_Type3 :
     
    22862442    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    22872443let rec preinstruction_rect_Type3 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2288 | ADD (x_3644, x_3643) -> h_ADD x_3644 x_3643
    2289 | ADDC (x_3646, x_3645) -> h_ADDC x_3646 x_3645
    2290 | SUBB (x_3648, x_3647) -> h_SUBB x_3648 x_3647
    2291 | INC x_3649 -> h_INC x_3649
    2292 | DEC x_3650 -> h_DEC x_3650
    2293 | MUL (x_3652, x_3651) -> h_MUL x_3652 x_3651
    2294 | DIV (x_3654, x_3653) -> h_DIV x_3654 x_3653
    2295 | DA x_3655 -> h_DA x_3655
    2296 | JC x_3656 -> h_JC x_3656
    2297 | JNC x_3657 -> h_JNC x_3657
    2298 | JB (x_3659, x_3658) -> h_JB x_3659 x_3658
    2299 | JNB (x_3661, x_3660) -> h_JNB x_3661 x_3660
    2300 | JBC (x_3663, x_3662) -> h_JBC x_3663 x_3662
    2301 | JZ x_3664 -> h_JZ x_3664
    2302 | JNZ x_3665 -> h_JNZ x_3665
    2303 | CJNE (x_3667, x_3666) -> h_CJNE x_3667 x_3666
    2304 | DJNZ (x_3669, x_3668) -> h_DJNZ x_3669 x_3668
    2305 | ANL x_3670 -> h_ANL x_3670
    2306 | ORL x_3671 -> h_ORL x_3671
    2307 | XRL x_3672 -> h_XRL x_3672
    2308 | CLR x_3673 -> h_CLR x_3673
    2309 | CPL x_3674 -> h_CPL x_3674
    2310 | RL x_3675 -> h_RL x_3675
    2311 | RLC x_3676 -> h_RLC x_3676
    2312 | RR x_3677 -> h_RR x_3677
    2313 | RRC x_3678 -> h_RRC x_3678
    2314 | SWAP x_3679 -> h_SWAP x_3679
    2315 | MOV x_3680 -> h_MOV x_3680
    2316 | MOVX x_3681 -> h_MOVX x_3681
    2317 | SETB x_3682 -> h_SETB x_3682
    2318 | PUSH x_3683 -> h_PUSH x_3683
    2319 | POP x_3684 -> h_POP x_3684
    2320 | XCH (x_3686, x_3685) -> h_XCH x_3686 x_3685
    2321 | XCHD (x_3688, x_3687) -> h_XCHD x_3688 x_3687
     2444| ADD (x_22713, x_22712) -> h_ADD x_22713 x_22712
     2445| ADDC (x_22715, x_22714) -> h_ADDC x_22715 x_22714
     2446| SUBB (x_22717, x_22716) -> h_SUBB x_22717 x_22716
     2447| INC x_22718 -> h_INC x_22718
     2448| DEC x_22719 -> h_DEC x_22719
     2449| MUL (x_22721, x_22720) -> h_MUL x_22721 x_22720
     2450| DIV (x_22723, x_22722) -> h_DIV x_22723 x_22722
     2451| DA x_22724 -> h_DA x_22724
     2452| JC x_22725 -> h_JC x_22725
     2453| JNC x_22726 -> h_JNC x_22726
     2454| JB (x_22728, x_22727) -> h_JB x_22728 x_22727
     2455| JNB (x_22730, x_22729) -> h_JNB x_22730 x_22729
     2456| JBC (x_22732, x_22731) -> h_JBC x_22732 x_22731
     2457| JZ x_22733 -> h_JZ x_22733
     2458| JNZ x_22734 -> h_JNZ x_22734
     2459| CJNE (x_22736, x_22735) -> h_CJNE x_22736 x_22735
     2460| DJNZ (x_22738, x_22737) -> h_DJNZ x_22738 x_22737
     2461| ANL x_22739 -> h_ANL x_22739
     2462| ORL x_22740 -> h_ORL x_22740
     2463| XRL x_22741 -> h_XRL x_22741
     2464| CLR x_22742 -> h_CLR x_22742
     2465| CPL x_22743 -> h_CPL x_22743
     2466| RL x_22744 -> h_RL x_22744
     2467| RLC x_22745 -> h_RLC x_22745
     2468| RR x_22746 -> h_RR x_22746
     2469| RRC x_22747 -> h_RRC x_22747
     2470| SWAP x_22748 -> h_SWAP x_22748
     2471| MOV x_22749 -> h_MOV x_22749
     2472| MOVX x_22750 -> h_MOVX x_22750
     2473| SETB x_22751 -> h_SETB x_22751
     2474| PUSH x_22752 -> h_PUSH x_22752
     2475| POP x_22753 -> h_POP x_22753
     2476| XCH (x_22755, x_22754) -> h_XCH x_22755 x_22754
     2477| XCHD (x_22757, x_22756) -> h_XCHD x_22757 x_22756
    23222478| RET -> h_RET
    23232479| RETI -> h_RETI
    23242480| NOP -> h_NOP
    2325 | JMP x_3689 -> h_JMP x_3689
     2481| JMP x_22758 -> h_JMP x_22758
    23262482
    23272483(** val preinstruction_rect_Type2 :
     
    23612517    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    23622518let rec preinstruction_rect_Type2 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2363 | ADD (x_3730, x_3729) -> h_ADD x_3730 x_3729
    2364 | ADDC (x_3732, x_3731) -> h_ADDC x_3732 x_3731
    2365 | SUBB (x_3734, x_3733) -> h_SUBB x_3734 x_3733
    2366 | INC x_3735 -> h_INC x_3735
    2367 | DEC x_3736 -> h_DEC x_3736
    2368 | MUL (x_3738, x_3737) -> h_MUL x_3738 x_3737
    2369 | DIV (x_3740, x_3739) -> h_DIV x_3740 x_3739
    2370 | DA x_3741 -> h_DA x_3741
    2371 | JC x_3742 -> h_JC x_3742
    2372 | JNC x_3743 -> h_JNC x_3743
    2373 | JB (x_3745, x_3744) -> h_JB x_3745 x_3744
    2374 | JNB (x_3747, x_3746) -> h_JNB x_3747 x_3746
    2375 | JBC (x_3749, x_3748) -> h_JBC x_3749 x_3748
    2376 | JZ x_3750 -> h_JZ x_3750
    2377 | JNZ x_3751 -> h_JNZ x_3751
    2378 | CJNE (x_3753, x_3752) -> h_CJNE x_3753 x_3752
    2379 | DJNZ (x_3755, x_3754) -> h_DJNZ x_3755 x_3754
    2380 | ANL x_3756 -> h_ANL x_3756
    2381 | ORL x_3757 -> h_ORL x_3757
    2382 | XRL x_3758 -> h_XRL x_3758
    2383 | CLR x_3759 -> h_CLR x_3759
    2384 | CPL x_3760 -> h_CPL x_3760
    2385 | RL x_3761 -> h_RL x_3761
    2386 | RLC x_3762 -> h_RLC x_3762
    2387 | RR x_3763 -> h_RR x_3763
    2388 | RRC x_3764 -> h_RRC x_3764
    2389 | SWAP x_3765 -> h_SWAP x_3765
    2390 | MOV x_3766 -> h_MOV x_3766
    2391 | MOVX x_3767 -> h_MOVX x_3767
    2392 | SETB x_3768 -> h_SETB x_3768
    2393 | PUSH x_3769 -> h_PUSH x_3769
    2394 | POP x_3770 -> h_POP x_3770
    2395 | XCH (x_3772, x_3771) -> h_XCH x_3772 x_3771
    2396 | XCHD (x_3774, x_3773) -> h_XCHD x_3774 x_3773
     2519| ADD (x_22799, x_22798) -> h_ADD x_22799 x_22798
     2520| ADDC (x_22801, x_22800) -> h_ADDC x_22801 x_22800
     2521| SUBB (x_22803, x_22802) -> h_SUBB x_22803 x_22802
     2522| INC x_22804 -> h_INC x_22804
     2523| DEC x_22805 -> h_DEC x_22805
     2524| MUL (x_22807, x_22806) -> h_MUL x_22807 x_22806
     2525| DIV (x_22809, x_22808) -> h_DIV x_22809 x_22808
     2526| DA x_22810 -> h_DA x_22810
     2527| JC x_22811 -> h_JC x_22811
     2528| JNC x_22812 -> h_JNC x_22812
     2529| JB (x_22814, x_22813) -> h_JB x_22814 x_22813
     2530| JNB (x_22816, x_22815) -> h_JNB x_22816 x_22815
     2531| JBC (x_22818, x_22817) -> h_JBC x_22818 x_22817
     2532| JZ x_22819 -> h_JZ x_22819
     2533| JNZ x_22820 -> h_JNZ x_22820
     2534| CJNE (x_22822, x_22821) -> h_CJNE x_22822 x_22821
     2535| DJNZ (x_22824, x_22823) -> h_DJNZ x_22824 x_22823
     2536| ANL x_22825 -> h_ANL x_22825
     2537| ORL x_22826 -> h_ORL x_22826
     2538| XRL x_22827 -> h_XRL x_22827
     2539| CLR x_22828 -> h_CLR x_22828
     2540| CPL x_22829 -> h_CPL x_22829
     2541| RL x_22830 -> h_RL x_22830
     2542| RLC x_22831 -> h_RLC x_22831
     2543| RR x_22832 -> h_RR x_22832
     2544| RRC x_22833 -> h_RRC x_22833
     2545| SWAP x_22834 -> h_SWAP x_22834
     2546| MOV x_22835 -> h_MOV x_22835
     2547| MOVX x_22836 -> h_MOVX x_22836
     2548| SETB x_22837 -> h_SETB x_22837
     2549| PUSH x_22838 -> h_PUSH x_22838
     2550| POP x_22839 -> h_POP x_22839
     2551| XCH (x_22841, x_22840) -> h_XCH x_22841 x_22840
     2552| XCHD (x_22843, x_22842) -> h_XCHD x_22843 x_22842
    23972553| RET -> h_RET
    23982554| RETI -> h_RETI
    23992555| NOP -> h_NOP
    2400 | JMP x_3775 -> h_JMP x_3775
     2556| JMP x_22844 -> h_JMP x_22844
    24012557
    24022558(** val preinstruction_rect_Type1 :
     
    24362592    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    24372593let rec preinstruction_rect_Type1 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2438 | ADD (x_3816, x_3815) -> h_ADD x_3816 x_3815
    2439 | ADDC (x_3818, x_3817) -> h_ADDC x_3818 x_3817
    2440 | SUBB (x_3820, x_3819) -> h_SUBB x_3820 x_3819
    2441 | INC x_3821 -> h_INC x_3821
    2442 | DEC x_3822 -> h_DEC x_3822
    2443 | MUL (x_3824, x_3823) -> h_MUL x_3824 x_3823
    2444 | DIV (x_3826, x_3825) -> h_DIV x_3826 x_3825
    2445 | DA x_3827 -> h_DA x_3827
    2446 | JC x_3828 -> h_JC x_3828
    2447 | JNC x_3829 -> h_JNC x_3829
    2448 | JB (x_3831, x_3830) -> h_JB x_3831 x_3830
    2449 | JNB (x_3833, x_3832) -> h_JNB x_3833 x_3832
    2450 | JBC (x_3835, x_3834) -> h_JBC x_3835 x_3834
    2451 | JZ x_3836 -> h_JZ x_3836
    2452 | JNZ x_3837 -> h_JNZ x_3837
    2453 | CJNE (x_3839, x_3838) -> h_CJNE x_3839 x_3838
    2454 | DJNZ (x_3841, x_3840) -> h_DJNZ x_3841 x_3840
    2455 | ANL x_3842 -> h_ANL x_3842
    2456 | ORL x_3843 -> h_ORL x_3843
    2457 | XRL x_3844 -> h_XRL x_3844
    2458 | CLR x_3845 -> h_CLR x_3845
    2459 | CPL x_3846 -> h_CPL x_3846
    2460 | RL x_3847 -> h_RL x_3847
    2461 | RLC x_3848 -> h_RLC x_3848
    2462 | RR x_3849 -> h_RR x_3849
    2463 | RRC x_3850 -> h_RRC x_3850
    2464 | SWAP x_3851 -> h_SWAP x_3851
    2465 | MOV x_3852 -> h_MOV x_3852
    2466 | MOVX x_3853 -> h_MOVX x_3853
    2467 | SETB x_3854 -> h_SETB x_3854
    2468 | PUSH x_3855 -> h_PUSH x_3855
    2469 | POP x_3856 -> h_POP x_3856
    2470 | XCH (x_3858, x_3857) -> h_XCH x_3858 x_3857
    2471 | XCHD (x_3860, x_3859) -> h_XCHD x_3860 x_3859
     2594| ADD (x_22885, x_22884) -> h_ADD x_22885 x_22884
     2595| ADDC (x_22887, x_22886) -> h_ADDC x_22887 x_22886
     2596| SUBB (x_22889, x_22888) -> h_SUBB x_22889 x_22888
     2597| INC x_22890 -> h_INC x_22890
     2598| DEC x_22891 -> h_DEC x_22891
     2599| MUL (x_22893, x_22892) -> h_MUL x_22893 x_22892
     2600| DIV (x_22895, x_22894) -> h_DIV x_22895 x_22894
     2601| DA x_22896 -> h_DA x_22896
     2602| JC x_22897 -> h_JC x_22897
     2603| JNC x_22898 -> h_JNC x_22898
     2604| JB (x_22900, x_22899) -> h_JB x_22900 x_22899
     2605| JNB (x_22902, x_22901) -> h_JNB x_22902 x_22901
     2606| JBC (x_22904, x_22903) -> h_JBC x_22904 x_22903
     2607| JZ x_22905 -> h_JZ x_22905
     2608| JNZ x_22906 -> h_JNZ x_22906
     2609| CJNE (x_22908, x_22907) -> h_CJNE x_22908 x_22907
     2610| DJNZ (x_22910, x_22909) -> h_DJNZ x_22910 x_22909
     2611| ANL x_22911 -> h_ANL x_22911
     2612| ORL x_22912 -> h_ORL x_22912
     2613| XRL x_22913 -> h_XRL x_22913
     2614| CLR x_22914 -> h_CLR x_22914
     2615| CPL x_22915 -> h_CPL x_22915
     2616| RL x_22916 -> h_RL x_22916
     2617| RLC x_22917 -> h_RLC x_22917
     2618| RR x_22918 -> h_RR x_22918
     2619| RRC x_22919 -> h_RRC x_22919
     2620| SWAP x_22920 -> h_SWAP x_22920
     2621| MOV x_22921 -> h_MOV x_22921
     2622| MOVX x_22922 -> h_MOVX x_22922
     2623| SETB x_22923 -> h_SETB x_22923
     2624| PUSH x_22924 -> h_PUSH x_22924
     2625| POP x_22925 -> h_POP x_22925
     2626| XCH (x_22927, x_22926) -> h_XCH x_22927 x_22926
     2627| XCHD (x_22929, x_22928) -> h_XCHD x_22929 x_22928
    24722628| RET -> h_RET
    24732629| RETI -> h_RETI
    24742630| NOP -> h_NOP
    2475 | JMP x_3861 -> h_JMP x_3861
     2631| JMP x_22930 -> h_JMP x_22930
    24762632
    24772633(** val preinstruction_rect_Type0 :
     
    25112667    'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **)
    25122668let rec preinstruction_rect_Type0 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function
    2513 | ADD (x_3902, x_3901) -> h_ADD x_3902 x_3901
    2514 | ADDC (x_3904, x_3903) -> h_ADDC x_3904 x_3903
    2515 | SUBB (x_3906, x_3905) -> h_SUBB x_3906 x_3905
    2516 | INC x_3907 -> h_INC x_3907
    2517 | DEC x_3908 -> h_DEC x_3908
    2518 | MUL (x_3910, x_3909) -> h_MUL x_3910 x_3909
    2519 | DIV (x_3912, x_3911) -> h_DIV x_3912 x_3911
    2520 | DA x_3913 -> h_DA x_3913
    2521 | JC x_3914 -> h_JC x_3914
    2522 | JNC x_3915 -> h_JNC x_3915
    2523 | JB (x_3917, x_3916) -> h_JB x_3917 x_3916
    2524 | JNB (x_3919, x_3918) -> h_JNB x_3919 x_3918
    2525 | JBC (x_3921, x_3920) -> h_JBC x_3921 x_3920
    2526 | JZ x_3922 -> h_JZ x_3922
    2527 | JNZ x_3923 -> h_JNZ x_3923
    2528 | CJNE (x_3925, x_3924) -> h_CJNE x_3925 x_3924
    2529 | DJNZ (x_3927, x_3926) -> h_DJNZ x_3927 x_3926
    2530 | ANL x_3928 -> h_ANL x_3928
    2531 | ORL x_3929 -> h_ORL x_3929
    2532 | XRL x_3930 -> h_XRL x_3930
    2533 | CLR x_3931 -> h_CLR x_3931
    2534 | CPL x_3932 -> h_CPL x_3932
    2535 | RL x_3933 -> h_RL x_3933
    2536 | RLC x_3934 -> h_RLC x_3934
    2537 | RR x_3935 -> h_RR x_3935
    2538 | RRC x_3936 -> h_RRC x_3936
    2539 | SWAP x_3937 -> h_SWAP x_3937
    2540 | MOV x_3938 -> h_MOV x_3938
    2541 | MOVX x_3939 -> h_MOVX x_3939
    2542 | SETB x_3940 -> h_SETB x_3940
    2543 | PUSH x_3941 -> h_PUSH x_3941
    2544 | POP x_3942 -> h_POP x_3942
    2545 | XCH (x_3944, x_3943) -> h_XCH x_3944 x_3943
    2546 | XCHD (x_3946, x_3945) -> h_XCHD x_3946 x_3945
     2669| ADD (x_22971, x_22970) -> h_ADD x_22971 x_22970
     2670| ADDC (x_22973, x_22972) -> h_ADDC x_22973 x_22972
     2671| SUBB (x_22975, x_22974) -> h_SUBB x_22975 x_22974
     2672| INC x_22976 -> h_INC x_22976
     2673| DEC x_22977 -> h_DEC x_22977
     2674| MUL (x_22979, x_22978) -> h_MUL x_22979 x_22978
     2675| DIV (x_22981, x_22980) -> h_DIV x_22981 x_22980
     2676| DA x_22982 -> h_DA x_22982
     2677| JC x_22983 -> h_JC x_22983
     2678| JNC x_22984 -> h_JNC x_22984
     2679| JB (x_22986, x_22985) -> h_JB x_22986 x_22985
     2680| JNB (x_22988, x_22987) -> h_JNB x_22988 x_22987
     2681| JBC (x_22990, x_22989) -> h_JBC x_22990 x_22989
     2682| JZ x_22991 -> h_JZ x_22991
     2683| JNZ x_22992 -> h_JNZ x_22992
     2684| CJNE (x_22994, x_22993) -> h_CJNE x_22994 x_22993
     2685| DJNZ (x_22996, x_22995) -> h_DJNZ x_22996 x_22995
     2686| ANL x_22997 -> h_ANL x_22997
     2687| ORL x_22998 -> h_ORL x_22998
     2688| XRL x_22999 -> h_XRL x_22999
     2689| CLR x_23000 -> h_CLR x_23000
     2690| CPL x_23001 -> h_CPL x_23001
     2691| RL x_23002 -> h_RL x_23002
     2692| RLC x_23003 -> h_RLC x_23003
     2693| RR x_23004 -> h_RR x_23004
     2694| RRC x_23005 -> h_RRC x_23005
     2695| SWAP x_23006 -> h_SWAP x_23006
     2696| MOV x_23007 -> h_MOV x_23007
     2697| MOVX x_23008 -> h_MOVX x_23008
     2698| SETB x_23009 -> h_SETB x_23009
     2699| PUSH x_23010 -> h_PUSH x_23010
     2700| POP x_23011 -> h_POP x_23011
     2701| XCH (x_23013, x_23012) -> h_XCH x_23013 x_23012
     2702| XCHD (x_23015, x_23014) -> h_XCHD x_23015 x_23014
    25472703| RET -> h_RET
    25482704| RETI -> h_RETI
    25492705| NOP -> h_NOP
    2550 | JMP x_3947 -> h_JMP x_3947
     2706| JMP x_23016 -> h_JMP x_23016
    25512707
    25522708(** val preinstruction_inv_rect_Type4 :
     
    49525108    'a1 **)
    49535109let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    4954 | ACALL x_4519 -> h_ACALL x_4519
    4955 | LCALL x_4520 -> h_LCALL x_4520
    4956 | AJMP x_4521 -> h_AJMP x_4521
    4957 | LJMP x_4522 -> h_LJMP x_4522
    4958 | SJMP x_4523 -> h_SJMP x_4523
    4959 | MOVC (x_4525, x_4524) -> h_MOVC x_4525 x_4524
    4960 | RealInstruction x_4526 -> h_RealInstruction x_4526
     5110| ACALL x_23588 -> h_ACALL x_23588
     5111| LCALL x_23589 -> h_LCALL x_23589
     5112| AJMP x_23590 -> h_AJMP x_23590
     5113| LJMP x_23591 -> h_LJMP x_23591
     5114| SJMP x_23592 -> h_SJMP x_23592
     5115| MOVC (x_23594, x_23593) -> h_MOVC x_23594 x_23593
     5116| RealInstruction x_23595 -> h_RealInstruction x_23595
    49615117
    49625118(** val instruction_rect_Type5 :
     
    49675123    'a1 **)
    49685124let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    4969 | ACALL x_4535 -> h_ACALL x_4535
    4970 | LCALL x_4536 -> h_LCALL x_4536
    4971 | AJMP x_4537 -> h_AJMP x_4537
    4972 | LJMP x_4538 -> h_LJMP x_4538
    4973 | SJMP x_4539 -> h_SJMP x_4539
    4974 | MOVC (x_4541, x_4540) -> h_MOVC x_4541 x_4540
    4975 | RealInstruction x_4542 -> h_RealInstruction x_4542
     5125| ACALL x_23604 -> h_ACALL x_23604
     5126| LCALL x_23605 -> h_LCALL x_23605
     5127| AJMP x_23606 -> h_AJMP x_23606
     5128| LJMP x_23607 -> h_LJMP x_23607
     5129| SJMP x_23608 -> h_SJMP x_23608
     5130| MOVC (x_23610, x_23609) -> h_MOVC x_23610 x_23609
     5131| RealInstruction x_23611 -> h_RealInstruction x_23611
    49765132
    49775133(** val instruction_rect_Type3 :
     
    49825138    'a1 **)
    49835139let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    4984 | ACALL x_4551 -> h_ACALL x_4551
    4985 | LCALL x_4552 -> h_LCALL x_4552
    4986 | AJMP x_4553 -> h_AJMP x_4553
    4987 | LJMP x_4554 -> h_LJMP x_4554
    4988 | SJMP x_4555 -> h_SJMP x_4555
    4989 | MOVC (x_4557, x_4556) -> h_MOVC x_4557 x_4556
    4990 | RealInstruction x_4558 -> h_RealInstruction x_4558
     5140| ACALL x_23620 -> h_ACALL x_23620
     5141| LCALL x_23621 -> h_LCALL x_23621
     5142| AJMP x_23622 -> h_AJMP x_23622
     5143| LJMP x_23623 -> h_LJMP x_23623
     5144| SJMP x_23624 -> h_SJMP x_23624
     5145| MOVC (x_23626, x_23625) -> h_MOVC x_23626 x_23625
     5146| RealInstruction x_23627 -> h_RealInstruction x_23627
    49915147
    49925148(** val instruction_rect_Type2 :
     
    49975153    'a1 **)
    49985154let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    4999 | ACALL x_4567 -> h_ACALL x_4567
    5000 | LCALL x_4568 -> h_LCALL x_4568
    5001 | AJMP x_4569 -> h_AJMP x_4569
    5002 | LJMP x_4570 -> h_LJMP x_4570
    5003 | SJMP x_4571 -> h_SJMP x_4571
    5004 | MOVC (x_4573, x_4572) -> h_MOVC x_4573 x_4572
    5005 | RealInstruction x_4574 -> h_RealInstruction x_4574
     5155| ACALL x_23636 -> h_ACALL x_23636
     5156| LCALL x_23637 -> h_LCALL x_23637
     5157| AJMP x_23638 -> h_AJMP x_23638
     5158| LJMP x_23639 -> h_LJMP x_23639
     5159| SJMP x_23640 -> h_SJMP x_23640
     5160| MOVC (x_23642, x_23641) -> h_MOVC x_23642 x_23641
     5161| RealInstruction x_23643 -> h_RealInstruction x_23643
    50065162
    50075163(** val instruction_rect_Type1 :
     
    50125168    'a1 **)
    50135169let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5014 | ACALL x_4583 -> h_ACALL x_4583
    5015 | LCALL x_4584 -> h_LCALL x_4584
    5016 | AJMP x_4585 -> h_AJMP x_4585
    5017 | LJMP x_4586 -> h_LJMP x_4586
    5018 | SJMP x_4587 -> h_SJMP x_4587
    5019 | MOVC (x_4589, x_4588) -> h_MOVC x_4589 x_4588
    5020 | RealInstruction x_4590 -> h_RealInstruction x_4590
     5170| ACALL x_23652 -> h_ACALL x_23652
     5171| LCALL x_23653 -> h_LCALL x_23653
     5172| AJMP x_23654 -> h_AJMP x_23654
     5173| LJMP x_23655 -> h_LJMP x_23655
     5174| SJMP x_23656 -> h_SJMP x_23656
     5175| MOVC (x_23658, x_23657) -> h_MOVC x_23658 x_23657
     5176| RealInstruction x_23659 -> h_RealInstruction x_23659
    50215177
    50225178(** val instruction_rect_Type0 :
     
    50275183    'a1 **)
    50285184let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function
    5029 | ACALL x_4599 -> h_ACALL x_4599
    5030 | LCALL x_4600 -> h_LCALL x_4600
    5031 | AJMP x_4601 -> h_AJMP x_4601
    5032 | LJMP x_4602 -> h_LJMP x_4602
    5033 | SJMP x_4603 -> h_SJMP x_4603
    5034 | MOVC (x_4605, x_4604) -> h_MOVC x_4605 x_4604
    5035 | RealInstruction x_4606 -> h_RealInstruction x_4606
     5185| ACALL x_23668 -> h_ACALL x_23668
     5186| LCALL x_23669 -> h_LCALL x_23669
     5187| AJMP x_23670 -> h_AJMP x_23670
     5188| LJMP x_23671 -> h_LJMP x_23671
     5189| SJMP x_23672 -> h_SJMP x_23672
     5190| MOVC (x_23674, x_23673) -> h_MOVC x_23674 x_23673
     5191| RealInstruction x_23675 -> h_RealInstruction x_23675
    50365192
    50375193(** val instruction_inv_rect_Type4 :
     
    51035259     | MOVC (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
    51045260     | RealInstruction a0 -> Obj.magic (fun _ dH -> dH __)) y
     5261
     5262(** val dpi1__o__RealInstruction__o__inject :
     5263    (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction
     5264    Types.sig0 **)
     5265let dpi1__o__RealInstruction__o__inject x2 =
     5266  RealInstruction x2.Types.dpi1
     5267
     5268(** val eject__o__RealInstruction__o__inject :
     5269    subaddressing_mode preinstruction Types.sig0 -> instruction Types.sig0 **)
     5270let eject__o__RealInstruction__o__inject x2 =
     5271  RealInstruction (Types.pi1 x2)
     5272
     5273(** val realInstruction__o__inject :
     5274    subaddressing_mode preinstruction -> instruction Types.sig0 **)
     5275let realInstruction__o__inject x1 =
     5276  RealInstruction x1
     5277
     5278(** val dpi1__o__RealInstruction :
     5279    (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction **)
     5280let dpi1__o__RealInstruction x1 =
     5281  RealInstruction x1.Types.dpi1
     5282
     5283(** val eject__o__RealInstruction :
     5284    subaddressing_mode preinstruction Types.sig0 -> instruction **)
     5285let eject__o__RealInstruction x1 =
     5286  RealInstruction (Types.pi1 x1)
    51055287
    51065288(** val eq_instruction : instruction -> instruction -> Bool.bool **)
     
    52985480    pseudo_instruction -> 'a1 **)
    52995481let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5300 | Instruction x_4772 -> h_Instruction x_4772
    5301 | Comment x_4773 -> h_Comment x_4773
    5302 | Cost x_4774 -> h_Cost x_4774
    5303 | Jmp x_4775 -> h_Jmp x_4775
    5304 | Jnz (x_4778, x_4777, x_4776) -> h_Jnz x_4778 x_4777 x_4776
    5305 | MovSuccessor (x_4781, x_4780, x_4779) ->
    5306   h_MovSuccessor x_4781 x_4780 x_4779
    5307 | Call x_4782 -> h_Call x_4782
    5308 | Mov (x_4784, x_4783) -> h_Mov x_4784 x_4783
     5482| Instruction x_23841 -> h_Instruction x_23841
     5483| Comment x_23842 -> h_Comment x_23842
     5484| Cost x_23843 -> h_Cost x_23843
     5485| Jmp x_23844 -> h_Jmp x_23844
     5486| Jnz (x_23847, x_23846, x_23845) -> h_Jnz x_23847 x_23846 x_23845
     5487| MovSuccessor (x_23850, x_23849, x_23848) ->
     5488  h_MovSuccessor x_23850 x_23849 x_23848
     5489| Call x_23851 -> h_Call x_23851
     5490| Mov (x_23853, x_23852) -> h_Mov x_23853 x_23852
    53095491
    53105492(** val pseudo_instruction_rect_Type5 :
     
    53165498    pseudo_instruction -> 'a1 **)
    53175499let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5318 | Instruction x_4794 -> h_Instruction x_4794
    5319 | Comment x_4795 -> h_Comment x_4795
    5320 | Cost x_4796 -> h_Cost x_4796
    5321 | Jmp x_4797 -> h_Jmp x_4797
    5322 | Jnz (x_4800, x_4799, x_4798) -> h_Jnz x_4800 x_4799 x_4798
    5323 | MovSuccessor (x_4803, x_4802, x_4801) ->
    5324   h_MovSuccessor x_4803 x_4802 x_4801
    5325 | Call x_4804 -> h_Call x_4804
    5326 | Mov (x_4806, x_4805) -> h_Mov x_4806 x_4805
     5500| Instruction x_23863 -> h_Instruction x_23863
     5501| Comment x_23864 -> h_Comment x_23864
     5502| Cost x_23865 -> h_Cost x_23865
     5503| Jmp x_23866 -> h_Jmp x_23866
     5504| Jnz (x_23869, x_23868, x_23867) -> h_Jnz x_23869 x_23868 x_23867
     5505| MovSuccessor (x_23872, x_23871, x_23870) ->
     5506  h_MovSuccessor x_23872 x_23871 x_23870
     5507| Call x_23873 -> h_Call x_23873
     5508| Mov (x_23875, x_23874) -> h_Mov x_23875 x_23874
    53275509
    53285510(** val pseudo_instruction_rect_Type3 :
     
    53345516    pseudo_instruction -> 'a1 **)
    53355517let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5336 | Instruction x_4816 -> h_Instruction x_4816
    5337 | Comment x_4817 -> h_Comment x_4817
    5338 | Cost x_4818 -> h_Cost x_4818
    5339 | Jmp x_4819 -> h_Jmp x_4819
    5340 | Jnz (x_4822, x_4821, x_4820) -> h_Jnz x_4822 x_4821 x_4820
    5341 | MovSuccessor (x_4825, x_4824, x_4823) ->
    5342   h_MovSuccessor x_4825 x_4824 x_4823
    5343 | Call x_4826 -> h_Call x_4826
    5344 | Mov (x_4828, x_4827) -> h_Mov x_4828 x_4827
     5518| Instruction x_23885 -> h_Instruction x_23885
     5519| Comment x_23886 -> h_Comment x_23886
     5520| Cost x_23887 -> h_Cost x_23887
     5521| Jmp x_23888 -> h_Jmp x_23888
     5522| Jnz (x_23891, x_23890, x_23889) -> h_Jnz x_23891 x_23890 x_23889
     5523| MovSuccessor (x_23894, x_23893, x_23892) ->
     5524  h_MovSuccessor x_23894 x_23893 x_23892
     5525| Call x_23895 -> h_Call x_23895
     5526| Mov (x_23897, x_23896) -> h_Mov x_23897 x_23896
    53455527
    53465528(** val pseudo_instruction_rect_Type2 :
     
    53525534    pseudo_instruction -> 'a1 **)
    53535535let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5354 | Instruction x_4838 -> h_Instruction x_4838
    5355 | Comment x_4839 -> h_Comment x_4839
    5356 | Cost x_4840 -> h_Cost x_4840
    5357 | Jmp x_4841 -> h_Jmp x_4841
    5358 | Jnz (x_4844, x_4843, x_4842) -> h_Jnz x_4844 x_4843 x_4842
    5359 | MovSuccessor (x_4847, x_4846, x_4845) ->
    5360   h_MovSuccessor x_4847 x_4846 x_4845
    5361 | Call x_4848 -> h_Call x_4848
    5362 | Mov (x_4850, x_4849) -> h_Mov x_4850 x_4849
     5536| Instruction x_23907 -> h_Instruction x_23907
     5537| Comment x_23908 -> h_Comment x_23908
     5538| Cost x_23909 -> h_Cost x_23909
     5539| Jmp x_23910 -> h_Jmp x_23910
     5540| Jnz (x_23913, x_23912, x_23911) -> h_Jnz x_23913 x_23912 x_23911
     5541| MovSuccessor (x_23916, x_23915, x_23914) ->
     5542  h_MovSuccessor x_23916 x_23915 x_23914
     5543| Call x_23917 -> h_Call x_23917
     5544| Mov (x_23919, x_23918) -> h_Mov x_23919 x_23918
    53635545
    53645546(** val pseudo_instruction_rect_Type1 :
     
    53705552    pseudo_instruction -> 'a1 **)
    53715553let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5372 | Instruction x_4860 -> h_Instruction x_4860
    5373 | Comment x_4861 -> h_Comment x_4861
    5374 | Cost x_4862 -> h_Cost x_4862
    5375 | Jmp x_4863 -> h_Jmp x_4863
    5376 | Jnz (x_4866, x_4865, x_4864) -> h_Jnz x_4866 x_4865 x_4864
    5377 | MovSuccessor (x_4869, x_4868, x_4867) ->
    5378   h_MovSuccessor x_4869 x_4868 x_4867
    5379 | Call x_4870 -> h_Call x_4870
    5380 | Mov (x_4872, x_4871) -> h_Mov x_4872 x_4871
     5554| Instruction x_23929 -> h_Instruction x_23929
     5555| Comment x_23930 -> h_Comment x_23930
     5556| Cost x_23931 -> h_Cost x_23931
     5557| Jmp x_23932 -> h_Jmp x_23932
     5558| Jnz (x_23935, x_23934, x_23933) -> h_Jnz x_23935 x_23934 x_23933
     5559| MovSuccessor (x_23938, x_23937, x_23936) ->
     5560  h_MovSuccessor x_23938 x_23937 x_23936
     5561| Call x_23939 -> h_Call x_23939
     5562| Mov (x_23941, x_23940) -> h_Mov x_23941 x_23940
    53815563
    53825564(** val pseudo_instruction_rect_Type0 :
     
    53885570    pseudo_instruction -> 'a1 **)
    53895571let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_MovSuccessor h_Call h_Mov = function
    5390 | Instruction x_4882 -> h_Instruction x_4882
    5391 | Comment x_4883 -> h_Comment x_4883
    5392 | Cost x_4884 -> h_Cost x_4884
    5393 | Jmp x_4885 -> h_Jmp x_4885
    5394 | Jnz (x_4888, x_4887, x_4886) -> h_Jnz x_4888 x_4887 x_4886
    5395 | MovSuccessor (x_4891, x_4890, x_4889) ->
    5396   h_MovSuccessor x_4891 x_4890 x_4889
    5397 | Call x_4892 -> h_Call x_4892
    5398 | Mov (x_4894, x_4893) -> h_Mov x_4894 x_4893
     5572| Instruction x_23951 -> h_Instruction x_23951
     5573| Comment x_23952 -> h_Comment x_23952
     5574| Cost x_23953 -> h_Cost x_23953
     5575| Jmp x_23954 -> h_Jmp x_23954
     5576| Jnz (x_23957, x_23956, x_23955) -> h_Jnz x_23957 x_23956 x_23955
     5577| MovSuccessor (x_23960, x_23959, x_23958) ->
     5578  h_MovSuccessor x_23960 x_23959 x_23958
     5579| Call x_23961 -> h_Call x_23961
     5580| Mov (x_23963, x_23962) -> h_Mov x_23963 x_23962
    53995581
    54005582(** val pseudo_instruction_inv_rect_Type4 :
     
    55645746| Mov (x, x0) -> Bool.False
    55655747
    5566 let subaddressing_modeel__o__mk_subaddressing_mode x = assert false
Note: See TracChangeset for help on using the changeset viewer.