code simplifications concerning Summary

 - Most of the time, the table registered via Summary.declare_summary
   is just a single reference. A new function Summary.ref now allows
   to both declare this ref and register it to summary in one shot.

 - Clarifications concerning the role of [init_function].
   For statically registered tables that don't need a special initializer,
   just do nothing there (see the new Summary.nop function).

 Beware: now that Summary exports a function named "ref", any code that
 do an "open Summary" will probably fail to compile.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 91 insertions, 205 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index bdb7bd3682..cf333a886e 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -83,10 +83,14 @@ type substitutive_objects =
    * Modules which where created with Module M:=mexpr or with
      Module M:SIG. ... End M. have the keep list empty.
 *)
+
 let modtab_substobjs =
-  ref (MPmap.empty : substitutive_objects MPmap.t)
+  Summary.ref (MPmap.empty : substitutive_objects MPmap.t)
+    ~name:"MODULE-INFO-1"
+
 let modtab_objects =
-  ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t)
+  Summary.ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t)
+    ~name:"MODULE-INFO-2"
 
 type current_module_info = {
   cur_mp : module_path; (** current started interactive module (if any) *)
@@ -101,34 +105,12 @@ let default_module_info =
     cur_typ = None;
     cur_typs = [] }
 
-let openmod_info = ref default_module_info
+let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO-3"
 
 (* The library_cache here is needed to avoid recalculations of
    substituted modules object during "reloading" of libraries *)
-let library_cache = ref Dirmap.empty
-
-let freeze_mod_tables () =
-  !modtab_substobjs,
-  !modtab_objects,
-  !openmod_info,
-  !library_cache
-
-let unfreeze_mod_tables (sobjs,objs,info,libcache) =
-  modtab_substobjs := sobjs;
-  modtab_objects := objs;
-  openmod_info := info;
-  library_cache := libcache
-
-let init_mod_tables () =
-  modtab_substobjs := MPmap.empty;
-  modtab_objects := MPmap.empty;
-  openmod_info := default_module_info;
-  library_cache := Dirmap.empty
-
-let _ = Summary.declare_summary "MODULE-INFO"
-  { Summary.freeze_function = freeze_mod_tables;
-    Summary.unfreeze_function = unfreeze_mod_tables;
-    Summary.init_function = init_mod_tables }
+let library_cache = Summary.ref Dirmap.empty ~name:"MODULE-INFO-4"
+
 
 (* auxiliary functions to transform full_path and kernel_name given
    by Lib into module_path and DirPath.t needed for modules *)
@@ -303,24 +285,14 @@ let in_modkeep : lib_objects -> obj =
    The module M gets its objects from SIG
 *)
 let modtypetab =
-  ref (MPmap.empty : substitutive_objects MPmap.t)
+  Summary.ref (MPmap.empty : substitutive_objects MPmap.t)
+    ~name:"MODTYPE-INFO-1"
 
 (* currently started interactive module type. We remember its arguments
    if it is a functor type *)
 let openmodtype_info =
-  ref ([],[] : MBId.t list * module_type_body list)
-
-let freeze_modtyp_tables () =
-  !modtypetab, !openmodtype_info
-let unfreeze_modtyp_tables (mtt,omti) =
-  modtypetab := mtt; openmodtype_info := omti
-let init_modtyp_tables () =
-  modtypetab := MPmap.empty; openmodtype_info := [],[]
-
-let _ = Summary.declare_summary "MODTYPE-INFO"
-  { Summary.freeze_function = freeze_modtyp_tables;
-    Summary.unfreeze_function = unfreeze_modtyp_tables;
-    Summary.init_function = init_modtyp_tables }
+  Summary.ref ([],[] : MBId.t list * module_type_body list)
+    ~name:"MODTYPE-INFO-2"
 
 let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
   let mp = mp_of_kn kn in
diff --git a/library/decls.ml b/library/decls.ml
index 0ceea8b433..a93913a770 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -20,12 +20,8 @@ open Libnames
 type variable_data =
     DirPath.t * bool (* opacity *) * Univ.constraints * logical_kind
 
