Merge pull request #753 from ejgallego/memo_bucket_stats

[memo] Provide Hashtbl stats API

CHANGES.md

@@ -13,6 +13,7 @@
  - [fleche] This achieves an almost 50% memory reduction for example
    when opening all of HoTT .v files (@ejgallego, @SkySkimmer,
    @bhaktishh, #744)
+ - [memo] Provide API to query Hashtbl stats (@ejgallego, #753)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

fleche/memo.ml

@@ -96,6 +96,8 @@ module MemoTable = struct
 
     (** sorted *)
     val all_freqs : unit -> int list
+
+    val stats : 'a t -> Hashtbl.statistics
   end
 
   module Make (H : Hashtbl.HashedType) : S with type key = H.t = struct
@@ -209,6 +211,9 @@ module type S = sig
   (** [freqs ()]: (sorted) histogram *)
   val all_freqs : unit -> int list
 
+  (** [stats ()]: hashtbl stats *)
+  val stats : unit -> Hashtbl.statistics
+
   (** debug data for input *)
   val input_info : input -> string
 
@@ -227,6 +232,7 @@ module SEval (E : EvalType) :
   let size () = Obj.reachable_words (Obj.magic cache)
   let input_info i = E.input_info i
   let all_freqs = HC.all_freqs
+  let stats () = HC.stats cache
   let clear () = HC.clear cache
 
   let in_cache i =
@@ -272,6 +278,7 @@ module CEval (E : LocEvalType) = struct
   let size () = Obj.reachable_words (Obj.magic cache)
   let all_freqs = HC.all_freqs
   let input_info = E.input_info
+  let stats () = HC.stats cache
   let clear () = HC.clear cache
 
   let in_cache i =

fleche/memo.mli

@@ -36,6 +36,9 @@ module type S = sig
   (** [freqs ()]: (sorted) histogram *)
   val all_freqs : unit -> int list
 
+  (** [stats ()]: hashtbl stats *)
+  val stats : unit -> Hashtbl.statistics
+
   (** debug data for input *)
   val input_info : input -> string
 

fleche/perf_analysis.ml

@@ -35,6 +35,7 @@ let node_time_compare (n1 : Doc.Node.t) (n2 : Doc.Node.t) =
 
 (* Old mode of sending only the 10 hotspots *)
 let hotspot = false
+let debug_hashtbl = false
 
 let make (doc : Doc.t) =
   let n_stm = List.length doc.nodes in
@@ -43,8 +44,15 @@ let make (doc : Doc.t) =
     if display_cache_size then Memo.all_size () |> float_of_int else 0.0
   in
   let summary =
-    Format.asprintf "{ num sentences: %d@\n; stats: %s; cache: %a@\n}" n_stm
-      stats Stats.pp_words cache_size
+    Format.asprintf "{ num sentences: %d@\n; stats: %s; cache: %a@}" n_stm stats
+      Stats.pp_words cache_size
+  in
+  let summary =
+    if debug_hashtbl then
+      summary
+      ^ Format.asprintf "{memo max bucket: %d}"
+          (Memo.Interp.stats ()).max_bucket_length
+    else summary
   in
   let timings =
     if hotspot then List.stable_sort node_time_compare doc.nodes |> list_take 10