source: src/utilities/RegisterSet.ma @ 1784

Last change on this file since 1784 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
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.