- Timestamp:
- Sep 30, 2011, 3:12:40 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/TranslateUtils.ma
r1282 r1283 39 39 fresh LabelTag (joint_if_luniverse … def). 40 40 41 definition change_label ≝42 λpars1,globals.λe: joint_statement (graph_params pars1 globals) globals.λl.43 match e with44 [ GOTO _ ⇒ GOTO … l45 | RETURN ⇒ RETURN ??46 | sequential instr _ ⇒ sequential … globals instr l].47 48 (*CSC: bad programming habit: the code below puts everywhere a fake49 label and then adds_graph fixes them *)50 (*CSC: this is just an instance of add_translates below! *)51 41 let rec adds_graph 52 42 (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)) 54 44 (start_lbl: label) (dest_lbl: label) 55 45 (def: joint_internal_function … (graph_params pars1 globals)) … … 59 49 | cons stmt stmt_list ⇒ 60 50 match stmt_list with 61 [ nil ⇒ add_graph … start_lbl ( change_label …stmt dest_lbl) def51 [ nil ⇒ add_graph … start_lbl (stmt dest_lbl) def 62 52 | _ ⇒ 63 53 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 66 55 adds_graph pars1 globals stmt_list tmp_lbl dest_lbl def]]. 67 56 68 (*CSC: bad programming habit: the code below puts everywhere a fake69 label and then adds_graph fixes them *)70 57 let rec add_translates 71 58 (pars1: params1) (globals: list ident)
Note: See TracChangeset
for help on using the changeset viewer.