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

9 files changed, 37 insertions, 24 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 5866d612e..894445de1 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -111,7 +111,6 @@ let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO-3"
    substituted modules object during "reloading" of libraries *)
 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 *)
 
@@ -887,7 +886,7 @@ let declare_include_ interp_struct me_asts =
     of summaries *)
 
 let protect_summaries f =
-  let fs = Summary.freeze_summaries () in
+  let fs = Summary.freeze_summaries ~marshallable:false in
   try f fs
   with reraise ->
     (* Something wrong: undo the whole process *)
diff --git a/library/goptions.ml b/library/goptions.ml
index bdc6ab89d..597c23b7d 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -240,7 +240,7 @@ let declare_option cast uncast
 		       load_function = (fun _ (_,v) -> write v)}
     in
     let _ = Summary.declare_summary (nickname key)
-	     { Summary.freeze_function = read;
+	     { Summary.freeze_function = (fun _ -> read ());
 	       Summary.unfreeze_function = write;
 	       Summary.init_function = (fun () -> write default) }
     in
diff --git a/library/lib.ml b/library/lib.ml
index e33bf5b15..0ba9fd919 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -249,7 +249,8 @@ let add_anonymous_leaf obj =
   add_entry oname (Leaf obj)
 
 let add_frozen_state () =
-  add_anonymous_entry (FrozenState (Summary.freeze_summaries()))
+  add_anonymous_entry
+    (FrozenState (Summary.freeze_summaries ~marshallable:false))
 
 (* Modules. *)
 
@@ -487,7 +488,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 = Summary.freeze_summaries() in
+  let fs = Summary.freeze_summaries ~marshallable:false 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);
@@ -608,7 +609,7 @@ let label_before_name (loc,id) =
 
 type frozen = Names.DirPath.t option * library_segment
 
-let freeze () = (!comp_name, !lib_stk)
+let freeze ~marshallable:_ = (!comp_name, !lib_stk)
 
 let unfreeze (mn,stk) =
   comp_name := mn;
diff --git a/library/lib.mli b/library/lib.mli
index ce57721fb..8ab98f775 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -172,7 +172,7 @@ val label_before_name : Names.Id.t Loc.located -> int
 
 type frozen
 
-val freeze : unit -> frozen
+val freeze : marshallable:bool -> frozen
 val unfreeze : frozen -> unit
 
 val init : unit -> unit
diff --git a/library/nametab.ml b/library/nametab.ml
index 1d43725f6..12cad7f55 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -543,7 +543,7 @@ let global_inductive r =
 type frozen = ccitab * dirtab * mptab * kntab
     * globrevtab * mprevtab * mptrevtab * knrevtab
 
-let freeze () : frozen =
+let freeze _ : frozen =
   !the_ccitab,
   !the_dirtab,
   !the_modtypetab,
diff --git a/library/states.ml b/library/states.ml
index 8b8193981..1fd3fa2e5 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -10,8 +10,8 @@ open System
 
 type state = Lib.frozen * Summary.frozen
 
-let freeze () =
-  (Lib.freeze(), Summary.freeze_summaries())
+let freeze ~marshallable =
+  (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
 
 let unfreeze (fl,fs) =
   Lib.unfreeze fl;
@@ -23,7 +23,7 @@ let (extern_state,intern_state) =
     extern_intern Coq_config.state_magic_number in
   (fun s ->
     let s = ensure_suffix s in
-    raw_extern s (freeze())),
+    raw_extern s (freeze ~marshallable:true)),
   (fun s ->
     let s = ensure_suffix s in
     let paths = Loadpath.get_paths () in
@@ -33,7 +33,7 @@ let (extern_state,intern_state) =
 (* Rollback. *)
 
 let with_heavy_rollback f h x =
-  let st = freeze () in
+  let st = freeze ~marshallable:false in
   try
     f x
   with reraise ->
@@ -44,8 +44,10 @@ let without_rollback f h x =
   with reraise -> raise (h reraise)
 
 let with_state_protection f x =
-  let st = freeze () in
+  let st = freeze ~marshallable:false in
   try
     let a = f x in unfreeze st; a
   with reraise ->
     (unfreeze st; raise reraise)
+
+
diff --git a/library/states.mli b/library/states.mli
index 26dec09e5..d186bf1c8 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -17,7 +17,7 @@ val intern_state : string -> unit
 val extern_state : string -> unit
 
 type state
-val freeze : unit -> state
+val freeze : marshallable:bool -> state
 val unfreeze : state -> unit
 
 (** {6 Rollback } *)
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
diff --git a/library/summary.mli b/library/summary.mli
index 36e265ddf..698034ad6 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -10,7 +10,9 @@
    in synchronization during the various backtracks of the system. *)
 
 type 'a summary_declaration = {
-  freeze_function : unit -> 'a;
+  (** freeze_function [true] is for marshalling to disk. 
+   *  e.g. lazy must be forced *)
+  freeze_function : bool -> 'a;
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
@@ -30,9 +32,10 @@ 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. *)
+    The [init_function] restores the reference to its initial value.
+    The [freeze_function] can be overridden *)
 
-val ref : name:string -> 'a -> 'a ref
+val ref : ?freeze:(bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref
 
 (** For global tables registered statically before the end of coqtop
     launch, the following empty [init_function] could be used. *)
@@ -44,7 +47,7 @@ val nop : unit -> unit
 
 type frozen
 
-val freeze_summaries : unit -> frozen
+val freeze_summaries : marshallable:bool -> frozen
 val unfreeze_summaries : frozen -> unit
 val init_summaries : unit -> unit