Cleaning, renaming obscure functions and documenting in Hashcons.

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

5 files changed, 81 insertions, 42 deletions

diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 7c2897be0..f71af15c7 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -13,29 +13,29 @@
 (* [t] is the type of object to hash-cons
  * [u] is the type of hash-cons functions for the sub-structures
  *   of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...).
- * [hash_sub u x] is a function that hash-cons the sub-structures of x using
+ * [hashcons u x] is a function that hash-cons the sub-structures of x using
  *   the hash-consing functions u provides.
  * [equal] is a comparison function. It is allowed to use physical equality
- *   on the sub-terms hash-consed by the hash_sub function.
+ *   on the sub-terms hash-consed by the hashcons function.
  * [hash] is the hash function given to the Hashtbl.Make function
  *
  * Note that this module type coerces to the argument of Hashtbl.Make.
  *)
 
-module type Comp =
+module type HashconsedType =
   sig
     type t
     type u
-    val hash_sub :  u -> t -> t
+    val hashcons :  u -> t -> t
     val equal : t -> t -> bool
     val hash : t -> int
   end
 
-(* The output is a function f such that
- * [f ()] has the side-effect of creating (internally) a hash-table of the
+(* The output is a function [generate] such that
+ * [generate ()] has the side-effect of creating (internally) a hash-table of the
  *   hash-consed objects. The result is a function taking the sub-hashcons
  *   functions and an object, and hashcons it. It does not really make sense
- *   to call f() with different sub-hcons functions. That's why we use the
+ *   to call generate() with different sub-hcons functions. That's why we use the
  *   wrappers simple_hcons, recursive_hcons, ... The latter just take as
  *   argument the sub-hcons functions (the tables are created at that moment),
  *   and returns the hcons function for t.
@@ -45,10 +45,10 @@ module type S =
   sig
     type t
     type u
-    val f : unit -> (u -> t -> t)
+    val generate : unit -> (u -> t -> t)
   end
 
-module Make(X:Comp) =
+module Make (X : HashconsedType) =
   struct
     type t = X.t
     type u = X.u
@@ -66,20 +66,20 @@ module Make(X:Comp) =
 
     (* The table is created when () is applied.
      * Hashconsing is then very simple:
-     *  1- hashcons the subterms using hash_sub and u
+     *  1- hashcons the subterms using hashcons and u
      *  2- look up in the table, if we do not get a hit, we add it
      *)
-    let f () =
+    let generate () =
       let tab = Htbl.create 97 in
         (fun u x ->
-           let y = X.hash_sub u x in
+           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)
   end
 
 (* A few usefull wrappers:
- * takes as argument the function f above and build a function of type
+ * takes as argument the function [generate] above and build a function of type
  * u -> t -> t that creates a fresh table each time it is applied to the
  * sub-hcons functions. *)
 
@@ -136,7 +136,7 @@ module Hstring = Make(
   struct
     type t = string
     type u = unit
-    let hash_sub () s =(* incr accesstr;*) s
+    let hashcons () s =(* incr accesstr;*) s
     let equal s1 s2 =(* incr comparaisonstr;
       if*) s1=s2(* then (incr successtr; true) else false*)
     let hash = Hashtbl.hash
@@ -175,7 +175,7 @@ module Hobj = Make(
   struct
     type t = Obj.t
     type u = (Obj.t -> Obj.t) * unit
-    let hash_sub (hrec,_) = hash_obj hrec
+    let hashcons (hrec,_) = hash_obj hrec
     let equal = comp_obj
     let hash = Hashtbl.hash
   end)
@@ -185,8 +185,8 @@ module Hobj = Make(
  *)
 (* string : string -> string *)
 (* obj : Obj.t -> Obj.t *)
-let string = register_hcons (simple_hcons Hstring.f) ()
-let obj = register_hcons (recursive_hcons Hobj.f) ()
+let string = register_hcons (simple_hcons Hstring.generate) ()
+let obj = register_hcons (recursive_hcons Hobj.generate) ()
 
 (* The unsafe polymorphic hashconsing function *)
 let magic_hash (c : 'a) =
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index b4a9da2f8..bafec6f91 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -8,43 +8,82 @@
 
 (** Generic hash-consing. *)
 
-module type Comp =
+module type HashconsedType =
   sig
+    (** {6 Generic hashconsing signature}
+
+        Given an equivalence relation [equal], a hashconsing function is a
+        function that associates the same canonical element to two elements
+        related by [equal]. Usually, the element chosen is canonical w.r.t.
+        physical equality [(==)], so as to reduce memory consumption and
+        enhance efficiency of equality tests.
+
+        In order to ensure canonicality, we need a way to remember the element
+        associated to a class of equivalence; this is done using a hidden state
+        generated by the [Make] functor.
+    *)
+
     type t
+    (** Type of objects to hashcons. *)
     type u
-    val hash_sub :  u -> t -> t
+    (** Type of hashcons functions for the sub-structures contained in [t].
+        Usually a tuple of functions. *)
+    val hashcons :  u -> t -> t
+    (** The actual hashconsing function, using its fist argument to recursively
+        hashcons substructures. *)
     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. *)
   end
 
 module type S =
   sig
     type t
+    (** Type of objects to hashcons. *)
     type u
-    val f : unit -> (u -> t -> t)
+    (** Type of hashcons functions for the sub-structures contained in [t]. *)
+    val generate : unit -> (u -> t -> t)
+    (** This has the side-effect of creating (internally) a hashtable of the
+        hashconsed objects. The result is a function taking the sub-hashcons
+        functions and an object, and hashconsing it. It does not really make sense
+        to call [generate] with different sub-hcons functions. That's why we use the
+        wrappers [simple_hcons], [recursive_hcons], ... The latter just take as
+        argument the sub-hcons functions (the tables are created at that moment),
+        and returns the hcons function for [t]. *)
   end
 
-module Make(X:Comp) : (S with type t = X.t and type u = X.u)
+module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u)
+(** Create a new hashconsing, given canonicalization functions. *)
+
+(** {6 Wrappers} *)
+
+(** * 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
+    sub-hash function [sub]. *)
+
 val recursive_hcons : (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
+(** As [simple_hcons] but intended to be used with well-founded data structures. *)
+
 val recursive_loop_hcons :
     (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
+(** As [simple_hcons] but intended to be used with any recursive data structure,
+    in particular if they contain loops. *)
+
 val recursive2_hcons :
   (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u1 -> 't1 -> 't1) ->
     (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u2 -> 't2 -> 't2) ->
       'u1 -> 'u2 -> ('t1 -> 't1) * ('t2 -> 't2)
+(** As [recursive_hcons] but with two mutually recursive structures. *)
 
-(** Declaring and reinitializing global hash-consing functions *)
-
-val init : unit -> unit
-val register_hcons : ('u -> 't -> 't) -> ('u -> 't -> 't)
+(** {6 Hashconsing of usual structures} *)
 
 module Hstring : (S with type t = string and type u = unit)
-module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit)
-
-val string : string -> string
-val obj : Obj.t -> Obj.t
-
-val magic_hash : 'a -> 'a
+(** Hashconsing of strings.  *)
 
+module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit)
+(** Hashconsing of OCaml values. *)
diff --git a/lib/hashtbl_alt.ml b/lib/hashset.ml
index 2780afe8f..28767df8f 100644
--- a/lib/hashtbl_alt.ml
+++ b/lib/hashset.ml
@@ -16,9 +16,9 @@
    given to the caller, which makes possible the interleaving of the
    hash key computation and the hash-consing. *)
 
-module type Hashtype = sig
+module type EqType = sig
   type t
-  val equals : t -> t -> bool
+  val equal : t -> t -> bool
 end
 
 module type S = sig
@@ -31,7 +31,7 @@ module type S = sig
   val may_add_and_get : int -> elt -> elt
 end
 
-module Make (E : Hashtype) =
+module Make (E : EqType) =
   struct
 
     type elt = E.t
@@ -72,7 +72,7 @@ module Make (E : Hashtype) =
       | Empty ->
 	add hash key; key
       | Cons (k, h, rest) ->
-	if hash == h && E.equals key k then k else aux rest
+	if hash == h && E.equal key k then k else aux rest
     in
     aux bucket
 
@@ -81,15 +81,15 @@ module Make (E : Hashtype) =
     match odata.(hash mod (Array.length odata)) with
       |	Empty -> add hash key; key
       | Cons (k1, h1, rest1) ->
-	if hash == h1 && E.equals key k1 then k1 else
+	if hash == h1 && E.equal key k1 then k1 else
 	  match rest1 with
             | Empty -> add hash key; key
 	    | Cons (k2, h2, rest2) ->
-              if hash == h2 && E.equals key k2 then k2 else
+              if hash == h2 && E.equal key k2 then k2 else
 		match rest2 with
 		  | Empty -> add hash key; key
 		  | Cons (k3, h3, rest3) ->
-		    if hash == h2 && E.equals key k3 then k3
+		    if hash == h2 && E.equal key k3 then k3
 		    else find_rec hash key rest3
 
 end
diff --git a/lib/hashtbl_alt.mli b/lib/hashset.mli
index 7a1dcd57f..4b260791b 100644
--- a/lib/hashtbl_alt.mli
+++ b/lib/hashset.mli
@@ -16,9 +16,9 @@
    given to the caller, which makes possible the interleaving of the
    hash key computation and the hash-consing. *)
 
-module type Hashtype = sig
+module type EqType = sig
   type t
-  val equals : t -> t -> bool
+  val equal : t -> t -> bool
 end
 
 module type S = sig
@@ -31,7 +31,7 @@ module type S = sig
   val may_add_and_get : int -> elt -> elt
 end
 
-module Make (E : Hashtype) : S with type elt = E.t
+module Make (E : EqType) : S with type elt = E.t
 
 module Combine : sig
   val combine : int -> int -> int
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 21eb7a4a5..a7d56c666 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -4,6 +4,7 @@ Compat
 Loc
 Errors
 Bigint
+Hashset
 Hashcons
 Dyn
 Segmenttree
@@ -23,4 +24,3 @@ Heap
 Dnet
 Store
 Unionfind
-Hashtbl_alt