source: src/common/Registers.ma @ 695

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

Rearrange Clight files a bit - will try to make them work again soon...

File size: 912 bytes
Line 
1
2(* NB: this is essentially the same as Graphs! *)
3
4include "basics/types.ma".
5include "binary/positive.ma".
6
7include "Maps.ma".
8
9definition register ≝ Pos.
10
11definition register_eq : ∀x,y:register. (x=y) + (x≠y).
12#x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y);
13[ #H %2 /2/; | #H %1 //; | #H %2 /2/ ] qed.
14
15record register_generation : Type[0] ≝ { reg_next : register }.
16
17definition register_new : register_generation → register × register_generation ≝
18λg. 〈reg_next g, mk_register_generation (succ (reg_next g))〉.
19
20definition register_env : Type[0] → Type[0] ≝ tree_t … PTree.
21definition register_empty : ∀T. register_env T ≝ λT. empty ? PTree T.
22definition register_lookup : ∀T. register_env T → register → option T ≝
23λT,g,l. get … l g.
24definition register_update : ∀T. register → T → register_env T → register_env T ≝
25λT,l,v,g. set … l v g.
Note: See TracBrowser for help on using the repository browser.