| 1 | include "ASM/I8051.ma". |
|---|
| 2 | include "common/Registers.ma". |
|---|
| 3 | |
|---|
| 4 | record 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 | |
|---|
| 20 | definition rs_list_set_empty: list Register ≝ [ ]. |
|---|
| 21 | |
|---|
| 22 | definition rs_list_set_singleton: Register → list Register ≝ λr. [ r ]. |
|---|
| 23 | |
|---|
| 24 | definition 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 | |
|---|
| 31 | definition 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 | |
|---|
| 39 | definition rs_list_set_exists ≝ |
|---|
| 40 | λr: Register. |
|---|
| 41 | λs: list Register. |
|---|
| 42 | member ? eq_Register r s. |
|---|
| 43 | |
|---|
| 44 | definition rs_list_set_union ≝ |
|---|
| 45 | λr: list Register. |
|---|
| 46 | λs: list Register. |
|---|
| 47 | nub_by ? eq_Register (r @ s). |
|---|
| 48 | |
|---|
| 49 | definition rs_list_set_subset ≝ |
|---|
| 50 | λr: list Register. |
|---|
| 51 | λs: list Register. |
|---|
| 52 | forall … (λx. member … eq_Register x s) r. |
|---|
| 53 | |
|---|
| 54 | definition rs_list_set_from_list ≝ |
|---|
| 55 | λr: list Register. |
|---|
| 56 | nub_by ? eq_Register r. |
|---|
| 57 | |
|---|
| 58 | definition 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. |
|---|
