Changeset 2162 for src/RTLabs


Ignore:
Timestamp:
Jul 6, 2012, 5:53:01 PM (7 years ago)
Author:
tranquil
Message:
  • yet another correction to joint
  • added functions adding prologues and epilogues in TranslateUtils?. Adding a prologue will preserve the invariant of having a cost label at the start of the function, without needing transformations later
  • redefined ERTL and rewritten RTLToERTL (with suffix "_paolo")
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r2155 r2162  
    743743      λr. tmpr ← tmpr .Or. r in
    744744    bret … 〈MOVE rtl_params globals 〈tmpr,srcr〉 ::
    745     map ?? f srcrs', (COND ? tmpr lbl_true : joint_step ??) 〉
     745    map ?? f srcrs', (COND tmpr lbl_true : joint_step ??) 〉
    746746  ].
    747747
     
    815815    ❬(match retr with
    816816      [ Some retr ⇒
    817         CALL_ID rtl_params f (rtl_args args lenv ?) (find_local_env retr lenv ?)
     817        CALL_ID rtl_params ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
    818818      | None ⇒
    819         CALL_ID rtl_params f (rtl_args args lenv ?) [ ]
     819        CALL_ID rtl_params ? f (rtl_args args lenv ?) [ ]
    820820      ] : bind_seq_block ???), lbl'❭
    821821  | St_call_ptr f args retr lbl' ⇒
Note: See TracChangeset for help on using the changeset viewer.