[777] | 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; |
---|

[782] | 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 |
---|

[777] | 15 | }. |
---|

| 16 | |
---|

| 17 | (* dpm: horrendously inefficient, but will do for now *) |
---|

| 18 | |
---|

| 19 | definition rs_list_set_empty: list register ≝ [ ]. |
---|

| 20 | |
---|

| 21 | definition rs_list_set_singleton: register → list register ≝ λr. [ r ]. |
---|

| 22 | |
---|

| 23 | definition 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 | |
---|

| 30 | definition 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 | |
---|

| 38 | definition rs_list_set_exists ≝ |
---|

| 39 | λr: register. |
---|

| 40 | λs: list register. |
---|

| 41 | member ? (eq_identifier ?) r s. |
---|

| 42 | |
---|

| 43 | definition rs_list_set_union ≝ |
---|

| 44 | λr: list register. |
---|

| 45 | λs: list register. |
---|

| 46 | nub_by ? (eq_identifier ?) (r @ s). |
---|

| 47 | |
---|

[782] | 48 | definition rs_list_set_from_list ≝ |
---|

| 49 | λr: list register. |
---|

| 50 | nub_by ? (eq_identifier ?) r. |
---|

| 51 | |
---|

[777] | 52 | definition 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 |
---|

[782] | 56 | rs_list_set_union |
---|

| 57 | (λx. x) rs_list_set_from_list. |
---|