source: src/utilities/Interference.ma @ 1196

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

some more changes, need some additional datastructures

File size: 3.1 KB
Line 
1include "basics/types.ma".
2include "basics/list.ma".
3include "common/Graphs.ma".
4include "common/Registers.ma".
5include "utilities/RegisterSet.ma".
6
7definition vertex ≝ nat. (* XXX: int in o'caml *)
8
9(* vertex sets *)
10axiom vertex_set: Type[0].
11axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A.
12axiom vs_filter: (vertex → bool) → vertex_set → vertex_set.
13axiom vs_subset: vertex_set → vertex_set → bool.
14
15(* vertex maps *)
16axiom vertex_map: Type[0] → Type[0].
17axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A.
18
19definition interference_graph ≝ graph label.
20
21definition ig_create: ∀rs. rs_set rs → interference_graph ≝
22  let 〈ignore_int, regmap, degree〉 ≝
23    rs_fold rs (λr. λv_regmap_degree.
24      let 〈v, regmap, degree〉 ≝ v_regmap_degree in
25        〈v + 1, (r, v)::regmap,
26
27
28
29
30let create regs =
31  let (_ : int), regmap, degree =
32    Register.Set.fold (fun r (v, regmap, degree) ->
33      v+1,
34      RegMap.add r v regmap,
35      PrioritySet.add v 0 degree
36    ) regs (0, RegMap.empty, PrioritySet.empty)
37  in
38  {
39    regmap = regmap;
40    ivv = Vertex.Map.empty;
41    ivh = Vertex.Map.empty;
42    pvv = Vertex.Map.empty;
43    pvh = Vertex.Map.empty;
44    degree = degree;
45    nmr = degree
46  }
47
48
49axiom ig_mki: interference_graph → (list register) × (list Register) →
50  (list register) × (list Register) → interference_graph.
51axiom ig_mkiph: interference_graph → list register → list Register →
52  interference_graph.
53axiom ig_mkppp: interference_graph → register → register → interference_graph.
54axiom ig_mkpph: interference_graph → register → Register → interference_graph.
55axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph.
56axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph.
57axiom ig_remove: interference_graph → vertex → interference_graph.
58axiom ig_freeze: interference_graph → vertex → interference_graph.
59axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph.
60axiom ig_droph: interference_graph → interference_graph.
61axiom ig_lookup: interference_graph → register → vertex.
62axiom ig_registers: interference_graph → vertex → list register.
63axiom ig_degree: interference_graph → vertex → nat.
64axiom ig_lowest: interference_graph → option (vertex × nat).
65axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat).
66axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
67  interference_graph → option vertex.
68axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
69axiom ig_ipp: interference_graph → vertex → vertex_set.
70axiom ig_iph: interference_graph → vertex → list Register.
71axiom ig_ppp: interference_graph → vertex → vertex_set.
72axiom ig_pph: interference_graph → vertex → list Register.
73definition ig_ppedge ≝ vertex × vertex.
74axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge.
75definition ig_phedge ≝ vertex × Register.
76axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge.
Note: See TracBrowser for help on using the repository browser.