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.

1 files 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;
   }