source: src/common/Registers.ma @ 726

Last change on this file since 726 was 726, checked in by campbell, 9 years ago

Change identifiers to Words in Clight and RTLabs semantics.

File size: 1.1 KB
Line 
1
2(* NB: this is essentially the same as Graphs! *)
3
4include "basics/types.ma".
5
6include "ASM/BitVectorTrie.ma".
7include "Clight/AST.ma".
8include "common/Errors.ma".
9
10definition register ≝ ident.
11
12definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ ident_eq.
13
14record register_generation : Type[0] ≝ { reg_next : register }.
15
16definition register_gen_new : register_generation ≝ mk_register_generation (zero ?).
17
18definition register_new : register_generation → res (register × register_generation) ≝
19λg. let 〈gen, carries〉 ≝ add_with_carries ? (reg_next g) (zero ?) true in
20    if get_index_v ?? carries 0 ? then Error ? else
21      OK ? 〈reg_next g, mk_register_generation gen〉.
22// qed.
23
24definition register_env : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
25definition register_empty : ∀T. register_env T ≝ λT. Stub T 16.
26definition register_lookup : ∀T. register_env T → register → option T ≝
27λT,g,l. lookup_opt T 16 l g.
28definition register_update : ∀T. register → T → register_env T → register_env T ≝
29λT,l,v,g. insert T 16 l v g.
Note: See TracBrowser for help on using the repository browser.