Last change
on this file since 648 was
639,
checked in by campbell, 9 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  

4  include "basics/types.ma". 

5  include "binary/positive.ma". 

6  

7  include "Maps.ma". 

8  

9  definition register ≝ Pos. 

10  

11  definition 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  

15  record register_generation : Type[0] ≝ { reg_next : register }. 

16  

17  definition register_new : register_generation → register × register_generation ≝ 

18  λg. 〈reg_next g, mk_register_generation (succ (reg_next g))〉. 

19  

20  definition register_env : Type[0] → Type[0] ≝ tree_t … PTree. 

21  definition register_empty : ∀T. register_env T ≝ λT. empty ? PTree T. 

22  definition register_lookup : ∀T. register_env T → register → option T ≝ 

23  λT,g,l. get … l g. 

24  definition 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.