renamed promise to future, tuned related interfaces;
authorwenzelm
Wed Oct 01 12:18:18 2008 +0200 (2008-10-01)
changeset 28446a01de3b3fa2e
parent 28445 526b8adcd117
child 28447 df77ed974a78
renamed promise to future, tuned related interfaces;
src/Pure/Isar/proof.ML
src/Pure/Isar/skip_proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/goal.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Oct 01 12:00:05 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Oct 01 12:18:18 2008 +0200
     1.3 @@ -114,8 +114,8 @@
     1.4      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
     1.5    val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     1.6      ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
     1.7 -  val can_promise: state -> bool
     1.8 -  val promise_proof: (state -> context) -> state -> context
     1.9 +  val can_defer: state -> bool
    1.10 +  val future_proof: (state -> context) -> state -> context
    1.11  end;
    1.12  
    1.13  structure Proof: PROOF =
    1.14 @@ -976,22 +976,22 @@
    1.15  end;
    1.16  
    1.17  
    1.18 -(* promise global proofs *)
    1.19 +(* defer global proofs *)
    1.20  
    1.21  fun is_initial state =
    1.22    (case try find_goal state of
    1.23      NONE => false
    1.24    | SOME (_, (_, {statement = (_, _, prop), goal, ...})) => Thm.eq_thm_prop (Goal.init prop, goal));
    1.25  
    1.26 -fun can_promise state =
    1.27 +fun can_defer state =
    1.28    can (assert_bottom true) state andalso
    1.29    can assert_backward state andalso
    1.30    is_initial state andalso
    1.31    not (schematic_goal state);
    1.32  
    1.33 -fun promise_proof make_proof state =
    1.34 +fun future_proof make_proof state =
    1.35    let
    1.36 -    val _ = can_promise state orelse error "Cannot promise proof";
    1.37 +    val _ = can_defer state orelse error "Cannot defer proof";
    1.38  
    1.39      val (goal_ctxt, (_, goal)) = find_goal state;
    1.40      val {statement as (kind, propss, cprop), messages, using, goal, before_qed, after_qed} = goal;
    1.41 @@ -1005,7 +1005,7 @@
    1.42        |> map_goal I (K (statement', messages, using, goal, before_qed, (#1 after_qed, after_qed')))
    1.43        |> make_proof
    1.44        |> (fn result_ctxt => ProofContext.get_fact_single result_ctxt (Facts.named this_name));
    1.45 -    val finished_goal = Goal.protect (Goal.promise_result goal_ctxt make_result prop);
    1.46 +    val finished_goal = Goal.protect (Goal.future_result goal_ctxt make_result prop);
    1.47    in
    1.48      state
    1.49      |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
     2.1 --- a/src/Pure/Isar/skip_proof.ML	Wed Oct 01 12:00:05 2008 +0200
     2.2 +++ b/src/Pure/Isar/skip_proof.ML	Wed Oct 01 12:18:18 2008 +0200
     2.3 @@ -36,7 +36,7 @@
     2.4    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
     2.5  
     2.6  fun prove ctxt xs asms prop tac =
     2.7 -  (if ! future_scheduler then Goal.prove_promise else Goal.prove) ctxt xs asms prop
     2.8 +  (if ! future_scheduler then Goal.prove_future else Goal.prove) ctxt xs asms prop
     2.9      (fn args => fn st =>
    2.10        if ! quick_and_dirty
    2.11        then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
     3.1 --- a/src/Pure/Isar/toplevel.ML	Wed Oct 01 12:00:05 2008 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Oct 01 12:18:18 2008 +0200
     3.3 @@ -694,10 +694,10 @@
     3.4    let val st' = command tr st
     3.5    in (st', st') end;
     3.6  
     3.7 -fun unit_result do_promise (tr, proof_trs) st =
     3.8 +fun unit_result immediate (tr, proof_trs) st =
     3.9    let val st' = command tr st in
    3.10 -    if do_promise andalso not (null proof_trs) andalso
    3.11 -      can proof_of st' andalso Proof.can_promise (proof_of st')
    3.12 +    if not immediate andalso not (null proof_trs) andalso
    3.13 +      can proof_of st' andalso Proof.can_defer (proof_of st')
    3.14      then
    3.15        let
    3.16          val (body_trs, end_tr) = split_last proof_trs;
    3.17 @@ -708,9 +708,9 @@
    3.18                => State (SOME (Proof (ProofNode.init prf, (Context.Proof, orig_gthy)), exit), prev))
    3.19              |> fold_map command_result body_trs ||> command end_tr
    3.20            in body_states := states; context_of result_state end;
    3.21 -        val proof_promise =
    3.22 -          end_tr |> reset_trans |> end_proof (K (Proof.promise_proof make_result));
    3.23 -        val st'' = command proof_promise st';
    3.24 +        val proof_future =
    3.25 +          end_tr |> reset_trans |> end_proof (K (Proof.future_proof make_result));
    3.26 +        val st'' = command proof_future st';
    3.27        in (fn () => (tr, st') :: (body_trs ~~ ! body_states) @ [(end_tr, st'')], st'') end
    3.28      else
    3.29        let val (states, st'') = fold_map command_result proof_trs st'
    3.30 @@ -721,8 +721,8 @@
    3.31    let
    3.32      val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
    3.33  
    3.34 -    val do_promise = ! future_scheduler andalso Multithreading.max_threads_value () > 1;
    3.35 -    val (future_results, end_state) = fold_map (unit_result do_promise) input toplevel;
    3.36 +    val immediate = not (! future_scheduler) orelse Multithreading.max_threads_value () <= 1;
    3.37 +    val (future_results, end_state) = fold_map (unit_result immediate) input toplevel;
    3.38      val _ =
    3.39        (case end_state of
    3.40          State (NONE, SOME (Theory (Context.Theory thy, _), _)) => Thm.join_futures thy
     4.1 --- a/src/Pure/goal.ML	Wed Oct 01 12:00:05 2008 +0200
     4.2 +++ b/src/Pure/goal.ML	Wed Oct 01 12:18:18 2008 +0200
     4.3 @@ -20,11 +20,11 @@
     4.4    val conclude: thm -> thm
     4.5    val finish: thm -> thm
     4.6    val norm_result: thm -> thm
     4.7 -  val promise_result: Proof.context -> (unit -> thm) -> term -> thm
     4.8 +  val future_result: Proof.context -> (unit -> thm) -> term -> thm
     4.9    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    4.10    val prove_multi: Proof.context -> string list -> term list -> term list ->
    4.11      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
    4.12 -  val prove_promise: Proof.context -> string list -> term list -> term ->
    4.13 +  val prove_future: Proof.context -> string list -> term list -> term ->
    4.14      ({prems: thm list, context: Proof.context} -> tactic) -> thm
    4.15    val prove: Proof.context -> string list -> term list -> term ->
    4.16      ({prems: thm list, context: Proof.context} -> tactic) -> thm
    4.17 @@ -96,9 +96,9 @@
    4.18    #> Drule.zero_var_indexes;
    4.19  
    4.20  
    4.21 -(* promise *)
    4.22 +(* future_result *)
    4.23  
    4.24 -fun promise_result ctxt result prop =
    4.25 +fun future_result ctxt result prop =
    4.26    let
    4.27      val thy = ProofContext.theory_of ctxt;
    4.28      val _ = Context.reject_draft thy;
    4.29 @@ -122,7 +122,7 @@
    4.30        Drule.implies_intr_list assms o
    4.31        Thm.adjust_maxidx_thm ~1 o result;
    4.32      val local_result =
    4.33 -      Thm.promise global_result (cert global_prop)
    4.34 +      Thm.future global_result (cert global_prop)
    4.35        |> Thm.instantiate (instT, [])
    4.36        |> Drule.forall_elim_list fixes
    4.37        |> fold (Thm.elim_implies o Thm.assume) assms;
    4.38 @@ -176,7 +176,7 @@
    4.39            end);
    4.40      val res =
    4.41        if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
    4.42 -      else promise_result ctxt' result (Thm.term_of stmt);
    4.43 +      else future_result ctxt' result (Thm.term_of stmt);
    4.44    in
    4.45      Conjunction.elim_balanced (length props) res
    4.46      |> map (Assumption.export false ctxt' ctxt)
    4.47 @@ -186,7 +186,7 @@
    4.48  
    4.49  val prove_multi = prove_common true;
    4.50  
    4.51 -fun prove_promise ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac);
    4.52 +fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac);
    4.53  fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
    4.54  
    4.55  fun prove_global thy xs asms prop tac =
     5.1 --- a/src/Pure/thm.ML	Wed Oct 01 12:00:05 2008 +0200
     5.2 +++ b/src/Pure/thm.ML	Wed Oct 01 12:18:18 2008 +0200
     5.3 @@ -152,7 +152,7 @@
     5.4    val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
     5.5    val freezeT: thm -> thm
     5.6    val join_futures: theory -> unit
     5.7 -  val promise: (unit -> thm) -> cterm -> thm
     5.8 +  val future: (unit -> thm) -> cterm -> thm
     5.9    val proof_of: thm -> Proofterm.proof
    5.10    val extern_oracles: theory -> xstring list
    5.11    val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
    5.12 @@ -1625,14 +1625,14 @@
    5.13    in while not (joined ()) do () end;
    5.14  
    5.15  
    5.16 -(* promise *)
    5.17 +(* future rule *)
    5.18  
    5.19 -fun promise_result i orig_thy orig_shyps orig_prop raw_thm =
    5.20 +fun future_result i orig_thy orig_shyps orig_prop raw_thm =
    5.21    let
    5.22      val _ = Theory.check_thy orig_thy;
    5.23      val thm = strip_shyps (transfer orig_thy raw_thm);
    5.24      val _ = Theory.check_thy orig_thy;
    5.25 -    fun err msg = raise THM ("promise_result: " ^ msg, 0, [thm]);
    5.26 +    fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
    5.27  
    5.28      val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
    5.29      val _ = prop aconv orig_prop orelse err "bad prop";
    5.30 @@ -1642,14 +1642,14 @@
    5.31      val _ = forall (fn (j, _) => j < i) promises orelse err "bad dependencies";
    5.32    in thm end;
    5.33  
    5.34 -fun promise make_result ct =
    5.35 +fun future make_result ct =
    5.36    let
    5.37      val {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = rep_cterm ct;
    5.38      val thy = Context.reject_draft (Theory.deref thy_ref);
    5.39 -    val _ = T <> propT andalso raise CTERM ("promise: prop expected", [ct]);
    5.40 +    val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
    5.41  
    5.42      val i = serial ();
    5.43 -    val future = Future.fork_background (promise_result i thy sorts prop o make_result);
    5.44 +    val future = Future.fork_background (future_result i thy sorts prop o make_result);
    5.45      val _ = add_future thy future;
    5.46    in
    5.47      Thm (make_deriv false [(i, future)] (Pt.promise_proof i prop),
    5.48 @@ -1663,9 +1663,9 @@
    5.49    end;
    5.50  
    5.51  
    5.52 -(* fulfill *)
    5.53 +(* join_deriv *)
    5.54  
    5.55 -fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) =
    5.56 +fun join_deriv (thm as Thm (Deriv {oracle, proof, promises}, args)) =
    5.57    let
    5.58      val _ = Exn.release_all (Future.join_results (rev (map #2 promises)));
    5.59      val results = map (apsnd Future.join) promises;
    5.60 @@ -1674,7 +1674,7 @@
    5.61      val ora = oracle orelse exists (oracle_of o #2) results;
    5.62    in Thm (make_deriv ora [] (Pt.fulfill proofs proof), args) end;
    5.63  
    5.64 -val proof_of = fulfill #> (fn Thm (Deriv {proof, ...}, _) => proof);
    5.65 +val proof_of = join_deriv #> (fn Thm (Deriv {proof, ...}, _) => proof);
    5.66  
    5.67  
    5.68