Changeset 2162 for src/RTLabs/RTLabsToRTL_paolo.ma

Timestamp:

Jul 6, 2012, 5:53:01 PM (8 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:

• src/RTLabs/RTLabsToRTL_paolo.ma (modified) (2 diffs)

src/RTLabs/RTLabsToRTL_paolo.ma

@@ -743 +743 @@
       λr. tmpr ← tmpr .Or. r in 
     bret … 〈MOVE rtl_params globals 〈tmpr,srcr〉 ::
-    map ?? f srcrs', (COND ? tmpr lbl_true : joint_step ??) 〉
+    map ?? f srcrs', (COND … tmpr lbl_true : joint_step ??) 〉
   ].
 
@@ -815 +815 @@
     ❬(match retr with
       [ Some retr ⇒
-        CALL_ID rtl_params f (rtl_args args lenv ?) (find_local_env retr lenv ?)
+        CALL_ID rtl_params ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
       | None ⇒
-        CALL_ID rtl_params f (rtl_args args lenv ?) [ ]
+        CALL_ID rtl_params ? f (rtl_args args lenv ?) [ ]
       ] : bind_seq_block ???), lbl'❭
   | St_call_ptr f args retr lbl' ⇒