A bounded heap of values of type 'a.

create n is a heap that holds at most n elements.

An element in a heap.

The index of an entry.

ptr e is the index of e.

• raises Invalid_arg

  if e has already been freed.

alloc t a ~extra_data adds the value a to t and returns a pointer to that value, or raises No_space if no space exists in t.

• parameter extra_data

  Prevent this from being GC'd until free is called.

free t p returns the element referenced by p and removes it from the heap. Has undefined behaviour if p has already been freed.

in_use t is the number of entries currently allocated.