 Timestamp:
 Sep 22, 2011, 2:29:52 PM (8 years ago)
 Location:
 src/ERTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1250 r1251 47 47 ]. 48 48 *) 49 50 definition lookup ≝ colouring.51 49 52 50 definition fresh_label ≝ … … 141 139 λr. 142 140 λl. 143 match lookupvaluation coloured_graph (inl … r) with141 match colouring valuation coloured_graph (inl … r) with 144 142 [ decision_spill off ⇒ 145 143 let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph (bitvector_of_nat … off) RegisterSST l in … … 159 157 λr. 160 158 λstmt. 161 match lookupvaluation coloured_graph (inl … r) with159 match colouring valuation coloured_graph (inl … r) with 162 160 [ decision_colour hwr ⇒ generate globals (joint_if_luniverse globals (ertl_params globals) int_fun) graph (stmt hwr) 163 161  decision_spill off ⇒ … … 343 341 [ pseudo p1 ⇒ 344 342 match regr with 345 [ pseudo p2 ⇒ move globals int_fun graph ( lookup valuation coloured_graph (inl … p1)) (lookupvaluation coloured_graph (inl … p2)) l346  hardware h ⇒ move globals int_fun graph ( lookupvaluation coloured_graph (inl … p1)) (decision_colour h) l343 [ pseudo p2 ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l 344  hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l 347 345 ] 348 346  hardware h1 ⇒ 349 347 match regr with 350 [ pseudo p ⇒ move globals int_fun graph (decision_colour h1) ( lookupvaluation coloured_graph (inl … p)) l348 [ pseudo p ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l 351 349  hardware h2 ⇒ 352 350 let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in 
src/ERTL/uses.ma
r1250 r1251 60 60 λint_fun: ertl_internal_function globals. 61 61 let graph ≝ recover_graph globals int_fun in 62 let uses ≝ tbl_fold ?? (examine_statement globals) (joint_if_graph… int_fun) (tbl_empty …) in62 let uses ≝ tbl_fold … (examine_statement globals) (joint_if_code … int_fun) (tbl_empty …) in 63 63 lookup uses. 64 64 *)
Note: See TracChangeset
for help on using the changeset viewer.