--- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Thu Jun 22 21:48:57 2017 +0200
@@ -959,7 +959,7 @@
| SOME {vcs, path, ...} =>
let
val (proved, unproved) = partition_vcs vcs;
- val _ = List.app Thm.consolidate (maps (#2 o snd) proved);
+ val _ = Thm.consolidate (maps (#2 o snd) proved);
val (proved', proved'') =
List.partition (fn (_, (_, thms, _, _)) =>
exists (#oracle o Thm.peek_status) thms) proved;
--- a/src/Pure/Concurrent/cache.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Concurrent/cache.ML Thu Jun 22 21:48:57 2017 +0200
@@ -23,7 +23,7 @@
(case lookup tab x of
SOME y => (y, tab)
| NONE =>
- let val y = Lazy.lazy (fn () => f x)
+ let val y = Lazy.lazy_name "cache" (fn () => f x)
in (y, update (x, y) tab) end))
|> Lazy.force;
in apply end;
--- a/src/Pure/Concurrent/event_timer.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Concurrent/event_timer.ML Thu Jun 22 21:48:57 2017 +0200
@@ -148,7 +148,7 @@
let
val req: request Single_Assignment.var = Single_Assignment.var "request";
fun abort () = ignore (cancel (Single_Assignment.await req));
- val promise: unit future = Future.promise abort;
+ val promise: unit future = Future.promise_name "event_timer" abort;
val _ = Single_Assignment.assign req (request time (Future.fulfill promise));
in promise end);
--- a/src/Pure/Concurrent/future.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Concurrent/future.ML Thu Jun 22 21:48:57 2017 +0200
@@ -37,7 +37,7 @@
val value: 'a -> 'a future
val cond_forks: params -> (unit -> 'a) list -> 'a future list
val map: ('a -> 'b) -> 'a future -> 'b future
- val promise_group: group -> (unit -> unit) -> 'a future
+ val promise_name: string -> (unit -> unit) -> 'a future
val promise: (unit -> unit) -> 'a future
val fulfill_result: 'a future -> 'a Exn.result -> unit
val fulfill: 'a future -> 'a -> unit
@@ -599,8 +599,9 @@
(* promised futures -- fulfilled by external means *)
-fun promise_group group abort : 'a future =
+fun promise_name name abort : 'a future =
let
+ val group = worker_subgroup ();
val result = Single_Assignment.var "promise" : 'a result;
fun assign () = assign_result group result Exn.interrupt_exn
handle Fail _ => true
@@ -612,10 +613,10 @@
Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
(fn _ => Exn.release (Exn.capture assign () before abort ()));
val task = SYNCHRONIZED "enqueue_passive" (fn () =>
- Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
+ Unsynchronized.change_result queue (Task_Queue.enqueue_passive group name job));
in Future {promised = true, task = task, result = result} end;
-fun promise abort = promise_group (worker_subgroup ()) abort;
+fun promise abort = promise_name "passive" abort;
fun fulfill_result (Future {promised, task, result}) res =
if not promised then raise Fail "Not a promised future"
--- a/src/Pure/Concurrent/lazy.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Concurrent/lazy.ML Thu Jun 22 21:48:57 2017 +0200
@@ -9,6 +9,7 @@
signature LAZY =
sig
type 'a lazy
+ val lazy_name: string -> (unit -> 'a) -> 'a lazy
val lazy: (unit -> 'a) -> 'a lazy
val value: 'a -> 'a lazy
val peek: 'a lazy -> 'a Exn.result option
@@ -16,6 +17,7 @@
val is_finished: 'a lazy -> bool
val force_result: 'a lazy -> 'a Exn.result
val force: 'a lazy -> 'a
+ val force_list: 'a lazy list -> 'a list
val map: ('a -> 'b) -> 'a lazy -> 'b lazy
val future: Future.params -> 'a lazy -> 'a future
end;
@@ -26,13 +28,14 @@
(* datatype *)
datatype 'a expr =
- Expr of unit -> 'a |
+ Expr of string * (unit -> 'a) |
Result of 'a future;
abstype 'a lazy = Lazy of 'a expr Synchronized.var
with
-fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
+fun lazy_name name e = Lazy (Synchronized.var "lazy" (Expr (name, e)));
+fun lazy e = lazy_name "lazy" e;
fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
fun peek (Lazy var) =
@@ -40,6 +43,12 @@
Expr _ => NONE
| Result res => Future.peek res);
+fun pending (Lazy var) =
+ (case Synchronized.value var of
+ Expr _ => true
+ | Result _ => false);
+
+
(* status *)
@@ -65,13 +74,13 @@
let
val (expr, x) =
Synchronized.change_result var
- (fn Expr e =>
- let val x = Future.promise I
- in ((SOME e, x), Result x) end
+ (fn Expr (name, e) =>
+ let val x = Future.promise_name name I
+ in ((SOME (name, e), x), Result x) end
| Result x => ((NONE, x), Result x));
in
(case expr of
- SOME e =>
+ SOME (name, e) =>
let
val res0 = Exn.capture (restore_attributes e) ();
val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
@@ -80,7 +89,7 @@
interrupt, until there is a fresh start*)
val _ =
if Exn.is_interrupt_exn res then
- Synchronized.change var (fn _ => Expr e)
+ Synchronized.change var (fn _ => Expr (name, e))
else ();
in res end
| NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
@@ -89,8 +98,13 @@
end;
-fun force r = Exn.release (force_result r);
-fun map f x = lazy (fn () => f (force x));
+fun force x = Exn.release (force_result x);
+
+fun force_list xs =
+ (List.app (fn x => if pending x then ignore (force_result x) else ()) xs;
+ map force xs);
+
+fun map f x = lazy_name "Lazy.map" (fn () => f (force x));
(* future evaluation *)
--- a/src/Pure/Concurrent/task_queue.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Thu Jun 22 21:48:57 2017 +0200
@@ -37,7 +37,7 @@
val cancel_all: queue -> group list * Thread.thread list
val finish: task -> queue -> bool * queue
val enroll: Thread.thread -> string -> group -> queue -> task * queue
- val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
+ val enqueue_passive: group -> string -> (unit -> bool) -> queue -> task * queue
val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
val extend: task -> (bool -> bool) -> queue -> queue option
val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
@@ -312,9 +312,9 @@
(* enqueue *)
-fun enqueue_passive group abort (Queue {groups, jobs, urgent}) =
+fun enqueue_passive group name abort (Queue {groups, jobs, urgent}) =
let
- val task = new_task group "passive" NONE;
+ val task = new_task group name NONE;
val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
in (task, make_queue groups' jobs' urgent) end;
--- a/src/Pure/Isar/code.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Isar/code.ML Thu Jun 22 21:48:57 2017 +0200
@@ -142,7 +142,7 @@
"\nof constant " ^ quote c ^
"\nis too specific compared to declared type\n" ^
string_of_typ thy ty_decl)
- end;
+ end;
fun check_const thy = check_unoverload thy o check_bare_const thy;
@@ -411,7 +411,7 @@
fun get_abstype_spec thy tyco = case get_type_entry thy tyco
of SOME (vs, Abstractor spec) => (vs, spec)
| _ => error ("Not an abstract type: " ^ tyco);
-
+
fun get_type_of_constr_or_abstr thy c =
case (body_type o const_typ thy) c
of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
@@ -463,7 +463,7 @@
^ "\nof constant " ^ quote c
^ "\nis too specific compared to declared type\n"
^ string_of_typ thy ty_decl)
- end;
+ end;
fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) =
let
@@ -760,7 +760,7 @@
fun nothing_cert ctxt c = Nothing (dummy_thm ctxt c);
fun cert_of_eqns ctxt c [] = Equations (dummy_thm ctxt c, [])
- | cert_of_eqns ctxt c raw_eqns =
+ | cert_of_eqns ctxt c raw_eqns =
let
val thy = Proof_Context.theory_of ctxt;
val eqns = burrow_fst (canonize_thms thy) raw_eqns;
@@ -1104,7 +1104,7 @@
let
val thm = Thm.close_derivation raw_thm;
val c = const_eqn thy thm;
- fun update_subsume verbose (thm, proper) eqns =
+ fun update_subsume verbose (thm, proper) eqns =
let
val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
@@ -1118,13 +1118,13 @@
else false
end;
fun drop (thm', proper') = if (proper orelse not proper')
- andalso matches_args (args_of thm') then
+ andalso matches_args (args_of thm') then
(if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
Thm.string_of_thm_global thy thm') else (); true)
else false;
in (thm, proper) :: filter_out drop eqns end;
fun natural_order eqns =
- (eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns []))
+ (eqns, Lazy.lazy_name "code" (fn () => fold (update_subsume false) eqns []))
fun add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)])
| add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
(*this restores the natural order and drops syntactic redundancies*)
--- a/src/Pure/Isar/toplevel.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Isar/toplevel.ML Thu Jun 22 21:48:57 2017 +0200
@@ -648,14 +648,10 @@
val get_result = Result.get o Proof.context_of;
val put_result = Proof.map_context o Result.put;
-fun timing_estimate include_head elem =
- let val trs = Thy_Syntax.flat_element elem |> not include_head ? tl
+fun timing_estimate elem =
+ let val trs = tl (Thy_Syntax.flat_element elem)
in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
-fun priority estimate =
- if estimate = Time.zeroTime then ~1
- else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
-
fun proof_future_enabled estimate st =
(case try proof_of st of
NONE => false
@@ -670,8 +666,7 @@
val st' =
if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
(Execution.fork
- {name = "Toplevel.diag", pos = pos_of tr,
- pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
+ {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
(fn () => command tr st); st)
else command tr st;
in (Result (tr, st'), st') end;
@@ -683,7 +678,7 @@
let
val (head_result, st') = atom_result keywords head_tr st;
val (body_elems, end_tr) = element_rest;
- val estimate = timing_estimate false elem;
+ val estimate = timing_estimate elem;
in
if not (proof_future_enabled estimate st')
then
@@ -698,7 +693,7 @@
val future_proof =
Proof.future_proof (fn state =>
Execution.fork
- {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = priority estimate}
+ {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1}
(fn () =>
let
val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
--- a/src/Pure/PIDE/active.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/PIDE/active.ML Thu Jun 22 21:48:57 2017 +0200
@@ -49,7 +49,7 @@
let
val i = serial ();
fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
- val promise = Future.promise abort : string future;
+ val promise = Future.promise_name "dialog" abort : string future;
val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
in (result_markup, promise) end;
--- a/src/Pure/PIDE/command.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/PIDE/command.ML Thu Jun 22 21:48:57 2017 +0200
@@ -264,7 +264,7 @@
(fn () =>
read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
in eval_state keywords span tr eval_state0 end;
- in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
+ in Eval {exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process} end;
end;
@@ -322,7 +322,7 @@
in
Print {
name = name, args = args, delay = delay, pri = pri, persistent = persistent,
- exec_id = exec_id, print_process = Lazy.lazy process}
+ exec_id = exec_id, print_process = Lazy.lazy_name "Command.print" process}
end;
fun bad_print name args exn =
--- a/src/Pure/PIDE/document.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/PIDE/document.ML Thu Jun 22 21:48:57 2017 +0200
@@ -371,7 +371,7 @@
let
val id = Document_ID.print command_id;
val span =
- Lazy.lazy (fn () =>
+ Lazy.lazy_name "Document.define_command" (fn () =>
Position.setmp_thread_data (Position.id_only id)
(fn () =>
let
--- a/src/Pure/Syntax/syntax.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Syntax/syntax.ML Thu Jun 22 21:48:57 2017 +0200
@@ -540,7 +540,7 @@
else
let
val input' = new_xprods2 @ input1;
- val gram' = Lazy.lazy (fn () => Parser.make_gram input');
+ val gram' = Lazy.lazy_name "Syntax.merge_syntax" (fn () => Parser.make_gram input');
in (input', gram') end);
in
Syntax
--- a/src/Pure/System/invoke_scala.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/System/invoke_scala.ML Thu Jun 22 21:48:57 2017 +0200
@@ -31,7 +31,7 @@
let
val id = new_id ();
fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
- val promise = Future.promise abort : string future;
+ val promise = Future.promise_name "invoke_scala" abort : string future;
val _ = Synchronized.change promises (Symtab.update (id, promise));
val _ = Output.protocol_message (Markup.invoke_scala name id) [arg];
in promise end;
--- a/src/Pure/more_thm.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/more_thm.ML Thu Jun 22 21:48:57 2017 +0200
@@ -645,7 +645,7 @@
Proofs.map (fold (cons o Thm.trim_context) more_thms);
fun consolidate_theory thy =
- List.app (Thm.consolidate o Thm.transfer thy) (rev (Proofs.get thy));
+ Thm.consolidate (map (Thm.transfer thy) (rev (Proofs.get thy)));
--- a/src/Pure/proofterm.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/proofterm.ML Thu Jun 22 21:48:57 2017 +0200
@@ -43,7 +43,7 @@
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
proof_body list -> 'a -> 'a
- val consolidate: proof_body -> unit
+ val consolidate: proof_body list -> unit
val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
val oracle_ord: oracle * oracle -> order
@@ -197,15 +197,16 @@
fun join_thms (thms: pthm list) =
Future.joins (map (thm_node_body o #2) thms);
-fun consolidate (PBody {thms, ...}) =
- List.app (Lazy.force o thm_node_consolidate o #2) thms;
+val consolidate =
+ maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
+ #> Lazy.force_list #> ignore;
fun make_thm_node name prop body =
Thm_Node {name = name, prop = prop, body = body,
consolidate =
- Lazy.lazy (fn () =>
+ Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
let val PBody {thms, ...} = Future.join body
- in List.app consolidate (join_thms thms) end)};
+ in consolidate (join_thms thms) end)};
(***** proof atoms *****)
@@ -1530,8 +1531,7 @@
fun fulfill_norm_proof thy ps body0 =
let
- val _ = List.app (consolidate o #2) ps;
- val _ = consolidate body0;
+ val _ = consolidate (map #2 ps @ [body0]);
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
val oracles =
unions_oracles
--- a/src/Pure/thm.ML Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/thm.ML Thu Jun 22 21:48:57 2017 +0200
@@ -86,7 +86,7 @@
val proof_bodies_of: thm list -> proof_body list
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
- val consolidate: thm -> unit
+ val consolidate: thm list -> unit
val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
val future: thm future -> cterm -> thm
val derivation_closed: thm -> bool
@@ -598,7 +598,7 @@
val proof_body_of = singleton proof_bodies_of;
val proof_of = Proofterm.proof_of o proof_body_of;
-val consolidate = ignore o proof_bodies_of o single;
+val consolidate = ignore o proof_bodies_of;
(* derivation status *)