-let vartab = ref (Id.Map.empty : variable_data Id.Map.t)
-
-let _ = Summary.declare_summary "VARIABLE"
-  { Summary.freeze_function = (fun () -> !vartab);
-    Summary.unfreeze_function = (fun ft -> vartab := ft);
-    Summary.init_function = (fun () -> vartab := Id.Map.empty) }
+let vartab =
+  Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
 
 let add_variable_data id o = vartab := Id.Map.add id o !vartab
 
@@ -42,12 +38,7 @@ let variable_exists id = Id.Map.mem id !vartab
 
 (** Datas associated to global parameters and constants *)
 
-let csttab = ref (Cmap.empty : logical_kind Cmap.t)
-
-let _ = Summary.declare_summary "CONSTANT"
-	  { Summary.freeze_function = (fun () -> !csttab);
-	    Summary.unfreeze_function = (fun ft -> csttab := ft);
-	    Summary.init_function = (fun () -> csttab := Cmap.empty) }
+let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT"
 
 let add_constant_kind kn k = csttab := Cmap.add kn k !csttab
 
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index c26f652dfa..64267db01e 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -10,28 +10,10 @@ open Libnames
 
 type discharged_hyps = full_path list
 
-let discharged_hyps_map = ref Spmap.empty
+let discharged_hyps_map = Summary.ref Spmap.empty ~name:"discharged_hypothesis"
 
 let set_discharged_hyps sp hyps =
   discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
 
 let get_discharged_hyps sp =
-  try
-   Spmap.find sp !discharged_hyps_map
-  with Not_found ->
-    []
-
-(*s Registration as global tables and rollback. *)
-
-let init () =
-  discharged_hyps_map := Spmap.empty
-
-let freeze () = !discharged_hyps_map
-
-let unfreeze dhm = discharged_hyps_map := dhm
-
-let _ =
-  Summary.declare_summary "discharged_hypothesis"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+  try Spmap.find sp !discharged_hyps_map with Not_found -> []
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
index bc90220dbf..f2173bf49c 100644
--- a/library/dischargedhypsmap.mli
+++ b/library/dischargedhypsmap.mli
@@ -13,8 +13,8 @@ open Nametab
 
 type discharged_hyps = full_path list
 
-(** Discharged hypothesis. Here we store the discharged hypothesis of each 
-    constant or inductive type declaration.                                *)
+(** Discharged hypothesis. Here we store the discharged hypothesis of each
+    constant or inductive type declaration. *)
 
 val set_discharged_hyps : full_path -> discharged_hyps -> unit
 val get_discharged_hyps : full_path -> discharged_hyps
diff --git a/library/global.ml b/library/global.ml
index 929f7418ff..f120ef1951 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -10,12 +10,11 @@ open Names
 open Term
 open Environ
 open Safe_typing
-open Summary
 
 (* We introduce here the global environment of the system, and we declare it
    as a synchronized table. *)
 
-let global_env = ref empty_environment
+let global_env = Summary.ref empty_environment ~name:"Global environment"
 
 let safe_env () = !global_env
 
@@ -23,12 +22,6 @@ let env () = env_of_safe_env !global_env
 
 let env_is_empty () = is_empty !global_env
 
-let _ =
-  declare_summary "Global environment"
-    { freeze_function = (fun () -> !global_env);
-      unfreeze_function = (fun fr -> global_env := fr);
-      init_function = (fun () -> global_env := empty_environment) }
-
 (* Then we export the functions of [Typing] on that environment. *)
 
 let universes () = universes (env())
diff --git a/library/goptions.ml b/library/goptions.ml
index 381b677262..bdc6ab89d2 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -65,17 +65,10 @@ module MakeTable =
 
     module MySet = Set.Make (struct type t = A.t let compare = compare end)
 
