From 80aba8d52c650ef8e4ada694c20bf12c15849694 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 8 Aug 2013 18:52:47 +0000
Subject: 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
---
 kernel/conv_oracle.mli |  2 +-
 kernel/declareops.ml   | 11 +++++++++++
 kernel/declareops.mli  |  1 +
 kernel/modops.ml       | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++
 kernel/modops.mli      |  2 ++
 kernel/safe_typing.ml  | 17 ++++++++++++++++-
 kernel/safe_typing.mli |  2 ++
 7 files changed, 85 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 822c3ea708..7bb62112c6 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 e597ea9a91..b0f320942e 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 635b8c47a3..0da7c85c74 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 39e5514c97..5f79c53637 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 30f9274d2f..c0943233b9 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 13368aab97..eb5c016922 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 210d601fbe..e9716930b8 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
-- 
cgit v1.2.3