source: src/common/Registers.ma @ 757

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

Lots more fixing to get both front and backends using same conventions and types.

File size: 481 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.
Note: See TracBrowser for help on using the repository browser.