# HG changeset patch
# User wenzelm
# Date 1222856298 -7200
# Node ID a01de3b3fa2edf94a973da645657a2fceb23f7b8
# Parent  526b8adcd1170f29ab033927835ea50c2f085b95
renamed promise to future, tuned related interfaces;

diff -r 526b8adcd117 -r a01de3b3fa2e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Oct 01 12:00:05 2008 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Oct 01 12:18:18 2008 +0200
@@ -114,8 +114,8 @@
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
-  val can_promise: state -> bool
-  val promise_proof: (state -> context) -> state -> context
+  val can_defer: state -> bool
+  val future_proof: (state -> context) -> state -> context
 end;
 
 structure Proof: PROOF =
@@ -976,22 +976,22 @@
 end;
 
 
-(* promise global proofs *)
+(* defer global proofs *)
 
 fun is_initial state =
   (case try find_goal state of
     NONE => false
   | SOME (_, (_, {statement = (_, _, prop), goal, ...})) => Thm.eq_thm_prop (Goal.init prop, goal));
 
-fun can_promise state =
+fun can_defer state =
   can (assert_bottom true) state andalso
   can assert_backward state andalso
   is_initial state andalso
   not (schematic_goal state);
 
-fun promise_proof make_proof state =
+fun future_proof make_proof state =
   let
-    val _ = can_promise state orelse error "Cannot promise proof";
+    val _ = can_defer state orelse error "Cannot defer proof";
 
     val (goal_ctxt, (_, goal)) = find_goal state;
     val {statement as (kind, propss, cprop), messages, using, goal, before_qed, after_qed} = goal;
@@ -1005,7 +1005,7 @@
       |> map_goal I (K (statement', messages, using, goal, before_qed, (#1 after_qed, after_qed')))
       |> make_proof
       |> (fn result_ctxt => ProofContext.get_fact_single result_ctxt (Facts.named this_name));
-    val finished_goal = Goal.protect (Goal.promise_result goal_ctxt make_result prop);
+    val finished_goal = Goal.protect (Goal.future_result goal_ctxt make_result prop);
   in
     state
     |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
diff -r 526b8adcd117 -r a01de3b3fa2e src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Wed Oct 01 12:00:05 2008 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Wed Oct 01 12:18:18 2008 +0200
@@ -36,7 +36,7 @@
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
 fun prove ctxt xs asms prop tac =
-  (if ! future_scheduler then Goal.prove_promise else Goal.prove) ctxt xs asms prop
+  (if ! future_scheduler then Goal.prove_future else Goal.prove) ctxt xs asms prop
     (fn args => fn st =>
       if ! quick_and_dirty
       then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
diff -r 526b8adcd117 -r a01de3b3fa2e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Oct 01 12:00:05 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Oct 01 12:18:18 2008 +0200
@@ -694,10 +694,10 @@
   let val st' = command tr st
   in (st', st') end;
 
-fun unit_result do_promise (tr, proof_trs) st =
+fun unit_result immediate (tr, proof_trs) st =
   let val st' = command tr st in
-    if do_promise andalso not (null proof_trs) andalso
-      can proof_of st' andalso Proof.can_promise (proof_of st')
+    if not immediate andalso not (null proof_trs) andalso
+      can proof_of st' andalso Proof.can_defer (proof_of st')
     then
       let
         val (body_trs, end_tr) = split_last proof_trs;
@@ -708,9 +708,9 @@
               => State (SOME (Proof (ProofNode.init prf, (Context.Proof, orig_gthy)), exit), prev))
             |> fold_map command_result body_trs ||> command end_tr
           in body_states := states; context_of result_state end;
