Module Prime_priqueue

A pure priority queue with element removal.

This implements priority queue in terms of a pure pairing heap. The additional remove operation is supported by adding removal nodes alongside regular nodes, and erasing matching regular nodes as they get merged by the remove_min operation.

This is most efficient when S.remove is rare compared to S.add and S.remove_min, otherwise a balanced tree may be better suited. In the most feasible case, the deletion-nodes created by S.remove gets flushed by S.remove_min at a rate comparable to their creation. If this is not the case, the S.gc function should be called at suitable intervals to keep the space overhead within a constant factor.