source: src/utilities/Interference.ma @ 1223

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

changes

File size: 13.8 KB
Line 
1include "basics/types.ma".
2include "basics/list.ma".
3include "common/Graphs.ma".
4include "common/Order.ma".
5include "common/Registers.ma".
6
7include "utilities/adt/table_adt.ma".
8include "utilities/adt/priority_set_adt.ma".
9include "utilities/adt/set_adt.ma".
10include "utilities/adt/set_table_adt.ma".
11include "utilities/adt/register_table.ma".
12
13(* definition vertex_set ≝ set vertex. *)
14definition vertex_priority_set ≝ priority_set vertex.
15definition vertex_set_table ≝ set_table vertex (set vertex).
16definition Register_set_table ≝ set_table vertex (set Register).
17definition Register_set ≝ set Register.
18
19record graph: Type[0] ≝
20{
21  g_regmap     : register_table;
22  g_ivv        : vertex_set_table;
23  g_ivh        : Register_set_table;
24  g_pvv        : vertex_set_table;
25  g_pvh        : Register_set_table;
26  g_degree     : vertex_priority_set;
27  g_nmr        : vertex_priority_set
28}.
29
30definition set_ivv ≝
31  λgraph.
32  λivv: vertex_set_table.
33    let regmap ≝ g_regmap graph in
34    let ivh    ≝ g_ivh graph in
35    let pvv    ≝ g_pvv graph in
36    let pvh    ≝ g_pvh graph in
37    let degree ≝ g_degree graph in
38    let nmr    ≝ g_nmr graph in
39      mk_graph
40        regmap ivv ivh pvv pvh degree nmr.
41
42definition set_ivh ≝
43  λgraph.
44  λivh: Register_set_table.
45    let regmap ≝ g_regmap graph in
46    let ivv    ≝ g_ivv graph in
47    let pvv    ≝ g_pvv graph in
48    let pvh    ≝ g_pvh graph in
49    let degree ≝ g_degree graph in
50    let nmr    ≝ g_nmr graph in
51      mk_graph
52        regmap ivv ivh pvv pvh degree nmr.
53
54definition set_degree ≝
55  λgraph.
56  λdegree: vertex_priority_set.
57    let regmap ≝ g_regmap graph in
58    let ivv    ≝ g_ivv graph in
59    let ivh    ≝ g_ivh graph in
60    let pvv    ≝ g_pvv graph in
61    let pvh    ≝ g_pvh graph in
62    let nmr    ≝ g_nmr graph in
63      mk_graph
64        regmap ivv ivh pvv pvh degree nmr.
65
66definition set_nmr ≝
67  λgraph.
68  λnmr: vertex_priority_set.
69    let regmap ≝ g_regmap graph in
70    let ivv    ≝ g_ivv graph in
71    let ivh    ≝ g_ivh graph in
72    let pvv    ≝ g_pvv graph in
73    let pvh    ≝ g_pvh graph in
74    let degree ≝ g_degree graph in
75      mk_graph
76        regmap ivv ivh pvv pvh degree nmr.
77
78definition sg_neighboursv ≝
79  λgraph: graph.
80  λv: vertex.
81    set_tbl_find … v (g_ivv graph).
82
83definition sg_existsvv ≝
84  λgraph.
85  λv1.
86  λv2.
87  match sg_neighboursv graph v2 with
88  [ None       ⇒ false (* XXX: ok? *)
89  | Some neigh ⇒ set_member ? eq_nat v1 neigh
90  ].
91
92definition sg_neighboursh ≝
93  λgraph.
94  λv.
95    set_tbl_find ? ? v (g_ivh graph).
96
97definition sg_existsvh ≝
98  λgraph.
99  λv.
100  λh.
101  match sg_neighboursh graph v with
102  [ None       ⇒ false (* XXX: ok? *)
103  | Some neigh ⇒ set_member ? eq_Register h neigh
104  ].
105
106definition sg_degree ≝
107  λgraph.
108  λv.
109  match sg_neighboursv graph v with
110  [ None ⇒ None ?
111  | Some neigh ⇒
112    match sg_neighboursh graph v with
113    [ None ⇒ None ?
114    | Some neigh' ⇒ Some ? ((set_size … neigh) + (set_size … neigh'))
115    ]
116  ].
117   
118definition sg_hwregs ≝
119  λgraph: graph.
120    let union ≝ λkey: vertex. set_union ? in
121    set_tbl_fold vertex ? ? union (g_ivh graph) (set_empty Register).
122
123axiom sg_iter: Type[0]. (* XXX: todo when i can be bothered *)
124
125definition sg_mkvvi ≝
126  λgraph.
127  λv1.
128  λv2.
129    set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (g_ivv graph)).
130
131definition sg_mkvv ≝
132  λgraph.
133  λv1.
134  λv2.
135    if eq_nat v1 v2 then
136      graph
137    else if sg_existsvv graph v1 v2 then
138      graph
139    else
140      sg_mkvvi graph v1 v2.
141
142definition sg_rmvv ≝
143  λgraph.
144  λv1.
145  λv2.
146    set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (g_ivv graph)).
147
148definition sg_rmvvifx ≝
149  λgraph.
150  λv1.
151  λv2.
152  if sg_existsvv graph v1 v2 then
153    sg_rmvv graph v1 v2
154  else
155    graph.
156
157definition sg_mkvhi ≝
158  λgraph.
159  λv.
160  λh.
161    set_ivh graph (set_tbl_update … v (set_insert … h) (g_ivh graph)).
162
163definition sg_mkvh ≝
164  λgraph.
165  λv.
166  λh.
167  if sg_existsvh graph v h then
168    graph
169  else
170    sg_mkvhi graph v h.
171
172definition sg_rmvh ≝
173  λgraph.
174  λv.
175  λh.
176    set_ivh graph (set_tbl_update … v (set_remove … h) (g_ivh graph)).
177
178definition sg_rmvhifx ≝
179  λgraph.
180  λv.
181  λh.
182    if sg_existsvh graph v h then
183      sg_rmvh graph v h
184    else
185      graph.
186
187definition sg_coalesce ≝
188  λg.
189  λx.
190  λy.
191  match sg_neighboursv g x with
192  [ None       ⇒ None ?
193  | Some neigh ⇒
194    let graph ≝ set_fold ? graph (λw. λg.
195      sg_mkvv (sg_rmvv g x w) y w) neigh g
196    in
197    match sg_neighboursh g x with
198    [ None ⇒ None ?
199    | Some neigh ⇒
200      let graph ≝ set_fold ? ? (λh. λg.
201        sg_mkvh (sg_rmvh g x h) y h) neigh g
202      in
203        Some … graph
204    ]
205  ].
206
207definition sg_coalesceh ≝
208  λg.
209  λx.
210  λh.
211  match sg_neighboursv g x with
212  [ None       ⇒ None ?
213  | Some neigh ⇒
214    let graph ≝ set_fold ? graph (λw. λg.
215      sg_mkvh (sg_rmvv g x w) w h) neigh g
216    in
217    match sg_neighboursh g x with
218    [ None ⇒ None ?
219    | Some neigh ⇒
220      let graph ≝ set_fold ? ? (λk. λg.
221        sg_rmvh graph x k) neigh g
222      in
223        Some … graph
224    ]
225  ].
226
227definition sg_remove ≝
228  λg.
229  λx.
230  match sg_neighboursv g x with
231  [ None ⇒ None ?
232  | Some neigh ⇒
233    let graph ≝
234      set_fold … (λw. λgraph.
235        sg_rmvv graph x w) neigh g
236    in
237    match sg_neighboursh graph x with
238    [ None ⇒ None ?
239    | Some neigh ⇒
240      let graph ≝ set_fold … (λh. λg.
241        sg_rmvh g x h) neigh graph
242      in
243        Some ? graph
244    ]
245  ].
246
247definition ig_mkvvi ≝
248  λgraph.
249  λv1.
250  λv2.
251  let graph ≝ sg_mkvvi graph v1 v2 in
252  let graph ≝ sg_rmvvifx graph v1 v2 in
253  let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) (g_degree graph)) in
254  let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) (g_nmr graph)) in
255    set_degree (set_nmr graph nmr') degree'.
256
257definition ig_rmvv ≝
258  λgraph.
259  λv1.
260  λv2.
261  let graph ≝ sg_rmvv graph v1 v2 in
262  let degree' ≝ pset_increment ? v1 (neg (repr 1)) (pset_increment ? v2 (neg (repr 1)) (g_degree graph)) in
263  let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) (g_nmr graph)) in
264    set_degree (set_nmr graph nmr') degree'.
265
266definition ig_mkvhi ≝
267  λgraph.
268  λv.
269  λh.
270  let graph ≝ sg_mkvhi graph v h in
271  let graph ≝ sg_rmvhifx graph v h in
272  let degree ≝ pset_increment ? v (repr 1) (g_degree graph) in
273  let nmr ≝ pset_incrementifx ? v (repr 1) (g_nmr graph) in
274    set_degree (set_nmr graph nmr) degree.
275
276definition ig_rmvh ≝
277  λgraph.
278  λv.
279  λh.
280  let graph ≝ sg_rmvh graph v h in
281  let degree ≝ pset_increment ? v (neg (repr 1)) (g_degree graph) in
282  let nmr ≝ pset_incrementifx ? v (neg (repr 1)) (g_nmr graph) in
283    set_degree (set_nmr graph nmr) degree.
284
285definition pref_nmr ≝
286  λgraph.
287  λv.
288  match sg_neighboursv graph v with
289  [ None       ⇒ false (* XXX: ok? *)
290  | Some neigh ⇒
291    match sg_neighboursh graph v with
292    [ None        ⇒ false
293    | Some neigh' ⇒
294      andb (set_is_empty ? neigh) (set_is_empty ? neigh')
295    ]
296  ].
297
298definition pref_mkcheck ≝
299  λgraph.
300  λv.
301    if pref_nmr graph v then
302      let nmr' ≝ pset_remove ? v (g_nmr graph) in
303        set_nmr graph nmr'
304    else
305      graph.
306
307definition pref_mkvvi ≝
308  λgraph.
309  λv1.
310  λv2.
311    if sg_existsvv graph v1 v2 then
312      graph
313    else
314      let graph ≝ pref_mkcheck graph v1 in
315      let graph ≝ pref_mkcheck graph v2 in
316        sg_mkvvi graph v1 v2.
317
318definition pref_mkvhi ≝
319  λgraph.
320  λv.
321  λh.
322  if sg_existsvh graph v h then
323    graph
324  else
325    let graph ≝ pref_mkcheck graph v in
326      sg_mkvhi graph v h.
327
328(* XXX: look at this carefully *)
329definition pref_rmcheck ≝
330  λgraph.
331  λv.
332  if pref_nmr graph v then
333    match pset_lookup ? v (g_degree graph) with
334    [ None ⇒ graph (* XXX: ok? *)
335    | Some pref ⇒
336      let nmr ≝ pset_insert ? v pref (g_nmr graph) in
337        set_nmr graph nmr
338    ]
339  else
340    graph.
341
342definition pref_rmvv ≝
343  λgraph.
344  λv1.
345  λv2.
346  let graph ≝ sg_rmvv graph v1 v2 in
347  let graph ≝ pref_rmcheck graph v1 in
348  let graph ≝ pref_rmcheck graph v2 in
349    graph.
350
351definition pref_rmvh ≝
352  λgraph.
353  λv.
354  λh.
355  let graph ≝ sg_rmvh graph v h in
356  let graph ≝ pref_rmcheck graph v in
357    graph.
358   
359definition ig_ipp ≝ sg_neighboursv.
360definition ig_iph ≝ sg_neighboursh.
361definition ig_ppp ≝ sg_neighboursv.
362definition ig_pph ≝ sg_neighboursh.
363definition ig_degree ≝ λgraph. λv. pset_lookup ? v (g_degree graph).
364definition ig_lowest ≝ λgraph. pset_lowest ? (g_degree graph).
365definition ig_lowest_non_move_related ≝ λgraph. pset_lowest ? (g_nmr graph).
366definition ig_fold ≝ λA: Type[0]. λf: vertex → A → A. λgraph. λaccu.
367  rt_fold … (λv. λ_. λaccu. f v accu) (g_regmap graph) accu.
368
369definition ig_minimum: ∀a: Type[0]. (a → a → order) → (vertex → a) → graph → option vertex ≝
370  λa: Type[0].
371  λcompare: a → a → order.
372  λf: vertex → a.
373  λgraph.
374  let folded ≝ ig_fold … (λw. λaccu.
375    let dw ≝ f w in
376      match accu with
377      [ None      ⇒ Some … 〈dw, w〉
378      | Some dv_v ⇒
379        let 〈dv, v〉 ≝ dv_v in
380          match compare dw dv with
381          [ order_lt ⇒ Some … 〈dw, w〉
382          | _        ⇒ accu
383          ]
384      ]) graph (None …)
385  in
386    match folded with
387    [ None          ⇒ None …
388    | Some ignore_v ⇒
389      let 〈ignore, v〉 ≝ ignore_v in
390        Some … v
391    ].
392   
393definition ig_ppedge ≝ vertex × vertex.
394
395definition ig_pppick ≝ λgraph. λp. set_tbl_pick … (g_pvv graph) p.
396
397definition ig_phedge ≝ vertex × Register.
398
399definition ig_phpick ≝ λgraph. λp. set_tbl_pick … (g_pvh graph) p.
400
401definition ig_create ≝
402  λregs.
403  let 〈ignore_int, table'', priority''〉 ≝
404    foldr … (λr. λv_table_priority'.
405      let 〈v, table', priority'〉 ≝ v_table_priority' in
406      let table'' ≝ rt_add r v table' in
407      let priority'' ≝ pset_insert ? v 0 priority' in
408        〈v + 1, table'', priority''〉) 〈0, rt_empty …, pset_empty …〉 regs
409  in
410      mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_tbl_empty …)
411      (set_tbl_empty …) priority'' priority''.
412definition ig_lookup ≝ λgraph. λr. rt_backward r (g_regmap graph).
413definition ig_registers ≝ λgraph. λv. rt_forward v (g_regmap graph).
414definition ig_mkipp ≝
415  λgraph.
416  λregs1.
417  λregs2.
418    set_fold … (λr1. λgraph.
419      let v1 ≝ ig_lookup graph r1 in
420        set_fold … (λr2. λgraph.
421          sg_mkvv graph v1 (ig_lookup graph r2)
422        ) regs2 graph
423    ) regs1 graph.
424definition ig_mkiph ≝
425  λgraph.
426  λregs.
427  λhwregs.
428    set_fold … (λr. λgraph.
429      let v ≝ ig_lookup graph r in
430        set_fold … (λh. λgraph.
431          sg_mkvh graph v h
432        ) hwregs graph
433    ) regs graph.
434definition ig_mki ≝
435  λgraph.
436  λregs1_hwregs1.
437  λregs2_hwregs2.
438  let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
439  let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
440  let graph ≝ ig_mkipp graph regs1 regs2 in
441  let graph ≝ ig_mkiph graph regs1 hwregs2 in
442  let graph ≝ ig_mkiph graph regs2 hwregs1 in
443    graph.
444definition ig_mkppp ≝
445  λgraph.
446  λr1.
447  λr2.
448  let v1 ≝ ig_lookup graph r1 in
449  let v2 ≝ ig_lookup graph r2 in
450  let graph ≝ sg_mkvv graph v1 v2 in
451    graph.
452definition ig_mkpph ≝
453  λgraph.
454  λr.
455  λh.
456  let v ≝ ig_lookup graph r in
457  let graph ≝ sg_mkvh graph v h in
458    graph.
459(*   
460(* XXX: precondition:
461  x \not\eq y
462  existsvv graph x y == false i.e. coalesce interfering edges *)
463definition ig_coalesce ≝
464  λgraph.
465  λx.
466  λy.
467  let graph ≝ sg_coalesce graph x y in
468
469let coalesce graph x y =
470
471  assert (x <> y); (* attempt to coalesce one vertex with itself *)
472  assert (not (interference#existsvv graph x y)); (* attempt to coalesce two interfering vertices *)
473
474  (* Perform coalescing in the two subgraphs. *)
475
476  let graph = interference#coalesce graph x y in
477  let graph = preference#coalesce graph x y in
478
479  (* Remove [x] from all tables. *)
480
481  {
482    graph with
483    regmap = RegMap.coalesce x y graph.regmap;
484    ivh = Vertex.Map.remove x graph.ivh;
485    pvh = Vertex.Map.remove x graph.pvh;
486    degree = PrioritySet.remove x graph.degree;
487    nmr = PrioritySet.remove x graph.nmr;
488  }
489 
490axiom ig_mkppp: interference_graph → register → register → interference_graph.
491axiom ig_mkpph: interference_graph → register → Register → interference_graph.
492axiom ig_coalesce: interference_graph → vertex → vertex → interference_graph.
493axiom ig_coalesceh: interference_graph → vertex → Register → interference_graph.
494axiom ig_remove: interference_graph → vertex → interference_graph.
495axiom ig_freeze: interference_graph → vertex → interference_graph.
496axiom ig_restrict: interference_graph → (vertex → bool) → interference_graph.
497axiom ig_droph: interference_graph → interference_graph.
498axiom ig_lookup: interference_graph → register → vertex.
499axiom ig_registers: interference_graph → vertex → list register.
500axiom ig_degree: interference_graph → vertex → nat.
501axiom ig_lowest: interference_graph → option (vertex × nat).
502axiom ig_lowest_non_move_related: interference_graph → option (vertex × nat).
503axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
504  interference_graph → option vertex.
505axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
506axiom ig_ipp: interference_graph → vertex → vertex_set.
507axiom ig_iph: interference_graph → vertex → list Register.
508axiom ig_ppp: interference_graph → vertex → vertex_set.
509axiom ig_pph: interference_graph → vertex → list Register.
510definition ig_ppedge ≝ vertex × vertex.
511axiom ig_pppick: interference_graph → (ig_ppedge → bool) → option ig_ppedge.
512definition ig_phedge ≝ vertex × Register.
513axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge.
514*)
Note: See TracBrowser for help on using the repository browser.