source: src/common/Registers.ma @ 882

Last change on this file since 882 was 777, checked in by mulligan, 10 years ago

Lots of work on RTL to ERTL pass from today.

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