source: src/utilities/RegisterSet.ma @ 2896

Last change on this file since 2896 was 1193, checked in by mulligan, 8 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.