source: src/common/Registers.ma @ 936

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

Lots of work on RTL to ERTL pass from today.

File size: 532 bytes
Line 
1
2(* NB: this is essentially the same as Graphs! *)
3
4include "basics/types.ma".
5
6include "ASM/BitVectorTrie.ma".
7include "common/Identifiers.ma".
8include "ASM/I8051.ma".
9
10axiom RegisterTag : String.
11
12definition register ≝ identifier RegisterTag.
13
14definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.
15
16definition register_env ≝ identifier_map RegisterTag.
17
18(* dpm: fix the Register/register mismatch *)
19axiom Register_of_register: register → Register.
20axiom register_of_Register: Register → register.
Note: See TracBrowser for help on using the repository browser.