Changeset 2743 for extracted/aSM.ml
 Timestamp:
 Feb 27, 2013, 9:27:58 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/aSM.ml
r2730 r2743 113 113 > 'a1) > addressing_mode > 'a1 **) 114 114 let 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_2 727 > h_DIRECT x_2727116  INDIRECT x_2 728 > h_INDIRECT x_2728117  EXT_INDIRECT x_2 729 > h_EXT_INDIRECT x_2729118  REGISTER x_2 730 > h_REGISTER x_2730115  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 119 119  ACC_A > h_ACC_A 120 120  ACC_B > h_ACC_B 121 121  DPTR > h_DPTR 122  DATA x_2 731 > h_DATA x_2731123  DATA16 x_2 732 > h_DATA16 x_2732122  DATA x_21800 > h_DATA x_21800 123  DATA16 x_21801 > h_DATA16 x_21801 124 124  ACC_DPTR > h_ACC_DPTR 125 125  ACC_PC > h_ACC_PC … … 127 127  INDIRECT_DPTR > h_INDIRECT_DPTR 128 128  CARRY > h_CARRY 129  BIT_ADDR x_2 733 > h_BIT_ADDR x_2733130  N_BIT_ADDR x_2 734 > h_N_BIT_ADDR x_2734131  RELATIVE x_2 735 > h_RELATIVE x_2735132  ADDR11 x_2 736 > h_ADDR11 x_2736133  ADDR16 x_2 737 > h_ADDR16 x_2737129  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 134 134 135 135 (** val addressing_mode_rect_Type5 : … … 141 141 > 'a1) > addressing_mode > 'a1 **) 142 142 let 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_2 758 > h_DIRECT x_2758144  INDIRECT x_2 759 > h_INDIRECT x_2759145  EXT_INDIRECT x_2 760 > h_EXT_INDIRECT x_2760146  REGISTER x_2 761 > h_REGISTER x_2761143  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 147 147  ACC_A > h_ACC_A 148 148  ACC_B > h_ACC_B 149 149  DPTR > h_DPTR 150  DATA x_2 762 > h_DATA x_2762151  DATA16 x_2 763 > h_DATA16 x_2763150  DATA x_21831 > h_DATA x_21831 151  DATA16 x_21832 > h_DATA16 x_21832 152 152  ACC_DPTR > h_ACC_DPTR 153 153  ACC_PC > h_ACC_PC … … 155 155  INDIRECT_DPTR > h_INDIRECT_DPTR 156 156  CARRY > h_CARRY 157  BIT_ADDR x_2 764 > h_BIT_ADDR x_2764158  N_BIT_ADDR x_2 765 > h_N_BIT_ADDR x_2765159  RELATIVE x_2 766 > h_RELATIVE x_2766160  ADDR11 x_2 767 > h_ADDR11 x_2767161  ADDR16 x_2 768 > h_ADDR16 x_2768157  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 162 162 163 163 (** val addressing_mode_rect_Type3 : … … 169 169 > 'a1) > addressing_mode > 'a1 **) 170 170 let 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_2 789 > h_DIRECT x_2789172  INDIRECT x_2 790 > h_INDIRECT x_2790173  EXT_INDIRECT x_2 791 > h_EXT_INDIRECT x_2791174  REGISTER x_2 792 > h_REGISTER x_2792171  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 175 175  ACC_A > h_ACC_A 176 176  ACC_B > h_ACC_B 177 177  DPTR > h_DPTR 178  DATA x_2 793 > h_DATA x_2793179  DATA16 x_2 794 > h_DATA16 x_2794178  DATA x_21862 > h_DATA x_21862 179  DATA16 x_21863 > h_DATA16 x_21863 180 180  ACC_DPTR > h_ACC_DPTR 181 181  ACC_PC > h_ACC_PC … … 183 183  INDIRECT_DPTR > h_INDIRECT_DPTR 184 184  CARRY > h_CARRY 185  BIT_ADDR x_2 795 > h_BIT_ADDR x_2795186  N_BIT_ADDR x_2 796 > h_N_BIT_ADDR x_2796187  RELATIVE x_2 797 > h_RELATIVE x_2797188  ADDR11 x_2 798 > h_ADDR11 x_2798189  ADDR16 x_2 799 > h_ADDR16 x_2799185  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 190 190 191 191 (** val addressing_mode_rect_Type2 : … … 197 197 > 'a1) > addressing_mode > 'a1 **) 198 198 let 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_2 820 > h_DIRECT x_2820200  INDIRECT x_2 821 > h_INDIRECT x_2821201  EXT_INDIRECT x_2 822 > h_EXT_INDIRECT x_2822202  REGISTER x_2 823 > h_REGISTER x_2823199  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 203 203  ACC_A > h_ACC_A 204 204  ACC_B > h_ACC_B 205 205  DPTR > h_DPTR 206  DATA x_2 824 > h_DATA x_2824207  DATA16 x_2 825 > h_DATA16 x_2825206  DATA x_21893 > h_DATA x_21893 207  DATA16 x_21894 > h_DATA16 x_21894 208 208  ACC_DPTR > h_ACC_DPTR 209 209  ACC_PC > h_ACC_PC … … 211 211  INDIRECT_DPTR > h_INDIRECT_DPTR 212 212  CARRY > h_CARRY 213  BIT_ADDR x_2 826 > h_BIT_ADDR x_2826214  N_BIT_ADDR x_2 827 > h_N_BIT_ADDR x_2827215  RELATIVE x_2 828 > h_RELATIVE x_2828216  ADDR11 x_2 829 > h_ADDR11 x_2829217  ADDR16 x_2 830 > h_ADDR16 x_2830213  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 218 218 219 219 (** val addressing_mode_rect_Type1 : … … 225 225 > 'a1) > addressing_mode > 'a1 **) 226 226 let 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_2 851 > h_DIRECT x_2851228  INDIRECT x_2 852 > h_INDIRECT x_2852229  EXT_INDIRECT x_2 853 > h_EXT_INDIRECT x_2853230  REGISTER x_2 854 > h_REGISTER x_2854227  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 231 231  ACC_A > h_ACC_A 232 232  ACC_B > h_ACC_B 233 233  DPTR > h_DPTR 234  DATA x_2 855 > h_DATA x_2855235  DATA16 x_2 856 > h_DATA16 x_2856234  DATA x_21924 > h_DATA x_21924 235  DATA16 x_21925 > h_DATA16 x_21925 236 236  ACC_DPTR > h_ACC_DPTR 237 237  ACC_PC > h_ACC_PC … … 239 239  INDIRECT_DPTR > h_INDIRECT_DPTR 240 240  CARRY > h_CARRY 241  BIT_ADDR x_2 857 > h_BIT_ADDR x_2857242  N_BIT_ADDR x_2 858 > h_N_BIT_ADDR x_2858243  RELATIVE x_2 859 > h_RELATIVE x_2859244  ADDR11 x_2 860 > h_ADDR11 x_2860245  ADDR16 x_2 861 > h_ADDR16 x_2861241  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 246 246 247 247 (** val addressing_mode_rect_Type0 : … … 253 253 > 'a1) > addressing_mode > 'a1 **) 254 254 let 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_2 882 > h_DIRECT x_2882256  INDIRECT x_2 883 > h_INDIRECT x_2883257  EXT_INDIRECT x_2 884 > h_EXT_INDIRECT x_2884258  REGISTER x_2 885 > h_REGISTER x_2885255  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 259 259  ACC_A > h_ACC_A 260 260  ACC_B > h_ACC_B 261 261  DPTR > h_DPTR 262  DATA x_2 886 > h_DATA x_2886263  DATA16 x_2 887 > h_DATA16 x_2887262  DATA x_21955 > h_DATA x_21955 263  DATA16 x_21956 > h_DATA16 x_21956 264 264  ACC_DPTR > h_ACC_DPTR 265 265  ACC_PC > h_ACC_PC … … 267 267  INDIRECT_DPTR > h_INDIRECT_DPTR 268 268  CARRY > h_CARRY 269  BIT_ADDR x_2 888 > h_BIT_ADDR x_2888270  N_BIT_ADDR x_2 889 > h_N_BIT_ADDR x_2889271  RELATIVE x_2 890 > h_RELATIVE x_2890272  ADDR11 x_2 891 > h_ADDR11 x_2891273  ADDR16 x_2 892 > h_ADDR16 x_2892269  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 274 274 275 275 (** val addressing_mode_inv_rect_Type4 : … … 1928 1928 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1929 1929 'a1) > subaddressing_mode > 'a1 **) 1930 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_ 3360=1931 let subaddressing_modeel = x_ 3360in1930 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_22429 = 1931 let subaddressing_modeel = x_22429 in 1932 1932 h_mk_subaddressing_mode subaddressing_modeel __ 1933 1933 … … 1935 1935 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1936 1936 'a1) > subaddressing_mode > 'a1 **) 1937 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_ 3362=1938 let subaddressing_modeel = x_ 3362in1937 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_22431 = 1938 let subaddressing_modeel = x_22431 in 1939 1939 h_mk_subaddressing_mode subaddressing_modeel __ 1940 1940 … … 1942 1942 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1943 1943 'a1) > subaddressing_mode > 'a1 **) 1944 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_ 3364=1945 let subaddressing_modeel = x_ 3364in1944 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_22433 = 1945 let subaddressing_modeel = x_22433 in 1946 1946 h_mk_subaddressing_mode subaddressing_modeel __ 1947 1947 … … 1949 1949 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1950 1950 'a1) > subaddressing_mode > 'a1 **) 1951 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_ 3366=1952 let subaddressing_modeel = x_ 3366in1951 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_22435 = 1952 let subaddressing_modeel = x_22435 in 1953 1953 h_mk_subaddressing_mode subaddressing_modeel __ 1954 1954 … … 1956 1956 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1957 1957 'a1) > subaddressing_mode > 'a1 **) 1958 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_ 3368=1959 let subaddressing_modeel = x_ 3368in1958 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_22437 = 1959 let subaddressing_modeel = x_22437 in 1960 1960 h_mk_subaddressing_mode subaddressing_modeel __ 1961 1961 … … 1963 1963 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1964 1964 'a1) > subaddressing_mode > 'a1 **) 1965 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_ 3370=1966 let subaddressing_modeel = x_ 3370in1965 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_22439 = 1966 let subaddressing_modeel = x_22439 in 1967 1967 h_mk_subaddressing_mode subaddressing_modeel __ 1968 1968 … … 2044 2044 let eject__o__subaddressing_modeel x0 x1 x3 = 2045 2045 subaddressing_modeel x0 x1 (Types.pi1 x3) 2046 2047 type 'x1 dpi1__o__subaddressing_mode = subaddressing_mode 2048 2049 type 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 **) 2055 let 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 **) 2062 let 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 **) 2070 let 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 **) 2077 let 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 **) 2084 let 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 **) 2092 let 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 **) 2099 let 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 **) 2106 let 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 **) 2113 let 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 **) 2119 let 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 **) 2125 let 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 **) 2131 let 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 **) 2137 let 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 **) 2143 let 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 **) 2149 let 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 **) 2155 let 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 **) 2161 let 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 **) 2167 let 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 **) 2174 let 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 **) 2181 let 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 **) 2188 let 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 **) 2194 let 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 **) 2200 let eject__o__mk_subaddressing_mode x1 x2 x3 = 2201 Types.pi1 x2 2046 2202 2047 2203 type subaddressing_mode_elim_type = __ … … 2136 2292 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2137 2293 let 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_34712139  ADDC (x_ 3474, x_3473) > h_ADDC x_3474 x_34732140  SUBB (x_ 3476, x_3475) > h_SUBB x_3476 x_34752141  INC x_ 3477 > h_INC x_34772142  DEC x_ 3478 > h_DEC x_34782143  MUL (x_ 3480, x_3479) > h_MUL x_3480 x_34792144  DIV (x_ 3482, x_3481) > h_DIV x_3482 x_34812145  DA x_ 3483 > h_DA x_34832146  JC x_ 3484 > h_JC x_34842147  JNC x_ 3485 > h_JNC x_34852148  JB (x_ 3487, x_3486) > h_JB x_3487 x_34862149  JNB (x_ 3489, x_3488) > h_JNB x_3489 x_34882150  JBC (x_ 3491, x_3490) > h_JBC x_3491 x_34902151  JZ x_ 3492 > h_JZ x_34922152  JNZ x_ 3493 > h_JNZ x_34932153  CJNE (x_ 3495, x_3494) > h_CJNE x_3495 x_34942154  DJNZ (x_ 3497, x_3496) > h_DJNZ x_3497 x_34962155  ANL x_ 3498 > h_ANL x_34982156  ORL x_ 3499 > h_ORL x_34992157  XRL x_ 3500 > h_XRL x_35002158  CLR x_ 3501 > h_CLR x_35012159  CPL x_ 3502 > h_CPL x_35022160  RL x_ 3503 > h_RL x_35032161  RLC x_ 3504 > h_RLC x_35042162  RR x_ 3505 > h_RR x_35052163  RRC x_ 3506 > h_RRC x_35062164  SWAP x_ 3507 > h_SWAP x_35072165  MOV x_ 3508 > h_MOV x_35082166  MOVX x_ 3509 > h_MOVX x_35092167  SETB x_ 3510 > h_SETB x_35102168  PUSH x_ 3511 > h_PUSH x_35112169  POP x_ 3512 > h_POP x_35122170  XCH (x_ 3514, x_3513) > h_XCH x_3514 x_35132171  XCHD (x_ 3516, x_3515) > h_XCHD x_3516 x_35152294  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 2172 2328  RET > h_RET 2173 2329  RETI > h_RETI 2174 2330  NOP > h_NOP 2175  JMP x_ 3517 > h_JMP x_35172331  JMP x_22586 > h_JMP x_22586 2176 2332 2177 2333 (** val preinstruction_rect_Type5 : … … 2211 2367 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2212 2368 let 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_35572214  ADDC (x_ 3560, x_3559) > h_ADDC x_3560 x_35592215  SUBB (x_ 3562, x_3561) > h_SUBB x_3562 x_35612216  INC x_ 3563 > h_INC x_35632217  DEC x_ 3564 > h_DEC x_35642218  MUL (x_ 3566, x_3565) > h_MUL x_3566 x_35652219  DIV (x_ 3568, x_3567) > h_DIV x_3568 x_35672220  DA x_ 3569 > h_DA x_35692221  JC x_ 3570 > h_JC x_35702222  JNC x_ 3571 > h_JNC x_35712223  JB (x_ 3573, x_3572) > h_JB x_3573 x_35722224  JNB (x_ 3575, x_3574) > h_JNB x_3575 x_35742225  JBC (x_ 3577, x_3576) > h_JBC x_3577 x_35762226  JZ x_ 3578 > h_JZ x_35782227  JNZ x_ 3579 > h_JNZ x_35792228  CJNE (x_ 3581, x_3580) > h_CJNE x_3581 x_35802229  DJNZ (x_ 3583, x_3582) > h_DJNZ x_3583 x_35822230  ANL x_ 3584 > h_ANL x_35842231  ORL x_ 3585 > h_ORL x_35852232  XRL x_ 3586 > h_XRL x_35862233  CLR x_ 3587 > h_CLR x_35872234  CPL x_ 3588 > h_CPL x_35882235  RL x_ 3589 > h_RL x_35892236  RLC x_ 3590 > h_RLC x_35902237  RR x_ 3591 > h_RR x_35912238  RRC x_ 3592 > h_RRC x_35922239  SWAP x_ 3593 > h_SWAP x_35932240  MOV x_ 3594 > h_MOV x_35942241  MOVX x_ 3595 > h_MOVX x_35952242  SETB x_ 3596 > h_SETB x_35962243  PUSH x_ 3597 > h_PUSH x_35972244  POP x_ 3598 > h_POP x_35982245  XCH (x_ 3600, x_3599) > h_XCH x_3600 x_35992246  XCHD (x_ 3602, x_3601) > h_XCHD x_3602 x_36012369  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 2247 2403  RET > h_RET 2248 2404  RETI > h_RETI 2249 2405  NOP > h_NOP 2250  JMP x_ 3603 > h_JMP x_36032406  JMP x_22672 > h_JMP x_22672 2251 2407 2252 2408 (** val preinstruction_rect_Type3 : … … 2286 2442 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2287 2443 let 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_36432289  ADDC (x_ 3646, x_3645) > h_ADDC x_3646 x_36452290  SUBB (x_ 3648, x_3647) > h_SUBB x_3648 x_36472291  INC x_ 3649 > h_INC x_36492292  DEC x_ 3650 > h_DEC x_36502293  MUL (x_ 3652, x_3651) > h_MUL x_3652 x_36512294  DIV (x_ 3654, x_3653) > h_DIV x_3654 x_36532295  DA x_ 3655 > h_DA x_36552296  JC x_ 3656 > h_JC x_36562297  JNC x_ 3657 > h_JNC x_36572298  JB (x_ 3659, x_3658) > h_JB x_3659 x_36582299  JNB (x_ 3661, x_3660) > h_JNB x_3661 x_36602300  JBC (x_ 3663, x_3662) > h_JBC x_3663 x_36622301  JZ x_ 3664 > h_JZ x_36642302  JNZ x_ 3665 > h_JNZ x_36652303  CJNE (x_ 3667, x_3666) > h_CJNE x_3667 x_36662304  DJNZ (x_ 3669, x_3668) > h_DJNZ x_3669 x_36682305  ANL x_ 3670 > h_ANL x_36702306  ORL x_ 3671 > h_ORL x_36712307  XRL x_ 3672 > h_XRL x_36722308  CLR x_ 3673 > h_CLR x_36732309  CPL x_ 3674 > h_CPL x_36742310  RL x_ 3675 > h_RL x_36752311  RLC x_ 3676 > h_RLC x_36762312  RR x_ 3677 > h_RR x_36772313  RRC x_ 3678 > h_RRC x_36782314  SWAP x_ 3679 > h_SWAP x_36792315  MOV x_ 3680 > h_MOV x_36802316  MOVX x_ 3681 > h_MOVX x_36812317  SETB x_ 3682 > h_SETB x_36822318  PUSH x_ 3683 > h_PUSH x_36832319  POP x_ 3684 > h_POP x_36842320  XCH (x_ 3686, x_3685) > h_XCH x_3686 x_36852321  XCHD (x_ 3688, x_3687) > h_XCHD x_3688 x_36872444  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 2322 2478  RET > h_RET 2323 2479  RETI > h_RETI 2324 2480  NOP > h_NOP 2325  JMP x_ 3689 > h_JMP x_36892481  JMP x_22758 > h_JMP x_22758 2326 2482 2327 2483 (** val preinstruction_rect_Type2 : … … 2361 2517 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2362 2518 let 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_37292364  ADDC (x_ 3732, x_3731) > h_ADDC x_3732 x_37312365  SUBB (x_ 3734, x_3733) > h_SUBB x_3734 x_37332366  INC x_ 3735 > h_INC x_37352367  DEC x_ 3736 > h_DEC x_37362368  MUL (x_ 3738, x_3737) > h_MUL x_3738 x_37372369  DIV (x_ 3740, x_3739) > h_DIV x_3740 x_37392370  DA x_ 3741 > h_DA x_37412371  JC x_ 3742 > h_JC x_37422372  JNC x_ 3743 > h_JNC x_37432373  JB (x_ 3745, x_3744) > h_JB x_3745 x_37442374  JNB (x_ 3747, x_3746) > h_JNB x_3747 x_37462375  JBC (x_ 3749, x_3748) > h_JBC x_3749 x_37482376  JZ x_ 3750 > h_JZ x_37502377  JNZ x_ 3751 > h_JNZ x_37512378  CJNE (x_ 3753, x_3752) > h_CJNE x_3753 x_37522379  DJNZ (x_ 3755, x_3754) > h_DJNZ x_3755 x_37542380  ANL x_ 3756 > h_ANL x_37562381  ORL x_ 3757 > h_ORL x_37572382  XRL x_ 3758 > h_XRL x_37582383  CLR x_ 3759 > h_CLR x_37592384  CPL x_ 3760 > h_CPL x_37602385  RL x_ 3761 > h_RL x_37612386  RLC x_ 3762 > h_RLC x_37622387  RR x_ 3763 > h_RR x_37632388  RRC x_ 3764 > h_RRC x_37642389  SWAP x_ 3765 > h_SWAP x_37652390  MOV x_ 3766 > h_MOV x_37662391  MOVX x_ 3767 > h_MOVX x_37672392  SETB x_ 3768 > h_SETB x_37682393  PUSH x_ 3769 > h_PUSH x_37692394  POP x_ 3770 > h_POP x_37702395  XCH (x_ 3772, x_3771) > h_XCH x_3772 x_37712396  XCHD (x_ 3774, x_3773) > h_XCHD x_3774 x_37732519  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 2397 2553  RET > h_RET 2398 2554  RETI > h_RETI 2399 2555  NOP > h_NOP 2400  JMP x_ 3775 > h_JMP x_37752556  JMP x_22844 > h_JMP x_22844 2401 2557 2402 2558 (** val preinstruction_rect_Type1 : … … 2436 2592 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2437 2593 let 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_38152439  ADDC (x_ 3818, x_3817) > h_ADDC x_3818 x_38172440  SUBB (x_ 3820, x_3819) > h_SUBB x_3820 x_38192441  INC x_ 3821 > h_INC x_38212442  DEC x_ 3822 > h_DEC x_38222443  MUL (x_ 3824, x_3823) > h_MUL x_3824 x_38232444  DIV (x_ 3826, x_3825) > h_DIV x_3826 x_38252445  DA x_ 3827 > h_DA x_38272446  JC x_ 3828 > h_JC x_38282447  JNC x_ 3829 > h_JNC x_38292448  JB (x_ 3831, x_3830) > h_JB x_3831 x_38302449  JNB (x_ 3833, x_3832) > h_JNB x_3833 x_38322450  JBC (x_ 3835, x_3834) > h_JBC x_3835 x_38342451  JZ x_ 3836 > h_JZ x_38362452  JNZ x_ 3837 > h_JNZ x_38372453  CJNE (x_ 3839, x_3838) > h_CJNE x_3839 x_38382454  DJNZ (x_ 3841, x_3840) > h_DJNZ x_3841 x_38402455  ANL x_ 3842 > h_ANL x_38422456  ORL x_ 3843 > h_ORL x_38432457  XRL x_ 3844 > h_XRL x_38442458  CLR x_ 3845 > h_CLR x_38452459  CPL x_ 3846 > h_CPL x_38462460  RL x_ 3847 > h_RL x_38472461  RLC x_ 3848 > h_RLC x_38482462  RR x_ 3849 > h_RR x_38492463  RRC x_ 3850 > h_RRC x_38502464  SWAP x_ 3851 > h_SWAP x_38512465  MOV x_ 3852 > h_MOV x_38522466  MOVX x_ 3853 > h_MOVX x_38532467  SETB x_ 3854 > h_SETB x_38542468  PUSH x_ 3855 > h_PUSH x_38552469  POP x_ 3856 > h_POP x_38562470  XCH (x_ 3858, x_3857) > h_XCH x_3858 x_38572471  XCHD (x_ 3860, x_3859) > h_XCHD x_3860 x_38592594  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 2472 2628  RET > h_RET 2473 2629  RETI > h_RETI 2474 2630  NOP > h_NOP 2475  JMP x_ 3861 > h_JMP x_38612631  JMP x_22930 > h_JMP x_22930 2476 2632 2477 2633 (** val preinstruction_rect_Type0 : … … 2511 2667 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2512 2668 let 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_39012514  ADDC (x_ 3904, x_3903) > h_ADDC x_3904 x_39032515  SUBB (x_ 3906, x_3905) > h_SUBB x_3906 x_39052516  INC x_ 3907 > h_INC x_39072517  DEC x_ 3908 > h_DEC x_39082518  MUL (x_ 3910, x_3909) > h_MUL x_3910 x_39092519  DIV (x_ 3912, x_3911) > h_DIV x_3912 x_39112520  DA x_ 3913 > h_DA x_39132521  JC x_ 3914 > h_JC x_39142522  JNC x_ 3915 > h_JNC x_39152523  JB (x_ 3917, x_3916) > h_JB x_3917 x_39162524  JNB (x_ 3919, x_3918) > h_JNB x_3919 x_39182525  JBC (x_ 3921, x_3920) > h_JBC x_3921 x_39202526  JZ x_ 3922 > h_JZ x_39222527  JNZ x_ 3923 > h_JNZ x_39232528  CJNE (x_ 3925, x_3924) > h_CJNE x_3925 x_39242529  DJNZ (x_ 3927, x_3926) > h_DJNZ x_3927 x_39262530  ANL x_ 3928 > h_ANL x_39282531  ORL x_ 3929 > h_ORL x_39292532  XRL x_ 3930 > h_XRL x_39302533  CLR x_ 3931 > h_CLR x_39312534  CPL x_ 3932 > h_CPL x_39322535  RL x_ 3933 > h_RL x_39332536  RLC x_ 3934 > h_RLC x_39342537  RR x_ 3935 > h_RR x_39352538  RRC x_ 3936 > h_RRC x_39362539  SWAP x_ 3937 > h_SWAP x_39372540  MOV x_ 3938 > h_MOV x_39382541  MOVX x_ 3939 > h_MOVX x_39392542  SETB x_ 3940 > h_SETB x_39402543  PUSH x_ 3941 > h_PUSH x_39412544  POP x_ 3942 > h_POP x_39422545  XCH (x_ 3944, x_3943) > h_XCH x_3944 x_39432546  XCHD (x_ 3946, x_3945) > h_XCHD x_3946 x_39452669  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 2547 2703  RET > h_RET 2548 2704  RETI > h_RETI 2549 2705  NOP > h_NOP 2550  JMP x_ 3947 > h_JMP x_39472706  JMP x_23016 > h_JMP x_23016 2551 2707 2552 2708 (** val preinstruction_inv_rect_Type4 : … … 4952 5108 'a1 **) 4953 5109 let 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_45194955  LCALL x_ 4520 > h_LCALL x_45204956  AJMP x_ 4521 > h_AJMP x_45214957  LJMP x_ 4522 > h_LJMP x_45224958  SJMP x_ 4523 > h_SJMP x_45234959  MOVC (x_ 4525, x_4524) > h_MOVC x_4525 x_45244960  RealInstruction x_ 4526 > h_RealInstruction x_45265110  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 4961 5117 4962 5118 (** val instruction_rect_Type5 : … … 4967 5123 'a1 **) 4968 5124 let 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_45354970  LCALL x_ 4536 > h_LCALL x_45364971  AJMP x_ 4537 > h_AJMP x_45374972  LJMP x_ 4538 > h_LJMP x_45384973  SJMP x_ 4539 > h_SJMP x_45394974  MOVC (x_ 4541, x_4540) > h_MOVC x_4541 x_45404975  RealInstruction x_ 4542 > h_RealInstruction x_45425125  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 4976 5132 4977 5133 (** val instruction_rect_Type3 : … … 4982 5138 'a1 **) 4983 5139 let 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_45514985  LCALL x_ 4552 > h_LCALL x_45524986  AJMP x_ 4553 > h_AJMP x_45534987  LJMP x_ 4554 > h_LJMP x_45544988  SJMP x_ 4555 > h_SJMP x_45554989  MOVC (x_ 4557, x_4556) > h_MOVC x_4557 x_45564990  RealInstruction x_ 4558 > h_RealInstruction x_45585140  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 4991 5147 4992 5148 (** val instruction_rect_Type2 : … … 4997 5153 'a1 **) 4998 5154 let 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_45675000  LCALL x_ 4568 > h_LCALL x_45685001  AJMP x_ 4569 > h_AJMP x_45695002  LJMP x_ 4570 > h_LJMP x_45705003  SJMP x_ 4571 > h_SJMP x_45715004  MOVC (x_ 4573, x_4572) > h_MOVC x_4573 x_45725005  RealInstruction x_ 4574 > h_RealInstruction x_45745155  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 5006 5162 5007 5163 (** val instruction_rect_Type1 : … … 5012 5168 'a1 **) 5013 5169 let 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_45835015  LCALL x_ 4584 > h_LCALL x_45845016  AJMP x_ 4585 > h_AJMP x_45855017  LJMP x_ 4586 > h_LJMP x_45865018  SJMP x_ 4587 > h_SJMP x_45875019  MOVC (x_ 4589, x_4588) > h_MOVC x_4589 x_45885020  RealInstruction x_ 4590 > h_RealInstruction x_45905170  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 5021 5177 5022 5178 (** val instruction_rect_Type0 : … … 5027 5183 'a1 **) 5028 5184 let 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_45995030  LCALL x_ 4600 > h_LCALL x_46005031  AJMP x_ 4601 > h_AJMP x_46015032  LJMP x_ 4602 > h_LJMP x_46025033  SJMP x_ 4603 > h_SJMP x_46035034  MOVC (x_ 4605, x_4604) > h_MOVC x_4605 x_46045035  RealInstruction x_ 4606 > h_RealInstruction x_46065185  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 5036 5192 5037 5193 (** val instruction_inv_rect_Type4 : … … 5103 5259  MOVC (a0, a1) > Obj.magic (fun _ dH > dH __ __) 5104 5260  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 **) 5265 let 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 **) 5270 let eject__o__RealInstruction__o__inject x2 = 5271 RealInstruction (Types.pi1 x2) 5272 5273 (** val realInstruction__o__inject : 5274 subaddressing_mode preinstruction > instruction Types.sig0 **) 5275 let realInstruction__o__inject x1 = 5276 RealInstruction x1 5277 5278 (** val dpi1__o__RealInstruction : 5279 (subaddressing_mode preinstruction, 'a1) Types.dPair > instruction **) 5280 let dpi1__o__RealInstruction x1 = 5281 RealInstruction x1.Types.dpi1 5282 5283 (** val eject__o__RealInstruction : 5284 subaddressing_mode preinstruction Types.sig0 > instruction **) 5285 let eject__o__RealInstruction x1 = 5286 RealInstruction (Types.pi1 x1) 5105 5287 5106 5288 (** val eq_instruction : instruction > instruction > Bool.bool **) … … 5298 5480 pseudo_instruction > 'a1 **) 5299 5481 let 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_47725301  Comment x_ 4773 > h_Comment x_47735302  Cost x_ 4774 > h_Cost x_47745303  Jmp x_ 4775 > h_Jmp x_47755304  Jnz (x_ 4778, x_4777, x_4776) > h_Jnz x_4778 x_4777 x_47765305  MovSuccessor (x_ 4781, x_4780, x_4779) >5306 h_MovSuccessor x_ 4781 x_4780 x_47795307  Call x_ 4782 > h_Call x_47825308  Mov (x_ 4784, x_4783) > h_Mov x_4784 x_47835482  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 5309 5491 5310 5492 (** val pseudo_instruction_rect_Type5 : … … 5316 5498 pseudo_instruction > 'a1 **) 5317 5499 let 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_47945319  Comment x_ 4795 > h_Comment x_47955320  Cost x_ 4796 > h_Cost x_47965321  Jmp x_ 4797 > h_Jmp x_47975322  Jnz (x_ 4800, x_4799, x_4798) > h_Jnz x_4800 x_4799 x_47985323  MovSuccessor (x_ 4803, x_4802, x_4801) >5324 h_MovSuccessor x_ 4803 x_4802 x_48015325  Call x_ 4804 > h_Call x_48045326  Mov (x_ 4806, x_4805) > h_Mov x_4806 x_48055500  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 5327 5509 5328 5510 (** val pseudo_instruction_rect_Type3 : … … 5334 5516 pseudo_instruction > 'a1 **) 5335 5517 let 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_48165337  Comment x_ 4817 > h_Comment x_48175338  Cost x_ 4818 > h_Cost x_48185339  Jmp x_ 4819 > h_Jmp x_48195340  Jnz (x_ 4822, x_4821, x_4820) > h_Jnz x_4822 x_4821 x_48205341  MovSuccessor (x_ 4825, x_4824, x_4823) >5342 h_MovSuccessor x_ 4825 x_4824 x_48235343  Call x_ 4826 > h_Call x_48265344  Mov (x_ 4828, x_4827) > h_Mov x_4828 x_48275518  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 5345 5527 5346 5528 (** val pseudo_instruction_rect_Type2 : … … 5352 5534 pseudo_instruction > 'a1 **) 5353 5535 let 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_48385355  Comment x_ 4839 > h_Comment x_48395356  Cost x_ 4840 > h_Cost x_48405357  Jmp x_ 4841 > h_Jmp x_48415358  Jnz (x_ 4844, x_4843, x_4842) > h_Jnz x_4844 x_4843 x_48425359  MovSuccessor (x_ 4847, x_4846, x_4845) >5360 h_MovSuccessor x_ 4847 x_4846 x_48455361  Call x_ 4848 > h_Call x_48485362  Mov (x_ 4850, x_4849) > h_Mov x_4850 x_48495536  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 5363 5545 5364 5546 (** val pseudo_instruction_rect_Type1 : … … 5370 5552 pseudo_instruction > 'a1 **) 5371 5553 let 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_48605373  Comment x_ 4861 > h_Comment x_48615374  Cost x_ 4862 > h_Cost x_48625375  Jmp x_ 4863 > h_Jmp x_48635376  Jnz (x_ 4866, x_4865, x_4864) > h_Jnz x_4866 x_4865 x_48645377  MovSuccessor (x_ 4869, x_4868, x_4867) >5378 h_MovSuccessor x_ 4869 x_4868 x_48675379  Call x_ 4870 > h_Call x_48705380  Mov (x_ 4872, x_4871) > h_Mov x_4872 x_48715554  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 5381 5563 5382 5564 (** val pseudo_instruction_rect_Type0 : … … 5388 5570 pseudo_instruction > 'a1 **) 5389 5571 let 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_48825391  Comment x_ 4883 > h_Comment x_48835392  Cost x_ 4884 > h_Cost x_48845393  Jmp x_ 4885 > h_Jmp x_48855394  Jnz (x_ 4888, x_4887, x_4886) > h_Jnz x_4888 x_4887 x_48865395  MovSuccessor (x_ 4891, x_4890, x_4889) >5396 h_MovSuccessor x_ 4891 x_4890 x_48895397  Call x_ 4892 > h_Call x_48925398  Mov (x_ 4894, x_4893) > h_Mov x_4894 x_48935572  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 5399 5581 5400 5582 (** val pseudo_instruction_inv_rect_Type4 : … … 5564 5746  Mov (x, x0) > Bool.False 5565 5747 5566 let subaddressing_modeel__o__mk_subaddressing_mode x = assert false
Note: See TracChangeset
for help on using the changeset viewer.