Changeset 2917
 Timestamp:
 Mar 20, 2013, 1:20:48 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL.ma
r2916 r2917 1 if eqb offset 0 then [ ] else 1 2 include "RTLabs/RTLabs_syntax.ma". 2 3 include "RTL/RTL.ma". … … 205 206 ∀srcrs2 : list psd_argument. 206 207 dests = srcrs1 → srcrs1 = srcrs2 → 207 bind_new register (list (joint_seq RTL globals))208 list (joint_seq RTL globals) 208 209 ≝ 209 210 λglobals: list ident. … … 270 271 definition translate_op_asym_unsigned : 271 272 ∀globals.Op2 → list register → list psd_argument → list psd_argument → 272 bind_new register (list (joint_seq RTL globals)) ≝273 list (joint_seq RTL globals) ≝ 273 274 λglobals,op,destrs,srcrs1,srcrs2. 274 275 let l ≝ destrs in … … 302 303  _ ⇒ True 303 304 ]. 304 305 305 306 definition translate_cst : 306 307 ∀ty. … … 320 321  Oaddrsymbol id offset ⇒ λcst_prf,prf. 321 322 let 〈r1, r2〉 ≝ make_addr … destrs ? in 322 [ADDRESS RTL globals id ? r1 r2 ; 323 r1 ← r1 .Add. byte_of_nat … offset ; 324 r2 ← r2 .Addc. zero_byte ] 323 ADDRESS RTL globals id ? r1 r2 :: 324 if eqb offset 0 then [ ] else 325 translate_op … Add 326 [r1 ; r2 ] [ r1 ; r2 ] [ byte_of_nat … offset ; zero_byte ] 327 (refl …) (refl …) 325 328  Oaddrstack offset ⇒ λcst_prf,prf. 326 329 let 〈r1, r2〉 ≝ make_addr … destrs ? in 327 [(rtl_stack_address r1 r2 : joint_seq RTL globals); 328 r1 ← r1 .Add. byte_of_nat … offset ; 329 r2 ← r2 .Addc. zero_byte ] 330 (rtl_stack_address r1 r2 : joint_seq RTL globals) :: 331 if eqb offset 0 then [ ] else 332 translate_op … Add 333 [r1 ; r2 ] [ r1 ; r2 ] [ byte_of_nat … offset ; zero_byte ] 334 (refl …) (refl …) 330 335 ] (pi2 … cst_sig). 331 336 @hide_prf … … 479 484 map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf. 480 485 481 definition translate_negint : ∀globals.? → ? → ? → bind_new register (list (joint_seq RTL globals)) ≝486 definition translate_negint : ∀globals.? → ? → ? → list (joint_seq RTL globals) ≝ 482 487 λglobals: list ident. 483 488 λdestrs: list register. 484 489 λsrcrs: list register. 485 490 λprf: destrs = srcrs. (* assert in caml code *) 486 translate_notint … destrs srcrs prf @ @491 translate_notint … destrs srcrs prf @ 487 492 translate_op ? Add destrs (map … (Reg ?) destrs) (one_args (destrs)) ??. 488 493 @hide_prf … … 567 572 (Σi.i<S k) → 568 573 (* the accumulator *) 569 bind_new register (list (joint_seq RTL globals)) →570 bind_new register (list (joint_seq RTL globals)) ≝574 list (joint_seq RTL globals) → 575 list (joint_seq RTL globals) ≝ 571 576 λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2, 572 577 tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc. … … 589 594 let tmp_destrs_view : list register ≝ 590 595 ltl ? tmp_destrs_dummy k in 591 [❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k  i) srcrs2 ?)] @ @592 translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @ @596 [❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k  i) srcrs2 ?)] @ 597 translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @ 593 598 acc 594 599 ]. … … 625 630 (* the step calculating all products with least significant byte going in the 626 631 kth position of the result *) 627 let translate_mul_k : (Σk.k<destrs) → bind_new register (list (joint_seq RTL globals)) →628 bind_new register (list (joint_seq RTL globals)) ≝632 let translate_mul_k : (Σk.k<destrs) → list (joint_seq RTL globals) → 633 list (joint_seq RTL globals) ≝ 629 634 λk_sig,acc.match k_sig with 630 635 [ mk_Sig k k_prf ⇒ … … 635 640 (* initializing tmp_destrs to zero 636 641 dummy is intentionally uninitialized *) 637 translate_fill_with_zero … tmp_destrs @ @642 translate_fill_with_zero … tmp_destrs @ 638 643 (* the main body, roughly: 639 644 for k in 0 ... n1 do 640 645 for i in 0 ... k do 641 646 translate_mul_i … k … i *) 642 foldr … translate_mul_k [ ] (range_strong (destrs)) @ @647 foldr … translate_mul_k [ ] (range_strong (destrs)) @ 643 648 (* epilogue: saving the result *) 644 649 translate_move … destrs (map … (Reg ?) tmp_destrs) ?.
Note: See TracChangeset
for help on using the changeset viewer.