diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 2be97c4ada4da..c293b2a9a8e8d 100644 --- a/kernel/typeops.ml +++ b/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