 Timestamp:
 Sep 20, 2011, 3:56:40 PM (10 years ago)
 Location:
 src/ERTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTL.ma
r1229 r1230 6 6 include "ASM/Arithmetic.ma". 7 7 8 (* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *) 9 8 (* XXX: define an interference graph for a function and colour it, allowing 9 the consultation of registers. *) 10 definition initial_colouring ≝ 11 λglobals. 12 λint_fun. 13 let 〈ignore, graph〉 ≝ build globals int_fun in 14 let coloured ≝ colour_initial graph in 15 coloured. 16 10 17 definition interference_lookup ≝ 11 λglobals. 12 λc: initial_colouring. 13 λint_fun. 14 λr. 15 16 17 colouring initial_colouring r. 18 let lkup ≝ ig_lookup graph r in ?. 19 check lkup. 20 tbl_find ?? lkup colour_colouring. 21 22 definition lookup: register → decision ≝ 23 λr. 24 match ? r with 25 [ colour_spill 26 27 axiom lookup: register → decision. 18 λcoloured: initial_colouring. 19 λr. 20 colouring … coloured r. 21 22 definition prepare_graph_for_second_colouring ≝ 23 λglobals: list ident. 24 λcoloured: initial_colouring. 25 let g ≝ the_graph decision coloured in 26 let restricted ≝ ig_restrict g (λv. 27 match colouring decision coloured v with 28 [ decision_spill ⇒ true 29  decision_colour _ ⇒ false 30 ] 31 ) 32 in restricted. 33 34 definition second_colouring ≝ 35 λglobals: list ident. 36 λcoloured. 37 let prepared ≝ prepare_graph_for_second_colouring globals coloured in 38 colour_stack prepared. 39 40 definition lookup ≝ 41 λinitial. 42 λsecond. 43 λr. 44 match interference_lookup initial r with 45 [ decision_colour _ ⇒ ? 46  decision_spill ⇒ ? 47 ]. 28 48 29 49 definition fresh_label ≝ 
src/ERTL/Interference.ma
r1229 r1230 34 34 35 35 definition initial_colouring ≝ coloured_graph decision. 36 axiom colour_initial: graph → initial_colouring. 36 37 definition stack_colouring ≝ coloured_graph nat. 38 axiom colour_stack: graph → stack_colouring. 37 39 38 40 … … 525 527 axiom ig_remove: graph → vertex → graph. 526 528 axiom ig_freeze: graph → vertex → graph. 527 axiom ig_restrict: graph → ( vertex → bool) → graph.529 axiom ig_restrict: graph → (register → bool) → graph. (* XXX: change *) 528 530 axiom ig_droph: graph → graph. 529 531 axiom ig_lookup: graph → register → vertex.
Note: See TracChangeset
for help on using the changeset viewer.