States: frozen states can hold closures

States.freeze takes ~marshallable:bool, so that (only) when we want to
marshal data to disk/network we can ask the freeze functions of the
summary to force lazy values.  The flag is propagated to Lib and Summary.

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

1 files changed, 14 insertions, 6 deletions

diff --git a/library/summary.ml b/library/summary.ml
index 056acd41c..53e9f7002 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -11,7 +11,7 @@ open Errors
 open Util
 
 type 'a summary_declaration = {
-  freeze_function : unit -> 'a;
+  freeze_function : bool -> 'a;
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
@@ -20,7 +20,7 @@ let summaries =
 
 let internal_declare_summary sumname sdecl =
   let (infun,outfun) = Dyn.create sumname in
-  let dyn_freeze () = infun (sdecl.freeze_function())
+  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
   let ddecl = {
@@ -43,10 +43,18 @@ let declare_summary sumname decl =
 
 type frozen = Dyn.t String.Map.t
 
-let freeze_summaries () =
+let freeze_summaries ~marshallable =
   let m = ref String.Map.empty in
   Hashtbl.iter
-    (fun id decl -> m := String.Map.add id (decl.freeze_function()) !m)
+    (fun id decl -> 
+       (* to debug missing Lazy.force 
+       if marshallable then begin
+         prerr_endline ("begin marshalling " ^ id);
+         ignore(Marshal.to_string (decl.freeze_function marshallable) []);
+         prerr_endline ("end marshalling " ^ id);
+       end;
+        /debug *)
+       m := String.Map.add id (decl.freeze_function marshallable) !m)
     summaries;
   !m
 
@@ -92,10 +100,10 @@ let unfreeze_summary datas =
 
 (** All-in-one reference declaration + registration *)
 
-let ref ~name x =
+let ref ?(freeze=fun _ r -> r) ~name x =
   let r = ref x in
   declare_summary name
-    { freeze_function = (fun () -> !r);
+    { freeze_function = (fun b -> freeze b !r);
       unfreeze_function = ((:=) r);
       init_function = (fun () -> r := x) };
   r