Library Heap

Parameter Heap : Set → Set.
Parameter Loc : Set.

Parameter empty : ∀ {A}, Heap A.
Parameter deref : ∀ {A}, Heap A → Loc → option A.
Parameter update : ∀ {A}, Heap A → Loc → A → Heap A.
Parameter alloc : ∀ {A}, Heap A → A → (Heap A × Loc).

Parameter hmap: ∀ {A B : Set}, (A → B) → Heap A → Heap B.

Axiom hmap_empty : ∀ {A B : Set} {f : A → B}, hmap f empty = empty.
Axiom hmap_deref : ∀ {A B : Set} {f : A → B} h l, deref (hmap f h) l = option_map f (deref h l).
Axiom hmap_update : ∀ {A B : Set} {f : A → B} h l e, update (hmap f h) l (f e) = hmap f (update h l e).
Axiom hmap_alloc : ∀ {A B : Set} {f : A → B} {h : Heap A} {h' : Heap A} l e,
                     alloc (hmap f h) (f e) = (hmap f h', l)
                     ↔ alloc h e = (h', l).