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

 1 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
Note: See TracChangeset
for help on using the changeset viewer.