--- a/src/HOL/Import/lazy_seq.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/HOL/Import/lazy_seq.ML Fri Dec 05 11:35:07 2008 +1100
@@ -80,7 +80,7 @@
structure LazySeq :> LAZY_SEQ =
struct
-datatype 'a seq = Seq of ('a * 'a seq) option Lazy.T
+datatype 'a seq = Seq of ('a * 'a seq) option lazy
exception Empty
--- a/src/Pure/Concurrent/future.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/Concurrent/future.ML Fri Dec 05 11:35:07 2008 +1100
@@ -30,21 +30,23 @@
val enabled: unit -> bool
type task = TaskQueue.task
type group = TaskQueue.group
- val thread_data: unit -> (string * task * group) option
- type 'a T
- val task_of: 'a T -> task
- val group_of: 'a T -> group
- val peek: 'a T -> 'a Exn.result option
- val is_finished: 'a T -> bool
- val future: group option -> task list -> bool -> (unit -> 'a) -> 'a T
- val fork: (unit -> 'a) -> 'a T
- val fork_background: (unit -> 'a) -> 'a T
- val join_results: 'a T list -> 'a Exn.result list
- val join_result: 'a T -> 'a Exn.result
- val join: 'a T -> 'a
+ val thread_data: unit -> (string * task) option
+ type 'a future
+ val task_of: 'a future -> task
+ val group_of: 'a future -> group
+ val peek: 'a future -> 'a Exn.result option
+ val is_finished: 'a future -> bool
+ val fork: (unit -> 'a) -> 'a future
+ val fork_group: group -> (unit -> 'a) -> 'a future
+ val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
+ val fork_background: (unit -> 'a) -> 'a future
+ val join_results: 'a future list -> 'a Exn.result list
+ val join_result: 'a future -> 'a Exn.result
+ val join: 'a future -> 'a
+ val map: ('a -> 'b) -> 'a future -> 'b future
val focus: task list -> unit
val interrupt_task: string -> unit
- val cancel: 'a T -> unit
+ val cancel: 'a future -> unit
val shutdown: unit -> unit
end;
@@ -63,7 +65,7 @@
type task = TaskQueue.task;
type group = TaskQueue.group;
-local val tag = Universal.tag () : (string * task * group) option Universal.tag in
+local val tag = Universal.tag () : (string * task) option Universal.tag in
fun thread_data () = the_default NONE (Thread.getLocal tag);
fun setmp_thread_data data f x = Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
end;
@@ -71,7 +73,7 @@
(* datatype future *)
-datatype 'a T = Future of
+datatype 'a future = Future of
{task: task,
group: group,
result: 'a Exn.result option ref};
@@ -140,7 +142,7 @@
fun execute name (task, group, run) =
let
val _ = trace_active ();
- val ok = setmp_thread_data (name, task, group) run ();
+ val ok = setmp_thread_data (name, task) run ();
val _ = SYNCHRONIZED "execute" (fn () =>
(change queue (TaskQueue.finish task);
if ok then ()
@@ -246,10 +248,10 @@
change_result queue (TaskQueue.enqueue group deps pri run) before notify_all ());
in Future {task = task, group = group, result = result} end;
-fun fork_common pri = future (Option.map #3 (thread_data ())) [] pri;
-
-fun fork e = fork_common true e;
-fun fork_background e = fork_common false e;
+fun fork e = future NONE [] true e;
+fun fork_group group e = future (SOME group) [] true e;
+fun fork_deps deps e = future NONE (map task_of deps) true e;
+fun fork_background e = future NONE [] false e;
(* join: retrieve results *)
@@ -274,7 +276,7 @@
(*alien thread -- refrain from contending for resources*)
while exists (not o is_finished) xs
do SYNCHRONIZED "join_thread" (fn () => wait "join_thread")
- | SOME (name, task, _) =>
+ | SOME (name, task) =>
(*proper task -- actively work towards results*)
let
val unfinished = xs |> map_filter
@@ -292,6 +294,8 @@
fun join_result x = singleton join_results x;
fun join x = Exn.release (join_result x);
+fun map f x = fork_deps [x] (fn () => f (join x));
+
(* misc operations *)
@@ -324,3 +328,6 @@
else ();
end;
+
+type 'a future = 'a Future.future;
+
--- a/src/Pure/Concurrent/par_list.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/Concurrent/par_list.ML Fri Dec 05 11:35:07 2008 +1100
@@ -31,7 +31,7 @@
if Future.enabled () then
let
val group = TaskQueue.new_group ();
- val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
+ val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
val _ = List.app (ignore o Future.join_result) futures;
in Future.join_results futures end
else map (Exn.capture f) xs;
--- a/src/Pure/General/lazy.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/General/lazy.ML Fri Dec 05 11:35:07 2008 +1100
@@ -8,13 +8,13 @@
signature LAZY =
sig
- type 'a T
- val same: 'a T * 'a T -> bool
- val lazy: (unit -> 'a) -> 'a T
- val value: 'a -> 'a T
- val peek: 'a T -> 'a Exn.result option
- val force: 'a T -> 'a
- val map_force: ('a -> 'a) -> 'a T -> 'a T
+ type 'a lazy
+ val same: 'a lazy * 'a lazy -> bool
+ val lazy: (unit -> 'a) -> 'a lazy
+ val value: 'a -> 'a lazy
+ val peek: 'a lazy -> 'a Exn.result option
+ val force: 'a lazy -> 'a
+ val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
end
structure Lazy :> LAZY =
@@ -22,13 +22,13 @@
(* datatype *)
-datatype 'a lazy =
+datatype 'a T =
Lazy of unit -> 'a |
Result of 'a Exn.result;
-type 'a T = 'a lazy ref;
+type 'a lazy = 'a T ref;
-fun same (r1: 'a T, r2) = r1 = r2;
+fun same (r1: 'a lazy, r2) = r1 = r2;
fun lazy e = ref (Lazy e);
fun value x = ref (Result (Exn.Result x));
@@ -58,3 +58,6 @@
fun map_force f = value o f o force;
end;
+
+type 'a lazy = 'a Lazy.lazy;
+
--- a/src/Pure/Isar/code.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/Isar/code.ML Fri Dec 05 11:35:07 2008 +1100
@@ -15,7 +15,7 @@
val add_default_eqn_attrib: Attrib.src
val del_eqn: thm -> theory -> theory
val del_eqns: string -> theory -> theory
- val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory
+ val add_eqnl: string * (thm * bool) list lazy -> theory -> theory
val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
val add_inline: thm -> theory -> theory
@@ -114,7 +114,7 @@
(* defining equations *)
-type eqns = bool * (thm * bool) list Lazy.T;
+type eqns = bool * (thm * bool) list lazy;
(*default flag, theorems with linear flag (perhaps lazy)*)
fun pretty_lthms ctxt r = case Lazy.peek r
--- a/src/Pure/Isar/proof.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/Isar/proof.ML Fri Dec 05 11:35:07 2008 +1100
@@ -115,7 +115,7 @@
val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
val is_relevant: state -> bool
- val future_proof: (state -> context) -> state -> context
+ val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
end;
structure Proof: PROOF =
@@ -990,7 +990,7 @@
not (is_initial state) orelse
schematic_goal state;
-fun future_proof make_proof state =
+fun future_proof proof state =
let
val _ = is_relevant state andalso error "Cannot fork relevant proof";
@@ -1004,16 +1004,19 @@
fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [Goal.conclude th]);
val this_name = ProofContext.full_bname (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
- fun make_result () = state
+ val result_ctxt =
+ state
|> map_contexts (Variable.auto_fixes prop)
|> 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.future_result goal_ctxt make_result prop);
- in
- state
- |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
- |> global_done_proof
- end;
+ |> proof;
+
+ val thm = result_ctxt |> Future.map (fn (_, ctxt) =>
+ ProofContext.get_fact_single ctxt (Facts.named this_name));
+ val finished_goal = Goal.protect (Goal.future_result goal_ctxt thm prop);
+ val state' =
+ state
+ |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
+ |> global_done_proof;
+ in (Future.map #1 result_ctxt, state') end;
end;
--- a/src/Pure/Isar/toplevel.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/Isar/toplevel.ML Fri Dec 05 11:35:07 2008 +1100
@@ -691,45 +691,62 @@
(* excursion of units, consisting of commands with proof *)
+structure States = ProofDataFun
+(
+ type T = state list future option;
+ fun init _ = NONE;
+);
+
fun command_result tr st =
let val st' = command tr st
in (st', st') end;
-fun unit_result immediate (tr, proof_trs) st =
+fun proof_result immediate (tr, proof_trs) st =
let val st' = command tr st in
if immediate orelse null proof_trs orelse
not (can proof_of st') orelse Proof.is_relevant (proof_of st')
then
let val (states, st'') = fold_map command_result proof_trs st'
- in (fn () => (tr, st') :: (proof_trs ~~ states), st'') end
+ in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end
else
let
val (body_trs, end_tr) = split_last proof_trs;
- val body_states = ref ([]: state list);
val finish = Context.Theory o ProofContext.theory_of;
- fun make_result prf =
- let val (states, State (result_node, _)) =
- (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
- => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
- |> fold_map command_result body_trs
- ||> command (end_tr |> set_print false)
- in body_states := states; presentation_context (Option.map #1 result_node) NONE end;
- val st'' = st'
- |> command (end_tr |> reset_trans |> end_proof (K (Proof.future_proof make_result)));
- in (fn () => (tr, st') :: (body_trs ~~ ! body_states) @ [(end_tr, st'')], st'') end
+
+ val future_proof = Proof.future_proof
+ (fn prf =>
+ Future.fork_background (fn () =>
+ let val (states, State (result_node, _)) =
+ (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
+ => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
+ |> fold_map command_result body_trs
+ ||> command (end_tr |> set_print false);
+ in (states, presentation_context (Option.map #1 result_node) NONE) end))
+ #> (fn (states, ctxt) => States.put (SOME states) ctxt);
+
+ val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
+
+ val states =
+ (case States.get (presentation_context (SOME (node_of st'')) NONE) of
+ NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
+ | SOME states => states);
+ val result = Lazy.lazy
+ (fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]);
+
+ in (result, st'') end
end;
-fun excursion input =
+fun excursion input = exception_trace (fn () =>
let
val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
val immediate = not (Future.enabled ());
- val (future_results, end_state) = fold_map (unit_result immediate) input toplevel;
+ val (future_results, end_state) = fold_map (proof_result immediate) input toplevel;
val _ =
(case end_state of
- State (NONE, SOME (Theory (Context.Theory thy, _), _)) => Thm.join_futures thy
+ State (NONE, SOME (Theory (Context.Theory thy, _), _)) => PureThy.force_proofs thy
| _ => error "Unfinished development at end of input");
- val results = maps (fn res => res ()) future_results;
- in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end;
+ val results = maps Lazy.force future_results;
+ in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end);
end;
--- a/src/Pure/ML-Systems/install_pp_polyml.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/ML-Systems/install_pp_polyml.ML Fri Dec 05 11:35:07 2008 +1100
@@ -4,13 +4,13 @@
Extra toplevel pretty-printing for Poly/ML.
*)
-install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Future.T) =>
+install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
(case Future.peek x of
NONE => str "<future>"
| SOME (Exn.Exn _) => str "<failed>"
| SOME (Exn.Result y) => print (y, depth)));
-install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Lazy.T) =>
+install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
(case Lazy.peek x of
NONE => str "<lazy>"
| SOME (Exn.Exn _) => str "<failed>"
--- a/src/Pure/Thy/thy_info.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/Thy/thy_info.ML Fri Dec 05 11:35:07 2008 +1100
@@ -320,14 +320,12 @@
val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
(case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
- val group = TaskQueue.new_group ();
fun future (name, body) tab =
let
val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
- val x = Future.future (SOME group) deps true body;
- in (x, Symtab.update (name, Future.task_of x) tab) end;
+ val x = Future.fork_deps deps body;
+ in (x, Symtab.update (name, x) tab) end;
val _ = ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty))));
- val _ = List.app (PureThy.force_proofs o get_theory o #1) tasks;
in () end;
local
@@ -589,8 +587,6 @@
(* finish all theories *)
-fun finish () = change_thys (Graph.map_nodes
- (fn (SOME _, SOME thy) => (NONE, (PureThy.force_proofs thy; SOME thy))
- | (_, entry) => (NONE, entry)));
+fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
end;
--- a/src/Pure/goal.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/goal.ML Fri Dec 05 11:35:07 2008 +1100
@@ -20,7 +20,7 @@
val conclude: thm -> thm
val finish: thm -> thm
val norm_result: thm -> thm
- val future_result: Proof.context -> (unit -> thm) -> term -> thm
+ val future_result: Proof.context -> thm future -> 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
@@ -116,11 +116,11 @@
val global_prop =
Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)));
- val global_result =
- Thm.generalize (map #1 tfrees, []) 0 o
- Drule.forall_intr_list fixes o
- Drule.implies_intr_list assms o
- Thm.adjust_maxidx_thm ~1 o result;
+ val global_result = result |> Future.map
+ (Thm.adjust_maxidx_thm ~1 #>
+ Drule.implies_intr_list assms #>
+ Drule.forall_intr_list fixes #>
+ Thm.generalize (map #1 tfrees, []) 0);
val local_result =
Thm.future global_result (cert global_prop)
|> Thm.instantiate (instT, [])
@@ -178,7 +178,7 @@
end);
val res =
if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
- else future_result ctxt' result (Thm.term_of stmt);
+ else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
in
Conjunction.elim_balanced (length props) res
|> map (Assumption.export false ctxt' ctxt)
--- a/src/Pure/proofterm.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/proofterm.ML Fri Dec 05 11:35:07 2008 +1100
@@ -22,10 +22,10 @@
| PAxm of string * term * typ list option
| Oracle of string * term * typ list option
| Promise of serial * term * typ list
- | PThm of serial * ((string * term * typ list option) * proof_body Lazy.T)
+ | PThm of serial * ((string * term * typ list option) * proof_body lazy)
and proof_body = PBody of
{oracles: (string * term) OrdList.T,
- thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
+ thms: (serial * (string * term * proof_body lazy)) OrdList.T,
proof: proof}
val %> : proof * term -> proof
@@ -36,10 +36,10 @@
include BASIC_PROOFTERM
type oracle = string * term
- type pthm = serial * (string * term * proof_body Lazy.T)
- val force_body: proof_body Lazy.T ->
+ type pthm = serial * (string * term * proof_body lazy)
+ val force_body: proof_body lazy ->
{oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
- val force_proof: proof_body Lazy.T -> proof
+ val force_proof: proof_body lazy -> proof
val proof_of: proof_body -> proof
val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
@@ -111,7 +111,7 @@
val promise_proof: theory -> serial -> term -> proof
val fulfill_proof: theory -> (serial * proof) list -> proof_body -> proof_body
val thm_proof: theory -> string -> term list -> term ->
- (serial * proof) list Lazy.T -> proof_body -> pthm * proof
+ (serial * proof) list lazy -> proof_body -> pthm * proof
val get_name: term list -> term -> proof -> string
(** rewriting on proof terms **)
@@ -143,14 +143,14 @@
| PAxm of string * term * typ list option
| Oracle of string * term * typ list option
| Promise of serial * term * typ list
- | PThm of serial * ((string * term * typ list option) * proof_body Lazy.T)
+ | PThm of serial * ((string * term * typ list option) * proof_body lazy)
and proof_body = PBody of
{oracles: (string * term) OrdList.T,
- thms: (serial * (string * term * proof_body Lazy.T)) OrdList.T,
+ thms: (serial * (string * term * proof_body lazy)) OrdList.T,
proof: proof};
type oracle = string * term;
-type pthm = serial * (string * term * proof_body Lazy.T);
+type pthm = serial * (string * term * proof_body lazy);
val force_body = Lazy.force #> (fn PBody args => args);
val force_proof = #proof o force_body;
--- a/src/Pure/pure_thy.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/pure_thy.ML Fri Dec 05 11:35:07 2008 +1100
@@ -59,7 +59,7 @@
structure FactsData = TheoryDataFun
(
- type T = Facts.T * unit Lazy.T list;
+ type T = Facts.T * unit lazy list;
val empty = (Facts.empty, []);
val copy = I;
fun extend (facts, _) = (facts, []);
@@ -80,7 +80,9 @@
(* proofs *)
fun lazy_proof thm = Lazy.lazy (fn () => Thm.force_proof thm);
-val force_proofs = List.app Lazy.force o #2 o FactsData.get;
+
+fun force_proofs thy =
+ ignore (Exn.release_all (map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy)))));
--- a/src/Pure/thm.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Pure/thm.ML Fri Dec 05 11:35:07 2008 +1100
@@ -146,8 +146,7 @@
val varifyT: thm -> thm
val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
val freezeT: thm -> thm
- val join_futures: theory -> unit
- val future: (unit -> thm) -> cterm -> thm
+ val future: thm future -> cterm -> thm
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
val force_proof: thm -> unit
@@ -347,8 +346,8 @@
tpairs: (term * term) list, (*flex-flex pairs*)
prop: term} (*conclusion*)
and deriv = Deriv of
- {all_promises: (serial * thm Future.T) OrdList.T,
- promises: (serial * thm Future.T) OrdList.T,
+ {all_promises: (serial * thm future) OrdList.T,
+ promises: (serial * thm future) OrdList.T,
body: Pt.proof_body};
type conv = cterm -> thm;
@@ -1587,36 +1586,7 @@
-(*** Promises ***)
-
-(* pending future derivations *)
-
-structure Futures = TheoryDataFun
-(
- type T = thm Future.T list ref;
- val empty : T = ref [];
- val copy = I; (*shared ref within all versions of whole theory body*)
- fun extend _ : T = ref [];
- fun merge _ _ : T = ref [];
-);
-
-val _ = Context.>> (Context.map_theory Futures.init);
-
-fun add_future thy future = CRITICAL (fn () => change (Futures.get thy) (cons future));
-
-fun join_futures thy =
- let
- val futures = Futures.get thy;
- fun joined () =
- (List.app (ignore o Future.join_result) (rev (! futures));
- CRITICAL (fn () =>
- let
- val (finished, unfinished) = List.partition Future.is_finished (! futures);
- val _ = futures := unfinished;
- in finished end)
- |> Future.join_results |> Exn.release_all |> null);
- in while not (joined ()) do () end;
-
+(*** Future theorems -- proofs with promises ***)
(* future rule *)
@@ -1635,15 +1605,14 @@
val _ = forall (fn (j, _) => j < i) all_promises orelse err "bad dependencies";
in thm end;
-fun future make_result ct =
+fun future future_thm ct =
let
val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
val thy = Context.reject_draft (Theory.deref thy_ref);
val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
val i = serial ();
- val future = Future.fork_background (future_result i thy sorts prop o norm_proof o make_result);
- val _ = add_future thy future;
+ val future = future_thm |> Future.map (future_result i thy sorts prop o norm_proof);
val promise = (i, future);
in
Thm (make_deriv [promise] [promise] [] [] (Pt.promise_proof thy i prop),
--- a/src/Tools/code/code_ml.ML Fri Dec 05 11:33:03 2008 +1100
+++ b/src/Tools/code/code_ml.ML Fri Dec 05 11:35:07 2008 +1100
@@ -912,7 +912,7 @@
structure CodeAntiqData = ProofDataFun
(
- type T = string list * (bool * (string * (string * (string * string) list) Lazy.T));
+ type T = string list * (bool * (string * (string * (string * string) list) lazy));
fun init _ = ([], (true, ("", Lazy.value ("", []))));
);