source: src/common/Registers.ma @ 710

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

Start of way to import RTLabs from prototype compiler.

File size: 1012 bytes
RevLine 
[639]1
2(* NB: this is essentially the same as Graphs! *)
3
4include "basics/types.ma".
[702]5include "utilities/binary/positive.ma".
[639]6
[702]7include "common/Maps.ma".
[639]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
[710]17definition register_gen_new : register_generation ≝ mk_register_generation one.
18
[639]19definition register_new : register_generation → register × register_generation ≝
20λg. 〈reg_next g, mk_register_generation (succ (reg_next g))〉.
21
22definition register_env : Type[0] → Type[0] ≝ tree_t … PTree.
23definition register_empty : ∀T. register_env T ≝ λT. empty ? PTree T.
24definition register_lookup : ∀T. register_env T → register → option T ≝
25λT,g,l. get … l g.
26definition register_update : ∀T. register → T → register_env T → register_env T ≝
27λT,l,v,g. set … l v g.
Note: See TracBrowser for help on using the repository browser.