source: src/utilities/Interference.ma @ 1145

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

changed naming in i8051 of classes of registers to make them consistent

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