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.