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

a lot added to interference graph calculation

File:
1 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.
Note: See TracChangeset for help on using the changeset viewer.