 Timestamp:
 Oct 3, 2011, 8:35:23 AM (9 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1283 r1284 52 52 sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉); 53 53 sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr); 54 sequential ertl_params_ … (LOAD … destr addr1 addr2)54 sequential ertl_params_ … (LOAD … destr addr1 addr2) 55 55 ] start_lbl dest_lbl def. 56 56 … … 67 67 let hdw_params ≝ get_params_hdw globals hdw_params in 68 68 hdw_params @ (get_params_stack … stack_params). 69 69 70 70 definition add_prologue ≝ 71 71 λglobals. … … 76 76 λdef. 77 77 let start_lbl ≝ joint_if_entry … (ertl_params globals) def in 78 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in78 let 〈tmp_lbl, def〉 ≝ fresh_label … def in 79 79 match lookup … (joint_if_code … def) start_lbl 80 80 return λx. x ≠ None ? → ertl_internal_function globals with … … 96 96 add_graph … tmp_lbl last_stmt def 97 97 ] ?. 98 [ cases start_lbl #x #H @H98 [ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *) 99 99  cases (none_absrd) /2/ ] 100 100 qed. … … 140 140 λdef. 141 141 let start_lbl ≝ joint_if_exit … (ertl_params globals) def in 142 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in142 let 〈tmp_lbl, def〉 ≝ fresh_label … def in 143 143 match lookup … (joint_if_code … def) start_lbl 144 144 return λx. x ≠ None ? → ertl_internal_function globals with … … 162 162 set_joint_if_exit … tmp_lbl def' ? 163 163 ] ?. 164 [ cases start_lbl #x #H @H164 [ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *) 165 165  cases (none_absrd) /2/ 166 166  cases daemon (* CSC: XXXXX *) … … 370 370 λstmt. 371 371 λdef: joint_internal_function … (ertl_params globals). 372 let 〈entry, nuniv〉 ≝ fresh_label … def in 373 let graph ≝ add ? ? (joint_if_code … def) entry stmt in 374 mk_joint_internal_function ? (ertl_params globals) 375 nuniv (joint_if_runiverse … def) it (joint_if_params … def) 376 (joint_if_locals … def) (joint_if_stacksize … def) graph 377 ? ?. 378 [ % [ @entry  @graph_add ] 379  cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL  @graph_add_lookup @LBL_PRF ] 372 let 〈entry, def〉 ≝ fresh_label … def in 373 let graph ≝ add … (joint_if_code … def) entry stmt in 374 set_joint_if_graph … (ertl_params globals) graph def ??. 375 [ (*% [ @entry  @graph_add ]*) cases daemon (*CSC: XXX *) 376  (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL  @graph_add_lookup @LBL_PRF 377 *) cases daemon (*CSC: XXX *) 378 ] 380 379 qed. 381 380 
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.