enhance marshallable option for freeze (minor TODO in safe_typing)

It can be:
`Yes      Full data, in a state that can be marshalled
`No       Full data, good for Undo only
`Shallow  Partial data, marshallable, good for slave processes

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

22 files changed, 142 insertions, 35 deletions

diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 822c3ea70..7bb62112c 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -36,5 +36,5 @@ val get_transp_state : unit -> transparent_state
 (****************************
    Summary operations *)
 type oracle
-val freeze   : bool -> oracle
+val freeze   : [ `Yes | `No | `Shallow ] -> oracle
 val unfreeze : oracle -> unit
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index e597ea9a9..b0f320942 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -211,6 +211,17 @@ let join_constant_body cb =
   | OpaqueDef d -> ignore(Future.join d)
   | _ -> ()
 
+let prune_constant_body cb =
+  let cst, cbo = cb.const_constraints, cb.const_body in
+  let cst' = Future.drop cst in
+  let cbo' = match cbo with
+    | OpaqueDef d ->
+        let d' = Future.drop d in
+        if d' == d then cbo else OpaqueDef d'
+    | _ -> cbo in
+  if cst' == cst && cbo' == cbo then cb
+  else {cb with const_constraints = cst'; const_body = cbo'}
+
 let string_of_side_effect = function
   | NewConstant (c,_) -> Names.string_of_con c
 type side_effects = side_effect list
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 635b8c47a..0da7c85c7 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -59,6 +59,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
 
 val join_constant_body : constant_body -> unit
+val prune_constant_body : constant_body -> constant_body
 
 (** {6 Hash-consing} *)
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 39e5514c9..5f79c5363 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -617,3 +617,55 @@ and join_struct_expr_body = function
        match wdcl with
        | With_module_body _ -> ()
        | With_definition_body (_, sb) -> join_constant_body sb
+
+let rec prune_module_body mb =
+  let me, mta, mt = mb.mod_expr, mb.mod_type_alg, mb.mod_type in
+  let me' = Option.smartmap prune_struct_expr_body me in
+  let mta' = Option.smartmap prune_struct_expr_body mta in
+  let mt' = prune_struct_expr_body mt in
+  if me' == me && mta' == mta && mt' == mt then mb
+  else {mb with mod_expr = me'; mod_type_alg = mta'; mod_type = mt'}
+and prune_structure_body struc =
+  let prune_body (l,body as orig) = match body with
+    | SFBconst sb ->
+        let sb' = prune_constant_body sb in
+        if sb == sb' then orig else (l, SFBconst sb')
+    | SFBmind _ -> orig
+    | SFBmodule m ->
+        let m' = prune_module_body m in
+        if m == m' then orig else (l, SFBmodule m')
+    | SFBmodtype m ->
+        let te, te_alg = m.typ_expr, m.typ_expr_alg in
+        let te' = prune_struct_expr_body te in
+        let te_alg' =
+          Option.smartmap prune_struct_expr_body te_alg in
+        if te' == te && te_alg' == te_alg then orig
+        else (l, SFBmodtype {m with typ_expr = te'; typ_expr_alg = te_alg'}) in
+  CList.smartmap prune_body struc
+and prune_struct_expr_body orig = match orig with
+  | SEBfunctor (id,t,e) ->
+      let te, ta = t.typ_expr, t.typ_expr_alg in
+      let te' = prune_struct_expr_body te in
+      let ta' = Option.smartmap prune_struct_expr_body ta in
+      let e' = prune_struct_expr_body e in
+      if te' == te && ta' == ta && e' == e then orig
+      else SEBfunctor(id, {t with typ_expr = te'; typ_expr_alg = ta'}, e')
+  | SEBident _ -> orig
+  | SEBstruct s ->
+      let s' = prune_structure_body s in
+      if s' == s then orig else SEBstruct s'
+  | SEBapply (mexpr,marg,u) ->
+      let mexpr' = prune_struct_expr_body mexpr in
+      let marg' = prune_struct_expr_body marg in
+      if mexpr' == mexpr && marg' == marg then orig
+      else SEBapply (mexpr', marg', u)
+  | SEBwith (seb,wdcl) ->
+      let seb' = prune_struct_expr_body seb in
+      let wdcl' = match wdcl with
+        | With_module_body _ -> wdcl
+        | With_definition_body (id, sb) ->
+            let sb' = prune_constant_body sb in
+            if sb' == sb then wdcl else With_definition_body (id, sb') in
+      if seb' == seb && wdcl' == wdcl then orig
+      else SEBwith (seb', wdcl')
+       
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 30f9274d2..c0943233b 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -54,6 +54,8 @@ val join_module_body : module_body -> unit
 val join_structure_body : structure_body -> unit
 val join_struct_expr_body : struct_expr_body -> unit
 
