Changeset 1282 for src/RTLabs

Timestamp:

Sep 28, 2011, 11:50:32 PM (9 years ago)

Author:

sacerdot

Message:

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

File:

• src/RTLabs/RTLAbstoRTL.ma (modified) (5 diffs)

src/RTLabs/RTLAbstoRTL.ma

@@ -144 +144 @@
 
 definition translate_cst_int_internal ≝
-  λglobals,dest_lbl,r,i. joint_st_sequential rtl_params_ globals (joint_instr_int … r i) dest_lbl.
+  λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
 
 (*CSC: XXXXX *)
@@ -161 +161 @@
   λdestr: register.
   λsrcr: register.
-    joint_st_sequential rtl_params_ globals (joint_instr_move … 〈destr,srcr〉) start_lbl.
+    sequential rtl_params_ globals (MOVE … 〈destr,srcr〉) start_lbl.
 
 definition translate_move ≝
@@ -212 +212 @@
     add_translates … [
       adds_graph rtl_params1 … [
-        joint_st_sequential rtl_params_ … (joint_instr_int rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl
+        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl
         ];
       translate_move globals destrs zeros
@@ -1015 +1015 @@
   λdef: joint_internal_function … (rtl_params globals).
   match stmt with
-  [ St_skip lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
+  [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
   | _ ⇒ ? ].
 (*
@@ -1087 +1087 @@
   let entry' ≝ f_entry def in
   let exit' ≝ f_exit def in
-  let graph' ≝ add … (empty_map ? ?) entry' (joint_st_goto … entry') in
-  let graph' ≝ add … graph' exit' (joint_st_goto … exit') in
+  let graph' ≝ add … (empty_map ? ?) entry' (GOTO … entry') in
+  let graph' ≝ add … graph' exit' (GOTO … exit') in
   let res ≝
     mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'