source: src/utilities/Interference.ma @ 1127

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

interference graphs axiomatised, more added to ertl

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