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

1 files changed, 18 insertions, 4 deletions

diff --git a/library/summary.ml b/library/summary.ml
index c6de35744..797cb64bf 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