Changeset 1223 for src/utilities


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

changes

Location:
src/utilities
Files:
6 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*)
  • src/utilities/adt/priority_set_adt.ma

    r1218 r1223  
    44include "common/Integers.ma".
    55
    6 include "utilities/adt/ordering.ma".
    76include "ASM/Util.ma".
    87
  • src/utilities/adt/register_table.ma

    r1211 r1223  
    11include "ASM/I8051.ma".
    22include "common/Registers.ma".
    3 include "utilities/adt/ordering.ma".
    43include "utilities/adt/set_adt.ma".
    54
    65definition vertex ≝ nat. (* XXX: int in o'caml *)
    76
     7(*
    88axiom Register_ordered: ordered Register.
    99axiom register_ordered: ordered register.
    1010axiom vertex_ordered: ordered vertex.
     11*)
    1112
    1213axiom register_table: Type[0].
    1314 
    1415axiom rt_empty : register_table.
     16
     17axiom rt_insert: vertex → set Register → register_table → register_table.
    1518 
    1619axiom rt_forward : vertex → register_table → set Register.
  • src/utilities/adt/set_adt.ma

    r1218 r1223  
    33include "arithmetics/nat.ma".
    44include "ASM/Util.ma".
    5 
    6 include "utilities/adt/ordering.ma".
    75
    86axiom set: Type[0] → Type[0].
     
    1311axiom set_insert: ∀elt_type. elt_type → set elt_type → set elt_type.
    1412axiom set_remove: ∀elt_type. elt_type → set elt_type → set elt_type.
    15 axiom set_member: ∀elt_type. elt_type → set elt_type → bool.
     13axiom set_member: ∀elt_type. (elt_type → elt_type → bool) → elt_type → set elt_type → bool.
    1614axiom set_forall: ∀elt_type. (elt_type → bool) → set elt_type → bool.
    1715axiom set_exists: ∀elt_type. (elt_type → bool) → set elt_type → bool.
    1816axiom set_filter: ∀elt_type. (elt_type → bool) → set elt_type → set elt_type.
    19 axiom set_equal: ∀elt_type. set elt_type → set elt_type → bool.
    2017axiom set_map: ∀elt_type, a. (elt_type → a) → set elt_type → set a.
    2118axiom set_fold: ∀elt_type, a: Type[0]. (elt_type → a → a) → set elt_type  → a → a.
     19axiom set_equal: ∀elt_type: Type[0]. (elt_type → elt_type → bool) →
     20  set elt_type → set elt_type → bool.
     21
     22(* XXX: define in terms of primitives *)
     23axiom set_diff: ∀elt_type: Type[0]. set elt_type → set elt_type → set elt_type.
    2224
    2325definition set_is_empty ≝
     
    4749definition set_subset ≝
    4850  λelt_type: Type[0].
     51  λeq      : elt_type → elt_type → bool.
    4952  λleft    : set elt_type.
    5053  λright   : set elt_type.
    51     set_forall elt_type (λelt. set_member elt_type elt right) left.
     54    set_forall elt_type (λelt. set_member elt_type eq elt right) left.
    5255
    5356definition set_subseteq ≝
    5457  λelt_type: Type[0].
     58  λeq      : elt_type → elt_type → bool.
    5559  λleft    : set elt_type.
    5660  λright   : set elt_type.
    57     set_equal elt_type left right ∧ (set_subset elt_type left right).
     61    set_equal elt_type eq left right ∧ (set_subset elt_type eq left right).
    5862
    5963definition set_union ≝
     
    6569definition set_intersection ≝
    6670  λelt_type: Type[0].
     71  λeq      : elt_type → elt_type → bool.
    6772  λleft    : set elt_type.
    6873  λright   : set elt_type.
    69     set_filter elt_type (λelt. set_member elt_type elt right) left.
     74    set_filter elt_type (λelt. set_member elt_type eq elt right) left.
  • src/utilities/adt/set_table_adt.ma

    r1218 r1223  
    33include "utilities/adt/set_adt.ma".
    44include "utilities/adt/table_adt.ma".
    5 include "utilities/adt/ordering.ma".
    65
    76axiom set_table: Type[0] → Type[0] → Type[0].
     
    2221                      → set_table key_type a -> b -> b.
    2322axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) →
    24                       (key_type → a → bool) → option (key_type × a).
     23                      ((key_type × a) → bool) → option (key_type × a).
    2524
    2625
  • src/utilities/adt/table_adt.ma

    r1218 r1223  
    55include "arithmetics/nat.ma".
    66
    7 include "utilities/adt/ordering.ma".
    87include "utilities/adt/equal.ma".
    98
Note: See TracChangeset for help on using the changeset viewer.