Changeset 3104
 Timestamp:
 Apr 6, 2013, 6:37:17 PM (5 years ago)
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

driver/extracted/aSM.ml
r3059 r3104 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_ 19160 > h_DIRECT x_19160116  INDIRECT x_ 19161 > h_INDIRECT x_19161117  EXT_INDIRECT x_ 19162 > h_EXT_INDIRECT x_19162118  REGISTER x_ 19163 > h_REGISTER x_19163115  DIRECT x_33 > h_DIRECT x_33 116  INDIRECT x_34 > h_INDIRECT x_34 117  EXT_INDIRECT x_35 > h_EXT_INDIRECT x_35 118  REGISTER x_36 > h_REGISTER x_36 119 119  ACC_A > h_ACC_A 120 120  ACC_B > h_ACC_B 121 121  DPTR > h_DPTR 122  DATA x_ 19164 > h_DATA x_19164123  DATA16 x_ 19165 > h_DATA16 x_19165122  DATA x_37 > h_DATA x_37 123  DATA16 x_38 > h_DATA16 x_38 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_ 19166 > h_BIT_ADDR x_19166130  N_BIT_ADDR x_ 19167 > h_N_BIT_ADDR x_19167131  RELATIVE x_ 19168 > h_RELATIVE x_19168132  ADDR11 x_ 19169 > h_ADDR11 x_19169133  ADDR16 x_ 19170 > h_ADDR16 x_19170129  BIT_ADDR x_39 > h_BIT_ADDR x_39 130  N_BIT_ADDR x_40 > h_N_BIT_ADDR x_40 131  RELATIVE x_41 > h_RELATIVE x_41 132  ADDR11 x_42 > h_ADDR11 x_42 133  ADDR16 x_43 > h_ADDR16 x_43 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_ 19191 > h_DIRECT x_19191144  INDIRECT x_ 19192 > h_INDIRECT x_19192145  EXT_INDIRECT x_ 19193 > h_EXT_INDIRECT x_19193146  REGISTER x_ 19194 > h_REGISTER x_19194143  DIRECT x_64 > h_DIRECT x_64 144  INDIRECT x_65 > h_INDIRECT x_65 145  EXT_INDIRECT x_66 > h_EXT_INDIRECT x_66 146  REGISTER x_67 > h_REGISTER x_67 147 147  ACC_A > h_ACC_A 148 148  ACC_B > h_ACC_B 149 149  DPTR > h_DPTR 150  DATA x_ 19195 > h_DATA x_19195151  DATA16 x_ 19196 > h_DATA16 x_19196150  DATA x_68 > h_DATA x_68 151  DATA16 x_69 > h_DATA16 x_69 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_ 19197 > h_BIT_ADDR x_19197158  N_BIT_ADDR x_ 19198 > h_N_BIT_ADDR x_19198159  RELATIVE x_ 19199 > h_RELATIVE x_19199160  ADDR11 x_ 19200 > h_ADDR11 x_19200161  ADDR16 x_ 19201 > h_ADDR16 x_19201157  BIT_ADDR x_70 > h_BIT_ADDR x_70 158  N_BIT_ADDR x_71 > h_N_BIT_ADDR x_71 159  RELATIVE x_72 > h_RELATIVE x_72 160  ADDR11 x_73 > h_ADDR11 x_73 161  ADDR16 x_74 > h_ADDR16 x_74 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_ 19222 > h_DIRECT x_19222172  INDIRECT x_ 19223 > h_INDIRECT x_19223173  EXT_INDIRECT x_ 19224 > h_EXT_INDIRECT x_19224174  REGISTER x_ 19225 > h_REGISTER x_19225171  DIRECT x_95 > h_DIRECT x_95 172  INDIRECT x_96 > h_INDIRECT x_96 173  EXT_INDIRECT x_97 > h_EXT_INDIRECT x_97 174  REGISTER x_98 > h_REGISTER x_98 175 175  ACC_A > h_ACC_A 176 176  ACC_B > h_ACC_B 177 177  DPTR > h_DPTR 178  DATA x_ 19226 > h_DATA x_19226179  DATA16 x_1 9227 > h_DATA16 x_19227178  DATA x_99 > h_DATA x_99 179  DATA16 x_100 > h_DATA16 x_100 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_1 9228 > h_BIT_ADDR x_19228186  N_BIT_ADDR x_1 9229 > h_N_BIT_ADDR x_19229187  RELATIVE x_1 9230 > h_RELATIVE x_19230188  ADDR11 x_1 9231 > h_ADDR11 x_19231189  ADDR16 x_1 9232 > h_ADDR16 x_19232185  BIT_ADDR x_101 > h_BIT_ADDR x_101 186  N_BIT_ADDR x_102 > h_N_BIT_ADDR x_102 187  RELATIVE x_103 > h_RELATIVE x_103 188  ADDR11 x_104 > h_ADDR11 x_104 189  ADDR16 x_105 > h_ADDR16 x_105 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_1 9253 > h_DIRECT x_19253200  INDIRECT x_1 9254 > h_INDIRECT x_19254201  EXT_INDIRECT x_1 9255 > h_EXT_INDIRECT x_19255202  REGISTER x_1 9256 > h_REGISTER x_19256199  DIRECT x_126 > h_DIRECT x_126 200  INDIRECT x_127 > h_INDIRECT x_127 201  EXT_INDIRECT x_128 > h_EXT_INDIRECT x_128 202  REGISTER x_129 > h_REGISTER x_129 203 203  ACC_A > h_ACC_A 204 204  ACC_B > h_ACC_B 205 205  DPTR > h_DPTR 206  DATA x_1 9257 > h_DATA x_19257207  DATA16 x_1 9258 > h_DATA16 x_19258206  DATA x_130 > h_DATA x_130 207  DATA16 x_131 > h_DATA16 x_131 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_1 9259 > h_BIT_ADDR x_19259214  N_BIT_ADDR x_1 9260 > h_N_BIT_ADDR x_19260215  RELATIVE x_1 9261 > h_RELATIVE x_19261216  ADDR11 x_1 9262 > h_ADDR11 x_19262217  ADDR16 x_1 9263 > h_ADDR16 x_19263213  BIT_ADDR x_132 > h_BIT_ADDR x_132 214  N_BIT_ADDR x_133 > h_N_BIT_ADDR x_133 215  RELATIVE x_134 > h_RELATIVE x_134 216  ADDR11 x_135 > h_ADDR11 x_135 217  ADDR16 x_136 > h_ADDR16 x_136 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_1 9284 > h_DIRECT x_19284228  INDIRECT x_1 9285 > h_INDIRECT x_19285229  EXT_INDIRECT x_1 9286 > h_EXT_INDIRECT x_19286230  REGISTER x_1 9287 > h_REGISTER x_19287227  DIRECT x_157 > h_DIRECT x_157 228  INDIRECT x_158 > h_INDIRECT x_158 229  EXT_INDIRECT x_159 > h_EXT_INDIRECT x_159 230  REGISTER x_160 > h_REGISTER x_160 231 231  ACC_A > h_ACC_A 232 232  ACC_B > h_ACC_B 233 233  DPTR > h_DPTR 234  DATA x_1 9288 > h_DATA x_19288235  DATA16 x_1 9289 > h_DATA16 x_19289234  DATA x_161 > h_DATA x_161 235  DATA16 x_162 > h_DATA16 x_162 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_1 9290 > h_BIT_ADDR x_19290242  N_BIT_ADDR x_1 9291 > h_N_BIT_ADDR x_19291243  RELATIVE x_1 9292 > h_RELATIVE x_19292244  ADDR11 x_1 9293 > h_ADDR11 x_19293245  ADDR16 x_1 9294 > h_ADDR16 x_19294241  BIT_ADDR x_163 > h_BIT_ADDR x_163 242  N_BIT_ADDR x_164 > h_N_BIT_ADDR x_164 243  RELATIVE x_165 > h_RELATIVE x_165 244  ADDR11 x_166 > h_ADDR11 x_166 245  ADDR16 x_167 > h_ADDR16 x_167 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_1 9315 > h_DIRECT x_19315256  INDIRECT x_1 9316 > h_INDIRECT x_19316257  EXT_INDIRECT x_19 317 > h_EXT_INDIRECT x_19317258  REGISTER x_19 318 > h_REGISTER x_19318255  DIRECT x_188 > h_DIRECT x_188 256  INDIRECT x_189 > h_INDIRECT x_189 257  EXT_INDIRECT x_190 > h_EXT_INDIRECT x_190 258  REGISTER x_191 > h_REGISTER x_191 259 259  ACC_A > h_ACC_A 260 260  ACC_B > h_ACC_B 261 261  DPTR > h_DPTR 262  DATA x_19 319 > h_DATA x_19319263  DATA16 x_193 20 > h_DATA16 x_19320262  DATA x_192 > h_DATA x_192 263  DATA16 x_193 > h_DATA16 x_193 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_19 321 > h_BIT_ADDR x_19321270  N_BIT_ADDR x_19 322 > h_N_BIT_ADDR x_19322271  RELATIVE x_19 323 > h_RELATIVE x_19323272  ADDR11 x_19 324 > h_ADDR11 x_19324273  ADDR16 x_19 325 > h_ADDR16 x_19325269  BIT_ADDR x_194 > h_BIT_ADDR x_194 270  N_BIT_ADDR x_195 > h_N_BIT_ADDR x_195 271  RELATIVE x_196 > h_RELATIVE x_196 272  ADDR11 x_197 > h_ADDR11 x_197 273  ADDR16 x_198 > h_ADDR16 x_198 274 274 275 275 (** val addressing_mode_inv_rect_Type4 : … … 1926 1926 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1927 1927 'a1) > subaddressing_mode > 'a1 **) 1928 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_ 19793=1929 let subaddressing_modeel = x_ 19793in1928 let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_666 = 1929 let subaddressing_modeel = x_666 in 1930 1930 h_mk_subaddressing_mode subaddressing_modeel __ 1931 1931 … … 1933 1933 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1934 1934 'a1) > subaddressing_mode > 'a1 **) 1935 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_ 19795=1936 let subaddressing_modeel = x_ 19795in1935 let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_668 = 1936 let subaddressing_modeel = x_668 in 1937 1937 h_mk_subaddressing_mode subaddressing_modeel __ 1938 1938 … … 1940 1940 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1941 1941 'a1) > subaddressing_mode > 'a1 **) 1942 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_ 19797=1943 let subaddressing_modeel = x_ 19797in1942 let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_670 = 1943 let subaddressing_modeel = x_670 in 1944 1944 h_mk_subaddressing_mode subaddressing_modeel __ 1945 1945 … … 1947 1947 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1948 1948 'a1) > subaddressing_mode > 'a1 **) 1949 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_ 19799=1950 let subaddressing_modeel = x_ 19799in1949 let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_672 = 1950 let subaddressing_modeel = x_672 in 1951 1951 h_mk_subaddressing_mode subaddressing_modeel __ 1952 1952 … … 1954 1954 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1955 1955 'a1) > subaddressing_mode > 'a1 **) 1956 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_ 19801=1957 let subaddressing_modeel = x_ 19801in1956 let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_674 = 1957 let subaddressing_modeel = x_674 in 1958 1958 h_mk_subaddressing_mode subaddressing_modeel __ 1959 1959 … … 1961 1961 Nat.nat > addressing_mode_tag Vector.vector > (addressing_mode > __ > 1962 1962 'a1) > subaddressing_mode > 'a1 **) 1963 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_ 19803=1964 let subaddressing_modeel = x_ 19803in1963 let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_676 = 1964 let subaddressing_modeel = x_676 in 1965 1965 h_mk_subaddressing_mode subaddressing_modeel __ 1966 1966 … … 2288 2288 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2289 2289 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 2290  ADD (x_ 19905, x_19904) > h_ADD x_19905 x_199042291  ADDC (x_ 19907, x_19906) > h_ADDC x_19907 x_199062292  SUBB (x_ 19909, x_19908) > h_SUBB x_19909 x_199082293  INC x_ 19910 > h_INC x_199102294  DEC x_ 19911 > h_DEC x_199112295  MUL (x_ 19913, x_19912) > h_MUL x_19913 x_199122296  DIV (x_ 19915, x_19914) > h_DIV x_19915 x_199142297  DA x_ 19916 > h_DA x_199162298  JC x_ 19917 > h_JC x_199172299  JNC x_ 19918 > h_JNC x_199182300  JB (x_ 19920, x_19919) > h_JB x_19920 x_199192301  JNB (x_ 19922, x_19921) > h_JNB x_19922 x_199212302  JBC (x_ 19924, x_19923) > h_JBC x_19924 x_199232303  JZ x_ 19925 > h_JZ x_199252304  JNZ x_ 19926 > h_JNZ x_199262305  CJNE (x_ 19928, x_19927) > h_CJNE x_19928 x_199272306  DJNZ (x_ 19930, x_19929) > h_DJNZ x_19930 x_199292307  ANL x_ 19931 > h_ANL x_199312308  ORL x_ 19932 > h_ORL x_199322309  XRL x_ 19933 > h_XRL x_199332310  CLR x_ 19934 > h_CLR x_199342311  CPL x_ 19935 > h_CPL x_199352312  RL x_ 19936 > h_RL x_199362313  RLC x_ 19937 > h_RLC x_199372314  RR x_ 19938 > h_RR x_199382315  RRC x_ 19939 > h_RRC x_199392316  SWAP x_ 19940 > h_SWAP x_199402317  MOV x_ 19941 > h_MOV x_199412318  MOVX x_ 19942 > h_MOVX x_199422319  SETB x_ 19943 > h_SETB x_199432320  PUSH x_ 19944 > h_PUSH x_199442321  POP x_ 19945 > h_POP x_199452322  XCH (x_ 19947, x_19946) > h_XCH x_19947 x_199462323  XCHD (x_ 19949, x_19948) > h_XCHD x_19949 x_199482290  ADD (x_778, x_777) > h_ADD x_778 x_777 2291  ADDC (x_780, x_779) > h_ADDC x_780 x_779 2292  SUBB (x_782, x_781) > h_SUBB x_782 x_781 2293  INC x_783 > h_INC x_783 2294  DEC x_784 > h_DEC x_784 2295  MUL (x_786, x_785) > h_MUL x_786 x_785 2296  DIV (x_788, x_787) > h_DIV x_788 x_787 2297  DA x_789 > h_DA x_789 2298  JC x_790 > h_JC x_790 2299  JNC x_791 > h_JNC x_791 2300  JB (x_793, x_792) > h_JB x_793 x_792 2301  JNB (x_795, x_794) > h_JNB x_795 x_794 2302  JBC (x_797, x_796) > h_JBC x_797 x_796 2303  JZ x_798 > h_JZ x_798 2304  JNZ x_799 > h_JNZ x_799 2305  CJNE (x_801, x_800) > h_CJNE x_801 x_800 2306  DJNZ (x_803, x_802) > h_DJNZ x_803 x_802 2307  ANL x_804 > h_ANL x_804 2308  ORL x_805 > h_ORL x_805 2309  XRL x_806 > h_XRL x_806 2310  CLR x_807 > h_CLR x_807 2311  CPL x_808 > h_CPL x_808 2312  RL x_809 > h_RL x_809 2313  RLC x_810 > h_RLC x_810 2314  RR x_811 > h_RR x_811 2315  RRC x_812 > h_RRC x_812 2316  SWAP x_813 > h_SWAP x_813 2317  MOV x_814 > h_MOV x_814 2318  MOVX x_815 > h_MOVX x_815 2319  SETB x_816 > h_SETB x_816 2320  PUSH x_817 > h_PUSH x_817 2321  POP x_818 > h_POP x_818 2322  XCH (x_820, x_819) > h_XCH x_820 x_819 2323  XCHD (x_822, x_821) > h_XCHD x_822 x_821 2324 2324  RET > h_RET 2325 2325  RETI > h_RETI 2326 2326  NOP > h_NOP 2327  JMP x_ 19950 > h_JMP x_199502327  JMP x_823 > h_JMP x_823 2328 2328 2329 2329 (** val preinstruction_rect_Type5 : … … 2363 2363 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2364 2364 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 2365  ADD (x_ 19991, x_19990) > h_ADD x_19991 x_199902366  ADDC (x_ 19993, x_19992) > h_ADDC x_19993 x_199922367  SUBB (x_ 19995, x_19994) > h_SUBB x_19995 x_199942368  INC x_ 19996 > h_INC x_199962369  DEC x_ 19997 > h_DEC x_199972370  MUL (x_ 19999, x_19998) > h_MUL x_19999 x_199982371  DIV (x_ 20001, x_20000) > h_DIV x_20001 x_200002372  DA x_ 20002 > h_DA x_200022373  JC x_ 20003 > h_JC x_200032374  JNC x_ 20004 > h_JNC x_200042375  JB (x_ 20006, x_20005) > h_JB x_20006 x_200052376  JNB (x_ 20008, x_20007) > h_JNB x_20008 x_200072377  JBC (x_ 20010, x_20009) > h_JBC x_20010 x_200092378  JZ x_ 20011 > h_JZ x_200112379  JNZ x_ 20012 > h_JNZ x_200122380  CJNE (x_ 20014, x_20013) > h_CJNE x_20014 x_200132381  DJNZ (x_ 20016, x_20015) > h_DJNZ x_20016 x_200152382  ANL x_ 20017 > h_ANL x_200172383  ORL x_ 20018 > h_ORL x_200182384  XRL x_ 20019 > h_XRL x_200192385  CLR x_ 20020 > h_CLR x_200202386  CPL x_ 20021 > h_CPL x_200212387  RL x_ 20022 > h_RL x_200222388  RLC x_ 20023 > h_RLC x_200232389  RR x_ 20024 > h_RR x_200242390  RRC x_ 20025 > h_RRC x_200252391  SWAP x_ 20026 > h_SWAP x_200262392  MOV x_ 20027 > h_MOV x_200272393  MOVX x_ 20028 > h_MOVX x_200282394  SETB x_ 20029 > h_SETB x_200292395  PUSH x_ 20030 > h_PUSH x_200302396  POP x_ 20031 > h_POP x_200312397  XCH (x_ 20033, x_20032) > h_XCH x_20033 x_200322398  XCHD (x_ 20035, x_20034) > h_XCHD x_20035 x_200342365  ADD (x_864, x_863) > h_ADD x_864 x_863 2366  ADDC (x_866, x_865) > h_ADDC x_866 x_865 2367  SUBB (x_868, x_867) > h_SUBB x_868 x_867 2368  INC x_869 > h_INC x_869 2369  DEC x_870 > h_DEC x_870 2370  MUL (x_872, x_871) > h_MUL x_872 x_871 2371  DIV (x_874, x_873) > h_DIV x_874 x_873 2372  DA x_875 > h_DA x_875 2373  JC x_876 > h_JC x_876 2374  JNC x_877 > h_JNC x_877 2375  JB (x_879, x_878) > h_JB x_879 x_878 2376  JNB (x_881, x_880) > h_JNB x_881 x_880 2377  JBC (x_883, x_882) > h_JBC x_883 x_882 2378  JZ x_884 > h_JZ x_884 2379  JNZ x_885 > h_JNZ x_885 2380  CJNE (x_887, x_886) > h_CJNE x_887 x_886 2381  DJNZ (x_889, x_888) > h_DJNZ x_889 x_888 2382  ANL x_890 > h_ANL x_890 2383  ORL x_891 > h_ORL x_891 2384  XRL x_892 > h_XRL x_892 2385  CLR x_893 > h_CLR x_893 2386  CPL x_894 > h_CPL x_894 2387  RL x_895 > h_RL x_895 2388  RLC x_896 > h_RLC x_896 2389  RR x_897 > h_RR x_897 2390  RRC x_898 > h_RRC x_898 2391  SWAP x_899 > h_SWAP x_899 2392  MOV x_900 > h_MOV x_900 2393  MOVX x_901 > h_MOVX x_901 2394  SETB x_902 > h_SETB x_902 2395  PUSH x_903 > h_PUSH x_903 2396  POP x_904 > h_POP x_904 2397  XCH (x_906, x_905) > h_XCH x_906 x_905 2398  XCHD (x_908, x_907) > h_XCHD x_908 x_907 2399 2399  RET > h_RET 2400 2400  RETI > h_RETI 2401 2401  NOP > h_NOP 2402  JMP x_ 20036 > h_JMP x_200362402  JMP x_909 > h_JMP x_909 2403 2403 2404 2404 (** val preinstruction_rect_Type3 : … … 2438 2438 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2439 2439 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 2440  ADD (x_ 20077, x_20076) > h_ADD x_20077 x_200762441  ADDC (x_ 20079, x_20078) > h_ADDC x_20079 x_200782442  SUBB (x_ 20081, x_20080) > h_SUBB x_20081 x_200802443  INC x_ 20082 > h_INC x_200822444  DEC x_ 20083 > h_DEC x_200832445  MUL (x_ 20085, x_20084) > h_MUL x_20085 x_200842446  DIV (x_ 20087, x_20086) > h_DIV x_20087 x_200862447  DA x_ 20088 > h_DA x_200882448  JC x_ 20089 > h_JC x_200892449  JNC x_ 20090 > h_JNC x_200902450  JB (x_ 20092, x_20091) > h_JB x_20092 x_200912451  JNB (x_ 20094, x_20093) > h_JNB x_20094 x_200932452  JBC (x_ 20096, x_20095) > h_JBC x_20096 x_200952453  JZ x_ 20097 > h_JZ x_200972454  JNZ x_ 20098 > h_JNZ x_200982455  CJNE (x_ 20100, x_20099) > h_CJNE x_20100 x_200992456  DJNZ (x_ 20102, x_20101) > h_DJNZ x_20102 x_201012457  ANL x_ 20103 > h_ANL x_201032458  ORL x_ 20104 > h_ORL x_201042459  XRL x_ 20105 > h_XRL x_201052460  CLR x_ 20106 > h_CLR x_201062461  CPL x_ 20107 > h_CPL x_201072462  RL x_ 20108 > h_RL x_201082463  RLC x_ 20109 > h_RLC x_201092464  RR x_ 20110 > h_RR x_201102465  RRC x_ 20111 > h_RRC x_201112466  SWAP x_ 20112 > h_SWAP x_201122467  MOV x_ 20113 > h_MOV x_201132468  MOVX x_ 20114 > h_MOVX x_201142469  SETB x_ 20115 > h_SETB x_201152470  PUSH x_ 20116 > h_PUSH x_201162471  POP x_ 20117 > h_POP x_201172472  XCH (x_ 20119, x_20118) > h_XCH x_20119 x_201182473  XCHD (x_ 20121, x_20120) > h_XCHD x_20121 x_201202440  ADD (x_950, x_949) > h_ADD x_950 x_949 2441  ADDC (x_952, x_951) > h_ADDC x_952 x_951 2442  SUBB (x_954, x_953) > h_SUBB x_954 x_953 2443  INC x_955 > h_INC x_955 2444  DEC x_956 > h_DEC x_956 2445  MUL (x_958, x_957) > h_MUL x_958 x_957 2446  DIV (x_960, x_959) > h_DIV x_960 x_959 2447  DA x_961 > h_DA x_961 2448  JC x_962 > h_JC x_962 2449  JNC x_963 > h_JNC x_963 2450  JB (x_965, x_964) > h_JB x_965 x_964 2451  JNB (x_967, x_966) > h_JNB x_967 x_966 2452  JBC (x_969, x_968) > h_JBC x_969 x_968 2453  JZ x_970 > h_JZ x_970 2454  JNZ x_971 > h_JNZ x_971 2455  CJNE (x_973, x_972) > h_CJNE x_973 x_972 2456  DJNZ (x_975, x_974) > h_DJNZ x_975 x_974 2457  ANL x_976 > h_ANL x_976 2458  ORL x_977 > h_ORL x_977 2459  XRL x_978 > h_XRL x_978 2460  CLR x_979 > h_CLR x_979 2461  CPL x_980 > h_CPL x_980 2462  RL x_981 > h_RL x_981 2463  RLC x_982 > h_RLC x_982 2464  RR x_983 > h_RR x_983 2465  RRC x_984 > h_RRC x_984 2466  SWAP x_985 > h_SWAP x_985 2467  MOV x_986 > h_MOV x_986 2468  MOVX x_987 > h_MOVX x_987 2469  SETB x_988 > h_SETB x_988 2470  PUSH x_989 > h_PUSH x_989 2471  POP x_990 > h_POP x_990 2472  XCH (x_992, x_991) > h_XCH x_992 x_991 2473  XCHD (x_994, x_993) > h_XCHD x_994 x_993 2474 2474  RET > h_RET 2475 2475  RETI > h_RETI 2476 2476  NOP > h_NOP 2477  JMP x_ 20122 > h_JMP x_201222477  JMP x_995 > h_JMP x_995 2478 2478 2479 2479 (** val preinstruction_rect_Type2 : … … 2513 2513 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2514 2514 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 2515  ADD (x_ 20163, x_20162) > h_ADD x_20163 x_201622516  ADDC (x_ 20165, x_20164) > h_ADDC x_20165 x_201642517  SUBB (x_ 20167, x_20166) > h_SUBB x_20167 x_201662518  INC x_ 20168 > h_INC x_201682519  DEC x_ 20169 > h_DEC x_201692520  MUL (x_ 20171, x_20170) > h_MUL x_20171 x_201702521  DIV (x_ 20173, x_20172) > h_DIV x_20173 x_201722522  DA x_ 20174 > h_DA x_201742523  JC x_ 20175 > h_JC x_201752524  JNC x_ 20176 > h_JNC x_201762525  JB (x_ 20178, x_20177) > h_JB x_20178 x_201772526  JNB (x_ 20180, x_20179) > h_JNB x_20180 x_201792527  JBC (x_ 20182, x_20181) > h_JBC x_20182 x_201812528  JZ x_ 20183 > h_JZ x_201832529  JNZ x_ 20184 > h_JNZ x_201842530  CJNE (x_ 20186, x_20185) > h_CJNE x_20186 x_201852531  DJNZ (x_ 20188, x_20187) > h_DJNZ x_20188 x_201872532  ANL x_ 20189 > h_ANL x_201892533  ORL x_ 20190 > h_ORL x_201902534  XRL x_ 20191 > h_XRL x_201912535  CLR x_ 20192 > h_CLR x_201922536  CPL x_ 20193 > h_CPL x_201932537  RL x_ 20194 > h_RL x_201942538  RLC x_ 20195 > h_RLC x_201952539  RR x_ 20196 > h_RR x_201962540  RRC x_ 20197 > h_RRC x_201972541  SWAP x_ 20198 > h_SWAP x_201982542  MOV x_ 20199 > h_MOV x_201992543  MOVX x_ 20200 > h_MOVX x_202002544  SETB x_ 20201 > h_SETB x_202012545  PUSH x_ 20202 > h_PUSH x_202022546  POP x_ 20203 > h_POP x_202032547  XCH (x_ 20205, x_20204) > h_XCH x_20205 x_202042548  XCHD (x_ 20207, x_20206) > h_XCHD x_20207 x_202062515  ADD (x_1036, x_1035) > h_ADD x_1036 x_1035 2516  ADDC (x_1038, x_1037) > h_ADDC x_1038 x_1037 2517  SUBB (x_1040, x_1039) > h_SUBB x_1040 x_1039 2518  INC x_1041 > h_INC x_1041 2519  DEC x_1042 > h_DEC x_1042 2520  MUL (x_1044, x_1043) > h_MUL x_1044 x_1043 2521  DIV (x_1046, x_1045) > h_DIV x_1046 x_1045 2522  DA x_1047 > h_DA x_1047 2523  JC x_1048 > h_JC x_1048 2524  JNC x_1049 > h_JNC x_1049 2525  JB (x_1051, x_1050) > h_JB x_1051 x_1050 2526  JNB (x_1053, x_1052) > h_JNB x_1053 x_1052 2527  JBC (x_1055, x_1054) > h_JBC x_1055 x_1054 2528  JZ x_1056 > h_JZ x_1056 2529  JNZ x_1057 > h_JNZ x_1057 2530  CJNE (x_1059, x_1058) > h_CJNE x_1059 x_1058 2531  DJNZ (x_1061, x_1060) > h_DJNZ x_1061 x_1060 2532  ANL x_1062 > h_ANL x_1062 2533  ORL x_1063 > h_ORL x_1063 2534  XRL x_1064 > h_XRL x_1064 2535  CLR x_1065 > h_CLR x_1065 2536  CPL x_1066 > h_CPL x_1066 2537  RL x_1067 > h_RL x_1067 2538  RLC x_1068 > h_RLC x_1068 2539  RR x_1069 > h_RR x_1069 2540  RRC x_1070 > h_RRC x_1070 2541  SWAP x_1071 > h_SWAP x_1071 2542  MOV x_1072 > h_MOV x_1072 2543  MOVX x_1073 > h_MOVX x_1073 2544  SETB x_1074 > h_SETB x_1074 2545  PUSH x_1075 > h_PUSH x_1075 2546  POP x_1076 > h_POP x_1076 2547  XCH (x_1078, x_1077) > h_XCH x_1078 x_1077 2548  XCHD (x_1080, x_1079) > h_XCHD x_1080 x_1079 2549 2549  RET > h_RET 2550 2550  RETI > h_RETI 2551 2551  NOP > h_NOP 2552  JMP x_ 20208 > h_JMP x_202082552  JMP x_1081 > h_JMP x_1081 2553 2553 2554 2554 (** val preinstruction_rect_Type1 : … … 2588 2588 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2589 2589 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 2590  ADD (x_ 20249, x_20248) > h_ADD x_20249 x_202482591  ADDC (x_ 20251, x_20250) > h_ADDC x_20251 x_202502592  SUBB (x_ 20253, x_20252) > h_SUBB x_20253 x_202522593  INC x_ 20254 > h_INC x_202542594  DEC x_ 20255 > h_DEC x_202552595  MUL (x_ 20257, x_20256) > h_MUL x_20257 x_202562596  DIV (x_ 20259, x_20258) > h_DIV x_20259 x_202582597  DA x_ 20260 > h_DA x_202602598  JC x_ 20261 > h_JC x_202612599  JNC x_ 20262 > h_JNC x_202622600  JB (x_ 20264, x_20263) > h_JB x_20264 x_202632601  JNB (x_ 20266, x_20265) > h_JNB x_20266 x_202652602  JBC (x_ 20268, x_20267) > h_JBC x_20268 x_202672603  JZ x_ 20269 > h_JZ x_202692604  JNZ x_ 20270 > h_JNZ x_202702605  CJNE (x_ 20272, x_20271) > h_CJNE x_20272 x_202712606  DJNZ (x_ 20274, x_20273) > h_DJNZ x_20274 x_202732607  ANL x_ 20275 > h_ANL x_202752608  ORL x_ 20276 > h_ORL x_202762609  XRL x_ 20277 > h_XRL x_202772610  CLR x_ 20278 > h_CLR x_202782611  CPL x_ 20279 > h_CPL x_202792612  RL x_ 20280 > h_RL x_202802613  RLC x_ 20281 > h_RLC x_202812614  RR x_ 20282 > h_RR x_202822615  RRC x_ 20283 > h_RRC x_202832616  SWAP x_ 20284 > h_SWAP x_202842617  MOV x_ 20285 > h_MOV x_202852618  MOVX x_ 20286 > h_MOVX x_202862619  SETB x_ 20287 > h_SETB x_202872620  PUSH x_ 20288 > h_PUSH x_202882621  POP x_ 20289 > h_POP x_202892622  XCH (x_ 20291, x_20290) > h_XCH x_20291 x_202902623  XCHD (x_ 20293, x_20292) > h_XCHD x_20293 x_202922590  ADD (x_1122, x_1121) > h_ADD x_1122 x_1121 2591  ADDC (x_1124, x_1123) > h_ADDC x_1124 x_1123 2592  SUBB (x_1126, x_1125) > h_SUBB x_1126 x_1125 2593  INC x_1127 > h_INC x_1127 2594  DEC x_1128 > h_DEC x_1128 2595  MUL (x_1130, x_1129) > h_MUL x_1130 x_1129 2596  DIV (x_1132, x_1131) > h_DIV x_1132 x_1131 2597  DA x_1133 > h_DA x_1133 2598  JC x_1134 > h_JC x_1134 2599  JNC x_1135 > h_JNC x_1135 2600  JB (x_1137, x_1136) > h_JB x_1137 x_1136 2601  JNB (x_1139, x_1138) > h_JNB x_1139 x_1138 2602  JBC (x_1141, x_1140) > h_JBC x_1141 x_1140 2603  JZ x_1142 > h_JZ x_1142 2604  JNZ x_1143 > h_JNZ x_1143 2605  CJNE (x_1145, x_1144) > h_CJNE x_1145 x_1144 2606  DJNZ (x_1147, x_1146) > h_DJNZ x_1147 x_1146 2607  ANL x_1148 > h_ANL x_1148 2608  ORL x_1149 > h_ORL x_1149 2609  XRL x_1150 > h_XRL x_1150 2610  CLR x_1151 > h_CLR x_1151 2611  CPL x_1152 > h_CPL x_1152 2612  RL x_1153 > h_RL x_1153 2613  RLC x_1154 > h_RLC x_1154 2614  RR x_1155 > h_RR x_1155 2615  RRC x_1156 > h_RRC x_1156 2616  SWAP x_1157 > h_SWAP x_1157 2617  MOV x_1158 > h_MOV x_1158 2618  MOVX x_1159 > h_MOVX x_1159 2619  SETB x_1160 > h_SETB x_1160 2620  PUSH x_1161 > h_PUSH x_1161 2621  POP x_1162 > h_POP x_1162 2622  XCH (x_1164, x_1163) > h_XCH x_1164 x_1163 2623  XCHD (x_1166, x_1165) > h_XCHD x_1166 x_1165 2624 2624  RET > h_RET 2625 2625  RETI > h_RETI 2626 2626  NOP > h_NOP 2627  JMP x_ 20294 > h_JMP x_202942627  JMP x_1167 > h_JMP x_1167 2628 2628 2629 2629 (** val preinstruction_rect_Type0 : … … 2663 2663 'a2 > 'a2 > (subaddressing_mode > 'a2) > 'a1 preinstruction > 'a2 **) 2664 2664 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 2665  ADD (x_ 20335, x_20334) > h_ADD x_20335 x_203342666  ADDC (x_ 20337, x_20336) > h_ADDC x_20337 x_203362667  SUBB (x_ 20339, x_20338) > h_SUBB x_20339 x_203382668  INC x_ 20340 > h_INC x_203402669  DEC x_ 20341 > h_DEC x_203412670  MUL (x_ 20343, x_20342) > h_MUL x_20343 x_203422671  DIV (x_ 20345, x_20344) > h_DIV x_20345 x_203442672  DA x_ 20346 > h_DA x_203462673  JC x_ 20347 > h_JC x_203472674  JNC x_ 20348 > h_JNC x_203482675  JB (x_ 20350, x_20349) > h_JB x_20350 x_203492676  JNB (x_ 20352, x_20351) > h_JNB x_20352 x_203512677  JBC (x_ 20354, x_20353) > h_JBC x_20354 x_203532678  JZ x_ 20355 > h_JZ x_203552679  JNZ x_ 20356 > h_JNZ x_203562680  CJNE (x_ 20358, x_20357) > h_CJNE x_20358 x_203572681  DJNZ (x_ 20360, x_20359) > h_DJNZ x_20360 x_203592682  ANL x_ 20361 > h_ANL x_203612683  ORL x_ 20362 > h_ORL x_203622684  XRL x_ 20363 > h_XRL x_203632685  CLR x_ 20364 > h_CLR x_203642686  CPL x_ 20365 > h_CPL x_203652687  RL x_ 20366 > h_RL x_203662688  RLC x_ 20367 > h_RLC x_203672689  RR x_ 20368 > h_RR x_203682690  RRC x_ 20369 > h_RRC x_203692691  SWAP x_ 20370 > h_SWAP x_203702692  MOV x_ 20371 > h_MOV x_203712693  MOVX x_ 20372 > h_MOVX x_203722694  SETB x_ 20373 > h_SETB x_203732695  PUSH x_ 20374 > h_PUSH x_203742696  POP x_ 20375 > h_POP x_203752697  XCH (x_ 20377, x_20376) > h_XCH x_20377 x_203762698  XCHD (x_ 20379, x_20378) > h_XCHD x_20379 x_203782665  ADD (x_1208, x_1207) > h_ADD x_1208 x_1207 2666  ADDC (x_1210, x_1209) > h_ADDC x_1210 x_1209 2667  SUBB (x_1212, x_1211) > h_SUBB x_1212 x_1211 2668  INC x_1213 > h_INC x_1213 2669  DEC x_1214 > h_DEC x_1214 2670  MUL (x_1216, x_1215) > h_MUL x_1216 x_1215 2671  DIV (x_1218, x_1217) > h_DIV x_1218 x_1217 2672  DA x_1219 > h_DA x_1219 2673  JC x_1220 > h_JC x_1220 2674  JNC x_1221 > h_JNC x_1221 2675  JB (x_1223, x_1222) > h_JB x_1223 x_1222 2676  JNB (x_1225, x_1224) > h_JNB x_1225 x_1224 2677  JBC (x_1227, x_1226) > h_JBC x_1227 x_1226 2678  JZ x_1228 > h_JZ x_1228 2679  JNZ x_1229 > h_JNZ x_1229 2680  CJNE (x_1231, x_1230) > h_CJNE x_1231 x_1230 2681  DJNZ (x_1233, x_1232) > h_DJNZ x_1233 x_1232 2682  ANL x_1234 > h_ANL x_1234 2683  ORL x_1235 > h_ORL x_1235 2684  XRL x_1236 > h_XRL x_1236 2685  CLR x_1237 > h_CLR x_1237 2686  CPL x_1238 > h_CPL x_1238 2687  RL x_1239 > h_RL x_1239 2688  RLC x_1240 > h_RLC x_1240 2689  RR x_1241 > h_RR x_1241 2690  RRC x_1242 > h_RRC x_1242 2691  SWAP x_1243 > h_SWAP x_1243 2692  MOV x_1244 > h_MOV x_1244 2693  MOVX x_1245 > h_MOVX x_1245 2694  SETB x_1246 > h_SETB x_1246 2695  PUSH x_1247 > h_PUSH x_1247 2696  POP x_1248 > h_POP x_1248 2697  XCH (x_1250, x_1249) > h_XCH x_1250 x_1249 2698  XCHD (x_1252, x_1251) > h_XCHD x_1252 x_1251 2699 2699  RET > h_RET 2700 2700  RETI > h_RETI 2701 2701  NOP > h_NOP 2702  JMP x_ 20380 > h_JMP x_203802702  JMP x_1253 > h_JMP x_1253 2703 2703 2704 2704 (** val preinstruction_inv_rect_Type4 : … … 5104 5104 'a1 **) 5105 5105 let rec instruction_rect_Type4 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 5106  ACALL x_ 20952 > h_ACALL x_209525107  LCALL x_ 20953 > h_LCALL x_209535108  AJMP x_ 20954 > h_AJMP x_209545109  LJMP x_ 20955 > h_LJMP x_209555110  SJMP x_ 20956 > h_SJMP x_209565111  MOVC (x_ 20958, x_20957) > h_MOVC x_20958 x_209575112  RealInstruction x_ 20959 > h_RealInstruction x_209595106  ACALL x_1825 > h_ACALL x_1825 5107  LCALL x_1826 > h_LCALL x_1826 5108  AJMP x_1827 > h_AJMP x_1827 5109  LJMP x_1828 > h_LJMP x_1828 5110  SJMP x_1829 > h_SJMP x_1829 5111  MOVC (x_1831, x_1830) > h_MOVC x_1831 x_1830 5112  RealInstruction x_1832 > h_RealInstruction x_1832 5113 5113 5114 5114 (** val instruction_rect_Type5 : … … 5119 5119 'a1 **) 5120 5120 let rec instruction_rect_Type5 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 5121  ACALL x_ 20968 > h_ACALL x_209685122  LCALL x_ 20969 > h_LCALL x_209695123  AJMP x_ 20970 > h_AJMP x_209705124  LJMP x_ 20971 > h_LJMP x_209715125  SJMP x_ 20972 > h_SJMP x_209725126  MOVC (x_ 20974, x_20973) > h_MOVC x_20974 x_209735127  RealInstruction x_ 20975 > h_RealInstruction x_209755121  ACALL x_1841 > h_ACALL x_1841 5122  LCALL x_1842 > h_LCALL x_1842 5123  AJMP x_1843 > h_AJMP x_1843 5124  LJMP x_1844 > h_LJMP x_1844 5125  SJMP x_1845 > h_SJMP x_1845 5126  MOVC (x_1847, x_1846) > h_MOVC x_1847 x_1846 5127  RealInstruction x_1848 > h_RealInstruction x_1848 5128 5128 5129 5129 (** val instruction_rect_Type3 : … … 5134 5134 'a1 **) 5135 5135 let rec instruction_rect_Type3 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 5136  ACALL x_ 20984 > h_ACALL x_209845137  LCALL x_ 20985 > h_LCALL x_209855138  AJMP x_ 20986 > h_AJMP x_209865139  LJMP x_ 20987 > h_LJMP x_209875140  SJMP x_ 20988 > h_SJMP x_209885141  MOVC (x_ 20990, x_20989) > h_MOVC x_20990 x_209895142  RealInstruction x_ 20991 > h_RealInstruction x_209915136  ACALL x_1857 > h_ACALL x_1857 5137  LCALL x_1858 > h_LCALL x_1858 5138  AJMP x_1859 > h_AJMP x_1859 5139  LJMP x_1860 > h_LJMP x_1860 5140  SJMP x_1861 > h_SJMP x_1861 5141  MOVC (x_1863, x_1862) > h_MOVC x_1863 x_1862 5142  RealInstruction x_1864 > h_RealInstruction x_1864 5143 5143 5144 5144 (** val instruction_rect_Type2 : … … 5149 5149 'a1 **) 5150 5150 let rec instruction_rect_Type2 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 5151  ACALL x_ 21000 > h_ACALL x_210005152  LCALL x_ 21001 > h_LCALL x_210015153  AJMP x_ 21002 > h_AJMP x_210025154  LJMP x_ 21003 > h_LJMP x_210035155  SJMP x_ 21004 > h_SJMP x_210045156  MOVC (x_ 21006, x_21005) > h_MOVC x_21006 x_210055157  RealInstruction x_ 21007 > h_RealInstruction x_210075151  ACALL x_1873 > h_ACALL x_1873 5152  LCALL x_1874 > h_LCALL x_1874 5153  AJMP x_1875 > h_AJMP x_1875 5154  LJMP x_1876 > h_LJMP x_1876 5155  SJMP x_1877 > h_SJMP x_1877 5156  MOVC (x_1879, x_1878) > h_MOVC x_1879 x_1878 5157  RealInstruction x_1880 > h_RealInstruction x_1880 5158 5158 5159 5159 (** val instruction_rect_Type1 : … … 5164 5164 'a1 **) 5165 5165 let rec instruction_rect_Type1 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 5166  ACALL x_ 21016 > h_ACALL x_210165167  LCALL x_ 21017 > h_LCALL x_210175168  AJMP x_ 21018 > h_AJMP x_210185169  LJMP x_ 21019 > h_LJMP x_210195170  SJMP x_ 21020 > h_SJMP x_210205171  MOVC (x_ 21022, x_21021) > h_MOVC x_21022 x_210215172  RealInstruction x_ 21023 > h_RealInstruction x_210235166  ACALL x_1889 > h_ACALL x_1889 5167  LCALL x_1890 > h_LCALL x_1890 5168  AJMP x_1891 > h_AJMP x_1891 5169  LJMP x_1892 > h_LJMP x_1892 5170  SJMP x_1893 > h_SJMP x_1893 5171  MOVC (x_1895, x_1894) > h_MOVC x_1895 x_1894 5172  RealInstruction x_1896 > h_RealInstruction x_1896 5173 5173 5174 5174 (** val instruction_rect_Type0 : … … 5179 5179 'a1 **) 5180 5180 let rec instruction_rect_Type0 h_ACALL h_LCALL h_AJMP h_LJMP h_SJMP h_MOVC h_RealInstruction = function 5181  ACALL x_ 21032 > h_ACALL x_210325182  LCALL x_ 21033 > h_LCALL x_210335183  AJMP x_ 21034 > h_AJMP x_210345184  LJMP x_ 21035 > h_LJMP x_210355185  SJMP x_ 21036 > h_SJMP x_210365186  MOVC (x_ 21038, x_21037) > h_MOVC x_21038 x_210375187  RealInstruction x_ 21039 > h_RealInstruction x_210395181  ACALL x_1905 > h_ACALL x_1905 5182  LCALL x_1906 > h_LCALL x_1906 5183  AJMP x_1907 > h_AJMP x_1907 5184  LJMP x_1908 > h_LJMP x_1908 5185  SJMP x_1909 > h_SJMP x_1909 5186  MOVC (x_1911, x_1910) > h_MOVC x_1911 x_1910 5187  RealInstruction x_1912 > h_RealInstruction x_1912 5188 5188 5189 5189 (** val instruction_inv_rect_Type4 : … … 5476 5476 > 'a1 **) 5477 5477 let rec pseudo_instruction_rect_Type4 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function 5478  Instruction x_2 1202 > h_Instruction x_212025479  Comment x_2 1203 > h_Comment x_212035480  Cost x_2 1204 > h_Cost x_212045481  Jmp x_2 1205 > h_Jmp x_212055482  Jnz (x_2 1208, x_21207, x_21206) > h_Jnz x_21208 x_21207 x_212065483  Call x_2 1209 > h_Call x_212095484  Mov (x_2 1212, x_21211, x_21210) > h_Mov x_21212 x_21211 x_212105478  Instruction x_2075 > h_Instruction x_2075 5479  Comment x_2076 > h_Comment x_2076 5480  Cost x_2077 > h_Cost x_2077 5481  Jmp x_2078 > h_Jmp x_2078 5482  Jnz (x_2081, x_2080, x_2079) > h_Jnz x_2081 x_2080 x_2079 5483  Call x_2082 > h_Call x_2082 5484  Mov (x_2085, x_2084, x_2083) > h_Mov x_2085 x_2084 x_2083 5485 5485 5486 5486 (** val pseudo_instruction_rect_Type5 : … … 5492 5492 > 'a1 **) 5493 5493 let rec pseudo_instruction_rect_Type5 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function 5494  Instruction x_2 1221 > h_Instruction x_212215495  Comment x_2 1222 > h_Comment x_212225496  Cost x_2 1223 > h_Cost x_212235497  Jmp x_2 1224 > h_Jmp x_212245498  Jnz (x_21 227, x_21226, x_21225) > h_Jnz x_21227 x_21226 x_212255499  Call x_21 228 > h_Call x_212285500  Mov (x_21 231, x_21230, x_21229) > h_Mov x_21231 x_21230 x_212295494  Instruction x_2094 > h_Instruction x_2094 5495  Comment x_2095 > h_Comment x_2095 5496  Cost x_2096 > h_Cost x_2096 5497  Jmp x_2097 > h_Jmp x_2097 5498  Jnz (x_2100, x_2099, x_2098) > h_Jnz x_2100 x_2099 x_2098 5499  Call x_2101 > h_Call x_2101 5500  Mov (x_2104, x_2103, x_2102) > h_Mov x_2104 x_2103 x_2102 5501 5501 5502 5502 (** val pseudo_instruction_rect_Type3 : … … 5508 5508 > 'a1 **) 5509 5509 let rec pseudo_instruction_rect_Type3 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function 5510  Instruction x_21 240 > h_Instruction x_212405511  Comment x_21 241 > h_Comment x_212415512  Cost x_21 242 > h_Cost x_212425513  Jmp x_21 243 > h_Jmp x_212435514  Jnz (x_21 246, x_21245, x_21244) > h_Jnz x_21246 x_21245 x_212445515  Call x_212 47 > h_Call x_212475516  Mov (x_212 50, x_21249, x_21248) > h_Mov x_21250 x_21249 x_212485510  Instruction x_2113 > h_Instruction x_2113 5511  Comment x_2114 > h_Comment x_2114 5512  Cost x_2115 > h_Cost x_2115 5513  Jmp x_2116 > h_Jmp x_2116 5514  Jnz (x_2119, x_2118, x_2117) > h_Jnz x_2119 x_2118 x_2117 5515  Call x_2120 > h_Call x_2120 5516  Mov (x_2123, x_2122, x_2121) > h_Mov x_2123 x_2122 x_2121 5517 5517 5518 5518 (** val pseudo_instruction_rect_Type2 : … … 5524 5524 > 'a1 **) 5525 5525 let rec pseudo_instruction_rect_Type2 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function 5526  Instruction x_21 259 > h_Instruction x_212595527  Comment x_21 260 > h_Comment x_212605528  Cost x_21 261 > h_Cost x_212615529  Jmp x_21 262 > h_Jmp x_212625530  Jnz (x_21 265, x_21264, x_21263) > h_Jnz x_21265 x_21264 x_212635531  Call x_21 266 > h_Call x_212665532  Mov (x_21 269, x_21268, x_21267) > h_Mov x_21269 x_21268 x_212675526  Instruction x_2132 > h_Instruction x_2132 5527  Comment x_2133 > h_Comment x_2133 5528  Cost x_2134 > h_Cost x_2134 5529  Jmp x_2135 > h_Jmp x_2135 5530  Jnz (x_2138, x_2137, x_2136) > h_Jnz x_2138 x_2137 x_2136 5531  Call x_2139 > h_Call x_2139 5532  Mov (x_2142, x_2141, x_2140) > h_Mov x_2142 x_2141 x_2140 5533 5533 5534 5534 (** val pseudo_instruction_rect_Type1 : … … 5540 5540 > 'a1 **) 5541 5541 let rec pseudo_instruction_rect_Type1 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function 5542  Instruction x_21 278 > h_Instruction x_212785543  Comment x_21 279 > h_Comment x_212795544  Cost x_21 280 > h_Cost x_212805545  Jmp x_21 281 > h_Jmp x_212815546  Jnz (x_21 284, x_21283, x_21282) > h_Jnz x_21284 x_21283 x_212825547  Call x_21 285 > h_Call x_212855548  Mov (x_21 288, x_21287, x_21286) > h_Mov x_21288 x_21287 x_212865542  Instruction x_2151 > h_Instruction x_2151 5543  Comment x_2152 > h_Comment x_2152 5544  Cost x_2153 > h_Cost x_2153 5545  Jmp x_2154 > h_Jmp x_2154 5546  Jnz (x_2157, x_2156, x_2155) > h_Jnz x_2157 x_2156 x_2155 5547  Call x_2158 > h_Call x_2158 5548  Mov (x_2161, x_2160, x_2159) > h_Mov x_2161 x_2160 x_2159 5549 5549 5550 5550 (** val pseudo_instruction_rect_Type0 : … … 5556 5556 > 'a1 **) 5557 5557 let rec pseudo_instruction_rect_Type0 h_Instruction h_Comment h_Cost h_Jmp h_Jnz h_Call h_Mov = function 5558  Instruction x_21 297 > h_Instruction x_212975559  Comment x_21 298 > h_Comment x_212985560  Cost x_21 299 > h_Cost x_212995561  Jmp x_21 300 > h_Jmp x_213005562  Jnz (x_21 303, x_21302, x_21301) > h_Jnz x_21303 x_21302 x_213015563  Call x_21 304 > h_Call x_213045564  Mov (x_21 307, x_21306, x_21305) > h_Mov x_21307 x_21306 x_213055558  Instruction x_2170 > h_Instruction x_2170 5559  Comment x_2171 > h_Comment x_2171 5560  Cost x_2172 > h_Cost x_2172 5561  Jmp x_2173 > h_Jmp x_2173 5562  Jnz (x_2176, x_2175, x_2174) > h_Jnz x_2176 x_2175 x_2174 5563  Call x_2177 > h_Call x_2177 5564  Mov (x_2180, x_2179, x_2178) > h_Mov x_2180 x_2179 x_2178 5565 5565 5566 5566 (** val pseudo_instruction_inv_rect_Type4 : … … 5778 5778 Types.prod List.list > identifier > __ > __ > 'a1) > 5779 5779 pseudo_assembly_program > 'a1 **) 5780 let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_2 1431=5780 let rec pseudo_assembly_program_rect_Type4 h_mk_pseudo_assembly_program x_2304 = 5781 5781 let { preamble = preamble0; code = code0; renamed_symbols = 5782 renamed_symbols0; final_label = final_label0 } = x_2 14315782 renamed_symbols0; final_label = final_label0 } = x_2304 5783 5783 in 5784 5784 h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 … … 5790 5790 Types.prod List.list > identifier > __ > __ > 'a1) > 5791 5791 pseudo_assembly_program > 'a1 **) 5792 let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_2 1433=5792 let rec pseudo_assembly_program_rect_Type5 h_mk_pseudo_assembly_program x_2306 = 5793 5793 let { preamble = preamble0; code = code0; renamed_symbols = 5794 renamed_symbols0; final_label = final_label0 } = x_2 14335794 renamed_symbols0; final_label = final_label0 } = x_2306 5795 5795 in 5796 5796 h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 … … 5802 5802 Types.prod List.list > identifier > __ > __ > 'a1) > 5803 5803 pseudo_assembly_program > 'a1 **) 5804 let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_2 1435=5804 let rec pseudo_assembly_program_rect_Type3 h_mk_pseudo_assembly_program x_2308 = 5805 5805 let { preamble = preamble0; code = code0; renamed_symbols = 5806 renamed_symbols0; final_label = final_label0 } = x_2 14355806 renamed_symbols0; final_label = final_label0 } = x_2308 5807 5807 in 5808 5808 h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 … … 5814 5814 Types.prod List.list > identifier > __ > __ > 'a1) > 5815 5815 pseudo_assembly_program > 'a1 **) 5816 let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_2 1437=5816 let rec pseudo_assembly_program_rect_Type2 h_mk_pseudo_assembly_program x_2310 = 5817 5817 let { preamble = preamble0; code = code0; renamed_symbols = 5818 renamed_symbols0; final_label = final_label0 } = x_2 14375818 renamed_symbols0; final_label = final_label0 } = x_2310 5819 5819 in 5820 5820 h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 … … 5826 5826 Types.prod List.list > identifier > __ > __ > 'a1) > 5827 5827 pseudo_assembly_program > 'a1 **) 5828 let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_2 1439=5828 let rec pseudo_assembly_program_rect_Type1 h_mk_pseudo_assembly_program x_2312 = 5829 5829 let { preamble = preamble0; code = code0; renamed_symbols = 5830 renamed_symbols0; final_label = final_label0 } = x_2 14395830 renamed_symbols0; final_label = final_label0 } = x_2312 5831 5831 in 5832 5832 h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 … … 5838 5838 Types.prod List.list > identifier > __ > __ > 'a1) > 5839 5839 pseudo_assembly_program > 'a1 **) 5840 let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_2 1441=5840 let rec pseudo_assembly_program_rect_Type0 h_mk_pseudo_assembly_program x_2314 = 5841 5841 let { preamble = preamble0; code = code0; renamed_symbols = 5842 renamed_symbols0; final_label = final_label0 } = x_2 14415842 renamed_symbols0; final_label = final_label0 } = x_2314 5843 5843 in 5844 5844 h_mk_pseudo_assembly_program preamble0 code0 __ renamed_symbols0 … … 5937 5937 (Types.pi1 5938 5938 (FoldStuff.foldl_strong program (fun prefix v tl _ i_mem > 5939 (let { Types.fst = i; Types.snd = mem } = Types.pi1 i_mem in 5940 (fun _ > { Types.fst = (Nat.S i); Types.snd = 5939 (let { Types.fst = eta24568; Types.snd = mem } = Types.pi1 i_mem in 5940 (fun _ > 5941 (let { Types.fst = i; Types.snd = bvi } = eta24568 in 5942 (fun _ > { Types.fst = { Types.fst = (Nat.S i); Types.snd = 5943 (Arithmetic.increment (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 5944 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 5945 Nat.O)))))))))))))))) bvi) }; Types.snd = 5941 5946 (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 5942 5947 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 5943 Nat.O)))))))))))))))) 5944 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S5945 (Nat.S(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S5946 (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem) })) __) { Types.fst =5947 Nat.O; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S(Nat.S5948 Nat.O)))))))))))))))) bvi v mem) })) __)) __) { Types.fst = 5949 { Types.fst = Nat.O; Types.snd = 5950 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 5951 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 5952 Nat.O))))))))))))))))) }; Types.snd = (BitVectorTrie.Stub (Nat.S 5948 5953 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 5949 (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd5954 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd 5950 5955 5951 5956 (** val load_code_memory : … … 5968 5973 costlabel_map > symboltable_type > BitVector.word > __ > 'a1) > 5969 5974 labelled_object_code > 'a1 **) 5970 let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_2 1457=5975 let rec labelled_object_code_rect_Type4 h_mk_labelled_object_code x_2330 = 5971 5976 let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = 5972 symboltable0; final_pc = final_pc0 } = x_2 14575977 symboltable0; final_pc = final_pc0 } = x_2330 5973 5978 in 5974 5979 h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ … … 5978 5983 costlabel_map > symboltable_type > BitVector.word > __ > 'a1) > 5979 5984 labelled_object_code > 'a1 **) 5980 let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_2 1459=5985 let rec labelled_object_code_rect_Type5 h_mk_labelled_object_code x_2332 = 5981 5986 let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = 5982 symboltable0; final_pc = final_pc0 } = x_2 14595987 symboltable0; final_pc = final_pc0 } = x_2332 5983 5988 in 5984 5989 h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ … … 5988 5993 costlabel_map > symboltable_type > BitVector.word > __ > 'a1) > 5989 5994 labelled_object_code > 'a1 **) 5990 let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_2 1461=5995 let rec labelled_object_code_rect_Type3 h_mk_labelled_object_code x_2334 = 5991 5996 let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = 5992 symboltable0; final_pc = final_pc0 } = x_2 14615997 symboltable0; final_pc = final_pc0 } = x_2334 5993 5998 in 5994 5999 h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ … … 5998 6003 costlabel_map > symboltable_type > BitVector.word > __ > 'a1) > 5999 6004 labelled_object_code > 'a1 **) 6000 let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_2 1463=6005 let rec labelled_object_code_rect_Type2 h_mk_labelled_object_code x_2336 = 6001 6006 let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = 6002 symboltable0; final_pc = final_pc0 } = x_2 14636007 symboltable0; final_pc = final_pc0 } = x_2336 6003 6008 in 6004 6009 h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ … … 6008 6013 costlabel_map > symboltable_type > BitVector.word > __ > 'a1) > 6009 6014 labelled_object_code > 'a1 **) 6010 let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_2 1465=6015 let rec labelled_object_code_rect_Type1 h_mk_labelled_object_code x_2338 = 6011 6016 let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = 6012 symboltable0; final_pc = final_pc0 } = x_2 14656017 symboltable0; final_pc = final_pc0 } = x_2338 6013 6018 in 6014 6019 h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ … … 6018 6023 costlabel_map > symboltable_type > BitVector.word > __ > 'a1) > 6019 6024 labelled_object_code > 'a1 **) 6020 let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_2 1467=6025 let rec labelled_object_code_rect_Type0 h_mk_labelled_object_code x_2340 = 6021 6026 let { oc = oc0; cm = cm0; costlabels = costlabels0; symboltable = 6022 symboltable0; final_pc = final_pc0 } = x_2 14676027 symboltable0; final_pc = final_pc0 } = x_2340 6023 6028 in 6024 6029 h_mk_labelled_object_code oc0 cm0 __ costlabels0 symboltable0 final_pc0 __ 
src/ASM/ASM.ma
r3082 r3104 1177 1177 (foldl_strong ? 1178 1178 (λprefix. 1179 Σres: nat × (BitVectorTrie Byte 16).1180 let 〈i, mem〉 ≝ res in1181 i = prefix ∧ 1179 Σres: nat × Word × (BitVectorTrie Byte 16). 1180 let 〈i,bvi,mem〉 ≝ res in 1181 i = prefix ∧ bvi = bitvector_of_nat … i ∧ 1182 1182 (i ≤ 2^16 → 1183 1183 ∀pc. ∀pc_ok: pc < prefix. … … 1185 1185 program 1186 1186 (λprefix,v,tl,prf,i_mem. 1187 let 〈i,mem〉 ≝ i_mem in 1188 〈S i,insert … (bitvector_of_nat … i) v mem〉) 1189 〈0,Stub Byte 16〉). 1190 [3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2 1191  % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …)) 1192  cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H H #H1 #H2 % 1193 [ >length_append >H1 normalize // 1187 let 〈i,bvi,mem〉 ≝ i_mem in 1188 〈S i,increment … bvi,insert … bvi v mem〉) 1189 〈0,zero ?,Stub Byte 16〉). 1190 [3: cases (foldl_strong ? (λprefix.Σres.?) ???) ** #i #bvi #mem ** #H1 #H3 >H1 #H2 @H2 1191  % // % // (*#_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))*) 1192  cases i_mem in p; ** #i' #bvi' #mem' normalize nodelta #H #EQ destruct(EQ) 1193 cases H H * #H1 #H3 #H2 destruct (p1) % 1194 [ % [ >length_append >H1 normalize // 1195  >increment_zero_bitvector_of_nat_1 >H3 <add_bitvector_of_nat % ] 1194 1196  #LE #pc #pc_ok 1195 1197 cases (le_to_or_lt_eq … pc_ok) … … 1198 1200 #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?); 1199 1201 <H1 <plus_n_O whd in ⊢ (???%); // 1200  >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/] 1202  >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix 1203 [2: /2 by lt_plus_to_lt_l/] 1201 1204 >H2 [2: @(transitive_le … LE) //] 1202 1205 cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ 1203 whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false % 1206 whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false % >H3 1204 1207 #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption 1205 1208 @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]] 
src/ASM/Assembly.ma
r3076 r3104 855 855 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in 856 856 let lookup_datalabels ≝ λx. 857 match lookup ASMTag … (construct_datalabels preamble)x with857 match lookup ASMTag … datalabels x with 858 858 [ Some addr ⇒ 〈XData, addr〉 859 859  None ⇒ 〈Code, lookup_labels x〉
Note: See TracChangeset
for help on using the changeset viewer.