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