Changeset 1250 for src/RTL/RTLtoERTL.ma

Timestamp:

Sep 22, 2011, 12:02:35 PM (10 years ago)

Author:

sacerdot

Message:

1. Sigma types projections moved to utilities/extralib.ma
2. Extended statement turned into extended instructions, decreasing the amount of code in the translations

File:

• src/RTL/RTLtoERTL.ma (modified) (1 diff)

src/RTL/RTLtoERTL.ma

@@ -3 +3 @@
 include "common/Identifiers.ma".
 include "ERTL/ERTL.ma".
+include "utilities/extralib.ma". (* CSC: Only for Sigma type projections *)
                       
 definition add_graph ≝
-  λl: label.
-  λstmt.
-  λp.
-  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
-  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
-  let ertl_if_params' ≝ ertl_if_params p in
-  let ertl_if_locals' ≝ ertl_if_locals p in
-  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
-  let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
-  let ertl_if_entry' ≝ ertl_if_entry p in
-  let ertl_if_exit' ≝ ertl_if_exit p in
-    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
-                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
-                              ertl_if_graph' ? ?.
+  λglobals.λl: label.λstmt.λp: joint_internal_function … (ertl_params globals).
+   let code ≝ add … (joint_if_code … p) l stmt in
+    mk_joint_internal_function … (ertl_params globals)
+     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
+     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
+     code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
   normalize nodelta;
-  [1: generalize in match ertl_if_entry';
-      #HYP
-      cases HYP
-      #LBL #LBL_PRF
-      %
-      [1: @LBL
-      |2: @graph_add_lookup
-          @LBL_PRF
-      ]
-  |2: generalize in match ertl_if_exit';
-      #HYP
-      cases HYP
-      #LBL #LBL_PRF
-      %
-      [1: @LBL
-      |2: @graph_add_lookup
-          @LBL_PRF
-      ]
-  ]
+  [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
+  #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
 qed.
                            
 definition fresh_label ≝
-  λdef.
-    fresh LabelTag (ertl_if_luniverse def).
+  λglobals.λdef: joint_internal_function … (ertl_params globals).
+    fresh LabelTag (joint_if_luniverse … def).
     
 definition change_label ≝
-  λl.
-  λe: ertl_statement.
+  λglobals.λe: joint_statement ertl_params_ globals.λl.
   match e with
-  [ ertl_st_skip _ ⇒ ertl_st_skip l
+  [ joint_st_goto _ ⇒ joint_st_goto … l
+  | joint_st_return ⇒ joint_st_return …
+  | joint_st_sequential instr _ ⇒ joint_st_sequential … instr l
+  | joint_st_extension ].
   | ertl_st_comment s _ ⇒ ertl_st_comment s l
   | ertl_st_cost c _ ⇒ ertl_st_cost c l