Rev | Line | |
---|

[1210] | 1 | include "ASM/I8051.ma". |
---|

| 2 | include "common/Registers.ma". |
---|

| 3 | include "utilities/adt/ordering.ma". |
---|

| 4 | include "utilities/adt/set_adt.ma". |
---|

| 5 | |
---|

| 6 | definition vertex ≝ nat. (* XXX: int in o'caml *) |
---|

| 7 | |
---|

| 8 | axiom Register_ordered: ordered Register. |
---|

| 9 | axiom register_ordered: ordered register. |
---|

| 10 | axiom vertex_ordered: ordered vertex. |
---|

| 11 | |
---|

| 12 | axiom register_table: Type[0]. |
---|

| 13 | |
---|

| 14 | axiom rt_empty : register_table. |
---|

| 15 | |
---|

| 16 | axiom rt_forward : vertex → register_table → set Register. |
---|

| 17 | axiom rt_backward: Register → register_table → vertex. |
---|

| 18 | |
---|

| 19 | axiom rt_add: Register → vertex → register_table → register_table. |
---|

| 20 | axiom rt_remove: vertex → register_table → register_table. |
---|

| 21 | |
---|

[1211] | 22 | axiom rt_fold: ∀a: Type[0]. (vertex → set Register → a → a) → |
---|

| 23 | register_table → a → a. |
---|

[1210] | 24 | |
---|

| 25 | axiom rt_coalesce: vertex → vertex → register_table → register_table. |
---|

| 26 | axiom rt_restrict: (vertex → bool) → register_table → register_table. |
---|

**Note:** See

TracBrowser
for help on using the repository browser.