source: src/utilities/Interference.ma @ 1192

Last change on this file since 1192 was 1192, checked in by mulligan, 8 years ago

some files that were missing / laying dormant on my computer

File size: 2.2 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].
10
11(* vertex maps *)
12axiom vertex_map: Type[0].
13
14definition interference_graph ≝ graph label.
15
16axiom ig_create: list register → interference_graph.
17axiom ig_mki: interference_graph → (list register) × (list Register) →
18  (list register) × (list Register) → interference_graph.
19axiom ig_mkiph: interference_graph → list register → list Register →
20  interference_graph.
21axiom ig_mkppp: interference_graph → register → register → interference_graph.
22axiom ig_mkpph: interference_graph → register → Register → interference_graph.
23axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph.
24axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph.
25axiom ig_remove: interference_graph → vertex → interference_graph.
26axiom ig_freeze: interference_graph → vertex → interference_graph.
27axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph.
28axiom ig_droph: interference_graph → interference_graph.
29axiom ig_lookup: interference_graph → register → vertex.
30axiom ig_registers: interference_graph → vertex → list register.
31axiom ig_degree: interference_graph → vertex → nat.
32axiom ig_lowest: interference_graph → option (vertex × nat).
33axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat).
34axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
35  interference_graph → option vertex.
36axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
37axiom ig_ipp: interference_graph → vertex → list vertex.
38axiom ig_iph: interference_graph → vertex → list Register.
39axiom ig_ppp: interference_graph → vertex → list vertex.
40axiom ig_pph: interference_graph → vertex → list Register.
41definition ig_ppedge ≝ vertex × vertex.
42axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge.
43definition ig_phedge ≝ vertex × Register.
44axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge.
Note: See TracBrowser for help on using the repository browser.