 Timestamp:
 Sep 13, 2011, 5:14:03 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/Interference.ma
r1208 r1209 48 48 foldr … (λr. λv_table_priority'. 49 49 let 〈v, table', priority'〉 ≝ v_table_priority' in 50 let table'' ≝ insert … reg_table r v table' in51 let priority'' ≝ insert … vertex_pset v 0 priority' in52 〈v + 1, table'', priority''〉) 〈0, empty …,empty …〉 regs50 let table'' ≝ tbl_insert … reg_table r v table' in 51 let priority'' ≝ ps_insert … vertex_pset v 0 priority' in 52 〈v + 1, table'', priority''〉) 〈0, tbl_empty …, ps_empty …〉 regs 53 53 in 54 54 mk_interference_graph 55 55 reg_table vertex_set vertex_pset Reg_set 56 table'' [ ] [ ] [ ] [ ] priority'' priority''. 56 table'' (set_empty …) (set_empty …) (set_empty …) 57 (set_empty …) priority'' priority''. 57 58 58 59 definition ig_mkipp: interference_graph → list register → list register → … … 62 63 λregs2. 63 64 foldr … (λr. λgraph. 64 let v1 ≝ lookup 65 let v1 ≝ lookup graph e1 in 65 66 66 67 let mkipp graph regs1 regs2 =
Note: See TracChangeset
for help on using the changeset viewer.