 Timestamp:
 Sep 14, 2011, 5:03:17 PM (9 years ago)
 Location:
 src/utilities
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/Interference.ma
r1211 r1212 7 7 include "utilities/adt/priority_set_adt.ma". 8 8 include "utilities/adt/set_adt.ma". 9 include "utilities/adt/set_table_adt.ma". 9 10 include "utilities/adt/register_table.ma". 10 11 … … 37 38 38 39 definition neighboursv ≝ 39 λ set_impl.40 λ graph: graph set_impl.41 set_ find … (ig_vertex_set … graph) v (getvv set_implgraph).40 λgraph: graph. 41 λv: vertex. 42 set_tbl_find … v (ig_ivv graph). 42 43 43 44 method neighborsv graph v = … … 62 63 ) regs1 graph 63 64 64 axiom ig_mkiph: interference_graph → list register → list Register →65 interference_graph.65 axiom ig_mkiph: graph → list register → list Register → 66 graph. 66 67 67 definition ig_mki: interference_graph → (list register) × (list Register) →68 (list register) × (list Register) → interference_graph ≝68 definition ig_mki: graph → (list register) × (list Register) → 69 (list register) × (list Register) → graph ≝ 69 70 λgraph. 70 71 λregs1_hwregs1. 
src/utilities/adt/set_table_adt.ma
r1210 r1212 4 4 include "utilities/adt/table_adt.ma". 5 5 include "utilities/adt/ordering.ma". 6 7 axiom set_table: Type[0] → Type[0] → Type[0]. 8 9 axiom set_tbl_find: ∀key_type, a. key_type → set_table key_type (set a) → option a. 10 axiom set_tbl_add: ∀key_type, a. key_type → set a 11 → set_table key_type (set a) → set_table key_type (set a). 12 axiom 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). 14 axiom set_tbl_mkedge: ∀key_type, a. key_type → a → set_table key_type (set a) → 15 set_table key_type (set a). 16 axiom set_tbl_rmedge: ∀key_type, a. key_type → a → set_table key_type (set a) → 17 set_table key_type (set a). 18 axiom set_tbl_iter: ∀key_type, a. (key_type → a → a) → 19 set_table key_type (set a) → set_table key_type (set a). 20 axiom set_tbl_fold: ∀key_type, a, b: Type[0]. (key_type → a → b → b) 21 → set_table key_type (set a) > b > b. 22 axiom 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.