From e4cc086eb69a10ad3360333c2c83f4a59a44c416 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 31 Jul 2014 20:26:27 +0200
Subject: Removing the call to Weak.get_copy in hashsets.

The rationale for its use comes from OCaml weak maps, and is justified by the
fact that Weak.get may prevent its return value to be collected by the GC during
the next slice even though nobody points to it. In our case, this is vastly
irrelevant because hashconsed values are not expected to be collected whatsoever
(save for exceptional cases). But Weak.get_copy is rather costly actually, at
least strictly more than the plain Weak.get.

Experimentally, I observe diminution of compilation time and even diminution
of memory consumption (!) after this patch, so I assume it is a net gain.
---
 lib/hashset.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/hashset.ml b/lib/hashset.ml
index f8d4274dee..edbf2c4b9e 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -174,12 +174,8 @@ module Make (E : EqType) =
     let rec loop i =
       if i >= sz then ifnotfound index
       else if h = hashes.(i) then begin
-        match Weak.get_copy bucket i with
-        | Some v when E.equal v d ->
-          begin match Weak.get bucket i with
-          | Some v -> v
-          | None -> loop (i + 1)
-          end
+        match Weak.get bucket i with
+        | Some v when E.equal v d -> v
         | _ -> loop (i + 1)
       end else loop (i + 1)
     in
-- 
cgit v1.2.3