aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-08-27 11:28:15 +0000
committerGitHub2020-08-27 11:28:15 +0000
commit79e91febb57976f802dc743f6411a831c45bb250 (patch)
treef60e39e9419483aeca3522fbaa8c166a0d2c8bd5
parent350a9ab832905dab0ff05ecb76ddb7472c271833 (diff)
parent72500ec169237ca98a5cfd5e4c0ff92b9c555eee (diff)
Merge PR #12867: Fast freeze summary
Reviewed-by: SkySkimmer
-rw-r--r--clib/dyn.ml17
-rw-r--r--clib/dyn.mli6
-rw-r--r--library/summary.ml12
3 files changed, 31 insertions, 4 deletions
diff --git a/clib/dyn.ml b/clib/dyn.ml
index 1ddbe5a7c2..8ef90a366e 100644
--- a/clib/dyn.ml
+++ b/clib/dyn.ml
@@ -49,6 +49,13 @@ sig
module Map(Value : ValueS) :
MapS with type 'a key = 'a tag and type 'a value = 'a Value.t
+
+ module HMap (V1 : ValueS)(V2 : ValueS) :
+ sig
+ type map = { map : 'a. 'a tag -> 'a V1.t -> 'a V2.t }
+ val map : map -> Map(V1).t -> Map(V2).t
+ end
+
end
module type S =
@@ -132,6 +139,16 @@ module Self : PreS = struct
let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m
let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu
end
+
+ module HMap (V1 : ValueS) (V2 : ValueS) =
+ struct
+ type map = { map : 'a. 'a tag -> 'a V1.t -> 'a V2.t }
+
+ let map (f : map) (m : Map(V1).t) : Map(V2).t =
+ Int.Map.mapi f.map m
+
+ end
+
end
include Self
diff --git a/clib/dyn.mli b/clib/dyn.mli
index 926d0f3135..4fd33b5242 100644
--- a/clib/dyn.mli
+++ b/clib/dyn.mli
@@ -75,6 +75,12 @@ sig
MapS with type 'a key = 'a tag and type 'a value = 'a Value.t
(** Map from type tags to values parameterized by the tag type *)
+ module HMap (V1 : ValueS)(V2 : ValueS) :
+ sig
+ type map = { map : 'a. 'a tag -> 'a V1.t -> 'a V2.t }
+ val map : map -> Map(V1).t -> Map(V2).t
+ end
+
module Easy : sig
(* To create a dynamic type on the fly *)
val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
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;
}