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_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 | |
---|

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_Register 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_Register r s. |
---|

42 | |
---|

43 | definition rs_list_set_union ≝ |
---|

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

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

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

47 | |
---|

48 | definition rs_list_set_from_list ≝ |
---|

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

50 | nub_by ? eq_Register r. |
---|

51 | |
---|

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

56 | rs_list_set_union |
---|

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