Language.Boogie.Heap

Generic heap with reference counting. This module provides relatively low-level interface to the heap data structure, while keeping its internal representation hidden and consistent.

Documentation

type Ref = Int

Reference (index in the heap)

refDoc :: Ref -> Doc

Pretty-printed reference

data Heap a

Heap

Instances

Eq a => Eq (Heap a)

Show a => Show (Heap a)

emptyHeap :: Heap a

Empty heap

at :: Show a => Heap a -> Ref -> a

at h r: value of r in heap h

alloc :: a -> Heap a -> (Ref, Heap a)

alloc v h : choose a free reference in heap h and store value v in there; return the reference and the updated heap

hasGarbage :: Heap a -> Bool

Does the heap have any garbage?

dealloc :: Heap a -> (Ref, Heap a)

Collect some garbage reference in the heap and return that reference and the new heap; the heap must have garbage

update :: Ref -> a -> Heap a -> Heap a

update r v h : set the value at reference r to v in h; r must be present in h

incRefCount :: Ref -> Heap a -> Heap a

incRefCount r h : increase reference count of r in h; r must be present in h

decRefCount :: Ref -> Heap a -> Heap a

decRefCount r h : decrease reference count of r in h; r must be present in h

heapDoc :: Show a => Heap a -> Doc

Pretty-printed heap