future proofs: pass actual futures to facilitate composite computations;
authorwenzelm
Thu Dec 04 23:02:56 2008 +0100 (2008-12-04)
changeset 28978f3e37d78b4f7
parent 28977 08990d02211f
child 28979 3ce619d8d432
future proofs: pass actual futures to facilitate composite computations;
removed join_futures -- superceded by higher-level PureThy.force_proofs;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Thu Dec 04 23:02:52 2008 +0100
     1.2 +++ b/src/Pure/thm.ML	Thu Dec 04 23:02:56 2008 +0100
     1.3 @@ -146,8 +146,7 @@
     1.4    val varifyT: thm -> thm
     1.5    val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
     1.6    val freezeT: thm -> thm
     1.7 -  val join_futures: theory -> unit
     1.8 -  val future: (unit -> thm) -> cterm -> thm
     1.9 +  val future: thm future -> cterm -> thm
    1.10    val proof_body_of: thm -> proof_body
    1.11    val proof_of: thm -> proof
    1.12    val force_proof: thm -> unit
    1.13 @@ -347,8 +346,8 @@
    1.14    tpairs: (term * term) list,                   (*flex-flex pairs*)
    1.15    prop: term}                                   (*conclusion*)
    1.16  and deriv = Deriv of
    1.17 - {all_promises: (serial * thm Future.T) OrdList.T,
    1.18 -  promises: (serial * thm Future.T) OrdList.T,
    1.19 + {all_promises: (serial * thm future) OrdList.T,
    1.20 +  promises: (serial * thm future) OrdList.T,
    1.21    body: Pt.proof_body};
    1.22  
    1.23  type conv = cterm -> thm;
    1.24 @@ -1587,36 +1586,7 @@
    1.25  
    1.26  
    1.27  
    1.28 -(*** Promises ***)
    1.29 -
    1.30 -(* pending future derivations *)
    1.31 -
    1.32 -structure Futures = TheoryDataFun
    1.33 -(
    1.34 -  type T = thm Future.T list ref;
    1.35 -  val empty : T = ref [];
    1.36 -  val copy = I;  (*shared ref within all versions of whole theory body*)
    1.37 -  fun extend _ : T = ref [];
    1.38 -  fun merge _ _ : T = ref [];
    1.39 -);
    1.40 -
    1.41 -val _ = Context.>> (Context.map_theory Futures.init);
    1.42 -
    1.43 -fun add_future thy future = CRITICAL (fn () => change (Futures.get thy) (cons future));
    1.44 -
    1.45 -fun join_futures thy =
    1.46 -  let
    1.47 -    val futures = Futures.get thy;
    1.48 -    fun joined () =
    1.49 -     (List.app (ignore o Future.join_result) (rev (! futures));
    1.50 -      CRITICAL (fn () =>
    1.51 -        let
    1.52 -          val (finished, unfinished) = List.partition Future.is_finished (! futures);
    1.53 -          val _ = futures := unfinished;
    1.54 -        in finished end)
    1.55 -      |> Future.join_results |> Exn.release_all |> null);
    1.56 -  in while not (joined ()) do () end;
    1.57 -
    1.58 +(*** Future theorems -- proofs with promises ***)
    1.59  
    1.60  (* future rule *)
    1.61  
    1.62 @@ -1635,15 +1605,14 @@
    1.63      val _ = forall (fn (j, _) => j < i) all_promises orelse err "bad dependencies";
    1.64    in thm end;
    1.65  
    1.66 -fun future make_result ct =
    1.67 +fun future future_thm ct =
    1.68    let
    1.69      val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
    1.70      val thy = Context.reject_draft (Theory.deref thy_ref);
    1.71      val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
    1.72  
    1.73      val i = serial ();
    1.74 -    val future = Future.fork_background (future_result i thy sorts prop o norm_proof o make_result);
    1.75 -    val _ = add_future thy future;
    1.76 +    val future = future_thm |> Future.map (future_result i thy sorts prop o norm_proof);
    1.77      val promise = (i, future);
    1.78    in
    1.79      Thm (make_deriv [promise] [promise] [] [] (Pt.promise_proof thy i prop),