Changeset 325 for Deliverables
 Timestamp:
 Nov 26, 2010, 10:36:54 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Fetch.ma
r324 r325 18 18 let 〈b,v〉≝ head … v in if b then 19 19 let 〈b,v〉≝ head … v in if b then 20 〈〈MOV [[relative]]((Left ?? (Left ?? (Left ?? (Left ?? (Right ?? (? 〈REGISTER v,ACC_A〉))))))), pc〉, one〉20 〈〈MOV … ((Left ?? (Left ?? (Left ?? (Left ?? (Right ?? (? 〈REGISTER v,ACC_A〉))))))), pc〉, one〉 21 21 else 22 22 let 〈b,v〉≝ head … v in if b then … … 213 213 let 〈b,v〉≝ head … v in if b then 214 214 let 〈b,v〉≝ head … v in if b then 215 〈〈JMP [[relative]]INDIRECT_DPTR, pc〉, two〉215 〈〈JMP … INDIRECT_DPTR, pc〉, two〉 216 216 else 217 217 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U3 C (BIT_ADDR b1)), pc〉, two〉*) 218 218 else 219 ? (*let 〈b,v〉≝ head … v in if b then219 let 〈b,v〉≝ head … v in if b then 220 220 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉 221 221 else 222 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNZ [[relative]] (RELATIVE b1)), pc〉, two〉 *)223 else 224 ?(*let 〈b,v〉≝ head … v in if b then222 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNZ [[relative]] (RELATIVE b1)), pc〉, two〉 223 else 224 let 〈b,v〉≝ head … v in if b then 225 225 ?(*〈〈XRL(U1 ACC_A (REGISTER v)), pc〉, one〉*) 226 226 else … … 243 243 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉 244 244 else 245 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JZ [[relative]] (RELATIVE b1)), pc〉, two〉 *)245 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JZ [[relative]] (RELATIVE b1)), pc〉, two〉 246 246 else 247 ?(*let 〈b,v〉≝ head … v in if b then247 let 〈b,v〉≝ head … v in if b then 248 248 let 〈b,v〉≝ head … v in if b then 249 249 ?(*〈〈ANL (U1 ACC_A (REGISTER v)), pc〉, one〉*) … … 269 269 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNC [[relative]] (RELATIVE b1)), pc〉, two〉 270 270 else 271 ?(*let 〈b,v〉≝ head … v in if b then271 let 〈b,v〉≝ head … v in if b then 272 272 ?(*〈〈ORL (U1 ACC_A (REGISTER v)), pc〉, one〉*) 273 273 else … … 290 290 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉 291 291 else 292 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JC [[relative]] (RELATIVE b1)), pc〉, two〉 *)*)292 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JC [[relative]] (RELATIVE b1)), pc〉, two〉 293 293 else 294 294 let 〈b,v〉≝ head … v in if b then 295 295 let 〈b,v〉≝ head … v in if b then 296 296 let 〈b,v〉≝ head … v in if b then 297 〈〈ADDC [[relative]]ACC_A (REGISTER v), pc〉, one〉298 else 299 let 〈b,v〉≝ head … v in if b then 300 let 〈b,v〉≝ head … v in if b then 301 〈〈ADDC [[relative]]ACC_A (INDIRECT (from_singl … v)), pc〉, one〉297 〈〈ADDC … ACC_A (REGISTER v), pc〉, one〉 298 else 299 let 〈b,v〉≝ head … v in if b then 300 let 〈b,v〉≝ head … v in if b then 301 〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉 302 302 else 303 303 let 〈b,v〉≝ head … v in if b then … … 308 308 let 〈b,v〉≝ head … v in if b then 309 309 let 〈b,v〉≝ head … v in if b then 310 〈〈RLC [[relative]]ACC_A, pc〉, one〉310 〈〈RLC … ACC_A, pc〉, one〉 311 311 else 312 312 〈〈RETI …, pc〉, two〉 … … 342 342 let 〈b,v〉≝ head … v in if b then 343 343 let 〈b,v〉≝ head … v in if b then 344 〈〈DEC [[relative]](REGISTER v), pc〉, one〉345 else 346 let 〈b,v〉≝ head … v in if b then 347 let 〈b,v〉≝ head … v in if b then 348 〈〈DEC [[relative]](INDIRECT (from_singl … v)), pc〉, one〉344 〈〈DEC … (REGISTER v), pc〉, one〉 345 else 346 let 〈b,v〉≝ head … v in if b then 347 let 〈b,v〉≝ head … v in if b then 348 〈〈DEC … (INDIRECT (from_singl … v)), pc〉, one〉 349 349 else 350 350 let 〈b,v〉≝ head … v in if b then … … 355 355 let 〈b,v〉≝ head … v in if b then 356 356 let 〈b,v〉≝ head … v in if b then 357 〈〈RRC [[relative]]ACC_A, pc〉, one〉357 〈〈RRC … ACC_A, pc〉, one〉 358 358 else 359 359 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, two〉 360 360 else 361 361 let 〈b,v〉≝ head … v in if b then 362 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP [[relative]](ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉363 else 364 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]](JBC [[relative]] (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉362 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉 363 else 364 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JBC [[relative]] (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉 365 365 else 366 366 let 〈b,v〉≝ head … v in if b then … … 385 385 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉 386 386 else 387 〈〈NOP [[relative]], pc〉, one〉.387 〈〈NOP …, pc〉, one〉. 388 388 @. 389 389 nqed.
Note: See TracChangeset
for help on using the changeset viewer.