Reusing the Hashset data structure in Hashcons. Hopefully, this should

not disrupt anything...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15836 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 14 deletions

diff --git a/lib/hashset.mli b/lib/hashset.mli
index 4b260791b8..17831caf99 100644
--- a/lib/hashset.mli
+++ b/lib/hashset.mli
@@ -6,15 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* The following module is a specialized version of [Hashtbl] that is
-   a better space saver. Actually, [Hashcons] instanciates [Hashtbl.t]
-   with [constr] used both as a key and as an image.  Thus, in each
-   cell of the internal bucketlist, there are two representations of
-   the same value. In this implementation, there is only one.
+(** The following module is a specialized version of [Hashtbl] that is
+    a better space saver. In each cell of the internal bucketlist of a
+    hashtable, there are two representations of the same value. In this
+    implementation, there is only one.
 
-   Besides, the responsibility of computing the hash function is now
-   given to the caller, which makes possible the interleaving of the
-   hash key computation and the hash-consing. *)
+    Besides, the responsibility of computing the hash function is now
+    given to the caller, which makes possible the interleaving of the
+    hash key computation and the hash-consing. *)
 
 module type EqType = sig
   type t
@@ -23,12 +22,17 @@ end
 
 module type S = sig
   type elt
-  (* [may_add_and_get key constr] uses [key] to look for [constr]
-     in the hash table [H]. If [constr] is in [H], returns the
-     specific representation that is stored in [H]. Otherwise,
-     [constr] is stored in [H] and will be used as the canonical
-     representation of this value in the future. *)
-  val may_add_and_get : int -> elt -> elt
+  (** Type of hashsets elements. *)
+  type t
+  (** Type of hashsets. *)
+  val create : int -> t
+  (** [create n] creates a fresh hashset with initial size [n]. *)
+  val repr : int -> elt -> t -> elt
+  (** [repr key constr set] uses [key] to look for [constr]
+      in the hashet [set]. If [constr] is in [set], returns the
+      specific representation that is stored in [set]. Otherwise,
+      [constr] is stored in [set] and will be used as the canonical
+      representation of this value in the future. *)
 end
 
 module Make (E : EqType) : S with type elt = E.t