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.