Ensuring the good invariants of hashcons table generation in the API.

8 files changed, 56 insertions, 73 deletions

diff --git a/checker/univ.ml b/checker/univ.ml
index a895021f0..323a373ec 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -432,7 +432,7 @@ struct
       include Hashcons.Make(ExprHash)
 
       let make =
-	Hashcons.simple_hcons generate Level.hcons
+	Hashcons.simple_hcons generate hcons Level.hcons
       let hash = ExprHash.hash
       let uid = hash
       let equal x y = x == y ||
@@ -1242,7 +1242,7 @@ struct
 
   module HInstance = Hashcons.Make(HInstancestruct)
 
-  let hcons = Hashcons.simple_hcons HInstance.generate Level.hcons
+  let hcons = Hashcons.simple_hcons HInstance.generate HInstance.hcons Level.hcons
     
   let empty = hcons [||]
 
diff --git a/kernel/constr.ml b/kernel/constr.ml
index e757c5b56..a01a534ee 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -991,7 +991,7 @@ module Hsorts =
     end)
 
 (* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *)
-let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
+let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind
 
 let hcons =
   hashcons
diff --git a/kernel/names.ml b/kernel/names.ml
index 13ea9e1d8..181f6c45e 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -108,7 +108,7 @@ struct
 
   module Hname = Hashcons.Make(Self_Hashcons)
 
-  let hcons = Hashcons.simple_hcons Hname.generate Id.hcons
+  let hcons = Hashcons.simple_hcons Hname.generate Hname.hcons Id.hcons
 
 end
 
@@ -175,7 +175,7 @@ struct
 
   module Hdir = Hashcons.Hlist(Id)
 
-  let hcons = Hashcons.recursive_hcons Hdir.generate Id.hcons
+  let hcons = Hashcons.recursive_hcons Hdir.generate Hdir.hcons Id.hcons
 
 end
 
@@ -239,7 +239,7 @@ struct
 
   module HashMBId = Hashcons.Make(Self_Hashcons)
 
-  let hcons = Hashcons.simple_hcons HashMBId.generate (Id.hcons, DirPath.hcons)
+  let hcons = Hashcons.simple_hcons HashMBId.generate HashMBId.hcons (Id.hcons, DirPath.hcons)
 
 end
 
@@ -335,7 +335,7 @@ module ModPath = struct
   module HashMP = Hashcons.Make(Self_Hashcons)
 
   let hcons =
-    Hashcons.simple_hcons HashMP.generate
+    Hashcons.simple_hcons HashMP.generate HashMP.hcons
       (DirPath.hcons,MBId.hcons,String.hcons)
 
 end
@@ -427,7 +427,7 @@ module KerName = struct
   module HashKN = Hashcons.Make(Self_Hashcons)
 
   let hcons =
-    Hashcons.simple_hcons HashKN.generate
+    Hashcons.simple_hcons HashKN.generate HashKN.hcons
       (ModPath.hcons,DirPath.hcons,String.hcons)
 end
 
@@ -663,10 +663,10 @@ module Hconstruct = Hashcons.Make(
     let hash = constructor_hash
   end)
 
-let hcons_con = Hashcons.simple_hcons Constant.HashKP.generate KerName.hcons
-let hcons_mind = Hashcons.simple_hcons MutInd.HashKP.generate KerName.hcons
-let hcons_ind = Hashcons.simple_hcons Hind.generate hcons_mind
-let hcons_construct = Hashcons.simple_hcons Hconstruct.generate hcons_ind
+let hcons_con = Hashcons.simple_hcons Constant.HashKP.generate Constant.HashKP.hcons KerName.hcons
+let hcons_mind = Hashcons.simple_hcons MutInd.HashKP.generate MutInd.HashKP.hcons KerName.hcons
+let hcons_ind = Hashcons.simple_hcons Hind.generate Hind.hcons hcons_mind
+let hcons_construct = Hashcons.simple_hcons Hconstruct.generate Hconstruct.hcons hcons_ind
 
 (*****************)
 
@@ -810,7 +810,7 @@ struct
 
   module HashProjection = Hashcons.Make(Self_Hashcons)
 
-  let hcons = Hashcons.simple_hcons HashProjection.generate hcons_con
+  let hcons = Hashcons.simple_hcons HashProjection.generate HashProjection.hcons hcons_con
 
   let compare (c, b) (c', b') =
     if b == b' then Constant.CanOrd.compare c c'
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index bfcdc0b4d..1462aad91 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -104,4 +104,4 @@ module Hsorts =
       let hash = Hashtbl.hash (** FIXME *)
     end)
 
-let hcons = Hashcons.simple_hcons Hsorts.generate hcons_univ
+let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
diff --git a/kernel/univ.ml b/kernel/univ.ml
index dd43e17be..2cac50fda 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -488,7 +488,7 @@ struct
       include Hashcons.Make(ExprHash)
 
       let make =
-	Hashcons.simple_hcons generate Level.hcons
+	Hashcons.simple_hcons generate hcons Level.hcons
       let hash = ExprHash.hash
       let equal x y = x == y ||
 	(let (u,n) = x and (v,n') = y in
@@ -1391,8 +1391,8 @@ module Hconstraints =
       let hash = Hashtbl.hash
     end)
 
-let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate Level.hcons
-let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate hcons_constraint
+let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate Hconstraint.hcons Level.hcons
+let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate Hconstraints.hcons hcons_constraint
 
 
 (** A value with universe constraints. *)
@@ -1775,7 +1775,7 @@ struct
 
   module HInstance = Hashcons.Make(HInstancestruct)
 
-  let hcons = Hashcons.simple_hcons HInstance.generate Level.hcons
+  let hcons = Hashcons.simple_hcons HInstance.generate HInstance.hcons Level.hcons
     
   let hash = HInstancestruct.hash
     
@@ -2125,7 +2125,7 @@ module Huniverse_set =
     end)
 
 let hcons_universe_set = 
