source: src/utilities/RegisterSet.ma @ 1282

Last change on this file since 1282 was 1193, checked in by mulligan, 10 years ago

work on colouring algorithm halted as it can be axiomatised. now implementing interference graphs (objects!)

File size: 1.7 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_subset: rs_set → rs_set → bool;
14  rs_to_list: rs_set → list Register;
15  rs_from_list: list Register → rs_set
16}.
17
18(* dpm: horrendously inefficient, but will do for now *)
19
20definition rs_list_set_empty: list Register ≝ [ ].
21
22definition rs_list_set_singleton: Register → list Register ≝ λr. [ r ].
23
24definition rs_list_set_fold ≝
25  λA: Type[0].
26  λf: Register → A → A.
27  λl: list Register.
28  λa: A.
29    foldr ? ? f a l.
30   
31definition rs_list_set_insert ≝
32  λr: Register.
33  λs: list Register.
34  match member ? eq_Register r s with
35  [ true ⇒ r :: s
36  | false ⇒ s
37  ].
38 
39definition rs_list_set_exists ≝
40  λr: Register.
41  λs: list Register.
42    member ? eq_Register r s.
43   
44definition rs_list_set_union ≝
45  λr: list Register.
46  λs: list Register.
47    nub_by ? eq_Register (r @ s).
48
49definition rs_list_set_subset ≝
50  λr: list Register.
51  λs: list Register.
52    forall … (λx. member … eq_Register x s) r.
53 
54definition rs_list_set_from_list ≝
55  λr: list Register.
56    nub_by ? eq_Register r.
57 
58definition register_list_set: register_set ≝
59  mk_register_set (list Register) rs_list_set_empty
60                  rs_list_set_singleton rs_list_set_fold
61                  rs_list_set_insert rs_list_set_exists
62                  rs_list_set_union
63                  rs_list_set_subset
64                  (λx. x) rs_list_set_from_list.
Note: See TracBrowser for help on using the repository browser.