source: src/utilities/RegisterSet.ma @ 782

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

More work on rtl-ertl pass from today, plus resolved conflict.

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_identifier ?) 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_identifier ?) r s.
42   
43definition rs_list_set_union ≝
44  λr: list register.
45  λs: list register.
46    nub_by ? (eq_identifier ?) (r @ s).
47 
48definition rs_list_set_from_list ≝
49  λr: list register.
50    nub_by ? (eq_identifier ?) 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.