source: src/Clight/Registers.ma @ 694

Last change on this file since 694 was 639, checked in by campbell, 10 years ago

Preliminary work on RTLabs semantics
Will move to somewhere more appropriate 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.