source: src/utilities/Interference.ma @ 1212

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

more added on interference graphs

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