Changeset 1063 for src/RTLabs/RTLAbstoRTL.ma
 Timestamp:
 Jul 11, 2011, 5:52:11 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1062 r1063 73 73 ]. 74 74 75 axiom fresh_regs_length: 76 ∀def: rtl_internal_function. 77 ∀n: nat. 78 (\snd (fresh_regs def n)) = n. 79 75 80 definition addr_regs ≝ 76 81 λregs. … … 487 492 λsrcrs1. 488 493 λsrcrs2. 494 λprf: srcrs1 = srcrs2. 489 495 λstart_lbl. 490 496 λdest_lbl. 491 497 λdef. 492 λprf: srcrs1 = srcrs2.493 498 match reduce_strong ? srcrs1 srcrs2 with 494 499 [ dp reduced first_reduced_proof ⇒ … … 586 591 λdestrs: list register. 587 592 λtmp_destrs: list register. 593 λdestrs_prf: destrs = tmp_destrs. 588 594 λsrcrs1: list register. 589 595 λdummy_lbl: label. 590 596 λ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]) 597 λi_prf. 598 λtranslates: list ?. 599 λsrcr2i: register. 600 let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in 601 let tmp_destrs2' ≝ 602 match tmp_destrs2 with 603 [ nil ⇒ [ ] 604  cons tmp_destr2 tmp_destrs2 ⇒ [ 605 adds_graph [ 606 rtl_st_clear_carry dummy_lbl; 607 rtl_st_int tmp_destr2 (zero ?) dummy_lbl 608 ]; 609 translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i; 610 translate_cst (Ointconst I8 (zero ?)) tmp_destrs1; 611 adds_graph [ 612 rtl_st_clear_carry dummy_lbl 613 ]; 614 translate_op Addc destrs destrs tmp_destrs destrs_prf 615 ] 616 ] 617 in 618 translates @ tmp_destrs2'. 619 620 definition translate_mul ≝ 621 λdestrs: list register. 622 λsrcrs1: list register. 623 λsrcrs2: list register. 624 λstart_lbl: label. 625 λdest_lbl: label. 626 λdef: rtl_internal_function. 627 let 〈def, dummy〉 ≝ fresh_reg def in 628 let 〈def, tmpr〉 ≝ fresh_reg def in 629 let 〈def, tmp_destrs〉 ≝ fresh_regs def (destrs) in 630 let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (srcrs1) in 631 let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (srcrs2) in 632 let insts_init ≝ [ 633 translate_move fresh_srcrs1 srcrs1; 634 translate_move fresh_srcrs2 srcrs2; 635 translate_cst (Ointconst I8 (zero ?)) destrs 636 ] 637 in 638 let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in 639 let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init. 640 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def. 641 642 let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def = 643 let (def, dummy) = fresh_reg def in 644 let (def, tmpr) = fresh_reg def in 645 let (def, tmp_destrs) = fresh_regs def (List.length destrs) in 646 let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in 647 let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in 648 let insts_init = 649 [translate_move fresh_srcrs1 srcrs1 ; 650 translate_move fresh_srcrs2 srcrs2 ; 651 translate_cst (AST.Cst_int 0) destrs] in 652 let f = λi. translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl i ? in 653 let insts_mul = MiscPottier.foldi f [] srcrs2 in 654 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def 608 655 609 656 definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.