--- a/Admin/polyml/future/ROOT.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/Admin/polyml/future/ROOT.ML Thu Aug 18 23:43:22 2011 +0200
@@ -78,6 +78,7 @@
use "General/table.ML";
use "General/graph.ML";
use "General/ord_list.ML";
+use "General/balanced_tree.ML";
structure Position =
struct
--- a/src/HOL/Unix/Nested_Environment.thy Thu Aug 18 14:08:39 2011 -0700
+++ b/src/HOL/Unix/Nested_Environment.thy Thu Aug 18 23:43:22 2011 +0200
@@ -518,7 +518,8 @@
qed
qed
-text {* Environments and code generation *}
+
+subsection {* Code generation *}
lemma [code, code del]:
"(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
@@ -526,39 +527,37 @@
lemma equal_env_code [code]:
fixes x y :: "'a\<Colon>equal"
and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
- shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
- HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z
- of None \<Rightarrow> (case g z
- of None \<Rightarrow> True | Some _ \<Rightarrow> False)
- | Some a \<Rightarrow> (case g z
- of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
+ shows
+ "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
+ HOL.equal x y \<and> (\<forall>z \<in> UNIV.
+ case f z of
+ None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
+ | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
proof (unfold equal)
- have "f = g \<longleftrightarrow> (\<forall>z. case f z
- of None \<Rightarrow> (case g z
- of None \<Rightarrow> True | Some _ \<Rightarrow> False)
- | Some a \<Rightarrow> (case g z
- of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")
+ have "f = g \<longleftrightarrow>
+ (\<forall>z. case f z of
+ None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
+ | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs by (auto split: option.splits)
next
- assume assm: ?rhs (is "\<forall>z. ?prop z")
+ assume ?rhs (is "\<forall>z. ?prop z")
show ?lhs
proof
fix z
- from assm have "?prop z" ..
+ from `?rhs` have "?prop z" ..
then show "f z = g z" by (auto split: option.splits)
qed
qed
then show "Env x f = Env y g \<longleftrightarrow>
- x = y \<and> (\<forall>z\<in>UNIV. case f z
- of None \<Rightarrow> (case g z
- of None \<Rightarrow> True | Some _ \<Rightarrow> False)
- | Some a \<Rightarrow> (case g z
- of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
+ x = y \<and> (\<forall>z\<in>UNIV.
+ case f z of
+ None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
+ | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
qed simp_all
lemma [code nbe]:
@@ -566,6 +565,8 @@
by (fact equal_refl)
lemma [code, code del]:
- "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
+ "(Code_Evaluation.term_of ::
+ ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) =
+ Code_Evaluation.term_of" ..
end
--- a/src/Pure/Concurrent/future.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/Concurrent/future.ML Thu Aug 18 23:43:22 2011 +0200
@@ -1,19 +1,15 @@
(* Title: Pure/Concurrent/future.ML
Author: Makarius
-Future values, see also
+Value-oriented parallelism via futures and promises. See also
http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf
Notes:
* Futures are similar to delayed evaluation, i.e. delay/force is
- generalized to fork/join (and variants). The idea is to model
- parallel value-oriented computations, but *not* communicating
- processes.
-
- * Futures are grouped; failure of one group member causes the whole
- group to be interrupted eventually. Groups are block-structured.
+ generalized to fork/join. The idea is to model parallel
+ value-oriented computations (not communicating processes).
* Forked futures are evaluated spontaneously by a farm of worker
threads in the background; join resynchronizes the computation and
@@ -21,13 +17,23 @@
* The pool of worker threads is limited, usually in correlation with
the number of physical cores on the machine. Note that allocation
- of runtime resources is distorted either if workers yield CPU time
- (e.g. via system sleep or wait operations), or if non-worker
+ of runtime resources may be distorted either if workers yield CPU
+ time (e.g. via system sleep or wait operations), or if non-worker
threads contend for significant runtime resources independently.
+ There is a limited number of replacement worker threads that get
+ activated in certain explicit wait conditions.
- * Promised futures are fulfilled by external means. There is no
- associated evaluation task, but other futures can depend on them
- as usual.
+ * Future tasks are organized in groups, which are block-structured.
+ When forking a new new task, the default is to open an individual
+ subgroup, unless some common group is specified explicitly.
+ Failure of one group member causes the immediate peers to be
+ interrupted eventually (i.e. none by default). Interrupted tasks
+ that lack regular result information, will pick up parallel
+ exceptions from the cumulative group context (as Par_Exn).
+
+ * Promised "passive" futures are fulfilled by external means. There
+ is no associated evaluation task, but other futures can depend on
+ them via regular join operations.
*)
signature FUTURE =
--- a/src/Pure/Concurrent/par_exn.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/Concurrent/par_exn.ML Thu Aug 18 23:43:22 2011 +0200
@@ -24,40 +24,44 @@
SOME i => (i, exn)
| NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
-val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial);
+val the_serial = the o get_exn_serial;
+
+val exn_ord = rev_order o int_ord o pairself the_serial;
(* parallel exceptions *)
-exception Par_Exn of exn Ord_List.T;
+exception Par_Exn of exn list;
+ (*non-empty list with unique identified elements sorted by exn_ord;
+ no occurrences of Par_Exn or Exn.Interrupt*)
-fun par_exns (Par_Exn exns) = SOME exns
- | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (serial exn)];
+fun par_exns (Par_Exn exns) = exns
+ | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
fun make exns =
- (case map_filter par_exns exns of
+ (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
[] => Exn.Interrupt
- | e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es)));
+ | es => Par_Exn es);
-fun dest (Par_Exn exns) = SOME (rev exns)
- | dest _ = NONE;
+fun dest (Par_Exn exns) = SOME exns
+ | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
(* parallel results *)
-fun all_res results = forall (fn Exn.Res _ => true | _ => false) results;
+fun release_all results =
+ if forall (fn Exn.Res _ => true | _ => false) results
+ then map Exn.release results
+ else raise make (map_filter Exn.get_exn results);
-fun release_all results =
- if all_res results then map Exn.release results
- else raise make (map_filter Exn.get_exn results);
+fun plain_exn (Exn.Res _) = NONE
+ | plain_exn (Exn.Exn (Par_Exn _)) = NONE
+ | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn;
fun release_first results =
- if all_res results then map Exn.release results
- else
- (case get_first
- (fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of
- NONE => Exn.interrupt ()
- | SOME exn => reraise exn);
+ (case get_first plain_exn results of
+ NONE => release_all results
+ | SOME exn => reraise exn);
end;
--- a/src/Pure/Concurrent/par_list.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/Concurrent/par_list.ML Thu Aug 18 23:43:22 2011 +0200
@@ -16,6 +16,7 @@
signature PAR_LIST =
sig
+ val managed_results: string -> ('a -> 'b) -> 'a list -> 'b Exn.result list
val map_name: string -> ('a -> 'b) -> 'a list -> 'b list
val map: ('a -> 'b) -> 'a list -> 'b list
val get_some: ('a -> 'b option) -> 'a list -> 'b option
--- a/src/Pure/Concurrent/par_list_sequential.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/Concurrent/par_list_sequential.ML Thu Aug 18 23:43:22 2011 +0200
@@ -7,6 +7,7 @@
structure Par_List: PAR_LIST =
struct
+fun managed_results _ f = map (Exn.capture f);
fun map_name _ = map;
val map = map;
val get_some = get_first;
--- a/src/Pure/General/output.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/General/output.ML Thu Aug 18 23:43:22 2011 +0200
@@ -31,13 +31,14 @@
val urgent_message_fn: (output -> unit) Unsynchronized.ref
val tracing_fn: (output -> unit) Unsynchronized.ref
val warning_fn: (output -> unit) Unsynchronized.ref
- val error_fn: (output -> unit) Unsynchronized.ref
+ val error_fn: (serial * output -> unit) Unsynchronized.ref
val prompt_fn: (output -> unit) Unsynchronized.ref
val status_fn: (output -> unit) Unsynchronized.ref
val report_fn: (output -> unit) Unsynchronized.ref
val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
end
val urgent_message: string -> unit
+ val error_msg': serial * string -> unit
val error_msg: string -> unit
val prompt: string -> unit
val status: string -> unit
@@ -92,7 +93,8 @@
val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
- val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
+ val error_fn =
+ Unsynchronized.ref (fn (_: serial, s) => raw_stdout (suffix "\n" (prefix_lines "*** " s)));
val prompt_fn = Unsynchronized.ref raw_stdout;
val status_fn = Unsynchronized.ref (fn _: output => ());
val report_fn = Unsynchronized.ref (fn _: output => ());
@@ -104,7 +106,8 @@
fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
fun tracing s = ! Private_Hooks.tracing_fn (output s);
fun warning s = ! Private_Hooks.warning_fn (output s);
-fun error_msg s = ! Private_Hooks.error_fn (output s);
+fun error_msg' (i, s) = ! Private_Hooks.error_fn (i, output s);
+fun error_msg s = error_msg' (serial (), s);
fun prompt s = ! Private_Hooks.prompt_fn (output s);
fun status s = ! Private_Hooks.status_fn (output s);
fun report s = ! Private_Hooks.report_fn (output s);
--- a/src/Pure/Isar/runtime.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/Isar/runtime.ML Thu Aug 18 23:43:22 2011 +0200
@@ -12,7 +12,7 @@
exception TOPLEVEL_ERROR
val debug: bool Unsynchronized.ref
val exn_context: Proof.context option -> exn -> exn
- val exn_messages: (exn -> Position.T) -> exn -> string list
+ val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
val exn_message: (exn -> Position.T) -> exn -> string
val debugging: ('a -> 'b) -> 'a -> 'b
val controlled_execution: ('a -> 'b) -> 'a -> 'b
@@ -57,47 +57,55 @@
val detailed = ! debug;
- fun exn_msgs context exn =
- if Exn.is_interrupt exn then []
- else
- (case Par_Exn.dest exn of
- SOME exns => maps (exn_msgs context) exns
- | NONE =>
+ fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
+ | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
+ | flatten context exn =
+ (case Par_Exn.dest exn of
+ SOME exns => maps (flatten context) exns
+ | NONE => [(context, Par_Exn.serial exn)]);
+
+ fun exn_msgs (context, (i, exn)) =
+ (case exn of
+ EXCURSION_FAIL (exn, loc) =>
+ map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
+ (sorted_msgs context exn)
+ | _ =>
+ let
+ val msg =
(case exn of
- Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
- | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
- | EXCURSION_FAIL (exn, loc) =>
- map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc))
- (exn_msgs context exn)
- | TERMINATE => ["Exit"]
- | TimeLimit.TimeOut => ["Timeout"]
- | TOPLEVEL_ERROR => ["Error"]
- | ERROR msg => [msg]
- | Fail msg => [raised exn "Fail" [msg]]
+ TERMINATE => "Exit"
+ | TimeLimit.TimeOut => "Timeout"
+ | TOPLEVEL_ERROR => "Error"
+ | ERROR msg => msg
+ | Fail msg => raised exn "Fail" [msg]
| THEORY (msg, thys) =>
- [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
+ raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
| Ast.AST (msg, asts) =>
- [raised exn "AST" (msg ::
- (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
+ raised exn "AST" (msg ::
+ (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))
| TYPE (msg, Ts, ts) =>
- [raised exn "TYPE" (msg ::
+ raised exn "TYPE" (msg ::
(if detailed then
if_context context Syntax.string_of_typ Ts @
if_context context Syntax.string_of_term ts
- else []))]
+ else []))
| TERM (msg, ts) =>
- [raised exn "TERM" (msg ::
- (if detailed then if_context context Syntax.string_of_term ts else []))]
+ raised exn "TERM" (msg ::
+ (if detailed then if_context context Syntax.string_of_term ts else []))
| THM (msg, i, thms) =>
- [raised exn ("THM " ^ string_of_int i) (msg ::
- (if detailed then if_context context Display.string_of_thm thms else []))]
- | _ => [raised exn (General.exnMessage exn) []]));
- in exn_msgs NONE e end;
+ raised exn ("THM " ^ string_of_int i) (msg ::
+ (if detailed then if_context context Display.string_of_thm thms else []))
+ | _ => raised exn (General.exnMessage exn) []);
+ in [(i, msg)] end)
+ and sorted_msgs context exn =
+ sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
+
+ in sorted_msgs NONE e end;
fun exn_message exn_position exn =
(case exn_messages exn_position exn of
[] => "Interrupt"
- | msgs => cat_lines msgs);
+ | msgs => cat_lines (map snd msgs));
(** controlled execution **)
--- a/src/Pure/Isar/toplevel.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/Isar/toplevel.ML Thu Aug 18 23:43:22 2011 +0200
@@ -84,7 +84,7 @@
val unknown_context: transition -> transition
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
val status: transition -> Markup.T -> unit
- val error_msg: transition -> string -> unit
+ val error_msg: transition -> serial * string -> unit
val add_hook: (transition -> state -> state -> unit) -> unit
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val command: transition -> state -> state
@@ -567,7 +567,7 @@
setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
fun error_msg tr msg =
- setmp_thread_position tr (fn () => Output.error_msg msg) ();
+ setmp_thread_position tr (fn () => Output.error_msg' msg) ();
(* post-transition hooks *)
--- a/src/Pure/ML/ml_compiler.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/ML/ml_compiler.ML Thu Aug 18 23:43:22 2011 +0200
@@ -7,7 +7,7 @@
signature ML_COMPILER =
sig
val exn_position: exn -> Position.T
- val exn_messages: exn -> string list
+ val exn_messages: exn -> (serial * string) list
val exn_message: exn -> string
val eval: bool -> Position.T -> ML_Lex.token list -> unit
end
--- a/src/Pure/PIDE/document.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/PIDE/document.ML Thu Aug 18 23:43:22 2011 +0200
@@ -264,11 +264,11 @@
fun run int tr st =
(case Toplevel.transition int tr st of
SOME (st', NONE) => ([], SOME st')
- | SOME (_, SOME exn_info) =>
- (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
+ | SOME (_, SOME (exn, _)) =>
+ (case ML_Compiler.exn_messages exn of
[] => Exn.interrupt ()
| errs => (errs, NONE))
- | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
+ | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
in
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Aug 18 23:43:22 2011 +0200
@@ -84,7 +84,7 @@
Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
- Output.Private_Hooks.error_fn := message (special "M") (special "N") "*** ";
+ Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
fun panic s =
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Aug 18 23:43:22 2011 +0200
@@ -166,7 +166,7 @@
Output.Private_Hooks.urgent_message_fn := (fn s => normalmsg Status s);
Output.Private_Hooks.tracing_fn := (fn s => normalmsg Tracing s);
Output.Private_Hooks.warning_fn := (fn s => errormsg Message Warning s);
- Output.Private_Hooks.error_fn := (fn s => errormsg Message Fatal s));
+ Output.Private_Hooks.error_fn := (fn (_, s) => errormsg Message Fatal s));
(* immediate messages *)
--- a/src/Pure/System/isabelle_process.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/System/isabelle_process.ML Thu Aug 18 23:43:22 2011 +0200
@@ -72,11 +72,11 @@
val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
in Mailbox.send mbox (chunk header @ chunk body) end;
-fun standard_message mbox with_serial ch body =
+fun standard_message mbox opt_serial ch body =
if body = "" then ()
else
message mbox ch
- ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
+ ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
(Position.properties_of (Position.thread_data ()))) body;
fun message_output mbox out_stream =
@@ -103,12 +103,12 @@
val mbox = Mailbox.create () : string list Mailbox.T;
val _ = Simple_Thread.fork false (message_output mbox out_stream);
in
- Output.Private_Hooks.status_fn := standard_message mbox false "B";
- Output.Private_Hooks.report_fn := standard_message mbox false "C";
- Output.Private_Hooks.writeln_fn := standard_message mbox true "D";
- Output.Private_Hooks.tracing_fn := standard_message mbox true "E";
- Output.Private_Hooks.warning_fn := standard_message mbox true "F";
- Output.Private_Hooks.error_fn := standard_message mbox true "G";
+ Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
+ Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
+ Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
+ Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
+ Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
+ Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
Output.Private_Hooks.raw_message_fn := message mbox "H";
Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
Output.Private_Hooks.prompt_fn := ignore;
--- a/src/Pure/System/isar.ML Thu Aug 18 14:08:39 2011 -0700
+++ b/src/Pure/System/isar.ML Thu Aug 18 23:43:22 2011 +0200
@@ -96,7 +96,7 @@
NONE => false
| SOME (_, SOME exn_info) =>
(set_exn (SOME exn_info);
- Toplevel.error_msg tr (ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
+ Toplevel.error_msg tr (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
true)
| SOME (st', NONE) =>
let