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

getting rid of typeclasslike records in favour of filelevel axioms. much too heavyweight to use effectively

File size:
905 bytes

Line  

1  include "ASM/I8051.ma". 

2  include "common/Registers.ma". 

3  include "utilities/adt/ordering.ma". 

4  include "utilities/adt/set_adt.ma". 

5  

6  definition vertex ≝ nat. (* XXX: int in o'caml *) 

7  

8  axiom Register_ordered: ordered Register. 

9  axiom register_ordered: ordered register. 

10  axiom vertex_ordered: ordered vertex. 

11  

12  axiom register_table: Type[0]. 

13  

14  axiom rt_empty : register_table. 

15  

16  axiom rt_forward : vertex → register_table → set Register. 

17  axiom rt_backward: Register → register_table → vertex. 

18  

19  axiom rt_add: Register → vertex → register_table → register_table. 

20  axiom rt_remove: vertex → register_table → register_table. 

21  

22  axiom rt_fold: ∀a: Type[0]. (vertex → set … set_impl Register → a → a) → 

23  register_table → a → a; 

24  

25  axiom rt_coalesce: vertex → vertex → register_table → register_table. 

26  axiom rt_restrict: (vertex → bool) → register_table → register_table. 

Note: See
TracBrowser
for help on using the repository browser.