diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-10-31 20:50:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-05 20:09:21 +0100 |
| commit | 450628742c1c5ef5391b0a16acfc99ad23205094 (patch) | |
| tree | d28b0c1a02939d84c2991729d8571face6eaa056 /checker/check.mllib | |
| parent | 8fc2509f354b02ec4e0a3eb6fabc329109686c47 (diff) | |
Added a new module HMap. It works (almost) like Map, except that it expects
the provided type to come with a hashing function. The internal representation
is changed, such that values are first compared w.r.t. to their hash.
This effectively saves a lot of comparisons which may be far more expensive
than O(1), as in the string case, hence resulting in an overall speedup.
CAVEAT: everything is not implemented yet, and order-sensitive functions
now do not respect the provided order anymore.
Diffstat (limited to 'checker/check.mllib')
| -rw-r--r-- | checker/check.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 1999317cd..80c7ac7e6 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -6,6 +6,7 @@ Hashcons CSet CMap Int +HMap Option Store Exninfo |