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

Last change on this file since 1208 was 1208, checked in by mulligan, 10 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
RevLine 
[1208]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.