-    let t = ref (MySet.empty : MySet.t)
-
-    let _ =
-      if A.synchronous then
-	let freeze () = !t in
-	let unfreeze c = t := c in
-	let init () = t := MySet.empty in
-	Summary.declare_summary nick
-          { Summary.freeze_function = freeze;
-            Summary.unfreeze_function = unfreeze;
-            Summary.init_function = init }
+    let t =
+      if A.synchronous
+      then Summary.ref MySet.empty ~name:nick
+      else ref MySet.empty
 
     let (add_option,remove_option) =
       if A.synchronous then
@@ -216,7 +209,6 @@ with Not_found ->
     or List.mem_assoc (nickname key) !ref_table
   then error "Sorry, this option name is already used."
 
-open Summary
 open Libobject
 open Lib
 
@@ -247,10 +239,10 @@ let declare_option cast uncast
 		       discharge_function = (fun (_,v) -> Some v);
 		       load_function = (fun _ (_,v) -> write v)}
     in
-    let _ = declare_summary (nickname key)
-	     { freeze_function = read;
-	       unfreeze_function = write;
-	       init_function = (fun () -> write default) }
+    let _ = Summary.declare_summary (nickname key)
+	     { Summary.freeze_function = read;
+	       Summary.unfreeze_function = write;
+	       Summary.init_function = (fun () -> write default) }
     in
     begin fun v -> add_anonymous_leaf (decl_obj v) end ,
     begin fun v -> add_anonymous_leaf (ldecl_obj v) end ,
diff --git a/library/heads.ml b/library/heads.ml
index e6c9bc9a85..022e61156d 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -52,19 +52,7 @@ module Evalrefmap =
   Map.Make (Evalreford)
 
 
-let head_map = ref Evalrefmap.empty
-
-let init () = head_map := Evalrefmap.empty
-
-let freeze () = !head_map
-
-let unfreeze hm = head_map := hm
-
-let _ =
-  Summary.declare_summary "Head_decl"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+let head_map = Summary.ref Evalrefmap.empty ~name:"Head_decl"
 
 let variable_head id  = Evalrefmap.find (EvalVarRef id) !head_map
 let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map
diff --git a/library/impargs.ml b/library/impargs.ml
index 56dca8e3f3..0026bc489c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -463,7 +463,7 @@ type implicit_discharge_request =
   | ImplInteractive of global_reference * implicits_flags *
       implicit_interactive_request
 
-let implicits_table = ref Refmap.empty
+let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
 
 let implicits_of_global ref =
   try
@@ -713,15 +713,3 @@ let rec select_impargs_size n = function
 let select_stronger_impargs = function
   | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *)
   | (_,impls)::_ -> impls
-
-(*s Registration as global tables *)
-
-let init () = implicits_table := Refmap.empty
-let freeze () = !implicits_table
-let unfreeze t = implicits_table := t
-
-let _ =
-  Summary.declare_summary "implicits"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
diff --git a/library/lib.ml b/library/lib.ml
index 30beb653f4..c7454edaf2 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -13,7 +13,6 @@ open Libnames
 open Globnames
 open Nameops
 open Libobject
-open Summary
 
 type is_type = bool (* Module Type or just Module *)
 type export = bool option (* None for a Module Type *)
@@ -217,10 +216,7 @@ let anonymous_id =
   fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n))
 
 let add_anonymous_entry node =
-  let id = anonymous_id () in
-  let name = make_oname id in
-  add_entry name node;
-  name
+  add_entry (make_oname (anonymous_id ())) node
 
 let add_leaf id obj =
   let (path, _) = current_prefix () in
@@ -253,7 +249,7 @@ let add_anonymous_leaf obj =
   add_entry oname (Leaf obj)
 
 let add_frozen_state () =
-  let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in ()
+  add_anonymous_entry (FrozenState (Summary.freeze_summaries()))
 
 (* Modules. *)
 
@@ -331,7 +327,7 @@ let start_compilation s mp =
   if not (Names.DirPath.equal (snd (snd (!path_prefix))) Names.DirPath.empty) then
     error "some sections are already opened";
   let prefix = s, (mp, Names.DirPath.empty) in
-  let _ = add_anonymous_entry (CompilingLibrary prefix) in
+  let () = add_anonymous_entry (CompilingLibrary prefix) in
   comp_name := Some s;
   path_prefix := prefix
 
