From 72500ec169237ca98a5cfd5e4c0ff92b9c555eee Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 20 Aug 2020 17:28:22 +0200
Subject: Use a map function instead of a fold when freezing summaries.

This is O(n) instead of O(n log n) and should be more efficient in practice.
---
 library/summary.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/library/summary.ml b/library/summary.ml
index 9ff707f842..221ac868fa 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -19,7 +19,8 @@ type 'a summary_declaration = {
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
-module DynMap = Dyn.Map(struct type 'a t = 'a summary_declaration end)
+module Decl = struct type 'a t = 'a summary_declaration end
+module DynMap = Dyn.Map(Decl)
 
 type ml_modules = (string * string option) list
 
@@ -46,7 +47,8 @@ let declare_summary_tag sumname decl =
 let declare_summary sumname decl =
   ignore(declare_summary_tag sumname decl)
 
-module Frozen = Dyn.Map(struct type 'a t = 'a end)
+module ID = struct type 'a t = 'a end
+module Frozen = Dyn.Map(ID)
 
 type frozen = {
   summaries : Frozen.t;
@@ -57,9 +59,11 @@ type frozen = {
 
 let empty_frozen = { summaries = Frozen.empty; ml_module = None }
 
+module HMap = Dyn.HMap(Decl)(ID)
+
 let freeze_summaries ~marshallable : frozen =
-  let fold (DynMap.Any (tag, decl)) accu = Frozen.add tag (decl.freeze_function ~marshallable) accu in
-  { summaries = DynMap.fold fold !sum_map Frozen.empty;
+  let map = { HMap.map = fun tag decl -> decl.freeze_function ~marshallable } in
+  { summaries = HMap.map map !sum_map;
     ml_module = Option.map (fun decl -> decl.freeze_function ~marshallable) !sum_mod;
   }
 
-- 
cgit v1.2.3