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

7 files changed, 78 insertions, 65 deletions

diff --git a/checker/check.mllib b/checker/check.mllib
index 6203c1fbb..c12b5953a 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -13,6 +13,7 @@ CList
 CArray
 Util
 Option
+Hashset
 Hashcons
 CUnix
 System
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 960dcb6de..afb8ac4e6 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -10,6 +10,7 @@ CList
 CArray
 Util
 Bigint
+Hashset
 Hashcons
 Predicate
 Option
diff --git a/kernel/term.ml b/kernel/term.ml
index 8ab04af24..42309c37e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1236,7 +1236,10 @@ let equals_constr t1 t2 =
 (** Note that the following Make has the side effect of creating
     once and for all the table we'll use for hash-consing all constr *)
 
-module H = Hashset.Make(struct type t = constr let equal = equals_constr end)
+module HashsetTerm = Hashset.Make(struct type t = constr let equal = equals_constr end)
+
+let term_table = HashsetTerm.create 19991
+(* The associative table to hashcons terms. *)
 
 open Hashset.Combine
 
@@ -1320,7 +1323,7 @@ let hcons_term (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
     let (y, h) = hash_term t in
     (* [h] must be positive. *)
     let h = h land 0x3FFFFFFF in
-    (H.may_add_and_get h y, h)
+    (HashsetTerm.repr h y term_table, h)
 
   in
   (* Make sure our statically allocated Rels (1 to 16) are considered
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index f71af15c7..8daeec944 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -58,11 +58,7 @@ module Make (X : HashconsedType) =
      * w.r.t (=), although the equality on keys is X.equal. This is
      * granted since we hcons the subterms before looking up in the table.
      *)
-    module Htbl = Hashtbl.Make(
-      struct type t=X.t
-             let hash=X.hash
-             let equal x1 x2 = (*incr comparaison;*) X.equal x1 x2
-      end)
+    module Htbl = Hashset.Make(X)
 
     (* The table is created when () is applied.
      * Hashconsing is then very simple:
@@ -73,9 +69,8 @@ module Make (X : HashconsedType) =
       let tab = Htbl.create 97 in
         (fun u x ->
            let y = X.hashcons u x in
-            (* incr acces;*)
-             try let r = Htbl.find tab y in(* incr succes;*) r
-             with Not_found -> Htbl.add tab y y; y)
+            Htbl.repr (X.hash y) y tab)
+
   end
 
 (* A few usefull wrappers:
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index bafec6f91..4246f5288 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -8,6 +8,8 @@
 
 (** Generic hash-consing. *)
 
+(** {6 Hashconsing functorial interface} *)
+
 module type HashconsedType =
   sig
     (** {6 Generic hashconsing signature}
@@ -30,12 +32,15 @@ module type HashconsedType =
         Usually a tuple of functions. *)
     val hashcons :  u -> t -> t
     (** The actual hashconsing function, using its fist argument to recursively
-        hashcons substructures. *)
+        hashcons substructures. It should be compatible with [equal], that is
+        [equal x (hashcons f x) = true]. *)
     val equal : t -> t -> bool
     (** A comparison function. It is allowed to use physical equality
         on the sub-terms hashconsed by the [hashcons] function. *)
     val hash : t -> int
-    (** A hash function passed to the underlying hashtable structure. *)
+    (** A hash function passed to the underlying hashtable structure. [hash]
+        should be compatible with [equal], i.e. if [equal x y = true] then
+        [hash x = hash y]. *)
   end
 
 module type S =
@@ -59,8 +64,8 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u)
 
 (** {6 Wrappers} *)
 
-(** * These are intended to be used together with instances of the [Make]
-      functor. *)
+(** These are intended to be used together with instances of the [Make]
+    functor. *)
 
 val simple_hcons : (unit -> 'u -> 't -> 't) -> ('u -> 't -> 't)
 (** [simple_hcons f sub obj] creates a new table each time it is applied to any
diff --git a/lib/hashset.ml b/lib/hashset.ml
index 28767df8f..7d2fd6f55 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -23,12 +23,9 @@ 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 t
+  val create : int -> t
+  val repr : int -> elt -> t -> elt
 end
 
 module Make (E : EqType) =
@@ -38,59 +35,66 @@ module Make (E : EqType) =
 
     type bucketlist = Empty | Cons of elt * int * bucketlist
 
-    let initial_size = 19991
-    let table_data = ref (Array.make initial_size Empty)
-    let table_size = ref 0
+    type t = {
+      mutable size : int;
+      mutable data : bucketlist array; }
+
+    let create s =
+      let s = min (max 1 s) Sys.max_array_length in
+      { size = 0; data = Array.make s Empty }
 
-    let resize () =
-      let odata = !table_data in
+    let resize table =
+      let odata = table.data in
       let osize = Array.length odata in
-    let nsize = min (2 * osize + 1) Sys.max_array_length in
-    if nsize <> osize then begin
-      let ndata = Array.create nsize Empty in
-      let rec insert_bucket = function
-	| Empty -> ()
-	| Cons (key, hash, rest) ->
-          let nidx = hash mod nsize in
-          ndata.(nidx) <- Cons (key, hash, ndata.(nidx));
-          insert_bucket rest
-      in
-      for i = 0 to osize - 1 do insert_bucket odata.(i) done;
-      table_data := ndata
-    end
+      let nsize = min (2 * osize + 1) Sys.max_array_length in
+      if nsize <> osize then begin
+        let ndata = Array.create nsize Empty in
+        let rec insert_bucket = function
+        | Empty -> ()
+        | Cons (key, hash, rest) ->
+            let nidx = hash mod nsize in
+            let obucket = ndata.(nidx) in
+            ndata.(nidx) <- Cons (key, hash, obucket);
+            insert_bucket rest
+        in
+        for i = 0 to osize - 1 do insert_bucket odata.(i) done;
+        table.data <- ndata
+      end
 
-  let add hash key =
-    let odata = !table_data in
+  let add hash key table =
+    let odata = table.data in
     let osize = Array.length odata in
     let i = hash mod osize in
     odata.(i) <- Cons (key, hash, odata.(i));
-    incr table_size;
-    if !table_size > osize lsl 1 then resize ()
+    table.size <- table.size + 1;
+    if table.size > osize lsl 1 then resize table
 
-  let find_rec hash key bucket =
+  let find_rec hash key table bucket =
     let rec aux = function
       | Empty ->
-	add hash key; key
+	add hash key table; key
       | Cons (k, h, rest) ->
 	if hash == h && E.equal key k then k else aux rest
     in
     aux bucket
 
-  let may_add_and_get hash key =
-    let odata = !table_data in
-    match odata.(hash mod (Array.length odata)) with
-      |	Empty -> add hash key; key
+  let repr hash key table =
+    let odata = table.data in
+    let osize = Array.length odata in
+    let i = hash mod osize in
+    match odata.(i) with
+      |	Empty -> add hash key table; key
       | Cons (k1, h1, rest1) ->
 	if hash == h1 && E.equal key k1 then k1 else
 	  match rest1 with
-            | Empty -> add hash key; key
+            | Empty -> add hash key table; key
 	    | Cons (k2, h2, rest2) ->
               if hash == h2 && E.equal key k2 then k2 else
 		match rest2 with
-		  | Empty -> add hash key; key
+		  | Empty -> add hash key table; key
 		  | Cons (k3, h3, rest3) ->
 		    if hash == h2 && E.equal key k3 then k3
-		    else find_rec hash key rest3
+		    else find_rec hash key table rest3
 
 end
 
diff --git a/lib/hashset.mli b/lib/hashset.mli
index 4b260791b..17831caf9 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