 Timestamp:
 Oct 10, 2011, 10:21:35 AM (8 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.