source: src/utilities/RegisterSet.ma @ 1075

Last change on this file since 1075 was 1075, checked in by mulligan, 9 years ago

nearly completed rtl -> ertl pass removing all option types with dep. types

File size: 1.5 KB
Line 
1include "ASM/I8051.ma".
2include "common/Registers.ma".
3
4record register_set: Type[1] ≝
5{
6  rs_set: Type[0];
7  rs_empty: rs_set;
8  rs_singleton: Register → rs_set;
9  rs_fold: ∀A: Type[0]. (Register → A → A) → rs_set → A → A;
10  rs_insert: Register → rs_set → rs_set;
11  rs_exists: Register → rs_set → bool;
12  rs_union: rs_set → rs_set → rs_set;
13  rs_to_list: rs_set → list Register;
14  rs_from_list: list Register → rs_set
15}.
16
17(* dpm: horrendously inefficient, but will do for now *)
18
19definition rs_list_set_empty: list Register ≝ [ ].
20
21definition rs_list_set_singleton: Register → list Register ≝ λr. [ r ].
22
23definition rs_list_set_fold ≝
24  λA: Type[0].
25  λf: Register → A → A.
26  λl: list Register.
27  λa: A.
28    foldr ? ? f a l.
29   
30definition rs_list_set_insert ≝
31  λr: Register.
32  λs: list Register.
33  match member ? eq_Register r s with
34  [ true ⇒ r :: s
35  | false ⇒ s
36  ].
37 
38definition rs_list_set_exists ≝
39  λr: Register.
40  λs: list Register.
41    member ? eq_Register r s.
42   
43definition rs_list_set_union ≝
44  λr: list Register.
45  λs: list Register.
46    nub_by ? eq_Register (r @ s).
47 
48definition rs_list_set_from_list ≝
49  λr: list Register.
50    nub_by ? eq_Register r.
51 
52definition register_list_set: register_set ≝
53  mk_register_set (list Register) rs_list_set_empty
54                  rs_list_set_singleton rs_list_set_fold
55                  rs_list_set_insert rs_list_set_exists
56                  rs_list_set_union
57                  (λx. x) rs_list_set_from_list.
Note: See TracBrowser for help on using the repository browser.