-  Hashcons.simple_hcons Huniverse_set.generate Level.hcons
+  Hashcons.simple_hcons Huniverse_set.generate Huniverse_set.hcons Level.hcons
 
 let hcons_universe_context_set (v, c) = 
   (hcons_universe_set v, hcons_constraints c)
diff --git a/lib/cString.ml b/lib/cString.ml
index 13ec4e9b7..b21df78cb 100644
--- a/lib/cString.ml
+++ b/lib/cString.ml
@@ -171,4 +171,4 @@ module List = struct
   let equal l l' = CList.equal equal l l'
 end
 
-let hcons = Hashcons.simple_hcons Hashcons.Hstring.generate ()
+let hcons = Hashcons.simple_hcons Hashcons.Hstring.generate Hashcons.Hstring.hcons ()
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 72381ae2b..731604991 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -31,24 +31,21 @@ module type HashconsedType =
     val hash : t -> int
   end
 
-(* 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 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.
- *)
+(** The output is a function [generate] such that [generate args] creates a
+    hash-table of the hash-consed objects, together with [hcons], a function
+    taking a table and an object, and hashcons it. For simplicity of use, we use
+    the wrapper functions defined below. *)
 
 module type S =
   sig
     type t
     type u
-    val generate : unit -> (u -> t -> t)
+    type table
+    val generate : u -> table
+    val hcons : table -> t -> t
   end
 
-module Make (X : HashconsedType) =
+module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) =
   struct
     type t = X.t
     type u = X.u
@@ -60,16 +57,15 @@ module Make (X : HashconsedType) =
      *)
     module Htbl = Hashset.Make(X)
 
-    (* The table is created when () is applied.
-     * Hashconsing is then very simple:
-     *  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 generate () =
+    type table = (Htbl.t * u)
+
+    let generate u =
       let tab = Htbl.create 97 in
-        (fun u x ->
-           let y = X.hashcons u x in
-            Htbl.repr (X.hash y) y tab)
+      (tab, u)
+
+    let hcons (tab, u) x =
+      let y = X.hashcons u x in
+      Htbl.repr (X.hash y) y tab
 
   end
 
@@ -79,9 +75,9 @@ module Make (X : HashconsedType) =
  * sub-hcons functions. *)
 
 (* For non-recursive types it is quite easy. *)
-let simple_hcons h u =
-  let h = h () in
-  fun x -> h u x
+let simple_hcons h f u =
+  let table = h u in
+  fun x -> f table x
 
 (* For a recursive type T, we write the module of sig Comp with u equals
  * to (T -> T) * u0
@@ -89,19 +85,14 @@ let simple_hcons h u =
  * The second one to hashcons the other sub-structures.
  * We just have to take the fixpoint of h
  *)
-let recursive_hcons h u =
-  let hc = h () in
-  let rec hrec x = hc (hrec,u) x in
+let recursive_hcons h f u =
+  let loop = ref (fun _ -> assert false) in
+  let self x = !loop x in
+  let table = h (self, u) in
+  let hrec x = f table x in
+  let () = loop := hrec in
   hrec
 
-(* For 2 mutually recursive types *)
-let recursive2_hcons h1 h2 u1 u2 =
-  let hc1 = h1 () in
-  let hc2 = h2 () in
-  let rec hrec1 x = hc1 (hrec1,hrec2,u1) x
-  and hrec2 x = hc2 (hrec1,hrec2,u2) x
-  in (hrec1,hrec2)
-
 (* A set of global hashcons functions *)
 let hashcons_resets = ref []
 let init() = List.iter (fun f -> f()) !hashcons_resets
@@ -206,8 +197,8 @@ module Hobj = Make(
  *)
 (* string : string -> string *)
 (* obj : Obj.t -> Obj.t *)
-let string = register_hcons (simple_hcons Hstring.generate) ()
-let obj = register_hcons (recursive_hcons Hobj.generate) ()
+let string = register_hcons (simple_hcons Hstring.generate Hstring.hcons) ()
+let obj = register_hcons (recursive_hcons Hobj.generate Hobj.hcons) ()
 
 (* The unsafe polymorphic hashconsing function *)
 let magic_hash (c : 'a) =
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index cf3a09af4..5bf0a4030 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -21,7 +21,7 @@ module type HashconsedType =
         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
+        associated to a class of equivalence; this is done using the table type
         generated by the [Make] functor.
     *)
 
@@ -50,14 +50,12 @@ module type S =
     (** Type of objects to hashcons. *)
     type u
     (** 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]. *)
+    type table
+    (** Type of hashconsing tables *)
+    val generate : u -> table
+    (** This create a hashtable of the hashconsed objects. *)
+    val hcons : table -> t -> t
+    (** Perform the hashconsing of the given object within the table. *)
   end
 
 module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u)
@@ -68,19 +66,13 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u)
 (** These are intended to be used together with instances of the [Make]
     functor. *)
 
-val simple_hcons : (unit -> 'u -> 't -> 't) -> ('u -> 't -> 't)
+val simple_hcons : ('u -> 'tab) -> ('tab -> '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)
+val recursive_hcons : (('t -> 't) * 'u -> 'tab) -> ('tab -> 't -> 't) -> ('u -> 't -> 't)
 (** As [simple_hcons] but intended to be used with well-founded data structures. *)
 
-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. *)
-
 (** {6 Hashconsing of usual structures} *)
 
 module type HashedType = sig type t val hash : t -> int end