 Timestamp:
 Oct 6, 2011, 11:19:25 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1296 r1306 508 508 ] 509 509 in 510 let f ≝ λi. translate_muli globals dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ?in511 let insts_mul ≝ foldi … [ ] srcrs2 in ?. [5: check insts_init.510 let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in 511 let insts_mul ≝ foldi … f [ ] srcrs2 in ?. 512 512 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def. 513 513 *) … … 680 680 λglobals: list ident. 681 681 λdestrs: list register. 682 λprf_destrs: lt 0 (destrs).682 λprf_destrs: 0 < destrs. 683 683 λsrcrs1: list register. 684 684 λsrcrs2: list register. … … 748 748 λglobals: list ident. 749 749 λdestrs: list register. 750 λdestrs_prf: lt 0 (destrs).750 λdestrs_prf: 0 < destrs. 751 751 λsrcrs1: list register. 752 752 λsrcrs2: list register. … … 786 786 λop2. 787 787 λdestrs: list register. 788 λdestrs_prf: lt 0 (destrs).788 λdestrs_prf: 0 < destrs. 789 789 λsrcrs1: list register. 790 790 λsrcrs2: list register. 791 λsrcrs1_prf: lt 0 (srcrs1). (*can this be relaxed? i think it can792 but we need more dep. typ. in modu/divu793 cases *)794 λsrcrs2_prf: lt 0 (srcrs2).791 λsrcrs1_prf: 0 < srcrs1. (* XXX: can this be relaxed? i think it can 792 but we need more dep. typ. in modu/divu 793 cases *) 794 λsrcrs2_prf: 0 < srcrs2. 795 795 λstart_lbl: label. 796 796 λdest_lbl: label. … … 988 988 sequential rtl_params_ globals (INT rtl_params_ globals tmpr off) 989 989 ]; 990 translate_op2 globals Oaddp tmp_addr ?addr [tmpr] ? ?;990 translate_op2 globals Oaddp tmp_addr … addr [tmpr] ? ?; 991 991 adds_graph rtl_params1 globals [ 992 992 sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr) … … 997 997 〈translates, result〉 998 998 in 999 let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero ?〉 srcrs in999 let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero …〉 srcrs in 1000 1000 add_translates rtl_params1 globals translates start_lbl dest_lbl def 1001 1001 ]. … … 1028 1028 translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def 1029 1029  St_op2 op2 destr srcr1 srcr2 lbl' ⇒ 1030 translate_op2 globals op2 (find_local_env destr lenv) …(find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def1030 translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def 1031 1031  St_load ignore addr destr lbl' ⇒ 1032 translate_load globals (find_local_env addr lenv) …(find_local_env destr lenv) lbl lbl' def1032 translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def 1033 1033  St_store ignore addr srcr lbl' ⇒ 1034 translate_store globals (find_local_env addr lenv) …(find_local_env srcr lenv) lbl lbl' def1034 translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def 1035 1035  St_call_id f args retr lbl' ⇒ 1036 1036 match retr with
Note: See TracChangeset
for help on using the changeset viewer.