1 | include "basics/types.ma". |
---|
2 | include "basics/list.ma". |
---|
3 | include "common/Graphs.ma". |
---|
4 | include "common/Registers.ma". |
---|
5 | |
---|
6 | include "utilities/adt/table_adt.ma". |
---|
7 | include "utilities/adt/priority_set_adt.ma". |
---|
8 | include "utilities/adt/set_adt.ma". |
---|
9 | include "utilities/adt/set_table_adt.ma". |
---|
10 | include "utilities/adt/register_table.ma". |
---|
11 | |
---|
12 | definition vertex_set ≝ set vertex. |
---|
13 | definition vertex_priority_set ≝ priority_set vertex. |
---|
14 | definition Register_set ≝ set Register. |
---|
15 | |
---|
16 | record graph: Type[1] ≝ |
---|
17 | { |
---|
18 | ig_regmap : register_table; |
---|
19 | ig_ivv : vertex_set; |
---|
20 | ig_ivh : Register_set; |
---|
21 | ig_pvv : vertex_set; |
---|
22 | ig_pvh : Register_set; |
---|
23 | ig_degree : vertex_priority_set; |
---|
24 | ig_nmr : vertex_priority_set |
---|
25 | }. |
---|
26 | |
---|
27 | definition ig_create ≝ |
---|
28 | λregs. |
---|
29 | let 〈ignore_int, table'', priority''〉 ≝ |
---|
30 | foldr … (λr. λv_table_priority'. |
---|
31 | let 〈v, table', priority'〉 ≝ v_table_priority' in |
---|
32 | let table'' ≝ rt_add r v table' in |
---|
33 | let priority'' ≝ ps_insert ? v 0 priority' in |
---|
34 | 〈v + 1, table'', priority''〉) 〈0, rt_empty …, ps_empty …〉 regs |
---|
35 | in |
---|
36 | mk_graph table'' (set_empty …) (set_empty …) (set_empty …) |
---|
37 | (set_empty …) priority'' priority''. |
---|
38 | |
---|
39 | definition neighboursv ≝ |
---|
40 | λgraph: graph. |
---|
41 | λv: vertex. |
---|
42 | set_tbl_find … v (ig_ivv graph). |
---|
43 | |
---|
44 | method neighborsv graph v = |
---|
45 | VertexSetMap.find v (self#getvv graph) |
---|
46 | |
---|
47 | definition ig_mkipp ≝ |
---|
48 | λset_impl. |
---|
49 | λgraph: interference_graph set_impl. |
---|
50 | λregs1. |
---|
51 | λregs2. |
---|
52 | set_fold … (ig_Reg_set … graph) (λr1. λgraph. |
---|
53 | let v1 ≝ lookup … graph r1 in |
---|
54 | set_fold … (ig_Reg_set … graph) (λr2. λgraph. |
---|
55 | ig_mkvv … |
---|
56 | |
---|
57 | let mkipp graph regs1 regs2 = |
---|
58 | Register.Set.fold (fun r1 graph -> |
---|
59 | let v1 = lookup graph r1 in |
---|
60 | Register.Set.fold (fun r2 graph -> |
---|
61 | interference#mkvv graph v1 (lookup graph r2) |
---|
62 | ) regs2 graph |
---|
63 | ) regs1 graph |
---|
64 | |
---|
65 | axiom ig_mkiph: graph → list register → list Register → |
---|
66 | graph. |
---|
67 | |
---|
68 | definition ig_mki: graph → (list register) × (list Register) → |
---|
69 | (list register) × (list Register) → graph ≝ |
---|
70 | λgraph. |
---|
71 | λregs1_hwregs1. |
---|
72 | λregs2_hwregs2. |
---|
73 | let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in |
---|
74 | let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in |
---|
75 | let graph ≝ ig_mkipp graph regs1 regs2 in |
---|
76 | let graph ≝ ig_mkiph graph regs1 hwregs2 in |
---|
77 | let graph ≝ ig_mkiph graph regs2 hwregs1 in |
---|
78 | graph. |
---|
79 | |
---|
80 | axiom ig_mkppp: interference_graph → register → register → interference_graph. |
---|
81 | axiom ig_mkpph: interference_graph → register → Register → interference_graph. |
---|
82 | axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph. |
---|
83 | axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph. |
---|
84 | axiom ig_remove: interference_graph → vertex → interference_graph. |
---|
85 | axiom ig_freeze: interference_graph → vertex → interference_graph. |
---|
86 | axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph. |
---|
87 | axiom ig_droph: interference_graph → interference_graph. |
---|
88 | axiom ig_lookup: interference_graph → register → vertex. |
---|
89 | axiom ig_registers: interference_graph → vertex → list register. |
---|
90 | axiom ig_degree: interference_graph → vertex → nat. |
---|
91 | axiom ig_lowest: interference_graph → option (vertex × nat). |
---|
92 | axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat). |
---|
93 | axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) → |
---|
94 | interference_graph → option vertex. |
---|
95 | axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A. |
---|
96 | axiom ig_ipp: interference_graph → vertex → vertex_set. |
---|
97 | axiom ig_iph: interference_graph → vertex → list Register. |
---|
98 | axiom ig_ppp: interference_graph → vertex → vertex_set. |
---|
99 | axiom ig_pph: interference_graph → vertex → list Register. |
---|
100 | definition ig_ppedge ≝ vertex × vertex. |
---|
101 | axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge. |
---|
102 | definition ig_phedge ≝ vertex × Register. |
---|
103 | axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge. |
---|