Changeset 1062 for src/RTLabs
- Timestamp:
- Jul 11, 2011, 2:09:03 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLAbstoRTL.ma
r1061 r1062 3 3 include "common/AssocList.ma". 4 4 include "common/Graphs.ma". 5 (* include "common/IntValue.ma". *)6 5 include "common/FrontEndOps.ma". 7 6 … … 463 462 λdest_lbl. 464 463 λdef. 465 λprf: | destrs | = | srcrs|.464 λprf: |destrs| = |srcrs|. 466 465 match op1 with 467 466 [ intermediate_op1_cast src_size src_sign dest_size ⇒ … … 523 522 ] 524 523 ]. 525 [ 1: @third_reduced_proof 526 | 3: @first_reduced_proof 527 528 let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def = 529 let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) = 530 MiscPottier.reduce srcrs1 srcrs2 in 531 let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in 532 let ((destrs_common, destrs_rest), _) = 533 MiscPottier.reduce destrs srcrs1_common in 534 let ((destrs_cted, destrs_rest), (srcrs_cted, _)) = 535 MiscPottier.reduce destrs_rest srcrs_rest in 536 let (def, tmpr) = fresh_reg def in 537 let insts_init = 538 [RTL.St_clear_carry start_lbl ; 539 RTL.St_int (tmpr, 0, start_lbl)] in 540 let f_add destr srcr1 srcr2 = 541 RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in 542 let insts_add = 543 MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in 544 let f_add_cted destr srcr = 545 RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in 546 let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in 547 let f_rest destr = 548 RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in 549 let insts_rest = List.map f_rest destrs_rest in 550 adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) 551 start_lbl dest_lbl def 524 cases not_implemented (* problem here with lengths of lists: possible bug? *) 525 qed. 526 527 let rec translate_mul1 528 (dummy: register) (tmpr: register) (destrs: list register) 529 (srcrs1: list register) (srcr2: register) (start_lbl: label) 530 on srcrs1 ≝ 531 match destrs with 532 [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl 533 | cons destr tl ⇒ 534 match tl with 535 [ nil ⇒ 536 match srcrs1 with 537 [ nil ⇒ 538 adds_graph [ 539 rtl_st_int tmpr (zero ?) start_lbl; 540 rtl_st_op2 Addc destr destr tmpr start_lbl 541 ] start_lbl 542 | cons srcr1 tl' ⇒ 543 adds_graph [ 544 rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl; 545 rtl_st_op2 Addc destr destr tmpr start_lbl 546 ] start_lbl 547 ] 548 | cons destr2 destrs ⇒ 549 match srcrs1 with 550 [ nil ⇒ 551 add_translates [ 552 adds_graph [ 553 rtl_st_int tmpr (zero ?) start_lbl; 554 rtl_st_op2 Addc destr destr tmpr start_lbl; 555 rtl_st_op2 Addc destr2 tmpr tmpr start_lbl 556 ]; 557 translate_cst (Ointconst I8 (zero ?)) destrs 558 ] start_lbl 559 | cons srcr1 srcrs1 ⇒ 560 match destrs with 561 [ nil ⇒ 562 add_translates [ 563 adds_graph [ 564 rtl_st_int tmpr (zero ?) start_lbl; 565 rtl_st_op2 Addc destr destr tmpr start_lbl; 566 rtl_st_op2 Addc destr2 tmpr tmpr start_lbl 567 ]; 568 translate_cst (Ointconst I8 (zero ?)) destrs 569 ] start_lbl 570 | cons destr2 destrs ⇒ 571 add_translates [ 572 adds_graph [ 573 rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl; 574 rtl_st_op2 Addc destr destr tmpr start_lbl 575 ]; 576 translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2 577 ] start_lbl 578 ] 579 ] 580 ] 581 ]. 582 583 definition translate_muli ≝ 584 λdummy: register. 585 λtmpr: register. 586 λdestrs: list register. 587 λtmp_destrs: list register. 588 λsrcrs1: list register. 589 λdummy_lbl: label. 590 λi: nat. 591 λtranslates. 592 λsrcr2i. 593 let 〈tmp_destrs1, tmp_destrs2〉 ≝ ? in ?. 594 595 let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates 596 srcr2i = 597 let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in 598 translates @ 599 (match tmp_destrs2 with 600 | [] -> [] 601 | tmp_destr2 :: tmp_destrs2 -> 602 [adds_graph [RTL.St_clear_carry dummy_lbl ; 603 RTL.St_int (tmp_destr2, 0, dummy_lbl)] ; 604 translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ; 605 translate_cst (AST.Cst_int 0) tmp_destrs1 ; 606 adds_graph [RTL.St_clear_carry dummy_lbl] ; 607 translate_op I8051.Addc destrs destrs tmp_destrs]) 552 608 553 609 definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.