-        val proof_promise =
-          end_tr |> reset_trans |> end_proof (K (Proof.promise_proof make_result));
-        val st'' = command proof_promise st';
+        val proof_future =
+          end_tr |> reset_trans |> end_proof (K (Proof.future_proof make_result));
+        val st'' = command proof_future st';
       in (fn () => (tr, st') :: (body_trs ~~ ! body_states) @ [(end_tr, st'')], st'') end
     else
       let val (states, st'') = fold_map command_result proof_trs st'
@@ -721,8 +721,8 @@
   let
     val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
 
-    val do_promise = ! future_scheduler andalso Multithreading.max_threads_value () > 1;
-    val (future_results, end_state) = fold_map (unit_result do_promise) input toplevel;
+    val immediate = not (! future_scheduler) orelse Multithreading.max_threads_value () <= 1;
+    val (future_results, end_state) = fold_map (unit_result immediate) input toplevel;
     val _ =
       (case end_state of
         State (NONE, SOME (Theory (Context.Theory thy, _), _)) => Thm.join_futures thy
diff -r 526b8adcd117 -r a01de3b3fa2e src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Oct 01 12:00:05 2008 +0200
+++ b/src/Pure/goal.ML	Wed Oct 01 12:18:18 2008 +0200
@@ -20,11 +20,11 @@
   val conclude: thm -> thm
   val finish: thm -> thm
   val norm_result: thm -> thm
-  val promise_result: Proof.context -> (unit -> thm) -> term -> thm
+  val future_result: Proof.context -> (unit -> thm) -> term -> thm
   val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
-  val prove_promise: Proof.context -> string list -> term list -> term ->
+  val prove_future: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
@@ -96,9 +96,9 @@
   #> Drule.zero_var_indexes;
 
 
-(* promise *)
+(* future_result *)
 
-fun promise_result ctxt result prop =
+fun future_result ctxt result prop =
   let
     val thy = ProofContext.theory_of ctxt;
     val _ = Context.reject_draft thy;
@@ -122,7 +122,7 @@
       Drule.implies_intr_list assms o
       Thm.adjust_maxidx_thm ~1 o result;
     val local_result =
-      Thm.promise global_result (cert global_prop)
+      Thm.future global_result (cert global_prop)
       |> Thm.instantiate (instT, [])
       |> Drule.forall_elim_list fixes
       |> fold (Thm.elim_implies o Thm.assume) assms;
@@ -176,7 +176,7 @@
           end);
     val res =
       if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
-      else promise_result ctxt' result (Thm.term_of stmt);
+      else future_result ctxt' result (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)
@@ -186,7 +186,7 @@
 
 val prove_multi = prove_common true;
 
-fun prove_promise ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac);
+fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac);
 fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
 
 fun prove_global thy xs asms prop tac =
diff -r 526b8adcd117 -r a01de3b3fa2e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Oct 01 12:00:05 2008 +0200
+++ b/src/Pure/thm.ML	Wed Oct 01 12:18:18 2008 +0200
@@ -152,7 +152,7 @@
   val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   val freezeT: thm -> thm
   val join_futures: theory -> unit
-  val promise: (unit -> thm) -> cterm -> thm
+  val future: (unit -> thm) -> cterm -> thm
   val proof_of: thm -> Proofterm.proof
   val extern_oracles: theory -> xstring list
   val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
@@ -1625,14 +1625,14 @@
   in while not (joined ()) do () end;
 
 
-(* promise *)
+(* future rule *)
 
-fun promise_result i orig_thy orig_shyps orig_prop raw_thm =
+fun future_result i orig_thy orig_shyps orig_prop raw_thm =
   let
     val _ = Theory.check_thy orig_thy;
     val thm = strip_shyps (transfer orig_thy raw_thm);
     val _ = Theory.check_thy orig_thy;
-    fun err msg = raise THM ("promise_result: " ^ msg, 0, [thm]);
+    fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
 
     val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
     val _ = prop aconv orig_prop orelse err "bad prop";
@@ -1642,14 +1642,14 @@
     val _ = forall (fn (j, _) => j < i) promises orelse err "bad dependencies";
   in thm end;
 
-fun promise make_result ct =
+fun future make_result ct =
   let
     val {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = rep_cterm ct;
     val thy = Context.reject_draft (Theory.deref thy_ref);
-    val _ = T <> propT andalso raise CTERM ("promise: prop expected", [ct]);
+    val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
 
     val i = serial ();
-    val future = Future.fork_background (promise_result i thy sorts prop o make_result);
+    val future = Future.fork_background (future_result i thy sorts prop o make_result);
     val _ = add_future thy future;
   in
     Thm (make_deriv false [(i, future)] (Pt.promise_proof i prop),
@@ -1663,9 +1663,9 @@
   end;
 
 
-(* fulfill *)
+(* join_deriv *)
 
-fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) =
+fun join_deriv (thm as Thm (Deriv {oracle, proof, promises}, args)) =
   let
     val _ = Exn.release_all (Future.join_results (rev (map #2 promises)));
     val results = map (apsnd Future.join) promises;
@@ -1674,7 +1674,7 @@
     val ora = oracle orelse exists (oracle_of o #2) results;
   in Thm (make_deriv ora [] (Pt.fulfill proofs proof), args) end;
 
-val proof_of = fulfill #> (fn Thm (Deriv {proof, ...}, _) => proof);
+val proof_of = join_deriv #> (fn Thm (Deriv {proof, ...}, _) => proof);