source: src/utilities/Interference.ma @ 1209

Last change on this file since 1209 was 1209, checked in by mulligan, 9 years ago

more work on int. graphs

File size: 4.7 KB
RevLine 
[1127]1include "basics/types.ma".
2include "basics/list.ma".
[1145]3include "common/Graphs.ma".
[1127]4include "common/Registers.ma".
5
[1208]6include "utilities/adt/table_adt.ma".
7include "utilities/adt/priority_set_adt.ma".
8include "utilities/adt/set_adt.ma".
9
[1192]10definition vertex ≝ nat. (* XXX: int in o'caml *)
11
12(* vertex sets *)
[1127]13axiom vertex_set: Type[0].
[1193]14axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A.
15axiom vs_filter: (vertex → bool) → vertex_set → vertex_set.
16axiom vs_subset: vertex_set → vertex_set → bool.
[1192]17
18(* vertex maps *)
[1193]19axiom vertex_map: Type[0] → Type[0].
20axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A.
[1127]21
[1208]22axiom ordered_vertex: ordered vertex.
23axiom ordered_register: ordered register.
24axiom ordered_Register: ordered Register.
[1192]25
[1208]26record interference_graph: Type[1] ≝
27{
28  ig_reg_table  : table_adt register vertex ordered_register;
29  ig_vertex_set : set_adt vertex ordered_vertex;
30  ig_vertex_pset: priority_set_adt vertex ordered_vertex;
31  ig_Reg_set    : set_adt Register ordered_Register;
32  ig_regmap     : table … ig_reg_table register vertex;
33  ig_ivv        : set … ig_vertex_set vertex;
34  ig_ivh        : set … ig_Reg_set Register;
35  ig_pvv        : set … ig_vertex_set vertex;
36  ig_pvh        : set … ig_Reg_set Register;
37  ig_degree     : priority_set … ig_vertex_pset vertex;
38  ig_nmr        : priority_set … ig_vertex_pset vertex
39}.
[1196]40
[1208]41definition ig_create ≝
42  λreg_table  : table_adt register vertex ordered_register.
43  λvertex_set : set_adt vertex ordered_vertex.
44  λvertex_pset: priority_set_adt vertex ordered_vertex.
45  λReg_set    : set_adt Register ordered_Register.
46  λregs.
47  let 〈ignore_int, table'', priority''〉 ≝
48    foldr … (λr. λv_table_priority'.
49      let 〈v, table', priority'〉 ≝ v_table_priority' in
[1209]50      let table'' ≝ tbl_insert … reg_table r v table' in
51      let priority'' ≝ ps_insert … vertex_pset v 0 priority' in
52        〈v + 1, table'', priority''〉) 〈0, tbl_empty …, ps_empty …〉 regs
[1208]53  in
54    mk_interference_graph
55      reg_table vertex_set vertex_pset Reg_set
[1209]56      table'' (set_empty …) (set_empty …) (set_empty …)
57      (set_empty …) priority'' priority''.
[1196]58
[1208]59definition ig_mkipp: interference_graph → list register → list register →
60  interference_graph ≝
61  λgraph.
62  λregs1.
63  λregs2.
64    foldr … (λr. λgraph.
[1209]65      let v1 ≝ lookup graph e1 in
[1196]66
[1208]67let mkipp graph regs1 regs2 =
68  Register.Set.fold (fun r1 graph ->
69    let v1 = lookup graph r1 in
70    Register.Set.fold (fun r2 graph ->
71      interference#mkvv graph v1 (lookup graph r2)
72    ) regs2 graph
73  ) regs1 graph
[1196]74
[1127]75axiom ig_mkiph: interference_graph → list register → list Register →
76  interference_graph.
[1208]77
78definition ig_mki: interference_graph → (list register) × (list Register) →
79  (list register) × (list Register) → interference_graph ≝
80  λgraph.
81  λregs1_hwregs1.
82  λregs2_hwregs2.
83    let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
84    let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
85    let graph ≝ ig_mkipp graph regs1 regs2 in
86    let graph ≝ ig_mkiph graph regs1 hwregs2 in
87    let graph ≝ ig_mkiph graph regs2 hwregs1 in
88      graph.
89 
[1127]90axiom ig_mkppp: interference_graph → register → register → interference_graph.
91axiom ig_mkpph: interference_graph → register → Register → interference_graph.
92axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph.
93axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph.
94axiom ig_remove: interference_graph → vertex → interference_graph.
95axiom ig_freeze: interference_graph → vertex → interference_graph.
96axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph.
97axiom ig_droph: interference_graph → interference_graph.
98axiom ig_lookup: interference_graph → register → vertex.
99axiom ig_registers: interference_graph → vertex → list register.
100axiom ig_degree: interference_graph → vertex → nat.
101axiom ig_lowest: interference_graph → option (vertex × nat).
102axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat).
103axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
104  interference_graph → option vertex.
105axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
[1193]106axiom ig_ipp: interference_graph → vertex → vertex_set.
[1127]107axiom ig_iph: interference_graph → vertex → list Register.
[1193]108axiom ig_ppp: interference_graph → vertex → vertex_set.
[1127]109axiom ig_pph: interference_graph → vertex → list Register.
110definition ig_ppedge ≝ vertex × vertex.
111axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge.
112definition ig_phedge ≝ vertex × Register.
113axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge.
Note: See TracBrowser for help on using the repository browser.