From 6b2ec938010c50dae3ec6c87ff8ea7f2a4012b92 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 17 Dec 2014 19:12:11 +0100
Subject: Ensuring the good invariants of hashcons table generation in the API.

---
 lib/cString.ml   |  2 +-
 lib/hashcons.ml  | 63 ++++++++++++++++++++++++--------------------------------
 lib/hashcons.mli | 26 ++++++++---------------
 3 files changed, 37 insertions(+), 54 deletions(-)

(limited to 'lib')

diff --git a/lib/cString.ml b/lib/cString.ml
index 13ec4e9b70..b21df78cbc 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 72381ae2bd..7316049917 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 cf3a09af4a..5bf0a40301 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
-- 
cgit v1.2.3