hconstr v3 use int map ref instead of hashtbl

Not sure if I messed up the hashtbl usage but it seems to produce big
buckets, which we then need to linearly scan.

Int map has exactly one bucket per hash and ends up faster.

~~~coq
Require Import Ltac2.Ltac2.

Require Import PrimInt63.

Set Debug "hconstr".

Inductive tree := Leaf (_:int) | Node (_:tree) (_:tree).

Import Constr.Unsafe.

Ltac2 rec big' node leaf n :=
  if Int.equal n 0 then leaf()
  else
    let n := Int.sub n 1 in
    let c := big' node leaf n in
    let c' := big' node leaf n in
    make (App node [|c; c'|]).

Lemma baz : tree.
  Time let x := Ref.ref '(0 :> int) in
  let leaf := 'Leaf in
  let leaf () :=
    let c := Ref.get x in
    let c' := (eval cbv in (add $c 1)) in
    Ref.set x c';
    make (App leaf [|c|])
  in
  let c := big' 'Node leaf 17 in
  Std.exact_no_check c.

Time Defined.
(* 16 -> master: 2s, hconstr v2: 8s
   17 -> master: 8s, hconstr v2: 31s, hconstr v3: 8s
 *)

(*
v2:

Debug: [hconstr] num_bindings = 393217
                          num_buckets = 262144
                          max_bucket_length = 16385
Debug: [hconstr] num_bindings = 1
                          num_buckets = 64
                          max_bucket_length = 1
*)

(*
v3:
Debug: [hconstr] hashes = 392326
                          bindings = 393217
                          most_collisions = 256
Debug: [hconstr] hashes = 1
                          bindings = 1
                          most_collisions = 1

*)
~~~

(BTW the hcons debug says

~~~
Debug: [hcons] num_bindings = 393291
                        num_buckets = 67482
                        max_bucket_length = 4103
~~~

which is sgnificantly smaller than the hconstr max bucket length, IDK why)

kernel/typeops.ml

@@ -661,7 +661,13 @@ module HConstr : sig
   (* May not be used on Rel! (subterms can be rels) *)
   val of_kind_nohashcons : (t,t,Sorts.t,UVars.Instance.t,Sorts.relevance) kind_of_term -> t
 
-  module Tbl : Hashtbl.S with type key = t
+  module Tbl : sig
+    type key = t
+    type 'a t
+    val find_opt : 'a t -> key -> 'a option
+    val add : 'a t -> key -> 'a -> unit
+    val create : int -> 'a t
+  end
 
 end = struct
 
@@ -775,7 +781,52 @@ let push_rel env =
     cnt = env.cnt;
   }
 
-module Tbl = Hashtbl.Make(Self)
+module Tbl = struct
+  type key = t
+
+  type 'a t = (key * 'a) list Int.Map.t ref
+
+  let create _ = ref Int.Map.empty
+
+  let add tbl key v =
+    tbl := Int.Map.update key.hash (function
+        | None -> Some [(key,v)]
+        | Some l -> Some ((key,v)::l))
+        !tbl
+
+  let find_opt tbl key =
+    match Int.Map.find_opt key.hash !tbl with
+    | None -> None
+    | Some l ->
+      List.find_map (fun (k',v) ->
+          if equal key k' then Some v else None)
+        l
+
+  type stats = {
+    hashes : int;
+    bindings : int;
+    most_collisions : int;
+  }
+
+  let empty_stats = {
+    hashes = 0;
+    bindings = 0;
+    most_collisions = 0;
+  }
+
+  let stats tbl =
+    Int.Map.fold (fun _ l acc ->
+        let len = List.length l in
+        {
+          hashes = acc.hashes + 1;
+          bindings = acc.bindings + len;
+          most_collisions = max acc.most_collisions len;
+        }
+      )
+      !tbl
+      empty_stats
+
+end
 
 let hash_annot = hash_annot Name.hash
 
@@ -971,12 +1022,11 @@ let of_constr env c =
   let tbl = Tbl.create 57 in
   let c = of_constr tbl local_env c in
   dbg Pp.(fun () ->
-      let open Hashtbl in
       let stats = Tbl.stats tbl in
       v 0 (
-        str "num_bindings = " ++ int stats.num_bindings ++ spc() ++
-        str "num_buckets = " ++ int stats.num_buckets ++ spc() ++
-        str "max_bucket_length = " ++ int stats.max_bucket_length
+        str "hashes = " ++ int stats.Tbl.hashes ++ spc() ++
+        str "bindings = " ++ int stats.Tbl.bindings ++ spc() ++
+        str "most_collisions = " ++ int stats.Tbl.most_collisions
     )
     );
   c