Future: ported to Ephemeron + exception enhancing

A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.

A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost.  This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).

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

8 files changed, 9 insertions, 75 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 4c2f22199..dbe83a856 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -126,7 +126,7 @@ let on_body f = function
   | Undef _ as x -> x
   | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs)))
   | OpaqueDef lc ->
-    OpaqueDef (Future.chain ~id:"Cooking.on_body" ~pure:true lc (fun lc ->
+    OpaqueDef (Future.chain lc (fun lc ->
         (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc)))))
 
 let constr_of_def = function
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 973859ede..3083c1738 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -52,8 +52,7 @@ let subst_const_type sub arity = match arity with
 let subst_const_def sub def = match def with
   | Undef _ -> def
   | Def c -> Def (subst_constr_subst sub c)
-  | OpaqueDef lc ->
-    OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
+  | OpaqueDef lc -> OpaqueDef (Future.chain lc (subst_lazy_constr sub))
 
 (* TODO : the native compiler seems to rely on a fresh (ref NotLinked)
    being created at each substitution. Quite ugly... For the moment,
@@ -100,7 +99,7 @@ let hcons_const_def = function
     Def (from_val (Term.hcons_constr constr))
   | OpaqueDef lc ->
     OpaqueDef
-      (Future.chain ~pure:true lc
+      (Future.chain lc
          (fun lc -> opaque_from_val (Term.hcons_constr (force_opaque lc))))
 
 let hcons_const_body cb =
@@ -242,17 +241,6 @@ 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
   | SEsubproof (c,_) -> Names.string_of_con c
   | SEscheme (cl,_) ->
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index f593b4547..177ae9d45 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -59,7 +59,6 @@ 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 76feb8498..6a0a952f7 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -592,7 +592,7 @@ let rec collect_mbid l sign =  match sign with
 let clean_bounded_mod_expr sign =
   if is_functor sign then collect_mbid MBIset.empty sign else sign
 
-(** {6 Stm machinery : join and prune } *)
+(** {6 Stm machinery } *)
 
 let rec join_module mb =
   implem_iter join_signature join_expression mb.mod_expr;
@@ -610,29 +610,3 @@ and join_structure struc = List.iter join_field struc
 and join_signature sign = functor_iter join_modtype join_structure sign
 and join_expression me = functor_iter join_modtype (fun _ -> ()) me
 
-let rec prune_module mb =
-  let me, mta, mt = mb.mod_expr, mb.mod_type_alg, mb.mod_type in
-  let mt' = prune_signature mt in
-  let me' = implem_smartmap prune_signature prune_expression me in
-  let mta' = Option.smartmap prune_expression mta 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_modtype mt =
-  let te, ta = mt.typ_expr, mt.typ_expr_alg in
-  let te' = prune_signature te in
-  let ta' = Option.smartmap prune_expression ta in
-  if te==te' && ta==ta' then mt else { mt with typ_expr=te'; typ_expr_alg=ta' }
-and prune_field (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 m in
-    if m == m' then orig else (l, SFBmodule m')
-  |SFBmodtype m ->
-    let m' = prune_modtype m in
-    if m == m' then orig else (l, SFBmodtype m')
-and prune_structure struc = List.smartmap prune_field struc
-and prune_signature sign = functor_smartmap prune_modtype prune_structure sign
-and prune_expression me = functor_smartmap prune_modtype (fun me -> me) me
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 6aed95988..11eb876ad 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -76,13 +76,11 @@ val subst_modtype_and_resolver : module_type_body -> module_path ->
 
 val clean_bounded_mod_expr : module_signature -> module_signature
 
-(** {6 Stm machinery : join and prune } *)
+(** {6 Stm machinery } *)
 
 val join_module : module_body -> unit
 val join_structure : structure_body -> unit
 
-val prune_structure : structure_body -> structure_body
-
 (** {6 Errors } *)
 
 type signature_mismatch_error =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 57e44a322..90d52572a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -197,28 +197,6 @@ let join_safe_environment e =
     (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 *)
-(* this is there to explore the opaque pre-env structure but is
- * not part of the trusted code base *)
-let prune_env env =
-  let open Pre_env in
-  let prune_ckey (cb,k) = Declareops.prune_constant_body cb, k in
-  let prune_globals glob =
-    { glob with env_constants = Cmap_env.map prune_ckey glob.env_constants }
-  in
-  let env = Environ.pre_env env in
-  Environ.env_of_pre_env {env with
-    env_globals = prune_globals env.env_globals;
-    env_named_vals = [];
-    env_rel_val = []}
-let prune_safe_environment e =
-  { e with
-    modvariant = (match e.modvariant with LIBRARY -> LIBRARY | _ -> NONE);
-    revstruct = Modops.prune_structure e.revstruct;
-    future_cst = [];
-    env = prune_env e.env }
-
-
 (** {6 Various checks } *)
 
 let exists_modlabel l senv = Label.Set.mem l senv.modlabels
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index a56bb8578..b16d5b63d 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -43,8 +43,6 @@ 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
 
 (** {6 Enriching a safe environment } *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 567511c93..987621619 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -84,9 +84,8 @@ let infer_declaration ?(what="UNKNOWN") env dcl =
   | DefinitionEntry c ->
       let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in
       if c.const_entry_opaque && not (Option.is_empty c.const_entry_type) then
-        let id = "infer_declaration " ^ what in
         let body_cst =
-          Future.chain ~id entry_body (fun (body, side_eff) ->
+          Future.chain entry_body (fun (body, side_eff) ->
             let body = handle_side_effects env body side_eff in
             let j, cst = infer env body in
             let j =
@@ -163,7 +162,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
-            OpaqueDef (Future.chain ~id:(string_of_con kn) lc (fun lc ->
+            OpaqueDef (Future.chain lc (fun lc ->
               let ids_typ = global_vars_set_constant_type env typ in
               let ids_def =
                 global_vars_set env (Lazyconstr.force_opaque lc) in
@@ -198,7 +197,7 @@ let translate_local_def env id centry =
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
 let handle_side_effects env ce = { ce with
-  const_entry_body = Future.chain ~id:"handle_side_effects" 
+  const_entry_body = Future.chain
     ce.const_entry_body (fun (body, side_eff) ->
-    handle_side_effects env body side_eff, Declareops.no_seff);
+       handle_side_effects env body side_eff, Declareops.no_seff);
 }