source: src/utilities/RegisterSet.ma @ 778

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

moved register set into correct place

File size: 1.3 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}.
14
15(* dpm: horrendously inefficient, but will do for now *)
16
17definition rs_list_set_empty: list register ≝ [ ].
18
19definition rs_list_set_singleton: register → list register ≝ λr. [ r ].
20
21definition rs_list_set_fold ≝
22  λA: Type[0].
23  λf: register → A → A.
24  λl: list register.
25  λa: A.
26    foldr ? ? f a l.
27   
28definition rs_list_set_insert ≝
29  λr: register.
30  λs: list register.
31  match member ? (eq_identifier ?) r s with
32  [ true ⇒ r :: s
33  | false ⇒ s
34  ].
35 
36definition rs_list_set_exists ≝
37  λr: register.
38  λs: list register.
39    member ? (eq_identifier ?) r s.
40   
41definition rs_list_set_union ≝
42  λr: list register.
43  λs: list register.
44    nub_by ? (eq_identifier ?) (r @ s).
45 
46definition register_list_set: register_set ≝
47  mk_register_set (list register) rs_list_set_empty
48                  rs_list_set_singleton rs_list_set_fold
49                  rs_list_set_insert rs_list_set_exists
50                  rs_list_set_union.
Note: See TracBrowser for help on using the repository browser.