diff options
| author | Pierre-Marie Pédrot | 2013-10-31 20:50:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-05 20:09:21 +0100 |
| commit | 450628742c1c5ef5391b0a16acfc99ad23205094 (patch) | |
| tree | d28b0c1a02939d84c2991729d8571face6eaa056 /dev | |
| 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 'dev')
| -rw-r--r-- | dev/printers.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index d9610fd25c..71c88bc21b 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -6,6 +6,7 @@ Hashcons CSet CMap Int +HMap Option Store Exninfo |