@@ -406,8 +402,9 @@ type variable_context = variable_info list
 type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t
 
 let sectab =
-  ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list *
-		Cooking.work_list * abstr_list) list)
+  Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list *
+		        Cooking.work_list * abstr_list) list)
+    ~name:"section-context"
 
 let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
@@ -475,16 +472,6 @@ let section_instance = function
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
 
-let init_sectab () = sectab := []
-let freeze_sectab () = !sectab
-let unfreeze_sectab s = sectab := s
-
-let _ =
-  Summary.declare_summary "section-context"
-    { Summary.freeze_function = freeze_sectab;
-      Summary.unfreeze_function = unfreeze_sectab;
-      Summary.init_function = init_sectab }
-
 (*************)
 (* Sections. *)
 
@@ -502,7 +489,7 @@ let open_section id =
   let name = make_path id, make_kn id (* this makes little sense however *) in
   if Nametab.exists_section dir then
     errorlabstrm "open_section" (pr_id id ++ str " already exists.");
-  let fs = freeze_summaries() in
+  let fs = Summary.freeze_summaries() in
   add_entry name (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
@@ -564,7 +551,7 @@ let set_lib_stk new_lib_stk =
   lib_stk := new_lib_stk;
   recalc_path_prefix ();
   let spf = match find_entry_p is_frozen_state with
-    | (sp, FrozenState f) -> unfreeze_summaries f; sp
+    | (sp, FrozenState f) -> Summary.unfreeze_summaries f; sp
     | _ -> assert false
   in
   let (after,_,_) = split_lib spf in
@@ -635,7 +622,7 @@ let init () =
   add_frozen_state ();
   comp_name := None;
   path_prefix := initial_prefix;
-  init_summaries()
+  Summary.init_summaries ()
 
 (* Misc *)
 
diff --git a/library/library.ml b/library/library.ml
index 7c34a62d07..e1ef4515d6 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -45,40 +45,16 @@ module LibraryMap = Map.Make(LibraryOrdered)
 module LibraryFilenameMap = Map.Make(LibraryOrdered)
 
 (* This is a map from names to loaded libraries *)
-let libraries_table = ref LibraryMap.empty
+let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY"
 
 (* This is the map of loaded libraries filename *)
 (* (not synchronized so as not to be caught in the states on disk) *)
 let libraries_filename_table = ref LibraryFilenameMap.empty
 
 (* These are the _ordered_ sets of loaded, imported and exported libraries *)
-let libraries_loaded_list = ref []
-let libraries_imports_list = ref []
-let libraries_exports_list = ref []
-
-let freeze () =
-  !libraries_table,
-  !libraries_loaded_list,
-  !libraries_imports_list,
-  !libraries_exports_list
-
-let unfreeze (mt,mo,mi,me) =
-  libraries_table := mt;
-  libraries_loaded_list := mo;
-  libraries_imports_list := mi;
-  libraries_exports_list := me
-
-let init () =
-  libraries_table := LibraryMap.empty;
-  libraries_loaded_list := [];
-  libraries_imports_list := [];
-  libraries_exports_list := []
-
-let _ =
-  Summary.declare_summary "MODULES"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD"
+let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT"
+let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT"
 
 (* various requests to the tables *)
 
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 315cbf96e9..873703aff9 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -20,13 +20,7 @@ type t = {
   path_is_root : bool;
 }
 
-let load_paths = ref ([] : t list)
-
-let () = Summary.declare_summary "LOADPATHS" {
-  Summary.freeze_function = (fun () -> !load_paths);
-  Summary.unfreeze_function = (fun l -> load_paths := l);
-  Summary.init_function = (fun () -> load_paths := []);
-}
+let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS"
 
 let logical p = p.path_logical
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 01324a3a42..1d43725f6f 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -540,19 +540,9 @@ let global_inductive r =
 (********************************************************************)
 (* Registration of tables as a global table and rollback            *)
 
-type frozen = ccitab * dirtab * mptab * kntab 
+type frozen = ccitab * dirtab * mptab * kntab
     * globrevtab * mprevtab * mptrevtab * knrevtab
 
-let init () =
-  the_ccitab := ExtRefTab.empty;
-  the_dirtab := DirTab.empty;
-  the_modtypetab := MPTab.empty;
-  the_tactictab := KnTab.empty;
-  the_globrevtab := Globrevtab.empty;
-  the_modrevtab := MPmap.empty;
-  the_modtyperevtab := MPmap.empty;
-  the_tacticrevtab := KNmap.empty
-
 let freeze () : frozen =
   !the_ccitab,
   !the_dirtab,
@@ -577,7 +567,7 @@ let _ =
   Summary.declare_summary "names"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = Summary.nop }
 
 (* Deprecated synonyms *)
 
