source: src/utilities/Interference.ma @ 1211

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

fixed interference file

File size: 4.0 KB
Line 
1include "basics/types.ma".
2include "basics/list.ma".
3include "common/Graphs.ma".
4include "common/Registers.ma".
5
6include "utilities/adt/table_adt.ma".
7include "utilities/adt/priority_set_adt.ma".
8include "utilities/adt/set_adt.ma".
9include "utilities/adt/register_table.ma".
10
11definition vertex_set ≝ set vertex.
12definition vertex_priority_set ≝ priority_set vertex.
13definition Register_set ≝ set Register.
14
15record graph: Type[1] ≝
16{
17  ig_regmap     : register_table;
18  ig_ivv        : vertex_set;
19  ig_ivh        : Register_set;
20  ig_pvv        : vertex_set;
21  ig_pvh        : Register_set;
22  ig_degree     : vertex_priority_set;
23  ig_nmr        : vertex_priority_set
24}.
25
26definition ig_create ≝
27  λregs.
28  let 〈ignore_int, table'', priority''〉 ≝
29    foldr … (λr. λv_table_priority'.
30      let 〈v, table', priority'〉 ≝ v_table_priority' in
31      let table'' ≝ rt_add r v table' in
32      let priority'' ≝ ps_insert ? v 0 priority' in
33        〈v + 1, table'', priority''〉) 〈0, rt_empty …, ps_empty …〉 regs
34  in
35      mk_graph table'' (set_empty …) (set_empty …) (set_empty …)
36      (set_empty …) priority'' priority''.
37
38definition neighboursv ≝
39  λset_impl.
40  λgraph: graph set_impl.
41    set_find … (ig_vertex_set … graph) v (getvv set_impl graph).
42
43  method neighborsv graph v =
44    VertexSetMap.find v (self#getvv graph)
45
46definition ig_mkipp ≝
47  λset_impl.
48  λgraph: interference_graph set_impl.
49  λregs1.
50  λregs2.
51    set_fold … (ig_Reg_set … graph) (λr1. λgraph.
52      let v1 ≝ lookup … graph r1 in
53        set_fold … (ig_Reg_set … graph) (λr2. λgraph.
54          ig_mkvv …
55
56let mkipp graph regs1 regs2 =
57  Register.Set.fold (fun r1 graph ->
58    let v1 = lookup graph r1 in
59    Register.Set.fold (fun r2 graph ->
60      interference#mkvv graph v1 (lookup graph r2)
61    ) regs2 graph
62  ) regs1 graph
63
64axiom ig_mkiph: interference_graph → list register → list Register →
65  interference_graph.
66
67definition ig_mki: interference_graph → (list register) × (list Register) →
68  (list register) × (list Register) → interference_graph ≝
69  λgraph.
70  λregs1_hwregs1.
71  λregs2_hwregs2.
72    let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
73    let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
74    let graph ≝ ig_mkipp graph regs1 regs2 in
75    let graph ≝ ig_mkiph graph regs1 hwregs2 in
76    let graph ≝ ig_mkiph graph regs2 hwregs1 in
77      graph.
78 
79axiom ig_mkppp: interference_graph → register → register → interference_graph.
80axiom ig_mkpph: interference_graph → register → Register → interference_graph.
81axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph.
82axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph.
83axiom ig_remove: interference_graph → vertex → interference_graph.
84axiom ig_freeze: interference_graph → vertex → interference_graph.
85axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph.
86axiom ig_droph: interference_graph → interference_graph.
87axiom ig_lookup: interference_graph → register → vertex.
88axiom ig_registers: interference_graph → vertex → list register.
89axiom ig_degree: interference_graph → vertex → nat.
90axiom ig_lowest: interference_graph → option (vertex × nat).
91axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat).
92axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
93  interference_graph → option vertex.
94axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
95axiom ig_ipp: interference_graph → vertex → vertex_set.
96axiom ig_iph: interference_graph → vertex → list Register.
97axiom ig_ppp: interference_graph → vertex → vertex_set.
98axiom ig_pph: interference_graph → vertex → list Register.
99definition ig_ppedge ≝ vertex × vertex.
100axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge.
101definition ig_phedge ≝ vertex × Register.
102axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge.
Note: See TracBrowser for help on using the repository browser.