aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-01 19:13:04 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-09 18:16:27 +0100
commit8c9166435d6926babf697c3f575a8653f465cc76 (patch)
tree146553666f8bc1cc619d9c30c4230232fea46464 /library
parentdea662ae5fd7225c06392e1b3f5acb1cd8e97e91 (diff)
[summary] Allow typed projections from global state + rework of internals.
In the transition towards a less global state handling we have the necessity of mix imperative setting [notably for the modules/section code] and functional handling of state [notably in the STM]. In that scenario, it is very convenient to have typed access to the Coq's `summary`. Thus, I reify the API to support typed access to the `summary`, and implement such access in a couple of convenient places. We also update some internal datatypes to simplify the `frozen` data type. We also remove the use of hashes as it doesn't really make things faster, and most operations are now over `Maps` anyways. I believe this goes in line with recent work by @ppedrot. We also deprecate the non-typed accessors, which were only supposed to be used in the STM, which is now ported to the finer primitives.
Diffstat (limited to 'library')
-rw-r--r--library/summary.ml201
-rw-r--r--library/summary.mli39
2 files changed, 122 insertions, 118 deletions
diff --git a/library/summary.ml b/library/summary.ml
index 9f49d1f83..5fe3160e1 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -13,17 +13,22 @@ open Util
module Dyn = Dyn.Make ()
type marshallable = [ `Yes | `No | `Shallow ]
+
type 'a summary_declaration = {
freeze_function : marshallable -> 'a;
unfreeze_function : 'a -> unit;
init_function : unit -> unit }
-let summaries = ref Int.Map.empty
+let sum_mod = ref None
+let sum_map = ref String.Map.empty
let mangle id = id ^ "-SUMMARY"
+let unmangle id = String.(sub id 0 (length id - 8))
+
+let ml_modules = "ML-MODULES"
-let internal_declare_summary hash sumname sdecl =
- let (infun, outfun) = Dyn.Easy.make_dyn (mangle sumname) in
+let internal_declare_summary fadd sumname sdecl =
+ let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in
let dyn_freeze b = infun (sdecl.freeze_function b)
and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
and dyn_init = sdecl.init_function in
@@ -32,140 +37,114 @@ let internal_declare_summary hash sumname sdecl =
unfreeze_function = dyn_unfreeze;
init_function = dyn_init }
in
- summaries := Int.Map.add hash (sumname, ddecl) !summaries
+ fadd sumname ddecl;
+ tag
-let all_declared_summaries = ref Int.Set.empty
+let declare_ml_modules_summary decl =
+ let ml_add _ ddecl = sum_mod := Some ddecl in
+ internal_declare_summary ml_add ml_modules decl
-let summary_names = ref []
-let name_of_summary name =
- try List.assoc name !summary_names
- with Not_found -> "summary name not found"
+let declare_ml_modules_summary decl =
+ ignore(declare_ml_modules_summary decl)
-let declare_summary sumname decl =
- let hash = String.hash sumname in
- let () = if Int.Map.mem hash !summaries then
- let (name, _) = Int.Map.find hash !summaries in
- anomaly ~label:"Summary.declare_summary"
- (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name ++ str ".")
+let declare_summary_tag sumname decl =
+ let fadd name ddecl = sum_map := String.Map.add name ddecl !sum_map in
+ let () = if String.Map.mem sumname !sum_map then
+ anomaly ~label:"Summary.declare_summary"
+ (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str sumname ++ str ".")
in
- all_declared_summaries := Int.Set.add hash !all_declared_summaries;
- summary_names := (hash, sumname) :: !summary_names;
- internal_declare_summary hash sumname decl
+ internal_declare_summary fadd sumname decl
+
+let declare_summary sumname decl =
+ ignore(declare_summary_tag sumname decl)
type frozen = {
- summaries : (int * Dyn.t) list;
+ summaries : Dyn.t String.Map.t;
(** Ordered list w.r.t. the first component. *)
ml_module : Dyn.t option;
(** Special handling of the ml_module summary. *)
}
-let empty_frozen = { summaries = []; ml_module = None; }
-
-let ml_modules = "ML-MODULES"
-let ml_modules_summary = String.hash ml_modules
+let empty_frozen = { summaries = String.Map.empty; ml_module = None }
let freeze_summaries ~marshallable : frozen =
- let fold id (_, decl) accu =
- (* to debug missing Lazy.force
- if marshallable <> `No then begin
- let id, _ = Int.Map.find id !summaries in
- prerr_endline ("begin marshalling " ^ id);
- ignore(Marshal.to_string (decl.freeze_function marshallable) []);
- prerr_endline ("end marshalling " ^ id);
- end;
- /debug *)
- let state = decl.freeze_function marshallable in
- if Int.equal id ml_modules_summary then { accu with ml_module = Some state }
- else { accu with summaries = (id, state) :: accu.summaries }
+ let smap decl = decl.freeze_function marshallable in
+ { summaries = String.Map.map smap !sum_map;
+ ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod;
+ }
+
+let unfreeze_single name state =
+ let decl =
+ try String.Map.find name !sum_map
+ with
+ | Not_found ->
+ CErrors.anomaly Pp.(str "trying to unfreeze unregistered summary " ++ str name)
in
- Int.Map.fold_right fold !summaries empty_frozen
-
-let unfreeze_summaries fs =
+ try decl.unfreeze_function state
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
+ Feedback.msg_warning
+ Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]);
+ iraise e
+
+let unfreeze_summaries { summaries; ml_module } =
(* The unfreezing of [ml_modules_summary] has to be anticipated since it
- * may modify the content of [summaries] ny loading new ML modules *)
- let (_, decl) =
- try Int.Map.find ml_modules_summary !summaries
- with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
- in
- let () = match fs.ml_module with
+ * may modify the content of [summaries] by loading new ML modules *)
+ begin match !sum_mod with
| None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
- | Some state -> decl.unfreeze_function state
- in
- let fold id (_, decl) states =
- if Int.equal id ml_modules_summary then states
- else match states with
- | [] ->
- let () = decl.init_function () in
- []
- | (nid, state) :: rstates ->
- if Int.equal id nid then
- let () = decl.unfreeze_function state in rstates
- else
- let () = decl.init_function () in states
+ | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module
+ end;
+ (** We must be independent on the order of the map! *)
+ let ufz name decl =
+ try decl.unfreeze_function String.Map.(find name summaries)
+ with Not_found ->
+ Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name);
+ decl.init_function ()
in
- let fold id decl state =
- try fold id decl state
- with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- Feedback.msg_error
- Pp.(seq [str "Error unfreezing summary %s\n%s\n%!";
- str (name_of_summary id);
- CErrors.iprint e]);
- iraise e
- in
- (** We rely on the order of the frozen list, and the order of folding *)
- ignore (Int.Map.fold_left fold !summaries fs.summaries)
+ (* String.Map.iter unfreeze_single !sum_map *)
+ String.Map.iter ufz !sum_map
let init_summaries () =
- Int.Map.iter (fun _ (_, decl) -> decl.init_function ()) !summaries
+ String.Map.iter (fun _ decl -> decl.init_function ()) !sum_map
(** For global tables registered statically before the end of coqtop
launch, the following empty [init_function] could be used. *)
let nop () = ()
-(** Selective freeze *)
+(** Summary projection *)
+let project_from_summary { summaries } tag =
+ let id = unmangle (Dyn.repr tag) in
+ let state = String.Map.find id summaries in
+ Option.get (Dyn.Easy.prj state tag)
+
+let modify_summary st tag v =
+ let id = unmangle (Dyn.repr tag) in
+ let summaries = String.Map.set id (Dyn.Easy.inj v tag) st.summaries in
+ {st with summaries}
-type frozen_bits = (int * Dyn.t) list
+let remove_from_summary st tag =
+ let id = unmangle (Dyn.repr tag) in
+ let summaries = String.Map.remove id st.summaries in
+ {st with summaries}
+
+(** Selective freeze *)
-let ids_of_string_list complement ids =
- if not complement then List.map String.hash ids
- else
- let fold accu id =
- let id = String.hash id in
- Int.Set.remove id accu
- in
- let ids = List.fold_left fold !all_declared_summaries ids in
- Int.Set.elements ids
+type frozen_bits = Dyn.t String.Map.t
let freeze_summary ~marshallable ?(complement=false) ids =
- let ids = ids_of_string_list complement ids in
- List.map (fun id ->
- let (_, summary) = Int.Map.find id !summaries in
- id, summary.freeze_function marshallable)
- ids
-
-let unfreeze_summary datas =
- List.iter
- (fun (id, data) ->
- let (name, summary) = Int.Map.find id !summaries in
- try summary.unfreeze_function data
- with e ->
- let e = CErrors.push e in
- prerr_endline ("Exception unfreezing " ^ name);
- iraise e)
- datas
+ let sub_map = String.Map.filter (fun id _ -> complement <> List.(mem id ids)) !sum_map in
+ String.Map.map (fun decl -> decl.freeze_function marshallable) sub_map
+
+let unfreeze_summary = String.Map.iter unfreeze_single
let surgery_summary { summaries; ml_module } bits =
- let summaries = List.map (fun (id, _ as orig) ->
- try id, List.assoc id bits
- with Not_found -> orig)
- summaries in
+ let summaries =
+ String.Map.fold (fun hash state sum -> String.Map.set hash state sum ) summaries bits in
{ summaries; ml_module }
let project_summary { summaries; ml_module } ?(complement=false) ids =
- let ids = ids_of_string_list complement ids in
- List.filter (fun (id, _) -> List.mem id ids) summaries
+ String.Map.filter (fun name _ -> complement <> List.(mem name ids)) summaries
let pointer_equal l1 l2 =
let ptr_equal d1 d2 =
@@ -174,19 +153,22 @@ let pointer_equal l1 l2 =
match Dyn.eq t1 t2 with
| None -> false
| Some Refl -> x1 == x2
- in
+ in
+ let l1, l2 = String.Map.bindings l1, String.Map.bindings l2 in
CList.for_all2eq
(fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2
(** All-in-one reference declaration + registration *)
-let ref ?(freeze=fun _ r -> r) ~name x =
+let ref_tag ?(freeze=fun _ r -> r) ~name x =
let r = ref x in
- declare_summary name
+ let tag = declare_summary_tag name
{ freeze_function = (fun b -> freeze b !r);
unfreeze_function = ((:=) r);
- init_function = (fun () -> r := x) };
- r
+ init_function = (fun () -> r := x) } in
+ r, tag
+
+let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x
module Local = struct
@@ -198,8 +180,7 @@ let (!) r =
let key, name = !r in
try CEphemeron.get key
with CEphemeron.InvalidKey ->
- let _, { init_function } =
- Int.Map.find (String.hash (mangle name)) !summaries in
+ let { init_function } = String.Map.find name !sum_map in
init_function ();
CEphemeron.get (fst !r)
diff --git a/library/summary.mli b/library/summary.mli
index d093d95f2..9fc6df6ad 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -36,6 +36,12 @@ type 'a summary_declaration = {
val declare_summary : string -> 'a summary_declaration -> unit
+(** We provide safe projection from the summary to the types stored in
+ it.*)
+module Dyn : Dyn.S
+
+val declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag
+
(** All-in-one reference declaration + summary registration.
It behaves just as OCaml's standard [ref] function, except
that a [declare_summary] is done, with [name] as string.
@@ -43,6 +49,7 @@ val declare_summary : string -> 'a summary_declaration -> unit
The [freeze_function] can be overridden *)
val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
+val ref_tag : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag
(* As [ref] but the value is local to a process, i.e. not sent to, say, proof
* workers. It is useful to implement a local cache for example. *)
@@ -55,10 +62,11 @@ module Local : sig
end
-(** Special name for the summary of ML modules. This summary entry is
- special because its unfreeze may load ML code and hence add summary
- entries. Thus is has to be recognizable, and handled appropriately *)
-val ml_modules : string
+(** Special summary for ML modules. This summary entry is special
+ because its unfreeze may load ML code and hence add summary
+ entries. Thus is has to be recognizable, and handled properly.
+ *)
+val declare_ml_modules_summary : 'a summary_declaration -> unit
(** For global tables registered statically before the end of coqtop
launch, the following empty [init_function] could be used. *)
@@ -75,16 +83,31 @@ val freeze_summaries : marshallable:marshallable -> frozen
val unfreeze_summaries : frozen -> unit
val init_summaries : unit -> unit
-(** The type [frozen_bits] is a snapshot of some of the registered tables *)
+(** Typed projection of the summary. Experimental API, use with CARE *)
+
+val modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen
+val project_from_summary : frozen -> 'a Dyn.tag -> 'a
+val remove_from_summary : frozen -> 'a Dyn.tag -> frozen
+
+(** The type [frozen_bits] is a snapshot of some of the registered
+ tables. It is DEPRECATED in favor of the typed projection
+ version. *)
+
type frozen_bits
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
-val freeze_summary :
- marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits
+[@@@ocaml.warning "-3"]
+val freeze_summary : marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
val unfreeze_summary : frozen_bits -> unit
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
val surgery_summary : frozen -> frozen_bits -> frozen
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
val pointer_equal : frozen_bits -> frozen_bits -> bool
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
+[@@@ocaml.warning "+3"]
(** {6 Debug} *)
-
val dump : unit -> (int * string) list