source: src/utilities/adt/register_table.ma @ 1211

Last change on this file since 1211 was 1211, checked in by mulligan, 9 years ago

fixed interference file

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