source: src/utilities/Interference.ma @ 1193

Last change on this file since 1193 was 1193, checked in by mulligan, 9 years ago

work on colouring algorithm halted as it can be axiomatised. now implementing interference graphs (objects!)

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