Changeset 1306


Ignore:
Timestamp:
Oct 6, 2011, 11:19:25 AM (8 years ago)
Author:
mulligan
Message:

small changes to rtlabs. what axioms remain look hard to close. need to discuss with csc

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1296 r1306  
    508508  ]
    509509  in
    510   let f ≝ λi. translate_muli globals dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
    511   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 ?.
    512512    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
    513513*)
     
    680680  λglobals: list ident.
    681681  λdestrs: list register.
    682   λprf_destrs: lt 0 (|destrs|).
     682  λprf_destrs: 0 < |destrs|.
    683683  λsrcrs1: list register.
    684684  λsrcrs2: list register.
     
    748748  λglobals: list ident.
    749749  λdestrs: list register.
    750   λdestrs_prf: lt 0 (|destrs|).
     750  λdestrs_prf: 0 < |destrs|.
    751751  λsrcrs1: list register.
    752752  λsrcrs2: list register.
     
    786786  λop2.
    787787  λdestrs: list register.
    788   λdestrs_prf: lt 0 (|destrs|).
     788  λdestrs_prf: 0 < |destrs|.
    789789  λsrcrs1: list register.
    790790  λsrcrs2: list register.
    791   λsrcrs1_prf: lt 0 (|srcrs1|). (* can this be relaxed? i think it can
    792                                    but we need more dep. typ. in modu/divu
    793                                    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|.
    795795  λstart_lbl: label.
    796796  λdest_lbl: label.
     
    988988          sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
    989989        ];
    990         translate_op2 globals Oaddp tmp_addr ? addr [tmpr] ? ?;
     990        translate_op2 globals Oaddp tmp_addr addr [tmpr] ? ?;
    991991        adds_graph rtl_params1 globals [
    992992          sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr)
     
    997997          〈translates, result〉
    998998    in
    999     let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero ?〉 srcrs in
     999    let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero 〉 srcrs in
    10001000      add_translates rtl_params1 globals translates start_lbl dest_lbl def
    10011001  ].
     
    10281028    translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
    10291029  | 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' def
     1030    translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
    10311031  | St_load ignore addr destr lbl' ⇒
    1032     translate_load globals (find_local_env addr lenv) (find_local_env destr lenv) lbl lbl' def
     1032    translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
    10331033  | St_store ignore addr srcr lbl' ⇒
    1034     translate_store globals (find_local_env addr lenv) (find_local_env srcr lenv) lbl lbl' def
     1034    translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
    10351035  | St_call_id f args retr lbl' ⇒
    10361036    match retr with
Note: See TracChangeset for help on using the changeset viewer.