--- a/NEWS Mon Jul 20 09:52:09 2009 +0200
+++ b/NEWS Mon Jul 20 13:52:27 2009 +0200
@@ -128,6 +128,9 @@
* Removed "compress" option from isabelle-process and isabelle usedir;
this is always enabled.
+* More fine-grained control of proof parallelism, cf.
+Goal.parallel_proofs in ML and usedir option -q LEVEL.
+
New in Isabelle2009 (April 2009)
--- a/doc-src/System/Thy/Presentation.thy Mon Jul 20 09:52:09 2009 +0200
+++ b/doc-src/System/Thy/Presentation.thy Mon Jul 20 13:52:27 2009 +0200
@@ -451,7 +451,8 @@
-g BOOL generate session graph image for document (default false)
-i BOOL generate theory browser information (default false)
-m MODE add print mode for output
- -p LEVEL set level of detail for proof objects
+ -p LEVEL set level of detail for proof objects (default 0)
+ -q LEVEL set level of parallel proof checking (default 1)
-r reset session path
-s NAME override session NAME
-t BOOL internal session timing (default false)
@@ -564,6 +565,12 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \medskip The @{verbatim "-q"} option specifies the level of parallel
+ proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel
+ proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
+ The resulting speedup may vary, depending on the number of worker
+ threads, granularity of proofs, and whether proof terms are enabled.
+
\medskip The @{verbatim "-t"} option produces a more detailed
internal timing report of the session.
@@ -583,13 +590,6 @@
bottle-necks, e.g.\ due to excessive wait states when locking
critical code sections.
- \medskip The @{verbatim "-Q"} option tells whether individual proofs
- should be checked in parallel; the default is @{verbatim true}.
- Note that fine-grained proof parallelism requires considerable
- amounts of extra memory, since full proof context information is
- maintained for each independent derivation thread, until checking is
- completed.
-
\medskip Any @{tool usedir} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
on others. For example, consider @{verbatim "Pure/FOL/ex"}, which
--- a/doc-src/System/Thy/document/Presentation.tex Mon Jul 20 09:52:09 2009 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Mon Jul 20 13:52:27 2009 +0200
@@ -477,7 +477,8 @@
-g BOOL generate session graph image for document (default false)
-i BOOL generate theory browser information (default false)
-m MODE add print mode for output
- -p LEVEL set level of detail for proof objects
+ -p LEVEL set level of detail for proof objects (default 0)
+ -q LEVEL set level of parallel proof checking (default 1)
-r reset session path
-s NAME override session NAME
-t BOOL internal session timing (default false)
@@ -581,6 +582,12 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \medskip The \verb|-q| option specifies the level of parallel
+ proof checking: \verb|0| no proofs, \verb|1| toplevel
+ proofs (default), \verb|2| toplevel and nested Isar proofs.
+ The resulting speedup may vary, depending on the number of worker
+ threads, granularity of proofs, and whether proof terms are enabled.
+
\medskip The \verb|-t| option produces a more detailed
internal timing report of the session.
@@ -599,13 +606,6 @@
bottle-necks, e.g.\ due to excessive wait states when locking
critical code sections.
- \medskip The \verb|-Q| option tells whether individual proofs
- should be checked in parallel; the default is \verb|true|.
- Note that fine-grained proof parallelism requires considerable
- amounts of extra memory, since full proof context information is
- maintained for each independent derivation thread, until checking is
- completed.
-
\medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
on others. For example, consider \verb|Pure/FOL/ex|, which
--- a/etc/settings Mon Jul 20 09:52:09 2009 +0200
+++ b/etc/settings Mon Jul 20 13:52:27 2009 +0200
@@ -96,7 +96,7 @@
# Specifically for the HOL image
HOL_USEDIR_OPTIONS=""
-#HOL_USEDIR_OPTIONS="-p 2 -Q false"
+#HOL_USEDIR_OPTIONS="-p 2 -q 1"
#Source file identification (default: full name + date stamp)
ISABELLE_FILE_IDENT=""
--- a/lib/Tools/usedir Mon Jul 20 09:52:09 2009 +0200
+++ b/lib/Tools/usedir Mon Jul 20 13:52:27 2009 +0200
@@ -19,7 +19,6 @@
echo " -D PATH dump generated document sources into PATH"
echo " -M MAX multithreading: maximum number of worker threads (default 1)"
echo " -P PATH set path for remote theory browsing information"
- echo " -Q BOOL check proofs in parallel (default true)"
echo " -T LEVEL multithreading: trace level (default 0)"
echo " -V VERSION declare alternative document VERSION"
echo " -b build mode (output heap image, using current dir)"
@@ -28,7 +27,8 @@
echo " -g BOOL generate session graph image for document (default false)"
echo " -i BOOL generate HTML and graph browser information (default false)"
echo " -m MODE add print mode for output"
- echo " -p LEVEL set level of detail for proof objects"
+ echo " -p LEVEL set level of detail for proof objects (default 0)"
+ echo " -q LEVEL set level of parallel proof checking (default 1)"
echo " -r reset session path"
echo " -s NAME override session NAME"
echo " -t BOOL internal session timing (default false)"
@@ -73,7 +73,6 @@
DUMP=""
MAXTHREADS="1"
RPATH=""
-PARALLEL_PROOFS="true"
TRACETHREADS="0"
DOCUMENT_VERSIONS=""
BUILD=""
@@ -84,14 +83,15 @@
MODES=""
RESET=false
SESSION=""
-PROOFS=0
+PROOFS="0"
+PARALLEL_PROOFS="1"
TIMING=false
VERBOSE=false
function getoptions()
{
OPTIND=1
- while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:t:v:" OPT
+ while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
do
case "$OPT" in
C)
@@ -112,9 +112,6 @@
P)
RPATH="$OPTARG"
;;
- Q)
- PARALLEL_PROOFS="$OPTARG"
- ;;
T)
check_number "$OPTARG"
TRACETHREADS="$OPTARG"
@@ -154,6 +151,10 @@
check_number "$OPTARG"
PROOFS="$OPTARG"
;;
+ q)
+ check_number "$OPTARG"
+ PARALLEL_PROOFS="$OPTARG"
+ ;;
r)
RESET=true
;;
--- a/src/Pure/Concurrent/future.ML Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Jul 20 13:52:27 2009 +0200
@@ -29,7 +29,7 @@
val enabled: unit -> bool
type task = Task_Queue.task
type group = Task_Queue.group
- val thread_data: unit -> (string * task) option
+ val is_worker: unit -> bool
type 'a future
val task_of: 'a future -> task
val group_of: 'a future -> group
@@ -40,6 +40,7 @@
val fork_group: group -> (unit -> 'a) -> 'a future
val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
val fork_pri: int -> (unit -> 'a) -> 'a future
+ val fork_local: int -> (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
@@ -66,11 +67,16 @@
type task = Task_Queue.task;
type group = Task_Queue.group;
-local val tag = Universal.tag () : (string * task) option Universal.tag in
+local
+ val tag = Universal.tag () : (string * task * group) 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;
+ fun setmp_thread_data data f x =
+ Library.setmp_thread_data tag (thread_data ()) (SOME data) f x;
end;
+val is_worker = is_some o thread_data;
+
(* datatype future *)
@@ -148,7 +154,7 @@
let
val _ = trace_active ();
val valid = Task_Queue.is_valid group;
- val ok = setmp_thread_data (name, task) (fn () =>
+ val ok = setmp_thread_data (name, task, group) (fn () =>
fold (fn job => fn ok => job valid andalso ok) jobs true) ();
val _ = SYNCHRONIZED "execute" (fn () =>
(change queue (Task_Queue.finish task);
@@ -277,6 +283,7 @@
fun fork_group group e = fork_future (SOME group) [] 0 e;
fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
fun fork_pri pri e = fork_future NONE [] pri e;
+fun fork_local pri e = fork_future (Option.map #3 (thread_data ())) [] pri e;
(* join *)
@@ -285,21 +292,10 @@
fun get_result x = the_default (Exn.Exn (SYS_ERROR "unfinished future")) (peek x);
-fun join_wait x =
- if SYNCHRONIZED "join_wait" (fn () => is_finished x orelse (wait (); false))
- then () else join_wait x;
-
-fun join_next x = (*requires SYNCHRONIZED*)
- if is_finished x then NONE
- else
- (case change_result queue Task_Queue.dequeue of
- NONE => (worker_wait (); join_next x)
- | some => some);
-
-fun join_loop x =
- (case SYNCHRONIZED "join" (fn () => join_next x) of
+fun join_deps deps =
+ (case SYNCHRONIZED "join" (fn () => change_result queue (Task_Queue.dequeue_towards deps)) of
NONE => ()
- | SOME work => (execute "join" work; join_loop x));
+ | SOME (work, deps') => (execute "join" work; join_deps deps'));
in
@@ -310,10 +306,16 @@
val _ = scheduler_check "join check";
val _ = Multithreading.self_critical () andalso
error "Cannot join future values within critical section";
- val _ =
- if is_some (thread_data ())
- then List.app join_loop xs (*proper task -- continue work*)
- else List.app join_wait xs; (*alien thread -- refrain from contending for resources*)
+
+ val worker = is_worker ();
+ fun join_wait x =
+ if SYNCHRONIZED "join_wait" (fn () =>
+ is_finished x orelse (if worker then worker_wait () else wait (); false))
+ then () else join_wait x;
+
+ val _ = if worker then join_deps (map task_of xs) else ();
+ val _ = List.app join_wait xs;
+
in map get_result xs end) ();
end;
@@ -347,7 +349,7 @@
fun interruptible_task f x =
if Multithreading.available then
Multithreading.with_attributes
- (if is_some (thread_data ())
+ (if is_worker ()
then Multithreading.restricted_interrupts
else Multithreading.regular_interrupts)
(fn _ => f) x
--- a/src/Pure/Concurrent/task_queue.ML Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Mon Jul 20 13:52:27 2009 +0200
@@ -24,6 +24,8 @@
val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue
val extend: task -> (bool -> bool) -> queue -> queue option
val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
+ val dequeue_towards: task list -> queue ->
+ (((task * group * (bool -> bool) list) * task list) option * queue)
val interrupt: queue -> task -> unit
val interrupt_external: queue -> string -> unit
val cancel: queue -> group -> bool
@@ -150,6 +152,28 @@
end;
+(* dequeue_towards -- adhoc dependencies *)
+
+fun dequeue_towards deps (queue as Queue {groups, jobs, ...}) =
+ let
+ fun ready task =
+ (case Task_Graph.get_node jobs task of
+ (group, Job list) =>
+ if null (Task_Graph.imm_preds jobs task) then SOME (task, group, rev list)
+ else NONE
+ | _ => NONE);
+ val tasks = filter (can (Task_Graph.get_node jobs)) deps;
+ in
+ (case get_first ready (Task_Graph.all_preds jobs tasks) of
+ NONE => (NONE, queue)
+ | SOME (result as (task, _, _)) =>
+ let
+ val jobs' = set_job task (Running (Thread.self ())) jobs;
+ val cache' = Unknown;
+ in (SOME (result, tasks), make_queue groups jobs' cache') end)
+ end;
+
+
(* sporadic interrupts *)
fun interrupt (Queue {jobs, ...}) task =
--- a/src/Pure/Isar/isar_cmd.ML Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Jul 20 13:52:27 2009 +0200
@@ -230,7 +230,7 @@
(* local endings *)
fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
-val local_terminal_proof = Toplevel.proof o Proof.local_terminal_proof;
+val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
val local_default_proof = Toplevel.proof Proof.local_default_proof;
val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
val local_done_proof = Toplevel.proof Proof.local_done_proof;
--- a/src/Pure/Isar/proof.ML Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/Isar/proof.ML Mon Jul 20 13:52:27 2009 +0200
@@ -1002,6 +1002,7 @@
val _ = assert_backward state;
val (goal_ctxt, (_, goal)) = find_goal state;
val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
+ val goal_txt = prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt);
val _ = is_relevant state andalso error "Cannot fork relevant proof";
@@ -1017,13 +1018,13 @@
val result_ctxt =
state
- |> map_contexts (Variable.declare_term prop)
+ |> map_contexts (fold Variable.declare_term goal_txt)
|> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
|> fork_proof;
val future_thm = result_ctxt |> Future.map (fn (_, x) =>
ProofContext.get_fact_single (get_context x) (Facts.named this_name));
- val finished_goal = exception_trace (fn () => Goal.future_result goal_ctxt future_thm prop');
+ val finished_goal = Goal.future_result goal_ctxt future_thm prop';
val state' =
state
|> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
@@ -1043,9 +1044,9 @@
local
fun future_terminal_proof proof1 proof2 meths int state =
- if int orelse is_relevant state orelse not (Goal.future_enabled ())
+ if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
then proof1 meths state
- else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
+ else snd (proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))) state);
in
--- a/src/Pure/ProofGeneral/preferences.ML Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Mon Jul 20 13:52:27 2009 +0200
@@ -84,6 +84,12 @@
fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
+val parallel_proof_pref =
+ let
+ fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1);
+ fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0);
+ in mkpref get set PgipTypes.Pgipbool "parallel-proofs" "Check proofs in parallel" end;
+
val thm_depsN = "thm_deps";
val thm_deps_pref =
let
@@ -171,9 +177,7 @@
nat_pref Multithreading.max_threads
"max-threads"
"Maximum number of threads",
- bool_pref Goal.parallel_proofs
- "parallel-proofs"
- "Check proofs in parallel"];
+ parallel_proof_pref];
val pure_preferences =
[(category_display, display_preferences),
--- a/src/Pure/System/session.ML Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/System/session.ML Mon Jul 20 13:52:27 2009 +0200
@@ -11,7 +11,7 @@
val welcome: unit -> string
val use_dir: string -> string -> bool -> string list -> bool -> bool ->
string -> bool -> string list -> string -> string -> bool * string ->
- string -> int -> bool -> bool -> int -> int -> bool -> unit
+ string -> int -> bool -> bool -> int -> int -> int -> unit
val finish: unit -> unit
end;
--- a/src/Pure/Thy/thy_info.ML Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Jul 20 13:52:27 2009 +0200
@@ -350,7 +350,7 @@
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 par_proofs = ! parallel_proofs;
+ val par_proofs = ! parallel_proofs >= 1;
fun fork (name, body) tab =
let
--- a/src/Pure/goal.ML Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/goal.ML Mon Jul 20 13:52:27 2009 +0200
@@ -6,7 +6,7 @@
signature BASIC_GOAL =
sig
- val parallel_proofs: bool ref
+ val parallel_proofs: int ref
val SELECT_GOAL: tactic -> int -> tactic
val CONJUNCTS: tactic -> int -> tactic
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -21,6 +21,7 @@
val finish: thm -> thm
val norm_result: thm -> thm
val future_enabled: unit -> bool
+ val local_future_enabled: unit -> bool
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 ->
@@ -95,10 +96,12 @@
(* future_enabled *)
-val parallel_proofs = ref true;
+val parallel_proofs = ref 1;
fun future_enabled () =
- Future.enabled () andalso ! parallel_proofs andalso is_some (Future.thread_data ());
+ Future.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
+
+fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
(* future_result *)
@@ -120,14 +123,15 @@
val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
val global_prop =
- Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop)));
+ cert (Term.map_types Logic.varifyT (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
+ |> Thm.weaken_sorts (Variable.sorts_of ctxt);
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.future global_result global_prop
|> Thm.instantiate (instT, [])
|> Drule.forall_elim_list fixes
|> fold (Thm.elim_implies o Thm.assume) assms;
--- a/src/Pure/proofterm.ML Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/proofterm.ML Mon Jul 20 13:52:27 2009 +0200
@@ -207,7 +207,8 @@
in ((oracle, true, failed), seen') end)
end);
in ((oracle orelse not (null oracles), unfinished, failed), seen) end;
- val (oracle, unfinished, failed) = #1 (fold status bodies ((false, false, false), Inttab.empty));
+ val (oracle, unfinished, failed) =
+ #1 (fold status bodies ((false, false, false), Inttab.empty));
in {oracle = oracle, unfinished = unfinished, failed = failed} end;
@@ -221,13 +222,14 @@
val all_oracles_of =
let
- fun collect (PBody {oracles, thms, ...}) = thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
- if Inttab.defined seen i then (x, seen)
- else
- let
- val body' = Future.join body;
- val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
- in (merge_oracles oracles x', seen') end);
+ fun collect (PBody {oracles, thms, ...}) =
+ thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
+ if Inttab.defined seen i then (x, seen)
+ else
+ let
+ val body' = Future.join body;
+ val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
+ in (merge_oracles oracles x', seen') end);
in fn body => #1 (collect body ([], Inttab.empty)) end;
fun approximate_proof_body prf =
@@ -292,7 +294,8 @@
| proof (OfClass (T, c)) = OfClass (typ T, c)
| proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
| proof (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts)
- | proof (PThm (i, ((a, prop, SOME Ts), body))) = PThm (i, ((a, prop, SOME (typs Ts)), body))
+ | proof (PThm (i, ((a, prop, SOME Ts), body))) =
+ PThm (i, ((a, prop, SOME (typs Ts)), body))
| proof _ = raise Same.SAME;
in Same.commit proof end;
@@ -332,7 +335,8 @@
| change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
| change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
| change_type opTs (Promise _) = error "change_type: unexpected promise"
- | change_type opTs (PThm (i, ((name, prop, _), body))) = PThm (i, ((name, prop, opTs), body))
+ | change_type opTs (PThm (i, ((name, prop, _), body))) =
+ PThm (i, ((name, prop, opTs), body))
| change_type _ prf = prf;
@@ -513,7 +517,8 @@
| subst' _ _ = raise Same.SAME
and substh' lev t = (subst' lev t handle Same.SAME => t);
- fun subst lev (AbsP (a, t, body)) = (AbsP (a, Same.map_option (subst' lev) t, substh lev body)
+ fun subst lev (AbsP (a, t, body)) =
+ (AbsP (a, Same.map_option (subst' lev) t, substh lev body)
handle Same.SAME => AbsP (a, t, subst lev body))
| subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body)
| subst lev (prf %% prf') = (subst lev prf %% substh lev prf'
--- a/src/Pure/pure_thy.ML Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/pure_thy.ML Mon Jul 20 13:52:27 2009 +0200
@@ -59,11 +59,11 @@
structure FactsData = TheoryDataFun
(
- type T = Facts.T * (unit lazy list * Task_Queue.group list);
- val empty = (Facts.empty, ([], []));
+ type T = Facts.T * (unit lazy list * Task_Queue.group Inttab.table);
+ val empty = (Facts.empty, ([], Inttab.empty));
val copy = I;
- fun extend (facts, _) = (facts, ([], []));
- fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
+ fun extend (facts, _) = (facts, ([], Inttab.empty));
+ fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], Inttab.empty));
);
@@ -84,7 +84,9 @@
fun join_proofs thy =
map_filter (Exn.get_exn o Lazy.force_result) (rev (#1 (#2 (FactsData.get thy))));
-fun cancel_proofs thy = List.app Future.cancel_group (#2 (#2 (FactsData.get thy)));
+fun cancel_proofs thy =
+ Inttab.fold (fn (_, group) => fn () => Future.cancel_group group)
+ (#2 (#2 (FactsData.get thy))) ();
@@ -144,9 +146,14 @@
(* enter_thms *)
+val pending_groups =
+ Thm.promises_of #> fold (fn (_, future) =>
+ if Future.is_finished future then I
+ else Inttab.update (`Task_Queue.group_id (Future.group_of future)));
+
fun enter_proofs (thy, thms) =
(FactsData.map (apsnd (fn (proofs, groups) =>
- (fold (cons o lazy_proof) thms proofs, fold Thm.pending_groups thms groups))) thy, thms);
+ (fold (cons o lazy_proof) thms proofs, fold pending_groups thms groups))) thy, thms);
fun enter_thms pre_name post_name app_att (b, thms) thy =
if Binding.is_empty b
--- a/src/Pure/thm.ML Mon Jul 20 09:52:09 2009 +0200
+++ b/src/Pure/thm.ML Mon Jul 20 13:52:27 2009 +0200
@@ -141,12 +141,12 @@
val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
val rename_boundvars: term -> term -> thm -> thm
- val future: thm future -> cterm -> thm
- val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
- val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
val join_proof: thm -> unit
+ val promises_of: thm -> (serial * thm future) list
+ val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
+ val future: thm future -> cterm -> thm
val get_name: thm -> string
val put_name: string -> thm -> thm
val extern_oracles: theory -> xstring list
@@ -345,9 +345,7 @@
tpairs: (term * term) list, (*flex-flex pairs*)
prop: term} (*conclusion*)
and deriv = Deriv of
- {max_promise: serial,
- open_promises: (serial * thm future) OrdList.T,
- promises: (serial * thm future) OrdList.T,
+ {promises: (serial * thm future) OrdList.T,
body: Pt.proof_body};
type conv = cterm -> thm;
@@ -504,11 +502,10 @@
(** derivations **)
-fun make_deriv max_promise open_promises promises oracles thms proof =
- Deriv {max_promise = max_promise, open_promises = open_promises, promises = promises,
- body = PBody {oracles = oracles, thms = thms, proof = proof}};
+fun make_deriv promises oracles thms proof =
+ Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
-val empty_deriv = make_deriv ~1 [] [] [] [] Pt.MinProof;
+val empty_deriv = make_deriv [] [] [] Pt.MinProof;
(* inference rules *)
@@ -516,13 +513,9 @@
fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
fun deriv_rule2 f
- (Deriv {max_promise = max1, open_promises = open_ps1, promises = ps1,
- body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
- (Deriv {max_promise = max2, open_promises = open_ps2, promises = ps2,
- body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
+ (Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
+ (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
let
- val max = Int.max (max1, max2);
- val open_ps = OrdList.union promise_ord open_ps1 open_ps2;
val ps = OrdList.union promise_ord ps1 ps2;
val oras = Pt.merge_oracles oras1 oras2;
val thms = Pt.merge_thms thms1 thms2;
@@ -532,10 +525,10 @@
| 1 => MinProof
| 0 => MinProof
| i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
- in make_deriv max open_ps ps oras thms prf end;
+ in make_deriv ps oras thms prf end;
fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
-fun deriv_rule0 prf = deriv_rule1 I (make_deriv ~1 [] [] [] [] prf);
+fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
@@ -1614,6 +1607,36 @@
(*** Future theorems -- proofs with promises ***)
+(* fulfilled proofs *)
+
+fun raw_body (Thm (Deriv {body, ...}, _)) = body;
+
+fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
+ let val ps = map (apsnd (fulfill_body o Future.join)) promises
+ in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
+
+fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
+val proof_of = Pt.proof_of o proof_body_of;
+val join_proof = ignore o proof_body_of;
+
+
+(* derivation status *)
+
+fun promises_of (Thm (Deriv {promises, ...}, _)) = promises;
+
+fun status_of (Thm (Deriv {promises, body}, _)) =
+ let
+ val ps = map (Future.peek o snd) promises;
+ val bodies = body ::
+ map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
+ val {oracle, unfinished, failed} = Pt.status_of bodies;
+ in
+ {oracle = oracle,
+ unfinished = unfinished orelse exists is_none ps,
+ failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
+ end;
+
+
(* future rule *)
fun future_result i orig_thy orig_shyps orig_prop raw_thm =
@@ -1623,12 +1646,13 @@
val _ = Theory.check_thy orig_thy;
fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
- val Thm (Deriv {max_promise, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
+ val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
val _ = prop aconv orig_prop orelse err "bad prop";
val _ = null tpairs orelse err "bad tpairs";
val _ = null hyps orelse err "bad hyps";
val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
- val _ = max_promise < i orelse err "bad dependencies";
+ val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
+ val _ = List.app (ignore o fulfill_body o Future.join o #2) promises;
in thm end;
fun future future_thm ct =
@@ -1639,9 +1663,8 @@
val i = serial ();
val future = future_thm |> Future.map (future_result i thy sorts prop);
- val promise = (i, future);
in
- Thm (make_deriv i [promise] [promise] [] [] (Pt.promise_proof thy i prop),
+ Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop),
{thy_ref = thy_ref,
tags = [],
maxidx = maxidx,
@@ -1652,57 +1675,21 @@
end;
-(* derivation status *)
-
-fun raw_proof_body_of (Thm (Deriv {body, ...}, _)) = body;
-val raw_proof_of = Proofterm.proof_of o raw_proof_body_of;
-
-fun pending_groups (Thm (Deriv {open_promises, ...}, _)) =
- fold (insert Task_Queue.eq_group o Future.group_of o #2) open_promises;
-
-fun status_of (Thm (Deriv {promises, body, ...}, _)) =
- let
- val ps = map (Future.peek o snd) promises;
- val bodies = body ::
- map_filter (fn SOME (Exn.Result th) => SOME (raw_proof_body_of th) | _ => NONE) ps;
- val {oracle, unfinished, failed} = Pt.status_of bodies;
- in
- {oracle = oracle,
- unfinished = unfinished orelse exists is_none ps,
- failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
- end;
-
-
-(* fulfilled proofs *)
-
-fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
- let
- val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));
- val ps = map (apsnd (raw_proof_body_of o Future.join)) promises;
- in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
-
-val proof_of = Proofterm.proof_of o proof_body_of;
-val join_proof = ignore o proof_body_of;
-
-
(* closed derivations with official name *)
fun get_name thm =
- Pt.get_name (hyps_of thm) (prop_of thm) (raw_proof_of thm);
+ Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
fun put_name name (thm as Thm (der, args)) =
let
- val Deriv {max_promise, open_promises, promises, body, ...} = der;
+ val Deriv {promises, body} = der;
val {thy_ref, hyps, prop, tpairs, ...} = args;
val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
val ps = map (apsnd (Future.map proof_body_of)) promises;
val thy = Theory.deref thy_ref;
val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
-
- val open_promises' = open_promises |> filter (fn (_, p) =>
- (case Future.peek p of SOME (Exn.Result _) => false | _ => true));
- val der' = make_deriv max_promise open_promises' [] [] [pthm] proof;
+ val der' = make_deriv [] [] [pthm] proof;
val _ = Theory.check_thy thy;
in Thm (der', args) end;
@@ -1718,7 +1705,7 @@
raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
else
let val (ora, prf) = Pt.oracle_proof name prop in
- Thm (make_deriv ~1 [] [] [ora] [] prf,
+ Thm (make_deriv [] [ora] [] prf,
{thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
tags = [],
maxidx = maxidx,