source: src/utilities/Interference.ma @ 1208

Last change on this file since 1208 was 1208, checked in by mulligan, 10 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.