source: src/common/Registers.ma @ 702

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

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

File size: 929 bytes
Line 
1
2(* NB: this is essentially the same as Graphs! *)
3
4include "basics/types.ma".
5include "utilities/binary/positive.ma".
6
7include "common/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.