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

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

changes

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