diff options
| author | Pierre-Marie Pédrot | 2016-08-22 17:13:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-22 18:33:41 +0200 |
| commit | fb9dfa53f2f71ed501be27213600143ee0b7554d (patch) | |
| tree | bfa08ea579cbd794dffad281221298c336c6fdd3 /lib/cMap.mli | |
| parent | c38f0ff80f28624b3cbf4df1e317f133caa94d1d (diff) | |
Fast path for set operations.
We consider an approximation of the size of sets before choosing the most
appropriate algorithm. This drastically affects some universe-polymorphic
code which was doing a lot of set operations on disimilar sizes.
Diffstat (limited to 'lib/cMap.mli')
| -rw-r--r-- | lib/cMap.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/cMap.mli b/lib/cMap.mli index 3ef7fa2c8a..2838b374ec 100644 --- a/lib/cMap.mli +++ b/lib/cMap.mli @@ -61,6 +61,9 @@ sig val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t (** As [mapi] but tries to preserve sharing. *) + val height : 'a t -> int + (** An indication of the logarithmic size of a map *) + module Unsafe : sig val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t |