Ignore:
Timestamp:
Sep 16, 2011, 5:15:35 PM (9 years ago)
Author:
mulligan
Message:

changes

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/utilities/Interference.ma

    r1219 r1223  
    22include "basics/list.ma".
    33include "common/Graphs.ma".
     4include "common/Order.ma".
    45include "common/Registers.ma".
    56
    … …  
    1011include "utilities/adt/register_table.ma".
    1112
    12 definition vertex_set ≝ set vertex.
     13(* definition vertex_set ≝ set vertex. *)
    1314definition vertex_priority_set ≝ priority_set vertex.
    1415definition vertex_set_table ≝ set_table vertex (set vertex).
    … …  
    1819record graph: Type[0] ≝
    1920{
    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
     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
    2728}.
    2829
    … …  
    3031  λgraph.
    3132  λ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
     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
    3839      mk_graph
    3940        regmap ivv ivh pvv pvh degree nmr.
    … …  
    4243  λgraph.
    4344  λ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
     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
    5051      mk_graph
    5152        regmap ivv ivh pvv pvh degree nmr.
    … …  
    5455  λgraph.
    5556  λ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
     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
    6263      mk_graph
    6364        regmap ivv ivh pvv pvh degree nmr.
    … …  
    6667  λgraph.
    6768  λ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
     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
    7475      mk_graph
    7576        regmap ivv ivh pvv pvh degree nmr.
    … …  
    7879  λgraph: graph.
    7980  λv: vertex.
    80     set_tbl_find … v (ig_ivv graph).
     81    set_tbl_find … v (g_ivv graph).
    8182
    8283definition sg_existsvv ≝
    … …  
    8687  match sg_neighboursv graph v2 with
    8788  [ None       ⇒ false (* XXX: ok? *)
    88   | Some neigh ⇒ set_member ? v1 neigh
     89  | Some neigh ⇒ set_member ? eq_nat v1 neigh
    8990  ].
    9091
    … …  
    9293  λgraph.
    9394  λv.
    94     set_tbl_find ? ? v (ig_ivh graph).
     95    set_tbl_find ? ? v (g_ivh graph).
    9596
    9697definition sg_existsvh ≝
    … …  
    100101  match sg_neighboursh graph v with
    101102  [ None       ⇒ false (* XXX: ok? *)
    102   | Some neigh ⇒ set_member ? h neigh
     103  | Some neigh ⇒ set_member ? eq_Register h neigh
    103104  ].
    104105
    … …  
    118119  λgraph: graph.
    119120    let union ≝ λkey: vertex. set_union ? in
    120     set_tbl_fold vertex ? ? union (ig_ivh graph) (set_empty Register).
     121    set_tbl_fold vertex ? ? union (g_ivh graph) (set_empty Register).
    121122
    122123axiom sg_iter: Type[0]. (* XXX: todo when i can be bothered *)
    … …  
    126127  λv1.
    127128  λv2.
    128     set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (ig_ivv graph)).
     129    set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (g_ivv graph)).
    129130
    130131definition sg_mkvv ≝
    … …  
    143144  λv1.
    144145  λv2.
    145     set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (ig_ivv graph)).
     146    set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (g_ivv graph)).
    146147
    147148definition sg_rmvvifx ≝
    … …  
    158159  λv.
    159160  λh.
    160     set_ivh graph (set_tbl_update … v (set_insert … h) (ig_ivh graph)).
     161    set_ivh graph (set_tbl_update … v (set_insert … h) (g_ivh graph)).
    161162
    162163definition sg_mkvh ≝
    … …  
    173174  λv.
    174175  λh.
    175     set_ivh graph (set_tbl_update … v (set_remove … h) (ig_ivh graph)).
     176    set_ivh graph (set_tbl_update … v (set_remove … h) (g_ivh graph)).
    176177
    177178definition sg_rmvhifx ≝
    … …  
    250251  let graph ≝ sg_mkvvi graph v1 v2 in
    251252  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
     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
    254255    set_degree (set_nmr graph nmr') degree'.
    255256
    … …  
    259260  λv2.
    260261  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
     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
    263264    set_degree (set_nmr graph nmr') degree'.
    264265
    … …  
    269270  let graph ≝ sg_mkvhi graph v h in
    270271  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
     272  let degree ≝ pset_increment ? v (repr 1) (g_degree graph) in
     273  let nmr ≝ pset_incrementifx ? v (repr 1) (g_nmr graph) in
    273274    set_degree (set_nmr graph nmr) degree.
    274275
    … …  
    278279  λh.
    279280  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
     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
    282283    set_degree (set_nmr graph nmr) degree.
    283284
    … …  
    299300  λv.
    300301    if pref_nmr graph v then
    301       let nmr' ≝ pset_remove ? v (ig_nmr graph) in
     302      let nmr' ≝ pset_remove ? v (g_nmr graph) in
    302303        set_nmr graph nmr'
    303304    else
    … …  
    330331  λv.
    331332  if pref_nmr graph v then
    332     match pset_lookup ? v (ig_degree graph) with
     333    match pset_lookup ? v (g_degree graph) with
    333334    [ None ⇒ graph (* XXX: ok? *)
    334335    | Some pref ⇒
    335       let nmr ≝ pset_insert ? v pref (ig_nmr graph) in
     336      let nmr ≝ pset_insert ? v pref (g_nmr graph) in
    336337        set_nmr graph nmr
    337338    ]
    … …  
    355356  let graph ≝ pref_rmcheck graph v in
    356357    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.
    357400
    358401definition ig_create ≝
    … …  
    365408        〈v + 1, table'', priority''〉) 〈0, rt_empty …, pset_empty …〉 regs
    366409  in
    367       mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_empty …)
    368       (set_empty …) priority'' priority''.
    369 
    370 
    371 
     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).
    372414definition ig_mkipp ≝
    373   λset_impl.
    374   λgraph: interference_graph set_impl.
     415  λgraph.
    375416  λregs1.
    376417  λ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 
    382 let 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 
    390 axiom ig_mkiph: graph → list register → list Register →
    391   graph.
    392 
    393 definition ig_mki: graph → (list register) × (list Register) →
    394   (list register) × (list Register) → graph ≝
     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 ≝
    395435  λgraph.
    396436  λregs1_hwregs1.
    397437  λ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.
     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  }
    404489 
    405490axiom ig_mkppp: interference_graph → register → register → interference_graph.
    … …  
    427512definition ig_phedge ≝ vertex × Register.
    428513axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge.
     514*)
Note: See TracChangeset for help on using the changeset viewer.