+val prune_structure_body : structure_body -> structure_body
+
 (** Errors *)
 
 type signature_mismatch_error =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 13368aab9..eb5c01692 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -132,12 +132,27 @@ let add_constraints cst senv =
 let is_curmod_library senv = 
   match senv.modinfo.variant with LIBRARY _ -> true | _ -> false
 
-let rec join_safe_environment e =
+let join_safe_environment e =
   join_structure_body e.revstruct;
   List.fold_left 
     (fun e fc -> add_constraints (Now (Future.join fc)) e)
     {e with future_cst = []} e.future_cst
 
+(* TODO : out of place and maybe incomplete w.r.t. modules *)
+let prune_env env =
+  let env = Environ.pre_env env in
+  let prune_ckey (cb,k) = Declareops.prune_constant_body cb, k in
+  let prune_globals glob =
+    {glob with Pre_env.env_constants =
+       Cmap_env.map prune_ckey glob.Pre_env.env_constants } in
+  Environ.env_of_pre_env
+    {env with Pre_env.env_globals = prune_globals env.Pre_env.env_globals}
+let prune_safe_environment e =
+  let e = {e with revstruct = prune_structure_body e.revstruct;
+                  future_cst = [];
+                  env = prune_env e.env} in
+  {e with old = e}
+
 let check_modlabel l senv =
   if exists_modlabel l senv then error_existing_label l
 let check_objlabel l senv =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 210d601fb..e9716930b 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -34,6 +34,8 @@ val is_curmod_library : safe_environment -> bool
 (* safe_environment has functional data affected by lazy computations,
  * thus this function returns a new safe_environment *)
 val join_safe_environment : safe_environment -> safe_environment
+(* future computations are just dropped by this function *)
+val prune_safe_environment : safe_environment -> safe_environment
 
 val empty_environment : safe_environment
 val is_empty : safe_environment -> bool
diff --git a/library/declaremods.ml b/library/declaremods.ml
index c8f9d6161..0dfee9787 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -822,7 +822,7 @@ end
 (** {6 Module operations handling summary freeze/unfreeze *)
 
 let protect_summaries f =
-  let fs = Summary.freeze_summaries ~marshallable:false in
+  let fs = Summary.freeze_summaries ~marshallable:`No in
   try f fs
   with reraise ->
     (* Something wrong: undo the whole process *)
diff --git a/library/global.ml b/library/global.ml
index a0528a624..22b69e4f2 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -27,10 +27,15 @@ let global_env = ref empty_environment
 let join_safe_environment () =
   global_env := Safe_typing.join_safe_environment !global_env
 
+let prune_safe_environment env = Safe_typing.prune_safe_environment env
+(* XXX TODO pass args so that these functions can stop at the current
+ * file boundaries *)
 let () =
   Summary.declare_summary "Global environment"
-    { Summary.freeze_function = (fun b ->
-        if b then join_safe_environment (); !global_env);
+    { Summary.freeze_function = (function
+        | `Yes -> join_safe_environment (); !global_env
+        | `No -> !global_env
+        | `Shallow -> prune_safe_environment !global_env);
       unfreeze_function = (fun fr -> global_env := fr);
       init_function = (fun () -> global_env := empty_environment) }
 
diff --git a/library/lib.ml b/library/lib.ml
index b4371812b..379d0e8ad 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -250,7 +250,7 @@ let add_anonymous_leaf obj =
 
 let add_frozen_state () =
   add_anonymous_entry
