Changeset 1218


Ignore:
Timestamp:
Sep 15, 2011, 4:56:30 PM (8 years ago)
Author:
mulligan
Message:

a lot added to interference graph calculation

Location:
src/utilities
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Interference.ma

    r1212 r1218  
    1212definition vertex_set ≝ set vertex.
    1313definition vertex_priority_set ≝ priority_set vertex.
     14definition vertex_set_table ≝ set_table vertex (set vertex).
     15definition Register_set_table ≝ set_table vertex (set Register).
    1416definition Register_set ≝ set Register.
    1517
    16 record graph: Type[1] ≝
     18record graph: Type[0] ≝
    1719{
    1820  ig_regmap     : register_table;
    19   ig_ivv        : vertex_set;
    20   ig_ivh        : Register_set;
     21  ig_ivv        : vertex_set_table;
     22  ig_ivh        : Register_set_table;
    2123  ig_pvv        : vertex_set;
    2224  ig_pvh        : Register_set;
     
    2426  ig_nmr        : vertex_priority_set
    2527}.
     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
     358
    26359
    27360definition ig_create ≝
     
    34367        〈v + 1, table'', priority''〉) 〈0, rt_empty …, ps_empty …〉 regs
    35368  in
    36       mk_graph table'' (set_empty …) (set_empty …) (set_empty …)
     369      mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_empty …)
    37370      (set_empty …) priority'' priority''.
    38371
    39 definition neighboursv ≝
    40   λgraph: graph.
    41   λv: vertex.
    42     set_tbl_find … v (ig_ivv graph).
    43 
    44   method neighborsv graph v =
    45     VertexSetMap.find v (self#getvv graph)
     372
    46373
    47374definition ig_mkipp ≝
  • src/utilities/adt/priority_set_adt.ma

    r1210 r1218  
    22include "basics/list.ma".
    33include "arithmetics/nat.ma".
     4include "common/Integers.ma".
    45
    56include "utilities/adt/ordering.ma".
     
    89axiom priority_set: Type[0] → Type[0].
    910 
    10 axiom ps_empty: ∀elt_type. priority_set elt_type.
    11 axiom ps_size: ∀elt_type. priority_set elt_type → nat.
     11axiom pset_empty: ∀elt_type. priority_set elt_type.
     12axiom pset_size: ∀elt_type. priority_set elt_type → nat.
    1213 
    13 axiom ps_to_list: ∀elt_type. priority_set elt_type → list (elt_type × nat).
     14axiom pset_to_list: ∀elt_type. priority_set elt_type → list (elt_type × nat).
    1415 
    15 axiom ps_insert: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type.
    16 axiom ps_remove: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type.
    17 axiom ps_lookup: ∀elt_type. elt_type → priority_set elt_type → option nat.
     16axiom pset_insert: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type.
     17axiom pset_remove: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type.
     18axiom pset_lookup: ∀elt_type. elt_type → priority_set elt_type → option nat.
    1819 
    19 axiom ps_increment: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type.
    20 axiom ps_modify: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type.
    21 axiom ps_lowest: ∀elt_type. priority_set elt_type → option (elt_type × nat).
     20axiom pset_increment: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type.
     21axiom pset_incrementifx: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type.
     22axiom pset_modify: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type.
     23axiom pset_lowest: ∀elt_type. priority_set elt_type → option (elt_type × nat).
    2224 
    23 axiom ps_equal: ∀elt_type. priority_set elt_type → priority_set elt_type → bool.
     25axiom pset_equal: ∀elt_type. priority_set elt_type → priority_set elt_type → bool.
    2426 
    25 axiom ps_map: ∀elt_type. ∀a: Type[0]. (elt_type → a) → priority_set elt_type → priority_set a.
    26 axiom ps_fold: ∀elt_type. ∀a: Type[0]. (elt_type → nat → a → a) → priority_set elt_type → a → a.
     27axiom pset_map: ∀elt_type. ∀a: Type[0]. (elt_type → a) → priority_set elt_type → priority_set a.
     28axiom pset_fold: ∀elt_type. ∀a: Type[0]. (elt_type → int → a → a) → priority_set elt_type → a → a.
    2729
    28 definition ps_is_empty ≝
     30definition pset_is_empty ≝
    2931  λelt_type         : Type[0].
    3032  λpriority_set     : priority_set elt_type.
    31     ps_size … priority_set = 0.
     33    pset_size … priority_set = 0.
    3234
    33 definition ps_singleton ≝
     35definition pset_singleton ≝
    3436  λelt_type        : Type[0].
    3537  λelt             : elt_type.
    3638  λpriority        : nat.
    37     ps_insert … elt priority (ps_empty elt_type).
     39    pset_insert … elt priority (pset_empty elt_type).
    3840
    39 definition from_list ≝
     41definition pset_from_list ≝
    4042  λelt_type        : Type[0].
    4143  λthe_list        : list (elt_type × nat).
    4244    foldr … (λelt_priority.
    4345      let 〈elt, priority〉 ≝ elt_priority in
    44         ps_insert elt_type elt priority)
    45           (ps_empty …) the_list.
     46        pset_insert elt_type elt priority)
     47          (pset_empty …) the_list.
  • src/utilities/adt/set_adt.ma

    r1210 r1218  
    22include "basics/list.ma".
    33include "arithmetics/nat.ma".
     4include "ASM/Util.ma".
    45
    56include "utilities/adt/ordering.ma".
     
    2324  λelt_type: Type[0].
    2425  λset: set elt_type.
    25     set_size elt_type set = 0.
     26    eq_nat (set_size elt_type set) 0.
    2627
    2728definition set_singleton ≝
  • src/utilities/adt/set_table_adt.ma

    r1212 r1218  
    77axiom set_table: Type[0] → Type[0] → Type[0].
    88
    9 axiom set_tbl_find: ∀key_type, a. key_type → set_table key_type (set a) → option a.
     9axiom set_tbl_empty: ∀key_type, a. set_table key_type a.
     10axiom set_tbl_find: ∀key_type, a. key_type → set_table key_type (set a) → option (set a).
    1011axiom set_tbl_add: ∀key_type, a. key_type → set a
    1112                     → set_table key_type (set a) → set_table key_type (set a).
     
    1920                      set_table key_type (set a) → set_table key_type (set a).
    2021axiom set_tbl_fold: ∀key_type, a, b: Type[0]. (key_type → a → b → b)
    21                       → set_table key_type (set a) -> b -> b.
     22                      → set_table key_type a -> b -> b.
    2223axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) →
    2324                      (key_type → a → bool) → option (key_type × a).
     25
     26
     27axiom set_tbl_homo_mkbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type).
     28axiom set_tbl_homo_rmbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type).
     29axiom set_tbl_homo_reverse: ∀key_type. set_table key_type (set key_type) → set_table key_type (set key_type).
     30axiom set_tbl_homo_restrict: ∀key_type. (key_type → bool) → set_table key_type (set key_type) → set_table key_type (set key_type).
  • src/utilities/adt/table_adt.ma

    r1210 r1218  
    3535axiom tbl_map    : ∀key_type, rng_type. ∀a: Type[0]. (rng_type → a) → table key_type rng_type
    3636                   → table key_type a.
    37 axiom tbl_fold   : ∀key_type, rng_type. ∀a: Type[0]. (key_type → a → a) → table key_type rng_type → a → a.
     37axiom tbl_fold   : ∀key_type, a, b: Type[0]. (key_type → a → b → b) → table key_type a → b → b.
    3838
    3939definition tbl_is_empty ≝
Note: See TracChangeset for help on using the changeset viewer.