# HG changeset patch
# User wenzelm
# Date 1313849187 -7200
# Node ID aa9c1e9ef2cec8a532c7f57edbe2bb68b4a740e9
# Parent  b28e091f683aed46a93441b4381d72e73ac8ca64
clarified fulfill_norm_proof: no join_thms yet;
clarified priority of fulfill_proof_future, which is followed by explicit join_thms;
explicit Thm.future_body_of without join yet;
tuned Thm.future_result: join_promises without fulfill_norm_proof;

diff -r b28e091f683a -r aa9c1e9ef2ce src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Sat Aug 20 15:52:29 2011 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat Aug 20 16:06:27 2011 +0200
@@ -40,7 +40,7 @@
                path = "",
                parents = parents};
           in cons entry end;
-    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
+    val deps = Proofterm.fold_body_thms add_dep (Future.joins (map Thm.future_body_of thms)) [];
   in Present.display_graph (sort_wrt #ID deps) end;
 
 
@@ -66,7 +66,8 @@
     val used =
       Proofterm.fold_body_thms
         (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
-        (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) new_thms) Symtab.empty;
+        (map Proofterm.strip_thm (Future.joins (map (Thm.future_body_of o #1 o #2) new_thms)))
+        Symtab.empty;
 
     fun is_unused a = not (Symtab.defined used a);
 
diff -r b28e091f683a -r aa9c1e9ef2ce src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Aug 20 15:52:29 2011 +0200
+++ b/src/Pure/proofterm.ML	Sat Aug 20 16:06:27 2011 +0200
@@ -37,7 +37,7 @@
 
   type oracle = string * term
   type pthm = serial * (string * term * proof_body future)
-  val join_body: proof_body -> unit
+  val check_body_thms: proof_body -> proof_body future
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
@@ -171,8 +171,13 @@
 type oracle = string * term;
 type pthm = serial * (string * term * proof_body future);
 
-fun join_thms thms = ignore (Future.joins (map (#3 o #2) thms));
-fun join_body (PBody {thms, ...}) = join_thms thms;
+fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
+
+fun check_body_thms (body as PBody {thms, ...}) =
+  (singleton o Future.cond_forks)
+    {name = "Proofterm.check_body_thms", group = NONE,
+      deps = map (Future.task_of o #3 o #2) thms, pri = ~1, interrupts = true}
+    (fn () => (join_thms thms; body));
 
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
@@ -1395,16 +1400,13 @@
       | fill _ = NONE;
     val (rules, procs) = get_data thy;
     val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
-    val _ = join_thms thms;
   in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
-fun fulfill_proof_future _ [] postproc body =
-      if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
-      else Future.map postproc body
+fun fulfill_proof_future _ [] postproc body = Future.map postproc body
   | fulfill_proof_future thy promises postproc body =
       (singleton o Future.forks)
         {name = "Proofterm.fulfill_proof_future", group = NONE,
-          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
+          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = ~1,
           interrupts = true}
         (fn () =>
           postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
@@ -1459,14 +1461,19 @@
     fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
     val body0 =
       if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
-      else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
       else
-        (singleton o Future.forks)
+        (singleton o Future.cond_forks)
           {name = "Proofterm.prepare_thm_proof", group = NONE,
             deps = [], pri = ~1, interrupts = true}
           (make_body0 o full_proof0);
 
-    fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
+    fun new_prf () =
+      let
+        val body' = body0
+          |> fulfill_proof_future thy promises postproc
+          |> Future.map (fn body as PBody {thms, ...} => (join_thms thms; body));
+      in (serial (), body') end;
+
     val (i, body') =
       (*non-deterministic, depends on unknown promises*)
       (case strip_combt (fst (strip_combP prf)) of
diff -r b28e091f683a -r aa9c1e9ef2ce src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Aug 20 15:52:29 2011 +0200
+++ b/src/Pure/thm.ML	Sat Aug 20 16:06:27 2011 +0200
@@ -95,9 +95,10 @@
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
   val extra_shyps: thm -> sort list
-  val join_proofs: thm list -> unit
+  val future_body_of: thm -> proof_body future
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
+  val join_proofs: thm list -> unit
   val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
   val derivation_name: thm -> string
@@ -510,17 +511,23 @@
 
 (* fulfilled proofs *)
 
-fun raw_body (Thm (Deriv {body, ...}, _)) = body;
+fun raw_body_of (Thm (Deriv {body, ...}, _)) = body;
+fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises;
+
+fun join_promises [] = ()
+  | join_promises promises = join_promises_of (Future.joins (map snd promises))
+and join_promises_of thms = join_promises (maps raw_promises_of thms);
 
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
-  Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
-    (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
-and fulfill_bodies futures = map fulfill_body (Future.joins futures);
+  Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body
+and fulfill_promises promises =
+  map fst promises ~~ map fulfill_body (Future.joins (map snd promises));
 
-fun join_proofs thms = ignore (map fulfill_body thms);
+val future_body_of = Proofterm.check_body_thms o fulfill_body;
+val proof_body_of = Future.join o future_body_of;
+val proof_of = Proofterm.proof_of o proof_body_of;
 
-fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
-val proof_of = Proofterm.proof_of o proof_body_of;
+fun join_proofs thms = (join_promises_of thms; Future.joins (map future_body_of thms); ());
 
 
 (* derivation status *)
@@ -529,7 +536,7 @@
   let
     val ps = map (Future.peek o snd) promises;
     val bodies = body ::
-      map_filter (fn SOME (Exn.Res th) => SOME (raw_body th) | _ => NONE) ps;
+      map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
     val {oracle, unfinished, failed} = Proofterm.status_of bodies;
   in
    {oracle = oracle,
@@ -552,7 +559,7 @@
     val _ = null hyps orelse err "bad hyps";
     val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
     val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
-    val _ = fulfill_bodies (map #2 promises);
+    val _ = join_promises promises;
   in thm end;
 
 fun future future_thm ct =