Changeset 1218 for src/utilities/adt


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

a lot added to interference graph calculation

Location:
src/utilities/adt
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • 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.