1 | include "basics/types.ma". |
---|
2 | include "basics/list.ma". |
---|
3 | include "common/Graphs.ma". |
---|
4 | include "common/Registers.ma". |
---|
5 | |
---|
6 | definition vertex ≝ nat. (* XXX: int in o'caml *) |
---|
7 | |
---|
8 | (* vertex sets *) |
---|
9 | axiom vertex_set: Type[0]. |
---|
10 | axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A. |
---|
11 | axiom vs_filter: (vertex → bool) → vertex_set → vertex_set. |
---|
12 | axiom vs_subset: vertex_set → vertex_set → bool. |
---|
13 | |
---|
14 | (* vertex maps *) |
---|
15 | axiom vertex_map: Type[0] → Type[0]. |
---|
16 | axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A. |
---|
17 | |
---|
18 | definition interference_graph ≝ graph label. |
---|
19 | |
---|
20 | axiom ig_create: list register → interference_graph. |
---|
21 | axiom ig_mki: interference_graph → (list register) × (list Register) → |
---|
22 | (list register) × (list Register) → interference_graph. |
---|
23 | axiom ig_mkiph: interference_graph → list register → list Register → |
---|
24 | interference_graph. |
---|
25 | axiom ig_mkppp: interference_graph → register → register → interference_graph. |
---|
26 | axiom ig_mkpph: interference_graph → register → Register → interference_graph. |
---|
27 | axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph. |
---|
28 | axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph. |
---|
29 | axiom ig_remove: interference_graph → vertex → interference_graph. |
---|
30 | axiom ig_freeze: interference_graph → vertex → interference_graph. |
---|
31 | axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph. |
---|
32 | axiom ig_droph: interference_graph → interference_graph. |
---|
33 | axiom ig_lookup: interference_graph → register → vertex. |
---|
34 | axiom ig_registers: interference_graph → vertex → list register. |
---|
35 | axiom ig_degree: interference_graph → vertex → nat. |
---|
36 | axiom ig_lowest: interference_graph → option (vertex × nat). |
---|
37 | axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat). |
---|
38 | axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) → |
---|
39 | interference_graph → option vertex. |
---|
40 | axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A. |
---|
41 | axiom ig_ipp: interference_graph → vertex → vertex_set. |
---|
42 | axiom ig_iph: interference_graph → vertex → list Register. |
---|
43 | axiom ig_ppp: interference_graph → vertex → vertex_set. |
---|
44 | axiom ig_pph: interference_graph → vertex → list Register. |
---|
45 | definition ig_ppedge ≝ vertex × vertex. |
---|
46 | axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge. |
---|
47 | definition ig_phedge ≝ vertex × Register. |
---|
48 | axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge. |
---|