source: src/utilities/Interference.ma @ 1183

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

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

File size: 2.1 KB
RevLine 
[1127]1include "basics/types.ma".
2include "basics/list.ma".
[1145]3include "common/Graphs.ma".
[1127]4include "common/Registers.ma".
5
[1145]6definition interference_graph ≝ graph label.
[1127]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.