src/Pure/proofterm.ML
changeset 44331 aa9c1e9ef2ce
parent 44330 b28e091f683a
child 44332 e10f6b873f88
     1.1 --- a/src/Pure/proofterm.ML	Sat Aug 20 15:52:29 2011 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Sat Aug 20 16:06:27 2011 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  
     1.5    type oracle = string * term
     1.6    type pthm = serial * (string * term * proof_body future)
     1.7 -  val join_body: proof_body -> unit
     1.8 +  val check_body_thms: proof_body -> proof_body future
     1.9    val proof_of: proof_body -> proof
    1.10    val join_proof: proof_body future -> proof
    1.11    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
    1.12 @@ -171,8 +171,13 @@
    1.13  type oracle = string * term;
    1.14  type pthm = serial * (string * term * proof_body future);
    1.15  
    1.16 -fun join_thms thms = ignore (Future.joins (map (#3 o #2) thms));
    1.17 -fun join_body (PBody {thms, ...}) = join_thms thms;
    1.18 +fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
    1.19 +
    1.20 +fun check_body_thms (body as PBody {thms, ...}) =
    1.21 +  (singleton o Future.cond_forks)
    1.22 +    {name = "Proofterm.check_body_thms", group = NONE,
    1.23 +      deps = map (Future.task_of o #3 o #2) thms, pri = ~1, interrupts = true}
    1.24 +    (fn () => (join_thms thms; body));
    1.25  
    1.26  fun proof_of (PBody {proof, ...}) = proof;
    1.27  val join_proof = Future.join #> proof_of;
    1.28 @@ -1395,16 +1400,13 @@
    1.29        | fill _ = NONE;
    1.30      val (rules, procs) = get_data thy;
    1.31      val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
    1.32 -    val _ = join_thms thms;
    1.33    in PBody {oracles = oracles, thms = thms, proof = proof} end;
    1.34  
    1.35 -fun fulfill_proof_future _ [] postproc body =
    1.36 -      if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
    1.37 -      else Future.map postproc body
    1.38 +fun fulfill_proof_future _ [] postproc body = Future.map postproc body
    1.39    | fulfill_proof_future thy promises postproc body =
    1.40        (singleton o Future.forks)
    1.41          {name = "Proofterm.fulfill_proof_future", group = NONE,
    1.42 -          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
    1.43 +          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = ~1,
    1.44            interrupts = true}
    1.45          (fn () =>
    1.46            postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
    1.47 @@ -1459,14 +1461,19 @@
    1.48      fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    1.49      val body0 =
    1.50        if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
    1.51 -      else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
    1.52        else
    1.53 -        (singleton o Future.forks)
    1.54 +        (singleton o Future.cond_forks)
    1.55            {name = "Proofterm.prepare_thm_proof", group = NONE,
    1.56              deps = [], pri = ~1, interrupts = true}
    1.57            (make_body0 o full_proof0);
    1.58  
    1.59 -    fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    1.60 +    fun new_prf () =
    1.61 +      let
    1.62 +        val body' = body0
    1.63 +          |> fulfill_proof_future thy promises postproc
    1.64 +          |> Future.map (fn body as PBody {thms, ...} => (join_thms thms; body));
    1.65 +      in (serial (), body') end;
    1.66 +
    1.67      val (i, body') =
    1.68        (*non-deterministic, depends on unknown promises*)
    1.69        (case strip_combt (fst (strip_combP prf)) of