Changeset 1212


Ignore:
Timestamp:
Sep 14, 2011, 5:03:17 PM (8 years ago)
Author:
mulligan
Message:

more added on interference graphs

Location:
src/utilities
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Interference.ma

    r1211 r1212  
    77include "utilities/adt/priority_set_adt.ma".
    88include "utilities/adt/set_adt.ma".
     9include "utilities/adt/set_table_adt.ma".
    910include "utilities/adt/register_table.ma".
    1011
     
    3738
    3839definition neighboursv ≝
    39   λset_impl.
    40   λgraph: graph set_impl.
    41     set_find … (ig_vertex_set … graph) v (getvv set_impl graph).
     40  λgraph: graph.
     41  λv: vertex.
     42    set_tbl_find … v (ig_ivv graph).
    4243
    4344  method neighborsv graph v =
     
    6263  ) regs1 graph
    6364
    64 axiom ig_mkiph: interference_graph → list register → list Register →
    65   interference_graph.
     65axiom ig_mkiph: graph → list register → list Register →
     66  graph.
    6667
    67 definition ig_mki: interference_graph → (list register) × (list Register) →
    68   (list register) × (list Register) → interference_graph ≝
     68definition ig_mki: graph → (list register) × (list Register) →
     69  (list register) × (list Register) → graph ≝
    6970  λgraph.
    7071  λregs1_hwregs1.
  • src/utilities/adt/set_table_adt.ma

    r1210 r1212  
    44include "utilities/adt/table_adt.ma".
    55include "utilities/adt/ordering.ma".
     6
     7axiom set_table: Type[0] → Type[0] → Type[0].
     8
     9axiom set_tbl_find: ∀key_type, a. key_type → set_table key_type (set a) → option a.
     10axiom set_tbl_add: ∀key_type, a. key_type → set a
     11                     → set_table key_type (set a) → set_table key_type (set a).
     12axiom set_tbl_update: ∀key_type, a. key_type → (set a → set a) → set_table key_type (set a)
     13                     → set_table key_type (set a).
     14axiom set_tbl_mkedge: ∀key_type, a. key_type → a → set_table key_type (set a) →
     15                         set_table key_type (set a).
     16axiom set_tbl_rmedge: ∀key_type, a. key_type → a → set_table key_type (set a) →
     17                         set_table key_type (set a).
     18axiom set_tbl_iter: ∀key_type, a. (key_type → a → a) →
     19                      set_table key_type (set a) → set_table key_type (set a).
     20axiom set_tbl_fold: ∀key_type, a, b: Type[0]. (key_type → a → b → b)
     21                      → set_table key_type (set a) -> b -> b.
     22axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) →
     23                      (key_type → a → bool) → option (key_type × a).
Note: See TracChangeset for help on using the changeset viewer.