Module Prime_accretion_map

Accumulation of a monoid over a map (prime.unstable).

Given a monoid operation, say ∗, these map-like structures maintains the of nested application of the operator over the elements of the map in key-order. E.g. given 5 elements inserted with keys such that the order is a, ..., e, then the accumulated result may be computed as (a ∗ b) ∗ (c ∗ (d ∗ e)) or any other associative combination, yielding the same result. The map is represented as a balanced tree, storing intermediate results, so adding or removing elements is amortized O(log n).

There are four functors depending on parametricity of the element type and whether or not the generator type is explicit.