Changeset 1284 for src/joint

Timestamp:

Oct 3, 2011, 8:35:23 AM (8 years ago)

Author:

sacerdot

Message:

Bugs fixed: fresh_label changes the label universe, but this was not propagated
correctly. Fixed in RTLtoERTL. To be fixed in RTLAbsToRTL and (maybe) in
ERTLtoRTL.

File:

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

src/joint/TranslateUtils.ma

@@ -35 +35 @@
 qed.
 
-definition fresh_label ≝
-  λglobals,params. λdef: joint_internal_function globals params.
-    fresh LabelTag (joint_if_luniverse … def).
-
-let rec adds_graph
-  (pars1: params1) (globals: list ident)
-  (stmt_list: list (label → joint_statement (graph_params_ pars1) globals))
-  (start_lbl: label) (dest_lbl: label)
-  (def: joint_internal_function … (graph_params pars1 globals))
-    on stmt_list ≝
-  match stmt_list with
-  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
-  | cons stmt stmt_list ⇒
-    match stmt_list with
-    [ nil ⇒ add_graph … start_lbl (stmt dest_lbl) def
-    | _ ⇒
-      let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
-      let def ≝ add_graph … start_lbl (stmt tmp_lbl) def in
-        adds_graph pars1 globals stmt_list tmp_lbl dest_lbl def]].
+definition fresh_label:
+ ∀pars0,globals. joint_internal_function … (graph_params pars0 globals) → label × (joint_internal_function … (graph_params pars0 globals)) ≝
+  λpars0,globals,def.
+    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
+     〈r,set_luniverse … def luniverse〉.
 
 let rec add_translates
@@ -66 +52 @@
     [ nil ⇒ trans start_lbl dest_lbl def
     | _ ⇒
-      let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
+      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
       let def ≝ trans start_lbl tmp_lbl def in
         add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
+
+definition adds_graph ≝
+ λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
+  add_translates … (map … (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).