|
Last change
on this file since 777 was
777,
checked in by mulligan, 10 years ago
|
|
Lots of work on RTL to ERTL pass from today.
|
|
File size:
1.3 KB
|
| Rev | Line | |
|---|
| [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; |
|---|
| 12 | rs_union: rs_set → rs_set → rs_set |
|---|
| 13 | }. |
|---|
| 14 | |
|---|
| 15 | (* dpm: horrendously inefficient, but will do for now *) |
|---|
| 16 | |
|---|
| 17 | definition rs_list_set_empty: list register ≝ [ ]. |
|---|
| 18 | |
|---|
| 19 | definition rs_list_set_singleton: register → list register ≝ λr. [ r ]. |
|---|
| 20 | |
|---|
| 21 | definition 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 | |
|---|
| 28 | definition 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 | |
|---|
| 36 | definition rs_list_set_exists ≝ |
|---|
| 37 | λr: register. |
|---|
| 38 | λs: list register. |
|---|
| 39 | member ? (eq_identifier ?) r s. |
|---|
| 40 | |
|---|
| 41 | definition rs_list_set_union ≝ |
|---|
| 42 | λr: list register. |
|---|
| 43 | λs: list register. |
|---|
| 44 | nub_by ? (eq_identifier ?) (r @ s). |
|---|
| 45 | |
|---|
| 46 | definition 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.
