From 76089d6b277b84fe1b8333f12d25b512a4cab9dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Mon, 1 Jul 2024 14:41:53 +0200
Subject: [PATCH] Avoid duplicate hashconsing of kerpairs

---
 clib/hashset.ml  | 19 +++++++++++++++++++
 clib/hashset.mli |  2 ++
 kernel/names.ml  | 17 ++++++++++-------
 3 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/clib/hashset.ml b/clib/hashset.ml
index 183c997425414..29f7eb3314c18 100644
--- a/clib/hashset.ml
+++ b/clib/hashset.ml
@@ -34,6 +34,7 @@ module type S = sig
   val create : int -> t
   val clear : t -> unit
   val repr : int -> elt -> t -> elt
+  val lookup : (elt -> elt -> bool) -> int -> elt -> t -> elt option
   val stats : t -> statistics
 end
 
@@ -180,6 +181,24 @@ module Make (E : EqType) =
 
   external unsafe_weak_get : 'a Weak.t -> int -> 'a option = "caml_weak_get"
 
+  let lookup eq h d t =
+    let table = t.table in
+    let index = get_index table h in
+    let bucket = Array.unsafe_get table index in
+    let hashes = Array.unsafe_get t.hashes index in
+    let sz = Weak.length bucket in
+    let pos = ref 0 in
+    let ans = ref None in
+    while !pos < sz && !ans == None do
+      let i = !pos in
+      if Int.equal h (Array.unsafe_get hashes i) then begin
+        match unsafe_weak_get bucket i with
+        | Some v as res when eq v d -> ans := res
+        | _ -> incr pos
+      end else incr pos
+    done;
+    !ans
+
   let repr h d t =
     let table = t.table in
     let index = get_index table h in
diff --git a/clib/hashset.mli b/clib/hashset.mli
index 4d7bd6211f2ec..8185f363b6bee 100644
--- a/clib/hashset.mli
+++ b/clib/hashset.mli
@@ -48,6 +48,8 @@ module type S = sig
       [constr] is stored in [set] and will be used as the canonical
       representation of this value in the future. *)
 
+  val lookup : (elt -> elt -> bool) -> int -> elt -> t -> elt option
+
   val stats : t -> statistics
   (** Recover statistics on the table. *)
 end
diff --git a/kernel/names.ml b/kernel/names.ml
index 70270b980dd81..f108d32eb61e1 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -565,7 +565,6 @@ module KerPair = struct
   module Self_Hashcons =
     struct
       type t = kernel_pair
-      type u = KerName.t -> KerName.t
       let hashcons hkn = function
         | Same kn -> Same (hkn kn)
         | Dual (knu,knc) -> make (hkn knu) (hkn knc)
@@ -579,15 +578,19 @@ module KerPair = struct
           the same canonical part is a logical invariant of the system, it
           is not necessarily an invariant in memory, so we treat kernel
           names as they are syntactically for hash-consing) *)
-      let hash = function
-      | Same kn -> KerName.hash kn
-      | Dual (knu, knc) ->
-        Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
     end
 
-  module HashKP = Hashcons.Make(Self_Hashcons)
+  module Tbl = Hashset.Make(Self_Hashcons)
+
+  let tab = Tbl.create 97
 
-  let hcons = Hashcons.simple_hcons HashKP.generate HashKP.hcons KerName.hcons
+  let hcons c =
+    let h = SyntacticOrd.hash c in
+    match Tbl.lookup SyntacticOrd.equal h c tab with
+    | Some v -> v
+    | None ->
+      let v = Self_Hashcons.hashcons KerName.hcons c in
+      Tbl.repr h v tab
 
 end