source: src/utilities/Interference.ma @ 1219

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

a little more added

File size: 11.3 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 vertex_set_table ≝ set_table vertex (set vertex).
15definition Register_set_table ≝ set_table vertex (set Register).
16definition Register_set ≝ set Register.
17
18record graph: Type[0] ≝
19{
20  ig_regmap     : register_table;
21  ig_ivv        : vertex_set_table;
22  ig_ivh        : Register_set_table;
23  ig_pvv        : vertex_set;
24  ig_pvh        : Register_set;
25  ig_degree     : vertex_priority_set;
26  ig_nmr        : vertex_priority_set
27}.
28
29definition set_ivv ≝
30  λgraph.
31  λivv: vertex_set_table.
32    let regmap ≝ ig_regmap graph in
33    let ivh    ≝ ig_ivh graph in
34    let pvv    ≝ ig_pvv graph in
35    let pvh    ≝ ig_pvh graph in
36    let degree ≝ ig_degree graph in
37    let nmr    ≝ ig_nmr graph in
38      mk_graph
39        regmap ivv ivh pvv pvh degree nmr.
40
41definition set_ivh ≝
42  λgraph.
43  λivh: Register_set_table.
44    let regmap ≝ ig_regmap graph in
45    let ivv    ≝ ig_ivv graph in
46    let pvv    ≝ ig_pvv graph in
47    let pvh    ≝ ig_pvh graph in
48    let degree ≝ ig_degree graph in
49    let nmr    ≝ ig_nmr graph in
50      mk_graph
51        regmap ivv ivh pvv pvh degree nmr.
52
53definition set_degree ≝
54  λgraph.
55  λdegree: vertex_priority_set.
56    let regmap ≝ ig_regmap graph in
57    let ivv    ≝ ig_ivv graph in
58    let ivh    ≝ ig_ivh graph in
59    let pvv    ≝ ig_pvv graph in
60    let pvh    ≝ ig_pvh graph in
61    let nmr    ≝ ig_nmr graph in
62      mk_graph
63        regmap ivv ivh pvv pvh degree nmr.
64
65definition set_nmr ≝
66  λgraph.
67  λnmr: vertex_priority_set.
68    let regmap ≝ ig_regmap graph in
69    let ivv    ≝ ig_ivv graph in
70    let ivh    ≝ ig_ivh graph in
71    let pvv    ≝ ig_pvv graph in
72    let pvh    ≝ ig_pvh graph in
73    let degree ≝ ig_degree graph in
74      mk_graph
75        regmap ivv ivh pvv pvh degree nmr.
76
77definition sg_neighboursv ≝
78  λgraph: graph.
79  λv: vertex.
80    set_tbl_find … v (ig_ivv graph).
81
82definition sg_existsvv ≝
83  λgraph.
84  λv1.
85  λv2.
86  match sg_neighboursv graph v2 with
87  [ None       ⇒ false (* XXX: ok? *)
88  | Some neigh ⇒ set_member ? v1 neigh
89  ].
90
91definition sg_neighboursh ≝
92  λgraph.
93  λv.
94    set_tbl_find ? ? v (ig_ivh graph).
95
96definition sg_existsvh ≝
97  λgraph.
98  λv.
99  λh.
100  match sg_neighboursh graph v with
101  [ None       ⇒ false (* XXX: ok? *)
102  | Some neigh ⇒ set_member ? h neigh
103  ].
104
105definition sg_degree ≝
106  λgraph.
107  λv.
108  match sg_neighboursv graph v with
109  [ None ⇒ None ?
110  | Some neigh ⇒
111    match sg_neighboursh graph v with
112    [ None ⇒ None ?
113    | Some neigh' ⇒ Some ? ((set_size … neigh) + (set_size … neigh'))
114    ]
115  ].
116   
117definition sg_hwregs ≝
118  λgraph: graph.
119    let union ≝ λkey: vertex. set_union ? in
120    set_tbl_fold vertex ? ? union (ig_ivh graph) (set_empty Register).
121
122axiom sg_iter: Type[0]. (* XXX: todo when i can be bothered *)
123
124definition sg_mkvvi ≝
125  λgraph.
126  λv1.
127  λv2.
128    set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (ig_ivv graph)).
129
130definition sg_mkvv ≝
131  λgraph.
132  λv1.
133  λv2.
134    if eq_nat v1 v2 then
135      graph
136    else if sg_existsvv graph v1 v2 then
137      graph
138    else
139      sg_mkvvi graph v1 v2.
140
141definition sg_rmvv ≝
142  λgraph.
143  λv1.
144  λv2.
145    set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (ig_ivv graph)).
146
147definition sg_rmvvifx ≝
148  λgraph.
149  λv1.
150  λv2.
151  if sg_existsvv graph v1 v2 then
152    sg_rmvv graph v1 v2
153  else
154    graph.
155
156definition sg_mkvhi ≝
157  λgraph.
158  λv.
159  λh.
160    set_ivh graph (set_tbl_update … v (set_insert … h) (ig_ivh graph)).
161
162definition sg_mkvh ≝
163  λgraph.
164  λv.
165  λh.
166  if sg_existsvh graph v h then
167    graph
168  else
169    sg_mkvhi graph v h.
170
171definition sg_rmvh ≝
172  λgraph.
173  λv.
174  λh.
175    set_ivh graph (set_tbl_update … v (set_remove … h) (ig_ivh graph)).
176
177definition sg_rmvhifx ≝
178  λgraph.
179  λv.
180  λh.
181    if sg_existsvh graph v h then
182      sg_rmvh graph v h
183    else
184      graph.
185
186definition sg_coalesce ≝
187  λg.
188  λx.
189  λy.
190  match sg_neighboursv g x with
191  [ None       ⇒ None ?
192  | Some neigh ⇒
193    let graph ≝ set_fold ? graph (λw. λg.
194      sg_mkvv (sg_rmvv g x w) y w) neigh g
195    in
196    match sg_neighboursh g x with
197    [ None ⇒ None ?
198    | Some neigh ⇒
199      let graph ≝ set_fold ? ? (λh. λg.
200        sg_mkvh (sg_rmvh g x h) y h) neigh g
201      in
202        Some … graph
203    ]
204  ].
205
206definition sg_coalesceh ≝
207  λg.
208  λx.
209  λh.
210  match sg_neighboursv g x with
211  [ None       ⇒ None ?
212  | Some neigh ⇒
213    let graph ≝ set_fold ? graph (λw. λg.
214      sg_mkvh (sg_rmvv g x w) w h) neigh g
215    in
216    match sg_neighboursh g x with
217    [ None ⇒ None ?
218    | Some neigh ⇒
219      let graph ≝ set_fold ? ? (λk. λg.
220        sg_rmvh graph x k) neigh g
221      in
222        Some … graph
223    ]
224  ].
225
226definition sg_remove ≝
227  λg.
228  λx.
229  match sg_neighboursv g x with
230  [ None ⇒ None ?
231  | Some neigh ⇒
232    let graph ≝
233      set_fold … (λw. λgraph.
234        sg_rmvv graph x w) neigh g
235    in
236    match sg_neighboursh graph x with
237    [ None ⇒ None ?
238    | Some neigh ⇒
239      let graph ≝ set_fold … (λh. λg.
240        sg_rmvh g x h) neigh graph
241      in
242        Some ? graph
243    ]
244  ].
245
246definition ig_mkvvi ≝
247  λgraph.
248  λv1.
249  λv2.
250  let graph ≝ sg_mkvvi graph v1 v2 in
251  let graph ≝ sg_rmvvifx graph v1 v2 in
252  let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) (ig_degree graph)) in
253  let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) (ig_nmr graph)) in
254    set_degree (set_nmr graph nmr') degree'.
255
256definition ig_rmvv ≝
257  λgraph.
258  λv1.
259  λv2.
260  let graph ≝ sg_rmvv graph v1 v2 in
261  let degree' ≝ pset_increment ? v1 (neg (repr 1)) (pset_increment ? v2 (neg (repr 1)) (ig_degree graph)) in
262  let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) (ig_nmr graph)) in
263    set_degree (set_nmr graph nmr') degree'.
264
265definition ig_mkvhi ≝
266  λgraph.
267  λv.
268  λh.
269  let graph ≝ sg_mkvhi graph v h in
270  let graph ≝ sg_rmvhifx graph v h in
271  let degree ≝ pset_increment ? v (repr 1) (ig_degree graph) in
272  let nmr ≝ pset_incrementifx ? v (repr 1) (ig_nmr graph) in
273    set_degree (set_nmr graph nmr) degree.
274
275definition ig_rmvh ≝
276  λgraph.
277  λv.
278  λh.
279  let graph ≝ sg_rmvh graph v h in
280  let degree ≝ pset_increment ? v (neg (repr 1)) (ig_degree graph) in
281  let nmr ≝ pset_incrementifx ? v (neg (repr 1)) (ig_nmr graph) in
282    set_degree (set_nmr graph nmr) degree.
283
284definition pref_nmr ≝
285  λgraph.
286  λv.
287  match sg_neighboursv graph v with
288  [ None       ⇒ false (* XXX: ok? *)
289  | Some neigh ⇒
290    match sg_neighboursh graph v with
291    [ None        ⇒ false
292    | Some neigh' ⇒
293      andb (set_is_empty ? neigh) (set_is_empty ? neigh')
294    ]
295  ].
296
297definition pref_mkcheck ≝
298  λgraph.
299  λv.
300    if pref_nmr graph v then
301      let nmr' ≝ pset_remove ? v (ig_nmr graph) in
302        set_nmr graph nmr'
303    else
304      graph.
305
306definition pref_mkvvi ≝
307  λgraph.
308  λv1.
309  λv2.
310    if sg_existsvv graph v1 v2 then
311      graph
312    else
313      let graph ≝ pref_mkcheck graph v1 in
314      let graph ≝ pref_mkcheck graph v2 in
315        sg_mkvvi graph v1 v2.
316
317definition pref_mkvhi ≝
318  λgraph.
319  λv.
320  λh.
321  if sg_existsvh graph v h then
322    graph
323  else
324    let graph ≝ pref_mkcheck graph v in
325      sg_mkvhi graph v h.
326
327(* XXX: look at this carefully *)
328definition pref_rmcheck ≝
329  λgraph.
330  λv.
331  if pref_nmr graph v then
332    match pset_lookup ? v (ig_degree graph) with
333    [ None ⇒ graph (* XXX: ok? *)
334    | Some pref ⇒
335      let nmr ≝ pset_insert ? v pref (ig_nmr graph) in
336        set_nmr graph nmr
337    ]
338  else
339    graph.
340
341definition pref_rmvv ≝
342  λgraph.
343  λv1.
344  λv2.
345  let graph ≝ sg_rmvv graph v1 v2 in
346  let graph ≝ pref_rmcheck graph v1 in
347  let graph ≝ pref_rmcheck graph v2 in
348    graph.
349
350definition pref_rmvh ≝
351  λgraph.
352  λv.
353  λh.
354  let graph ≝ sg_rmvh graph v h in
355  let graph ≝ pref_rmcheck graph v in
356    graph.
357
358definition ig_create ≝
359  λregs.
360  let 〈ignore_int, table'', priority''〉 ≝
361    foldr … (λr. λv_table_priority'.
362      let 〈v, table', priority'〉 ≝ v_table_priority' in
363      let table'' ≝ rt_add r v table' in
364      let priority'' ≝ pset_insert ? v 0 priority' in
365        〈v + 1, table'', priority''〉) 〈0, rt_empty …, pset_empty …〉 regs
366  in
367      mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_empty …)
368      (set_empty …) priority'' priority''.
369
370
371
372definition ig_mkipp ≝
373  λset_impl.
374  λgraph: interference_graph set_impl.
375  λregs1.
376  λregs2.
377    set_fold … (ig_Reg_set … graph) (λr1. λgraph.
378      let v1 ≝ lookup … graph r1 in
379        set_fold … (ig_Reg_set … graph) (λr2. λgraph.
380          ig_mkvv …
381
382let mkipp graph regs1 regs2 =
383  Register.Set.fold (fun r1 graph ->
384    let v1 = lookup graph r1 in
385    Register.Set.fold (fun r2 graph ->
386      interference#mkvv graph v1 (lookup graph r2)
387    ) regs2 graph
388  ) regs1 graph
389
390axiom ig_mkiph: graph → list register → list Register →
391  graph.
392
393definition ig_mki: graph → (list register) × (list Register) →
394  (list register) × (list Register) → graph ≝
395  λgraph.
396  λregs1_hwregs1.
397  λregs2_hwregs2.
398    let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
399    let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
400    let graph ≝ ig_mkipp graph regs1 regs2 in
401    let graph ≝ ig_mkiph graph regs1 hwregs2 in
402    let graph ≝ ig_mkiph graph regs2 hwregs1 in
403      graph.
404 
405axiom ig_mkppp: interference_graph → register → register → interference_graph.
406axiom ig_mkpph: interference_graph → register → Register → interference_graph.
407axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph.
408axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph.
409axiom ig_remove: interference_graph → vertex → interference_graph.
410axiom ig_freeze: interference_graph → vertex → interference_graph.
411axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph.
412axiom ig_droph: interference_graph → interference_graph.
413axiom ig_lookup: interference_graph → register → vertex.
414axiom ig_registers: interference_graph → vertex → list register.
415axiom ig_degree: interference_graph → vertex → nat.
416axiom ig_lowest: interference_graph → option (vertex × nat).
417axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat).
418axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
419  interference_graph → option vertex.
420axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
421axiom ig_ipp: interference_graph → vertex → vertex_set.
422axiom ig_iph: interference_graph → vertex → list Register.
423axiom ig_ppp: interference_graph → vertex → vertex_set.
424axiom ig_pph: interference_graph → vertex → list Register.
425definition ig_ppedge ≝ vertex × vertex.
426axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge.
427definition ig_phedge ≝ vertex × Register.
428axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge.
Note: See TracBrowser for help on using the repository browser.