| Line | |
|---|
| 1 | include "ASM/I8051.ma". |
|---|
| 2 | include "common/Registers.ma". |
|---|
| 3 | include "utilities/adt/set_adt.ma". |
|---|
| 4 | |
|---|
| 5 | definition vertex ≝ nat. (* XXX: int in o'caml *) |
|---|
| 6 | |
|---|
| 7 | (* |
|---|
| 8 | axiom Register_ordered: ordered Register. |
|---|
| 9 | axiom register_ordered: ordered register. |
|---|
| 10 | axiom vertex_ordered: ordered vertex. |
|---|
| 11 | *) |
|---|
| 12 | |
|---|
| 13 | axiom register_table: Type[0]. |
|---|
| 14 | |
|---|
| 15 | axiom rt_empty : register_table. |
|---|
| 16 | |
|---|
| 17 | axiom rt_insert: vertex → set Register → register_table → register_table. |
|---|
| 18 | |
|---|
| 19 | axiom rt_forward : vertex → register_table → set Register. |
|---|
| 20 | axiom rt_backward: Register → register_table → vertex. |
|---|
| 21 | |
|---|
| 22 | axiom rt_add: Register → vertex → register_table → register_table. |
|---|
| 23 | axiom rt_remove: vertex → register_table → register_table. |
|---|
| 24 | |
|---|
| 25 | axiom rt_fold: ∀a: Type[0]. (vertex → set Register → a → a) → |
|---|
| 26 | register_table → a → a. |
|---|
| 27 | |
|---|
| 28 | axiom rt_coalesce: vertex → vertex → register_table → register_table. |
|---|
| 29 | axiom rt_restrict: (vertex → bool) → register_table → register_table. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
