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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/TranslateUtils.ma
r1283 r1284 35 35 qed. 36 36 37 definition fresh_label ≝ 38 λglobals,params. λdef: joint_internal_function globals params. 39 fresh LabelTag (joint_if_luniverse … def). 40 41 let rec adds_graph 42 (pars1: params1) (globals: list ident) 43 (stmt_list: list (label → joint_statement (graph_params_ pars1) globals)) 44 (start_lbl: label) (dest_lbl: label) 45 (def: joint_internal_function … (graph_params pars1 globals)) 46 on stmt_list ≝ 47 match stmt_list with 48 [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def 49  cons stmt stmt_list ⇒ 50 match stmt_list with 51 [ nil ⇒ add_graph … start_lbl (stmt dest_lbl) def 52  _ ⇒ 53 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in 54 let def ≝ add_graph … start_lbl (stmt tmp_lbl) def in 55 adds_graph pars1 globals stmt_list tmp_lbl dest_lbl def]]. 37 definition fresh_label: 38 ∀pars0,globals. joint_internal_function … (graph_params pars0 globals) → label × (joint_internal_function … (graph_params pars0 globals)) ≝ 39 λpars0,globals,def. 40 let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in 41 〈r,set_luniverse … def luniverse〉. 56 42 57 43 let rec add_translates … … 66 52 [ nil ⇒ trans start_lbl dest_lbl def 67 53  _ ⇒ 68 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in54 let 〈tmp_lbl, def〉 ≝ fresh_label … def in 69 55 let def ≝ trans start_lbl tmp_lbl def in 70 56 add_translates pars1 globals translate_list tmp_lbl dest_lbl def]]. 57 58 definition adds_graph ≝ 59 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals). 60 add_translates … (map … (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
Note: See TracChangeset
for help on using the changeset viewer.