stm: (initial) support for -coq-slaves

Stm contains many TODO items to improve the thing, but it should
be already possible to play with it (but not use it in production).

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

2 files changed, 27 insertions, 20 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 1f5ee7f756..58eb2e21d8 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -264,30 +264,36 @@ type closed_proof =
   (Entries.definition_entry list * lemma_possible_guards *
     Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
 
-let close_proof ~now ?(fix_exn = fun x -> x) ps side_eff =
-  let { pid; section_vars; compute_guard; strength; hook; proof } = ps in
-  let entries = List.map (fun (c, t) -> { Entries.
-    const_entry_body = Future.chain side_eff (fun () ->
-      try Proof.return (cur_pstate ()).proof c with
-      | Proof.UnfinishedProof ->
-          raise (fix_exn(Errors.UserError("last tactic before Qed",
-            str"Attempt to save an incomplete proof")))
-      | Proof.HasUnresolvedEvar ->
-          raise (fix_exn(Errors.UserError("last tactic before Qed",
-            str"Attempt to save a proof with existential " ++
-            str"variables still non-instantiated"))));
+let close_proof ~now fpl =
+  let { pid;section_vars;compute_guard;strength;hook;proof } = cur_pstate () in
+  let initial_goals = Proof.initial_goals proof in
+  let entries = Future.map2 (fun p (c, t) -> { Entries.
+    const_entry_body = p;
     const_entry_secctx = section_vars;
     const_entry_type  = Some t;
     const_entry_inline_code = false;
-    const_entry_opaque = true }) (Proof.initial_goals proof) in
+    const_entry_opaque = true }) fpl initial_goals in
   if now then
     List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries;
   (pid, (entries, compute_guard, strength, hook))
 
-let close_future_proof ~fix_exn proof =
-  close_proof ~now:false ~fix_exn (cur_pstate ()) proof
+let return_proof ~fix_exn =
+  let { proof } = cur_pstate () in
+  let initial_goals = Proof.initial_goals proof in
+  List.map (fun (c, _) ->
+   try Proof.return proof c with
+   | Proof.UnfinishedProof ->
+       raise (fix_exn(Errors.UserError("last tactic before Qed",
+         str"Attempt to save an incomplete proof")))
+   | Proof.HasUnresolvedEvar ->
+       raise (fix_exn(Errors.UserError("last tactic before Qed",
+         str"Attempt to save a proof with existential " ++
+         str"variables still non-instantiated"))))
+   initial_goals
+
+let close_future_proof proof = close_proof ~now:false proof
 let close_proof () =
-  close_proof ~now:true (cur_pstate ()) (Future.from_val())
+  close_proof ~now:true (Future.from_val (return_proof ~fix_exn:(fun x -> x)))
 
 (**********************************************************)
 (*                                                        *)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 4462255dd8..5922075ec7 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -66,11 +66,12 @@ type closed_proof =
 
 val close_proof : unit -> closed_proof
 
-(* A future proof may be executed later on, out of the control of Stm
-   that knows which state was (for example) supposed to close the proof
-   bit did not. Hence fix_exn to enrich it *)
+(* Intermediate step necessary to delegate the future.
+ * Both access the current proof state. The formes is supposed to be
+ * chained with a computation that completed the proof *)
+val return_proof : fix_exn:(exn -> exn) -> Entries.proof_output list
 val close_future_proof :
-  fix_exn:(exn -> exn) -> unit Future.computation -> closed_proof
+  Entries.proof_output list Future.computation -> closed_proof
 
 exception NoSuchProof