Changeset 1230 for src/ERTL/ERTLToLTL.ma
 Timestamp:
 Sep 20, 2011, 3:56:40 PM (10 years ago)
 File:

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