-    (FrozenState (Summary.freeze_summaries ~marshallable:false))
+    (FrozenState (Summary.freeze_summaries ~marshallable:`No))
 
 (* Modules. *)
 
@@ -485,7 +485,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 ~marshallable:false in
+  let fs = Summary.freeze_summaries ~marshallable:`No 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);
@@ -529,7 +529,9 @@ let close_section () =
 
 type frozen = Names.DirPath.t option * library_segment
 
-let freeze ~marshallable:_ = (!comp_name, !lib_stk)
+let freeze ~marshallable =
+  if marshallable = `Shallow then !comp_name, []
+  else !comp_name, !lib_stk
 
 let unfreeze (mn,stk) =
   comp_name := mn;
diff --git a/library/lib.mli b/library/lib.mli
index 04f8d0775..1362fabf8 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -151,7 +151,7 @@ val close_section : unit -> unit
 
 type frozen
 
-val freeze : marshallable:bool -> frozen
+val freeze : marshallable:Summary.marshallable -> frozen
 val unfreeze : frozen -> unit
 
 val init : unit -> unit
diff --git a/library/library.ml b/library/library.ml
index 0766a62d7..472b1fb1d 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -44,20 +44,17 @@ module LibraryOrdered = DirPath
 module LibraryMap = Map.Make(LibraryOrdered)
 module LibraryFilenameMap = Map.Make(LibraryOrdered)
 
-let join x = Safe_typing.join_compiled_library x.library_compiled
 (* This is a map from names to loaded libraries *)
-let freeze b l = if b then (LibraryMap.iter (fun _ x -> join x) l; l) else l
-let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" ~freeze
+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 freeze b l = if b then (List.iter join l; l) else l
-let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" ~freeze
-let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" ~freeze
-let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" ~freeze
+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/states.ml b/library/states.ml
index 93b2c120e..a06e7ce80 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -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 ~marshallable:true)),
+    raw_extern s (freeze ~marshallable:`Yes)),
   (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_state_protection f x =
-  let st = freeze ~marshallable:false in
+  let st = freeze ~marshallable:`No in
   try
     let a = f x in unfreeze st; a
   with reraise ->
diff --git a/library/states.mli b/library/states.mli
index da6f33d65..0babae6af 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 : marshallable:bool -> state
+val freeze : marshallable:Summary.marshallable -> state
 val unfreeze : state -> unit
 
 (** {6 Rollback } *)
diff --git a/library/summary.ml b/library/summary.ml
index 53e9f7002..b46ce85b1 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -10,8 +10,9 @@ open Pp
 open Errors
 open Util
 
+type marshallable = [ `Yes | `No | `Shallow ]
 type 'a summary_declaration = {
-  freeze_function : bool -> 'a;
+  freeze_function : marshallable -> 'a;
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
@@ -48,7 +49,7 @@ let freeze_summaries ~marshallable =
   Hashtbl.iter
     (fun id decl -> 
        (* to debug missing Lazy.force 
-       if marshallable then begin
+       if marshallable <> `No then begin
          prerr_endline ("begin marshalling " ^ id);
          ignore(Marshal.to_string (decl.freeze_function marshallable) []);
          prerr_endline ("end marshalling " ^ id);
diff --git a/library/summary.mli b/library/summary.mli
index 698034ad6..38d5fc7e8 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -9,10 +9,15 @@
 (** This module registers the declaration of global tables, which will be kept
    in synchronization during the various backtracks of the system. *)
 
+type marshallable =
+  [ `Yes       (* Full data will be marshalled to disk                        *)
+  | `No        (* Full data will be store in memory, e.g. for Undo            *)
+  | `Shallow ] (* Only part of the data will be marshalled to a slave process *)
+
 type 'a summary_declaration = {
   (** freeze_function [true] is for marshalling to disk. 
    *  e.g. lazy must be forced *)
-  freeze_function : bool -> 'a;
+  freeze_function : marshallable -> 'a;
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
@@ -35,7 +40,7 @@ val declare_summary : string -> 'a summary_declaration -> unit
     The [init_function] restores the reference to its initial value.
     The [freeze_function] can be overridden *)
 
