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.

3 files changed, 324 insertions, 0 deletions

diff --git a/lib/clib.mllib b/lib/clib.mllib
index 6164212e13..2547ed2297 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -6,6 +6,7 @@ Hashcons
 CSet
 CMap
 Int
+HMap
 Option
 Store
 Exninfo
diff --git a/lib/hMap.ml b/lib/hMap.ml
new file mode 100644
index 0000000000..cf5d0dfbcd
--- /dev/null
+++ b/lib/hMap.ml
@@ -0,0 +1,298 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module type HashedType =
+sig
+  type t
+  val compare : t -> t -> int
+  val hash : t -> int
+end
+
+module SetMake(M : HashedType) =
+struct
+  (** Hash Sets use hashes to prevent doing too many comparison tests. They
+      associate to each hash the set of keys having that hash.
+
+      Invariants:
+
+      1. There is no empty set in the intmap.
+      2. All values in the same set have the same hash, which is the int to
+         which it is associated in the intmap.
+  *)
+
+  module Set = Set.Make(M)
+
+  type elt = M.t
+
+  type t = Set.t Int.Map.t
+
+  let empty = Int.Map.empty
+
+  let is_empty = Int.Map.is_empty
+
+  let mem x s =
+    let h = M.hash x in
+    try
+      let m = Int.Map.find h s in
+      Set.mem x m
+    with Not_found -> false
+
+  let add x s =
+    let h = M.hash x in
+    try
+      let m = Int.Map.find h s in
+      let m = Set.add x m in
+      Int.Map.update h m s
+    with Not_found ->
+      let m = Set.singleton x in
+      Int.Map.add h m s
+
+  let singleton x =
+    let h = M.hash x in
+    let m = Set.singleton x in
+    Int.Map.singleton h m
+
+  let remove x s =
+    let h = M.hash x in
+    try
+      let m = Int.Map.find h s in
+      let m = Set.remove x m in
+      if Set.is_empty m then
+        Int.Map.remove h s
+      else
+        Int.Map.update h m s
+    with Not_found -> s
+
+  let union s1 s2 =
+    let fu _ m1 m2 = match m1, m2 with
+    | None, None -> None
+    | (Some _ as m), None | None, (Some _ as m) -> m
+    | Some m1, Some m2 -> Some (Set.union m1 m2)
+    in
+    Int.Map.merge fu s1 s2
+
+  let inter s1 s2 =
+    let fu _ m1 m2 = match m1, m2 with
+    | None, None -> None
+    | (Some _ as m), None | None, (Some _ as m) -> m
+    | Some m1, Some m2 ->
+      let m = Set.inter m1 m2 in
+      if Set.is_empty m then None else Some m
+    in
+    Int.Map.merge fu s1 s2
+
+  let diff s1 s2 =
+    let fu _ m1 m2 = match m1, m2 with
+    | None, None -> None
+    | (Some _ as m), None | None, (Some _ as m) -> m
+    | Some m1, Some m2 ->
+      let m = Set.diff m1 m2 in
+      if Set.is_empty m then None else Some m
+    in
+    Int.Map.merge fu s1 s2
+
+  let compare s1 s2 = Int.Map.compare Set.compare s1 s2
+
+  let equal s1 s2 = Int.Map.equal Set.equal s1 s2
+
+  let subset s1 s2 =
+    let check h m1 =
+      let m2 = try Int.Map.find h s2 with Not_found -> Set.empty in
+      Set.subset m1 m2
+    in
+    Int.Map.for_all check s1
+
+  let iter f s =
+    let fi _ m = Set.iter f m in
+    Int.Map.iter fi s
+
+  let fold f s accu =
+    let ff _ m accu = Set.fold f m accu in
+    Int.Map.fold ff s accu
+
+  let for_all f s =
+    let ff _ m = Set.for_all f m in
+    Int.Map.for_all ff s
+
+  let exists f s =
+    let fe _ m = Set.exists f m in
+    Int.Map.exists fe s
+
+  let filter f s =
+    let ff m = Set.filter f m in
+    let s = Int.Map.map ff s in
+    Int.Map.filter (fun _ m -> not (Set.is_empty m)) s
+
+  let partition f s = assert false (** TODO *)
+
+  let cardinal s =
+    let fold _ m accu = accu + Set.cardinal m in
+    Int.Map.fold fold s 0
+
+  let elements s =
+    let fold _ m accu = Set.fold (fun x accu -> x :: accu) m accu in
+    Int.Map.fold fold s []
+
+  let min_elt _ = assert false (** Cannot be implemented efficiently *)
+
+  let max_elt _ = assert false (** Cannot be implemented efficiently *)
+
+  let choose s =
+    let (_, m) = Int.Map.choose s in
+    Set.choose m
+
+  let split s x = assert false
+
+end
+
+module Make(M : HashedType) =
+struct
+  (** This module is essentially the same as SetMake, except that we have maps
+      instead of sets in the intmap. Invariants are the same. *)
+  module Set = SetMake(M)
+  module Map = CMap.Make(M)
+
+  type key = M.t
+
+  type 'a t = 'a Map.t Int.Map.t
+
+  let empty = Int.Map.empty
+
+  let is_empty = Int.Map.is_empty
+
+  let mem k s =
+    let h = M.hash k in
+    try
+      let m = Int.Map.find h s in
+      Map.mem k m
+    with Not_found -> false
+
+  let add k x s =
+    let h = M.hash k in
+    try
+      let m = Int.Map.find h s in
+      let m = Map.add k x m in
+      Int.Map.update h m s
+    with Not_found ->
+      let m = Map.singleton k x in
+      Int.Map.add h m s
+
+  let singleton k x =
+    let h = M.hash k in
+    Int.Map.singleton h (Map.singleton k x)
+
+  let remove k s =
+    let h = M.hash k in
+    try
+      let m = Int.Map.find h s in
+      let m = Map.remove k m in
+      if Map.is_empty m then
+        Int.Map.remove h s
+      else
+        Int.Map.update h m s
+    with Not_found -> s
+
+  let merge f s1 s2 =
+    let fm h m1 m2 = match m1, m2 with
+    | None, None -> None
+    | Some m, None ->
+      let m = Map.merge f m Map.empty in
+      if Map.is_empty m then None
+      else Some m
+    | None, Some m ->
+      let m = Map.merge f Map.empty m in
+      if Map.is_empty m then None
+      else Some m
+    | Some m1, Some m2 ->
+      let m = Map.merge f m1 m2 in
+      if Map.is_empty m then None
+      else Some m
+    in
+    Int.Map.merge fm s1 s2
+
+  let compare f s1 s2 =
+    let fc m1 m2 = Map.compare f m1 m2 in
+    Int.Map.compare fc s1 s2
+
+  let equal f s1 s2 =
+    let fe m1 m2 = Map.equal f m1 m2 in
+    Int.Map.equal fe s1 s2
+
+  let iter f s =
+    let fi _ m = Map.iter f m in
+    Int.Map.iter fi s
+
+  let fold f s accu =
+    let ff _ m accu = Map.fold f m accu in
+    Int.Map.fold ff s accu
+
+  let for_all f s =
+    let ff _ m = Map.for_all f m in
+    Int.Map.for_all ff s
+
+  let exists f s =
+    let fe _ m = Map.exists f m in
+    Int.Map.exists fe s
+
+  let filter f s =
+    let ff m = Map.filter f m in
+    let s = Int.Map.map ff s in
+    Int.Map.filter (fun _ m -> not (Map.is_empty m)) s
+
+  let partition f s = assert false (** TODO *)
+
+  let cardinal s =
+    let fold _ m accu = accu + Map.cardinal m in
+    Int.Map.fold fold s 0
+
+  let bindings s =
+    let fold _ m accu = Map.fold (fun k x accu -> (k, x) :: accu) m accu in
+    Int.Map.fold fold s []
+
+  let min_binding _ = assert false (** Cannot be implemented efficiently *)
+
+  let max_binding _ = assert false (** Cannot be implemented efficiently *)
+
+  let choose s =
+    let (_, m) = Int.Map.choose s in
+    Map.choose m
+
+  let find k s =
+    let h = M.hash k in
+    let m = Int.Map.find h s in
+    Map.find k m
+
+  let split k s = assert false (** TODO *)
+
+  let map f s =
+    let fs m = Map.map f m in
+    Int.Map.map fs s
+
+  let mapi f s =
+    let fs m = Map.mapi f m in
+    Int.Map.map fs s
+
+  let modify k f s =
+    let h = M.hash k in
+    let m = Int.Map.find h s in
+    let m = Map.modify k f m in
+    Int.Map.update h m s
+
+  let bind f s =
+    let fb m = Map.bind f m in
+    Int.Map.map fb s
+
+  let domain s = Int.Map.map Map.domain s
+
+  let update k x s =
+    let h = M.hash k in
+    let m = Int.Map.find h s in
+    let m = Map.update k x m in
+    Int.Map.update h m s
+
+end
diff --git a/lib/hMap.mli b/lib/hMap.mli
new file mode 100644
index 0000000000..4519ba316a
--- /dev/null
+++ b/lib/hMap.mli
@@ -0,0 +1,25 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module type HashedType =
+sig
+  type t
+  val compare : t -> t -> int
+  val hash : t -> int
+end
+
+(** Hash maps are maps that take advantage of having a hash on keys. This is
+    essentially a hash table, except that it uses purely functional maps instead
+    of arrays.
+
+    CAVEAT: order-related functions like [fold] or [iter] do not respect the
+    provided order anymore! It's your duty to do something sensible to prevent
+    this if you need it. In particular, [min_binding] and [max_binding] are now
+    made meaningless.
+*)
+module Make(M : HashedType) : CMap.ExtS with type key = M.t