Changeset 347 for Deliverables/D4.1/Matita/Interpret.ma
 Timestamp:
 Nov 30, 2010, 6:13:00 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Interpret.ma
r343 r347 10 10 λb. 11 11 zero eight @@ b. 12 13 naxiom daemon: False. 12 14 13 15 ndefinition execute_1: Status → Status ≝ … … 395 397 ] (subaddressing_modein … addr) 396 398  MOVC addr1 addr2 ⇒ 397 match addr2 return λx. bool_to_Prop (is_in [[ acc_dptr; acc_pc ]] x) → ? with 398 [ ACC_DPTR ⇒ λacc_dptr: True. ? 399  ACC_PC ⇒ λacc_pc: True. ? 400  _ ⇒ λother: False. ? 401 ] (subaddressing_modein … ?) 399 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with 400 [ ACC_DPTR ⇒ λacc_dptr: True. 401 let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in 402 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 403 let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in 404 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in 405 set_8051_sfr s SFR_ACC_A result 406  ACC_PC ⇒ λacc_pc: True. 407 let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in 408 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat sixteen one) in 409 (* DPM: Under specified: does the carry from PC incrementation affect the *) 410 (* addition of the PC with the DPTR? At the moment, no. *) 411 let s ≝ set_program_counter s inc_pc in 412 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in 413 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in 414 set_8051_sfr s SFR_ACC_A result 415  _ ⇒ λother: False. ? 416 ] (subaddressing_modein … addr2) 417  MOVX addr ⇒ 418 (* DPM: only copies  doesn't affect I/O *) 419 match addr with 420 [ Left l ⇒ 421 let 〈addr1, addr2〉 ≝ l in 422 set_arg_8 s addr1 (get_arg_8 s false addr2) 423  Right r ⇒ 424 let 〈addr1, addr2〉 ≝ r in 425 set_arg_8 s addr1 (get_arg_8 s false addr2) 426 ] 427  MOV addr ⇒ 428 match addr with 429 [ Left l ⇒ 430 match l with 431 [ Left l' ⇒ 432 match l' with 433 [ Left l'' ⇒ 434 match l'' with 435 [ Left l''' ⇒ 436 match l''' with 437 [ Left l'''' ⇒ 438 let 〈addr1, addr2〉 ≝ l'''' in 439 set_arg_8 s addr1 (get_arg_8 s false addr2) 440  Right r'''' ⇒ 441 let 〈addr1, addr2〉 ≝ r'''' in 442 set_arg_8 s addr1 (get_arg_8 s false addr2) 443 ] 444  Right r''' ⇒ 445 let 〈addr1, addr2〉 ≝ r''' in 446 set_arg_8 s addr1 (get_arg_8 s false addr2) 447 ] 448  Right r'' ⇒ 449 let 〈addr1, addr2〉 ≝ r'' in 450 set_arg_16 s (get_arg_16 s addr2) addr1 451 ] 452  Right r ⇒ 453 let 〈addr1, addr2〉 ≝ r in 454 set_arg_1 s addr1 (get_arg_1 s addr2 false) 455 ] 456  Right r ⇒ 457 let 〈addr1, addr2〉 ≝ r in 458 set_arg_1 s addr1 (get_arg_1 s addr2 false) 459 ] 460  LCALL addr ⇒ 461 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 462 [ ADDR16 a ⇒ λaddr16: True. 463 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in 464 let s ≝ set_8051_sfr s SFR_SP new_sp in 465 let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in 466 let s ≝ write_at_stack_pointer s pc_bl in 467 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in 468 let s ≝ set_8051_sfr s SFR_SP new_sp in 469 let s ≝ write_at_stack_pointer s pc_bu in 470 set_program_counter s a 471  _ ⇒ λother: False. ? 472 ] (subaddressing_modein … addr) 473  ACALL addr ⇒ 474 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 475 [ ADDR11 a ⇒ λaddr11: True. 476 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in 477 let s ≝ set_8051_sfr s SFR_SP new_sp in 478 let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in 479 let s ≝ write_at_stack_pointer s pc_bl in 480 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in 481 let s ≝ set_8051_sfr s SFR_SP new_sp in 482 let s ≝ write_at_stack_pointer s pc_bu in 483 let 〈thr, eig〉 ≝ split ? three eight a in 484 let 〈fiv, thr'〉 ≝ split ? five three pc_bu in 485 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 486 set_program_counter s new_addr 487  _ ⇒ λother: False. ? 488 ] (subaddressing_modein … addr) 402 489  NOP ⇒ s 403  _ ⇒ s404 490 ] 405 491 in 406 492 s. 493 ncases daemon; 494 nqed. 495 496 nlet rec execute (n: Nat) (s: Status) on n: Status ≝ 497 match n with 498 [ Z ⇒ s 499  S o ⇒ execute o (execute_1 s) 500 ].
Note: See TracChangeset
for help on using the changeset viewer.