-val ref : ?freeze:(bool -> 'a -> 'a) -> name:string -> 'a -> 'a ref
+val ref : ?freeze:(marshallable -> '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. *)
@@ -47,7 +52,7 @@ val nop : unit -> unit
 
 type frozen
 
-val freeze_summaries : marshallable:bool -> frozen
+val freeze_summaries : marshallable:marshallable -> frozen
 val unfreeze_summaries : frozen -> unit
 val init_summaries : unit -> unit
 
@@ -55,5 +60,5 @@ val init_summaries : unit -> unit
 type frozen_bits
 
 val freeze_summary :
-  marshallable:bool -> ?complement:bool -> string list -> frozen_bits
+  marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits
 val unfreeze_summary : frozen_bits -> unit
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 0c0aac715..470d19b71 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -391,6 +391,13 @@ module V82 = struct
 end
 
 type state = pstate list
-let freeze () = !pstates
+let drop_hook_mode p = { p with hook = None; mode = None }
+        
+let freeze ~marshallable =
+  match marshallable with
+  | `Yes ->
+      Errors.anomaly (Pp.str"full marshalling of proof state not supported")
+  | `Shallow -> List.map drop_hook_mode !pstates
+  | `No -> !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index a5fe33992..61bb5c0dd 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -140,5 +140,5 @@ module V82 : sig
 end
 
 type state
-val freeze : unit -> state
+val freeze : marshallable:[`Yes | `No | `Shallow] -> state
 val unfreeze : state -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1dba38001..394cce6ce 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -128,7 +128,7 @@ let compile_files () =
     | [] -> ()
     | [vf] -> compile_file vf (* One compilation : no need to save init state *)
     | l ->
-      let init_state = States.freeze ~marshallable:false in
+      let init_state = States.freeze ~marshallable:`No in
       let coqdoc_init_state = Lexer.location_table () in
       List.iter
         (fun vf ->
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 46037bcbc..e9fd0620d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1075,7 +1075,7 @@ let inNotation : notation_obj -> obj =
 (**********************************************************************)
 
 let with_lib_stk_protection f x =
-  let fs = Lib.freeze false in
+  let fs = Lib.freeze `No in
   try let a = f x in Lib.unfreeze fs; a
   with reraise ->
     let reraise = Errors.push reraise in
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 218929f23..d9d63d796 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -382,7 +382,7 @@ end = struct (* {{{ *)
   (* hack to make futures functional *)
   let in_t, out_t = Dyn.create "state4future"
   let () = Future.set_freeze
-    (fun () -> in_t (freeze_global_state (), !cur_id))
+    (fun () -> in_t (freeze_global_state `No, !cur_id))
     (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
 
   let is_cached id =
@@ -407,14 +407,21 @@ end = struct (* {{{ *)
     Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg));
     Stateid.add_state_id e ?valid id
 
-  let define ?(cache=false) f id =
+  let string_of_cache = function
+    | `Yes -> "Yes" | `No -> "No" | `Marshallable -> "Marshallable"
+  let marshallable_of_cache = function
+    | `Yes -> `No
+    | `No -> assert false
+    | `Marshallable -> `Shallow
+
+  let define ?(cache=`No) f id =
     if is_cached id then
       anomaly (str"defining state "++str(string_of_state_id id)++str" twice");
     try
       prerr_endline ("defining " ^
         string_of_state_id id ^ " (cache=" ^ string_of_bool cache ^ ")");
       f ();
-      if cache then freeze id;
+      if cache <> `No then freeze (marshallable_of_cache cache) id;
       cur_id := id;
       feedback ~state_id:id Interface.Processed;
       VCS.reached id true;
@@ -466,8 +473,8 @@ let known_state ~cache id =
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
   let cherry_pick_non_pstate () =
-    Summary.freeze_summary ~marshallable:false ~complement:true pstate,
-    Lib.freeze ~marshallable:false in
+    Summary.freeze_summary ~marshallable:`No ~complement:true pstate,
+    Lib.freeze ~marshallable:`No in
   let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in
 
   let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 88802fc34..888c3411d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -188,7 +188,7 @@ let set_formatter_translator() =
 let pr_new_syntax loc ocom =
   let loc = Loc.unloc loc in
   if !beautify_file then set_formatter_translator();
-  let fs = States.freeze ~marshallable:false in
+  let fs = States.freeze ~marshallable:`No in
   let com = match ocom with
     | Some VernacNop -> mt()
     | Some com -> Ppvernac.pr_vernac com