source: src/utilities/Interference.ma @ 1208

Last change on this file since 1208 was 1208, checked in by mulligan, 8 years ago

added adts for sets, tables and priority sets in order to make life easier when working on the interference graph code

File size: 4.7 KB
Line 
1include "basics/types.ma".
2include "basics/list.ma".
3include "common/Graphs.ma".
4include "common/Registers.ma".
5
6include "utilities/adt/table_adt.ma".
7include "utilities/adt/priority_set_adt.ma".
8include "utilities/adt/set_adt.ma".
9
10definition vertex ≝ nat. (* XXX: int in o'caml *)
11
12(* vertex sets *)
13axiom vertex_set: Type[0].
14axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A.
15axiom vs_filter: (vertex → bool) → vertex_set → vertex_set.
16axiom vs_subset: vertex_set → vertex_set → bool.
17
18(* vertex maps *)
19axiom vertex_map: Type[0] → Type[0].
20axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A.
21
22axiom ordered_vertex: ordered vertex.
23axiom ordered_register: ordered register.
24axiom ordered_Register: ordered Register.
25
26record 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
41definition 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'' ≝ insert … reg_table r v table' in
51      let priority'' ≝ insert … vertex_pset v 0 priority' in
52        〈v + 1, table'', priority''〉) 〈0, empty …, empty …〉 regs
53  in
54    mk_interference_graph
55      reg_table vertex_set vertex_pset Reg_set
56      table'' [ ] [ ] [ ] [ ] priority'' priority''.
57
58definition ig_mkipp: interference_graph → list register → list register →
59  interference_graph ≝
60  λgraph.
61  λregs1.
62  λregs2.
63    foldr … (λr. λgraph.
64      let v1 ≝ lookup
65
66let mkipp graph regs1 regs2 =
67  Register.Set.fold (fun r1 graph ->
68    let v1 = lookup graph r1 in
69    Register.Set.fold (fun r2 graph ->
70      interference#mkvv graph v1 (lookup graph r2)
71    ) regs2 graph
72  ) regs1 graph
73
74axiom ig_mkiph: interference_graph → list register → list Register →
75  interference_graph.
76
77definition ig_mki: interference_graph → (list register) × (list Register) →
78  (list register) × (list Register) → interference_graph ≝
79  λgraph.
80  λregs1_hwregs1.
81  λregs2_hwregs2.
82    let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
83    let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
84    let graph ≝ ig_mkipp graph regs1 regs2 in
85    let graph ≝ ig_mkiph graph regs1 hwregs2 in
86    let graph ≝ ig_mkiph graph regs2 hwregs1 in
87      graph.
88 
89axiom ig_mkppp: interference_graph → register → register → interference_graph.
90axiom ig_mkpph: interference_graph → register → Register → interference_graph.
91axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph.
92axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph.
93axiom ig_remove: interference_graph → vertex → interference_graph.
94axiom ig_freeze: interference_graph → vertex → interference_graph.
95axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph.
96axiom ig_droph: interference_graph → interference_graph.
97axiom ig_lookup: interference_graph → register → vertex.
98axiom ig_registers: interference_graph → vertex → list register.
99axiom ig_degree: interference_graph → vertex → nat.
100axiom ig_lowest: interference_graph → option (vertex × nat).
101axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat).
102axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
103  interference_graph → option vertex.
104axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
105axiom ig_ipp: interference_graph → vertex → vertex_set.
106axiom ig_iph: interference_graph → vertex → list Register.
107axiom ig_ppp: interference_graph → vertex → vertex_set.
108axiom ig_pph: interference_graph → vertex → list Register.
109definition ig_ppedge ≝ vertex × vertex.
110axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge.
111definition ig_phedge ≝ vertex × Register.
112axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge.
Note: See TracBrowser for help on using the repository browser.