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

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

added adts for sets, tables and priority sets in order to make life easier when working on the interference graph code

File size: 2.1 KB
Line 
1include "basics/types.ma".
2include "basics/list.ma".
3include "arithmetics/nat.ma".
4
5include "utilities/adt/ordering.ma".
6include "ASM/Util.ma".
7
8record priority_set_adt
9  (elt_type: Type[0]) (order: ordered elt_type): Type[1] ≝
10{
11  priority_set: Type[0] → Type[0];
12 
13  ps_empty       : priority_set elt_type;
14  ps_size        : priority_set elt_type → nat;
15 
16  ps_to_list     : priority_set elt_type → list (elt_type × nat);
17 
18  ps_insert      : elt_type → nat → priority_set elt_type → priority_set elt_type;
19  ps_remove      : elt_type → priority_set elt_type → priority_set elt_type;
20  ps_lookup      : elt_type → priority_set elt_type → option nat;
21 
22  ps_increment   : elt_type → priority_set elt_type → priority_set elt_type;
23  ps_modify      : elt_type → nat → priority_set elt_type → priority_set elt_type;
24  ps_lowest      : priority_set elt_type → option (elt_type × nat);
25 
26  ps_equal       : priority_set elt_type → priority_set elt_type → bool;
27 
28  ps_map         : ∀a: Type[0]. (elt_type → a) → priority_set elt_type → priority_set a;
29  ps_fold        : ∀a: Type[0]. (elt_type → nat → a → a) → priority_set elt_type
30                  → a → a 
31}.
32
33definition ps_is_empty ≝
34  λelt_type         : Type[0].
35  λorder            : ordered elt_type.
36  λpriority_set_adt : priority_set_adt elt_type order.
37  λpriority_set     : priority_set elt_type order priority_set_adt elt_type.
38    ps_size … priority_set = 0.
39
40definition ps_singleton ≝
41  λelt_type        : Type[0].
42  λorder           : ordered elt_type.
43  λpriority_set_adt: priority_set_adt elt_type order.
44  λelt             : elt_type.
45  λpriority        : nat.
46    ps_insert … elt priority (ps_empty elt_type order priority_set_adt).
47
48definition from_list ≝
49  λelt_type        : Type[0].
50  λorder           : ordered elt_type.
51  λpriority_set_adt: priority_set_adt elt_type order.
52  λthe_list        : list (elt_type × nat).
53    foldr … (λelt_priority.
54      let 〈elt, priority〉 ≝ elt_priority in
55        ps_insert elt_type order priority_set_adt elt priority)
56          (ps_empty …) the_list.
Note: See TracBrowser for help on using the repository browser.