source: src/utilities/RegisterSet.ma @ 2474

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

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

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