Changeset 1283 for src/joint


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r1282 r1283  
    3939    fresh LabelTag (joint_if_luniverse … def).
    4040
    41 definition change_label ≝
    42   λpars1,globals.λe: joint_statement (graph_params pars1 globals) globals.λl.
    43   match e with
    44   [ GOTO _ ⇒ GOTO … l
    45   | RETURN ⇒ RETURN ??
    46   | sequential instr _ ⇒ sequential … globals instr l].
    47 
    48 (*CSC: bad programming habit: the code below puts everywhere a fake
    49   label and then adds_graph fixes them *)
    50 (*CSC: this is just an instance of add_translates below! *)
    5141let rec adds_graph
    5242  (pars1: params1) (globals: list ident)
    53   (stmt_list: list (joint_statement (graph_params_ pars1) globals))
     43  (stmt_list: list (label → joint_statement (graph_params_ pars1) globals))
    5444  (start_lbl: label) (dest_lbl: label)
    5545  (def: joint_internal_function … (graph_params pars1 globals))
     
    5949  | cons stmt stmt_list ⇒
    6050    match stmt_list with
    61     [ nil ⇒ add_graph … start_lbl (change_label … stmt dest_lbl) def
     51    [ nil ⇒ add_graph … start_lbl (stmt dest_lbl) def
    6252    | _ ⇒
    6353      let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    64       let stmt ≝ change_label … stmt tmp_lbl in
    65       let def ≝ add_graph … start_lbl stmt def in
     54      let def ≝ add_graph … start_lbl (stmt tmp_lbl) def in
    6655        adds_graph pars1 globals stmt_list tmp_lbl dest_lbl def]].
    6756
    68 (*CSC: bad programming habit: the code below puts everywhere a fake
    69   label and then adds_graph fixes them *)
    7057let rec add_translates
    7158  (pars1: params1) (globals: list ident)
Note: See TracChangeset for help on using the changeset viewer.