diff --git a/library/summary.ml b/library/summary.ml
index c6de357443..797cb64bfb 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -19,6 +19,9 @@ let summaries =
   (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t)
 
 let internal_declare_summary sumname sdecl =
+  if Hashtbl.mem summaries sumname then
+    anomaly ~label:"Summary.declare_summary"
+      (str "Cannot declare a summary twice: " ++ str sumname);
   let (infun,outfun) = Dyn.create sumname in
   let dyn_freeze () = infun (sdecl.freeze_function())
   and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
@@ -28,9 +31,6 @@ let internal_declare_summary sumname sdecl =
     unfreeze_function = dyn_unfreeze;
     init_function = dyn_init }
   in
-  if Hashtbl.mem summaries sumname then
-    anomaly ~label:"Summary.declare_summary"
-      (str "Cannot declare a summary twice: " ++ str sumname);
   Hashtbl.add summaries sumname ddecl
 
 let declare_summary sumname decl =
@@ -45,7 +45,6 @@ let freeze_summaries () =
     summaries;
   !m
 
-
 let unfreeze_summaries fs =
   Hashtbl.iter
     (fun id decl ->
@@ -55,3 +54,18 @@ let unfreeze_summaries fs =
 
 let init_summaries () =
   Hashtbl.iter (fun _ decl -> decl.init_function()) summaries
+
+(** For global tables registered statically before the end of coqtop
+    launch, the following empty [init_function] could be used. *)
+
+let nop () = ()
+
+(** All-in-one reference declaration + registration *)
+
+let ref ~name x =
+  let r = ref x in
+  declare_summary name
+    { freeze_function = (fun () -> !r);
+      unfreeze_function = ((:=) r);
+      init_function = (fun () -> r := x) };
+  r
diff --git a/library/summary.mli b/library/summary.mli
index 7ded099abf..fd1b324c93 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -14,17 +14,36 @@ type 'a summary_declaration = {
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
+(** For tables registered during the launch of coqtop, the [init_function]
+    will be run only once, during an [init_summaries] done at the end of
+    coqtop initialization. For tables registered later (for instance
+    during a plugin dynlink), [init_function] is used when unfreezing
+    an earlier frozen state that doesn't contain any value for this table.
+
+    Beware: for tables registered dynamically after the initialization
+    of Coq, their init functions may not be run immediately. It is hence
+    the responsability of plugins to initialize themselves properly.
+*)
+
 val declare_summary : string -> 'a summary_declaration -> unit
 
+(** 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.
+    The [init_function] restores the reference to its initial value. *)
+
+val ref : name:string -> 'a -> 'a ref
+
+(** For global tables registered statically before the end of coqtop
+    launch, the following empty [init_function] could be used. *)
+
+val nop : unit -> unit
+
+(** The type [frozen] is a snapshot of the states of all the registered
+    tables of the system. *)
+
 type frozen
 
 val freeze_summaries : unit -> frozen
 val unfreeze_summaries : frozen -> unit
 val init_summaries : unit -> unit
-
-(** Beware: if some code is dynamically loaded via dynlink after the
-    initialization of Coq, the init functions of any summary declared
-    by this code may not be run. It is hence the responsability of
-    plugins to initialize themselves properly.
-*)
-