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

Last change on this file since 1210 was 1210, checked in by mulligan, 8 years ago

getting rid of typeclass-like records in favour of file-level axioms. much too heavyweight to use effectively

File size: 905 bytes
Line 
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
22axiom rt_fold: ∀a: Type[0]. (vertex → set … set_impl Register → a → a) →
23   register_table → a → a;
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.