Changeset 324 for Deliverables
 Timestamp:
 Nov 26, 2010, 10:29:58 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Fetch.ma
r323 r324 18 18 let 〈b,v〉≝ head … v in if b then 19 19 let 〈b,v〉≝ head … v in if b then 20 〈〈MOV ?((Left ?? (Left ?? (Left ?? (Left ?? (Right ?? (? 〈REGISTER v,ACC_A〉))))))), pc〉, one〉20 〈〈MOV [[relative]] ((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 … … 59 59 let 〈b,v〉≝ head … v in if b then 60 60 let 〈b,v〉≝ head … v in if b then 61 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (DJNZ …(REGISTER v) (RELATIVE b1)), pc〉, two〉61 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (DJNZ [[relative]] (REGISTER v) (RELATIVE b1)), pc〉, two〉 62 62 else 63 63 let 〈b,v〉≝ head … v in if b then … … 66 66 else 67 67 let 〈b,v〉≝ head … v in if b then 68 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (DJNZ …(DIRECT b1) (RELATIVE b2)), pc〉, two〉68 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (DJNZ [[relative]] (DIRECT b1) (RELATIVE b2)), pc〉, two〉 69 69 else 70 70 〈〈DA … ACC_A, pc〉, one〉 … … 155 155 let 〈b,v〉≝ head … v in if b then 156 156 let 〈b,v〉≝ head … v in if b then 157 〈〈SUBB … ACC_A (INDIRECT (from_sing g… v)), pc〉, one〉157 〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉 158 158 else 159 159 let 〈b,v〉≝ head … v in if b then … … 164 164 let 〈b,v〉≝ head … v in if b then 165 165 let 〈b,v〉≝ head … v in if b then 166 〈〈MOVC … ACC_A (ACC_ A_DPTR), pc〉, two〉166 〈〈MOVC … ACC_A (ACC_DPTR), pc〉, two〉 167 167 else 168 168 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U6 (BIT_ADDR b1) C), pc〉, two〉*) … … 187 187 let 〈b,v〉≝ head … v in if b then 188 188 let 〈b,v〉≝ head … v in if b then 189 〈〈MOVC … ACC_A (ACC_ A_PC), pc〉, two〉189 〈〈MOVC … ACC_A (ACC_PC), pc〉, two〉 190 190 else 191 191 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U3 C (BIT_ADDR b1)), pc〉, two〉*) … … 213 213 let 〈b,v〉≝ head … v in if b then 214 214 let 〈b,v〉≝ head … v in if b then 215 〈〈JMP … IND_DPTR, pc〉, two〉215 〈〈JMP [[relative]] 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 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 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〉*) … … 267 267 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉 268 268 else 269 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNC …(RELATIVE b1)), pc〉, two〉270 else 271 let 〈b,v〉≝ head … v in if b then269 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNC [[relative]] (RELATIVE b1)), pc〉, two〉 270 else 271 ?(*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 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 …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〉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〉 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 …ACC_A, pc〉, one〉310 〈〈RLC [[relative]] ACC_A, pc〉, one〉 311 311 else 312 312 〈〈RETI …, pc〉, two〉 … … 315 315 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉 316 316 else 317 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JNB (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉317 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JNB [[relative]] (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉 318 318 else 319 319 let 〈b,v〉≝ head … v in if b then … … 338 338 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉 339 339 else 340 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JB …(BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉340 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JB [[relative]] (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉 341 341 else 342 342 let 〈b,v〉≝ head … v in if b then 343 343 let 〈b,v〉≝ head … v in if b then 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〉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〉 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 …ACC_A, pc〉, one〉358 else 359 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 ( mk_word b1b2)), pc〉, two〉360 else 361 let 〈b,v〉≝ head … v in if b then 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 …(BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉357 〈〈RRC [[relative]] ACC_A, pc〉, one〉 358 else 359 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, two〉 360 else 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〉 365 365 else 366 366 let 〈b,v〉≝ head … v in if b then … … 380 380 〈〈RR … ACC_A, pc〉, one〉 381 381 else 382 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 ( mk_word b1b2)), pc〉, two〉382 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, two〉 383 383 else 384 384 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 …, pc〉, one〉.387 〈〈NOP [[relative]], pc〉, one〉. 388 388 @. 389 389 nqed.
Note: See TracChangeset
for help on using the changeset viewer.