Changeset 1331 for src/RTLabs
- Timestamp:
- Oct 10, 2011, 10:21:35 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL.ma
r1325 r1331 539 539 translates @ tmp_destrs2'. 540 540 541 (* 541 axiom foldi_strong: 542 ∀a: Type[0]. 543 ∀b: Type[0]. 544 ∀the_list: list b. 545 ∀f: ∀n: nat. n ≤ |the_list| → a → b → a. 546 ∀seed: a. 547 a. 548 542 549 definition translate_mul ≝ 543 550 λglobals: list ident. … … 545 552 λsrcrs1: list register. 546 553 λsrcrs2: list register. 554 λregs_proof: |srcrs2| = |destrs|. 547 555 λstart_lbl: label. 548 556 λdest_lbl: label. … … 550 558 let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in 551 559 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 552 let 〈def, tmp_destrs〉 ≝ fresh_regs rtl_params0 globals def (|destrs|) in 553 let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in 554 let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in 555 let insts_init ≝ [ 556 translate_move globals fresh_srcrs1 srcrs1; 557 translate_move globals fresh_srcrs2 srcrs2; 558 translate_cst globals (Ointconst I8 (zero …)) destrs 559 ] 560 in 561 let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in 562 let insts_mul ≝ foldi … f [ ] srcrs2 in ?. 563 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def. 564 *) 565 566 axiom translate_mul: 567 ∀globals: list ident. 568 ∀destrs: list register. 569 ∀srcrs1: list register. 570 ∀srcrs2: list register. 571 ∀start_lbl: label. 572 ∀dest_lbl: label. 573 ∀def: rtl_internal_function globals. 574 rtl_internal_function globals. 560 match fresh_regs_strong rtl_params0 globals def (|destrs|) with 561 [ dp def_tmp_destrs tmp_destrs_prf ⇒ 562 let def ≝ \fst def_tmp_destrs in 563 let tmp_destrs ≝ \snd def_tmp_destrs in 564 let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in 565 let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in 566 let insts_init ≝ [ 567 translate_move globals fresh_srcrs1 srcrs1; 568 translate_move globals fresh_srcrs2 srcrs2; 569 translate_cst globals (Ointconst I8 (zero …)) destrs 570 ] 571 in 572 let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in 573 let f' ≝ λi. λproof: i ≤ |srcrs2|. f i ? in 574 let insts_mul ≝ foldi_strong ? ? srcrs2 f' [ ] in 575 add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def 576 ]. 577 >tmp_destrs_prf 578 <regs_proof 579 assumption 580 qed. 575 581 576 582 definition translate_divumodu8 ≝ … … 853 859 but we need more dep. typ. in modu/divu 854 860 cases *) 855 λsrcrs2_prf: 0 < |srcrs2|.861 λsrcrs2_prf: |srcrs2| = |destrs|. 856 862 λstart_lbl: label. 857 863 λdest_lbl: label. … … 869 875 translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 870 876 | Omul ⇒ 871 translate_mul globals destrs srcrs1 srcrs2 start_lbl dest_lbl def877 translate_mul globals destrs srcrs1 srcrs2 ? start_lbl dest_lbl def 872 878 | Odivu ⇒ 873 879 match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with … … 959 965 | _ ⇒ ? (* assert false, implemented in run time or float op *) 960 966 ]. 961 [ 2,6: normalize in nil_absrd;967 [ 3,7: normalize in nil_absrd; 962 968 cases(not_le_Sn_O 0) 963 969 #HYP cases(HYP nil_absrd) 964 | 3,7,12,17,13,15,18,19,20,21,14,16: 970 | 4,8,19,20,21,22,17,18,24: 971 >srcrs2_prf 972 assumption 973 | 1,23: 965 974 assumption 966 975 | *: cases not_implemented (* yes, really *)
Note: See TracChangeset
for help on using the changeset viewer.