1 | include "basics/types.ma". |
---|
2 | include "basics/list.ma". |
---|
3 | include "common/Graphs.ma". |
---|
4 | include "common/Registers.ma". |
---|
5 | include "utilities/RegisterSet.ma". |
---|
6 | |
---|
7 | definition vertex ≝ nat. (* XXX: int in o'caml *) |
---|
8 | |
---|
9 | (* vertex sets *) |
---|
10 | axiom vertex_set: Type[0]. |
---|
11 | axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A. |
---|
12 | axiom vs_filter: (vertex → bool) → vertex_set → vertex_set. |
---|
13 | axiom vs_subset: vertex_set → vertex_set → bool. |
---|
14 | |
---|
15 | (* vertex maps *) |
---|
16 | axiom vertex_map: Type[0] → Type[0]. |
---|
17 | axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A. |
---|
18 | |
---|
19 | definition interference_graph ≝ graph label. |
---|
20 | |
---|
21 | definition ig_create: ∀rs. rs_set rs → interference_graph ≝ |
---|
22 | let 〈ignore_int, regmap, degree〉 ≝ |
---|
23 | rs_fold rs (λr. λv_regmap_degree. |
---|
24 | let 〈v, regmap, degree〉 ≝ v_regmap_degree in |
---|
25 | 〈v + 1, (r, v)::regmap, |
---|
26 | |
---|
27 | |
---|
28 | |
---|
29 | |
---|
30 | let create regs = |
---|
31 | let (_ : int), regmap, degree = |
---|
32 | Register.Set.fold (fun r (v, regmap, degree) -> |
---|
33 | v+1, |
---|
34 | RegMap.add r v regmap, |
---|
35 | PrioritySet.add v 0 degree |
---|
36 | ) regs (0, RegMap.empty, PrioritySet.empty) |
---|
37 | in |
---|
38 | { |
---|
39 | regmap = regmap; |
---|
40 | ivv = Vertex.Map.empty; |
---|
41 | ivh = Vertex.Map.empty; |
---|
42 | pvv = Vertex.Map.empty; |
---|
43 | pvh = Vertex.Map.empty; |
---|
44 | degree = degree; |
---|
45 | nmr = degree |
---|
46 | } |
---|
47 | |
---|
48 | |
---|
49 | axiom ig_mki: interference_graph → (list register) × (list Register) → |
---|
50 | (list register) × (list Register) → interference_graph. |
---|
51 | axiom ig_mkiph: interference_graph → list register → list Register → |
---|
52 | interference_graph. |
---|
53 | axiom ig_mkppp: interference_graph → register → register → interference_graph. |
---|
54 | axiom ig_mkpph: interference_graph → register → Register → interference_graph. |
---|
55 | axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph. |
---|
56 | axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph. |
---|
57 | axiom ig_remove: interference_graph → vertex → interference_graph. |
---|
58 | axiom ig_freeze: interference_graph → vertex → interference_graph. |
---|
59 | axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph. |
---|
60 | axiom ig_droph: interference_graph → interference_graph. |
---|
61 | axiom ig_lookup: interference_graph → register → vertex. |
---|
62 | axiom ig_registers: interference_graph → vertex → list register. |
---|
63 | axiom ig_degree: interference_graph → vertex → nat. |
---|
64 | axiom ig_lowest: interference_graph → option (vertex × nat). |
---|
65 | axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat). |
---|
66 | axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) → |
---|
67 | interference_graph → option vertex. |
---|
68 | axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A. |
---|
69 | axiom ig_ipp: interference_graph → vertex → vertex_set. |
---|
70 | axiom ig_iph: interference_graph → vertex → list Register. |
---|
71 | axiom ig_ppp: interference_graph → vertex → vertex_set. |
---|
72 | axiom ig_pph: interference_graph → vertex → list Register. |
---|
73 | definition ig_ppedge ≝ vertex × vertex. |
---|
74 | axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge. |
---|
75 | definition ig_phedge ≝ vertex × Register. |
---|
76 | axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge. |
---|