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 | |
---|
10 | definition vertex ≝ nat. (* XXX: int in o'caml *) |
---|
11 | |
---|
12 | (* vertex sets *) |
---|
13 | axiom vertex_set: Type[0]. |
---|
14 | axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A. |
---|
15 | axiom vs_filter: (vertex → bool) → vertex_set → vertex_set. |
---|
16 | axiom vs_subset: vertex_set → vertex_set → bool. |
---|
17 | |
---|
18 | (* vertex maps *) |
---|
19 | axiom vertex_map: Type[0] → Type[0]. |
---|
20 | axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A. |
---|
21 | |
---|
22 | axiom ordered_vertex: ordered vertex. |
---|
23 | axiom ordered_register: ordered register. |
---|
24 | axiom ordered_Register: ordered Register. |
---|
25 | |
---|
26 | record interference_graph: Type[1] ≝ |
---|
27 | { |
---|
28 | ig_reg_table : table_adt register vertex ordered_register; |
---|
29 | ig_vertex_set : set_adt vertex ordered_vertex; |
---|
30 | ig_vertex_pset: priority_set_adt vertex ordered_vertex; |
---|
31 | ig_Reg_set : set_adt Register ordered_Register; |
---|
32 | ig_regmap : table … ig_reg_table register vertex; |
---|
33 | ig_ivv : set … ig_vertex_set vertex; |
---|
34 | ig_ivh : set … ig_Reg_set Register; |
---|
35 | ig_pvv : set … ig_vertex_set vertex; |
---|
36 | ig_pvh : set … ig_Reg_set Register; |
---|
37 | ig_degree : priority_set … ig_vertex_pset vertex; |
---|
38 | ig_nmr : priority_set … ig_vertex_pset vertex |
---|
39 | }. |
---|
40 | |
---|
41 | definition ig_create ≝ |
---|
42 | λreg_table : table_adt register vertex ordered_register. |
---|
43 | λvertex_set : set_adt vertex ordered_vertex. |
---|
44 | λvertex_pset: priority_set_adt vertex ordered_vertex. |
---|
45 | λReg_set : set_adt Register ordered_Register. |
---|
46 | λregs. |
---|
47 | let 〈ignore_int, table'', priority''〉 ≝ |
---|
48 | foldr … (λr. λv_table_priority'. |
---|
49 | let 〈v, table', priority'〉 ≝ v_table_priority' in |
---|
50 | 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 | in |
---|
54 | mk_interference_graph |
---|
55 | reg_table vertex_set vertex_pset Reg_set |
---|
56 | table'' (set_empty …) (set_empty …) (set_empty …) |
---|
57 | (set_empty …) priority'' priority''. |
---|
58 | |
---|
59 | definition ig_mkipp: interference_graph → list register → list register → |
---|
60 | interference_graph ≝ |
---|
61 | λgraph. |
---|
62 | λregs1. |
---|
63 | λregs2. |
---|
64 | foldr … (λr. λgraph. |
---|
65 | let v1 ≝ lookup graph e1 in |
---|
66 | |
---|
67 | let mkipp graph regs1 regs2 = |
---|
68 | Register.Set.fold (fun r1 graph -> |
---|
69 | let v1 = lookup graph r1 in |
---|
70 | Register.Set.fold (fun r2 graph -> |
---|
71 | interference#mkvv graph v1 (lookup graph r2) |
---|
72 | ) regs2 graph |
---|
73 | ) regs1 graph |
---|
74 | |
---|
75 | axiom ig_mkiph: interference_graph → list register → list Register → |
---|
76 | interference_graph. |
---|
77 | |
---|
78 | definition ig_mki: interference_graph → (list register) × (list Register) → |
---|
79 | (list register) × (list Register) → interference_graph ≝ |
---|
80 | λgraph. |
---|
81 | λregs1_hwregs1. |
---|
82 | λregs2_hwregs2. |
---|
83 | let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in |
---|
84 | let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in |
---|
85 | let graph ≝ ig_mkipp graph regs1 regs2 in |
---|
86 | let graph ≝ ig_mkiph graph regs1 hwregs2 in |
---|
87 | let graph ≝ ig_mkiph graph regs2 hwregs1 in |
---|
88 | graph. |
---|
89 | |
---|
90 | axiom ig_mkppp: interference_graph → register → register → interference_graph. |
---|
91 | axiom ig_mkpph: interference_graph → register → Register → interference_graph. |
---|
92 | axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph. |
---|
93 | axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph. |
---|
94 | axiom ig_remove: interference_graph → vertex → interference_graph. |
---|
95 | axiom ig_freeze: interference_graph → vertex → interference_graph. |
---|
96 | axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph. |
---|
97 | axiom ig_droph: interference_graph → interference_graph. |
---|
98 | axiom ig_lookup: interference_graph → register → vertex. |
---|
99 | axiom ig_registers: interference_graph → vertex → list register. |
---|
100 | axiom ig_degree: interference_graph → vertex → nat. |
---|
101 | axiom ig_lowest: interference_graph → option (vertex × nat). |
---|
102 | axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat). |
---|
103 | axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) → |
---|
104 | interference_graph → option vertex. |
---|
105 | axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A. |
---|
106 | axiom ig_ipp: interference_graph → vertex → vertex_set. |
---|
107 | axiom ig_iph: interference_graph → vertex → list Register. |
---|
108 | axiom ig_ppp: interference_graph → vertex → vertex_set. |
---|
109 | axiom ig_pph: interference_graph → vertex → list Register. |
---|
110 | definition ig_ppedge ≝ vertex × vertex. |
---|
111 | axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge. |
---|
112 | definition ig_phedge ≝ vertex × Register. |
---|
113 | axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge. |
---|