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

5 files changed, 18 insertions, 90 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 42099f5dbb..4562c5aa5f 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -15,14 +15,9 @@ open Util
 open Libobject
 (*i*)
 
-let empty_name_table = (Refmap.empty : Name.t list list Refmap.t)
-let name_table = ref empty_name_table
-
-let _ =
-  Summary.declare_summary "rename-arguments"
-    { Summary.freeze_function = (fun () -> !name_table);
-      Summary.unfreeze_function = (fun r -> name_table := r);
-      Summary.init_function = (fun () -> name_table := empty_name_table) }
+let name_table =
+  Summary.ref (Refmap.empty : Name.t list list Refmap.t)
+    ~name:"rename-arguments"
 
 type req =
   | ReqLocal
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d9a22b3e78..82dda8e0f4 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -164,11 +164,7 @@ let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
 
 (* Generator of metavariables *)
 let new_meta =
-  let meta_ctr = ref 0 in
-  Summary.declare_summary "meta counter"
-    { Summary.freeze_function = (fun () -> !meta_ctr);
-      Summary.unfreeze_function = (fun n -> meta_ctr := n);
-      Summary.init_function = (fun () -> meta_ctr := 0) };
+  let meta_ctr = Summary.ref 0 ~name:"meta counter" in
   fun () -> incr meta_ctr; !meta_ctr
 
 let mk_new_meta () = mkMeta(new_meta())
@@ -262,11 +258,7 @@ let make_pure_subst evi args =
 
 (* Generator of existential names *)
 let new_untyped_evar =
-  let evar_ctr = ref 0 in
-  Summary.declare_summary "evar counter"
-    { Summary.freeze_function = (fun () -> !evar_ctr);
-      Summary.unfreeze_function = (fun n -> evar_ctr := n);
-      Summary.init_function = (fun () -> evar_ctr := 0) };
+  let evar_ctr = Summary.ref 0 ~name:"evar counter" in
   fun () -> incr evar_ctr; existential_of_int !evar_ctr
 
 (*------------------------------------*
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 7c2ac1a27b..5aced6e10c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -39,8 +39,10 @@ type struc_typ = {
   s_PROJKIND : (Name.t * bool) list;
   s_PROJ : constant option list }
 
-let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
-let projection_table = ref Cmap.empty
+let structure_table =
+  Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs"
+let projection_table =
+  Summary.ref Cmap.empty ~name:"record-projs"
 
 (* TODO: could be unify struc_typ and struc_tuple ? in particular,
    is the inductive always (fst constructor) ? It seems so... *)
@@ -126,15 +128,7 @@ module MethodsDnet : Term_dnet.S
      let direction = true
    end)
 
-let meth_dnet = ref MethodsDnet.empty
-
-open Summary
-
-let _ =
-  declare_summary "record-methods-state"
-    { freeze_function = (fun () -> !meth_dnet);
-      unfreeze_function = (fun m -> meth_dnet := m);
-      init_function = (fun () -> meth_dnet := MethodsDnet.empty) }
+let meth_dnet = Summary.ref MethodsDnet.empty ~name:"record-methods-state"
 
 open Libobject
 
@@ -194,7 +188,9 @@ type cs_pattern =
   | Sort_cs of sorts_family
   | Default_cs
 
-let object_table = ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t)
+let object_table =
+  Summary.ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t)
+    ~name:"record-canonical-structs"
 
 let canonical_projections () =
   Refmap.fold (fun x -> List.fold_right (fun (y,c) acc -> ((x,y),c)::acc))
@@ -346,21 +342,3 @@ let is_open_canonical_projection env sigma (c,args) =
       not (isConstruct hd) 
     with Failure _ -> false
   with Not_found -> false
-
-let freeze () =
-  !structure_table, !projection_table, !object_table
-
-let unfreeze (s,p,o) =
-  structure_table := s; projection_table := p; object_table := o
-
-let init () =
-  structure_table := Indmap.empty; projection_table := Cmap.empty;
-  object_table := Refmap.empty
-
-let _ = init()
-
-let _ =
-  Summary.declare_summary "objdefs"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b46b69c624..efc2a7467f 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -134,22 +134,7 @@ type constant_evaluation =
 
 type frozen = constant_evaluation Cmap.t
 
-let eval_table = ref (Cmap.empty : frozen)
-
-let init () =
-  eval_table := Cmap.empty
-
-let freeze () =
-  !eval_table
-
-let unfreeze ct =
-  eval_table := ct
-
-let _ =
-  Summary.declare_summary "evaluation"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+let eval_table = Summary.ref (Cmap.empty : frozen) ~name:"evaluation"
 
 (* [compute_consteval] determines whether c is an "elimination constant"
 
@@ -548,13 +533,8 @@ type behaviour = {
   b_dont_expose_case: bool;
 }
 
-let behaviour_table = ref (Refmap.empty : behaviour Refmap.t)
-
-let _ =
-  Summary.declare_summary "simplbehaviour"
-    { Summary.freeze_function = (fun () -> !behaviour_table);
-      Summary.unfreeze_function = (fun x -> behaviour_table := x);
-      Summary.init_function = (fun () -> behaviour_table := Refmap.empty) }
+let behaviour_table =
+  Summary.ref (Refmap.empty : behaviour Refmap.t) ~name:"simplbehaviour"
 
 type simpl_flag = [ `SimplDontExposeCase | `SimplNeverUnfold ]
 type req =
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 25109ffcf0..86ff2a28fe 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -93,25 +93,8 @@ let new_instance cl pri glob impl =
  * states management
  *)
 
-let classes : typeclasses ref = ref Gmap.empty
-
-let instances : instances ref = ref Gmap.empty
-
-let freeze () = !classes, !instances
-
-let unfreeze (cl,is) =
-  classes:=cl;
-  instances:=is
-
-let init () =
-  classes:= Gmap.empty;
-  instances:= Gmap.empty
-
-let _ =
-  Summary.declare_summary "classes_and_instances"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+let classes : typeclasses ref = Summary.ref Gmap.empty ~name:"classes"
+let instances : instances ref = Summary.ref Gmap.empty ~name:"instances"
 
 let class_info c =
   try Gmap.find c !classes