diff options
| author | coqbot-app[bot] | 2020-08-27 11:28:15 +0000 |
|---|---|---|
| committer | GitHub | 2020-08-27 11:28:15 +0000 |
| commit | 79e91febb57976f802dc743f6411a831c45bb250 (patch) | |
| tree | f60e39e9419483aeca3522fbaa8c166a0d2c8bd5 /library | |
| parent | 350a9ab832905dab0ff05ecb76ddb7472c271833 (diff) | |
| parent | 72500ec169237ca98a5cfd5e4c0ff92b9c555eee (diff) | |
Merge PR #12867: Fast freeze summary
Reviewed-by: SkySkimmer
Diffstat (limited to 'library')
| -rw-r--r-- | library/summary.ml | 12 |
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; } |
