source: src/utilities/adt/priority_set_adt.ma @ 1218

Last change on this file since 1218 was 1218, checked in by mulligan, 8 years ago

a lot added to interference graph calculation

File size: 2.0 KB
Line 
1include "basics/types.ma".
2include "basics/list.ma".
3include "arithmetics/nat.ma".
4include "common/Integers.ma".
5
6include "utilities/adt/ordering.ma".
7include "ASM/Util.ma".
8
9axiom priority_set: Type[0] → Type[0].
10 
11axiom pset_empty: ∀elt_type. priority_set elt_type.
12axiom pset_size: ∀elt_type. priority_set elt_type → nat.
13 
14axiom pset_to_list: ∀elt_type. priority_set elt_type → list (elt_type × nat).
15 
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.
19 
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).
24 
25axiom pset_equal: ∀elt_type. priority_set elt_type → priority_set elt_type → bool.
26 
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.
29
30definition pset_is_empty ≝
31  λelt_type         : Type[0].
32  λpriority_set     : priority_set elt_type.
33    pset_size … priority_set = 0.
34
35definition pset_singleton ≝
36  λelt_type        : Type[0].
37  λelt             : elt_type.
38  λpriority        : nat.
39    pset_insert … elt priority (pset_empty elt_type).
40
41definition pset_from_list ≝
42  λelt_type        : Type[0].
43  λthe_list        : list (elt_type × nat).
44    foldr … (λelt_priority.
45      let 〈elt, priority〉 ≝ elt_priority in
46        pset_insert elt_type elt priority)
47          (pset_empty …) the_list.
Note: See TracBrowser for help on using the repository browser.