1 files changed, 111 insertions, 114 deletions

diff --git a/library/summary.ml b/library/summary.ml
index 6efa07f3..7ef19fbf 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -1,29 +1,36 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Pp
 open CErrors
 open Util
 
-module Dyn = Dyn.Make(struct end)
+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,138 +39,126 @@ 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)
+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 warn_summary_out_of_scope =
+  let name = "summary-out-of-scope" in
+  let category = "dev" in
+  let default = CWarnings.Disabled in
+  CWarnings.create ~name ~category ~default (fun name ->
+    Pp.str (Printf.sprintf
+      "A Coq plugin was loaded inside a local scope (such as a Section). It is recommended to load plugins at the start of the file. Summary entry: %s"
+      name)
+    )
+
+let unfreeze_summaries ?(partial=false) { 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)
-  in
-  let () = match fs.ml_module with
-  | None -> anomaly (str "Undeclared summary " ++ str ml_modules)
-  | 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
+   * 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 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 ->
+      if not partial then begin
+        warn_summary_out_of_scope name;
+        decl.init_function ()
+      end;
   in
-  let fold id decl state =
-    try fold id decl state
-    with e when CErrors.noncritical e ->
-      let e = CErrors.push e in
-      Printf.eprintf "Error unfrezing summay %s\n%s\n%!"
-        (name_of_summary id) (Pp.string_of_ppcmds (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 =
@@ -172,19 +167,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
 
@@ -196,8 +194,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)