Changeset 1283 for src/joint

Timestamp:

Sep 30, 2011, 3:12:40 AM (9 years ago)

Author:

sacerdot

Message:

Bad programming practice removed: change_label is no longer required and
add_graph now takes function from label to statements in place of taking
statements containing a wrong label to be fixed.

File:

• src/joint/TranslateUtils.ma (modified) (2 diffs)

src/joint/TranslateUtils.ma

@@ -39 +39 @@
     fresh LabelTag (joint_if_luniverse … def).
 
-definition change_label ≝
-  λpars1,globals.λe: joint_statement (graph_params pars1 globals) globals.λl.
-  match e with
-  [ GOTO _ ⇒ GOTO … l
-  | RETURN ⇒ RETURN ??
-  | sequential instr _ ⇒ sequential … globals instr l].
-
-(*CSC: bad programming habit: the code below puts everywhere a fake
-  label and then adds_graph fixes them *)
-(*CSC: this is just an instance of add_translates below! *)
 let rec adds_graph
   (pars1: params1) (globals: list ident)
-  (stmt_list: list (joint_statement (graph_params_ pars1) globals))
+  (stmt_list: list (label → joint_statement (graph_params_ pars1) globals))
   (start_lbl: label) (dest_lbl: label)
   (def: joint_internal_function … (graph_params pars1 globals))
@@ -59 +49 @@
   | cons stmt stmt_list ⇒
     match stmt_list with
-    [ nil ⇒ add_graph … start_lbl (change_label … stmt dest_lbl) def
+    [ nil ⇒ add_graph … start_lbl (stmt dest_lbl) def
     | _ ⇒
       let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
-      let stmt ≝ change_label … stmt tmp_lbl in
-      let def ≝ add_graph … start_lbl stmt def in
+      let def ≝ add_graph … start_lbl (stmt tmp_lbl) def in
         adds_graph pars1 globals stmt_list tmp_lbl dest_lbl def]].
 
-(*CSC: bad programming habit: the code below puts everywhere a fake
-  label and then adds_graph fixes them *)
 let rec add_translates
   (pars1: params1) (globals: list ident)