1.1 --- a/Admin/polyml/future/ROOT.ML Wed Aug 17 15:03:30 2011 -0700
1.2 +++ b/Admin/polyml/future/ROOT.ML Wed Aug 17 15:12:34 2011 -0700
1.3 @@ -7,6 +7,22 @@
1.4 NONE => raise exn
1.5 | SOME location => PolyML.raiseWithLocation (exn, location));
1.6
1.7 +fun set_exn_serial i exn =
1.8 + let
1.9 + val (file, startLine, endLine) =
1.10 + (case PolyML.exceptionLocation exn of
1.11 + NONE => ("", 0, 0)
1.12 + | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
1.13 + val location =
1.14 + {file = file, startLine = startLine, endLine = endLine,
1.15 + startPosition = ~ i, endPosition = 0};
1.16 + in PolyML.raiseWithLocation (exn, location) handle e => e end;
1.17 +
1.18 +fun get_exn_serial exn =
1.19 + (case Option.map #startPosition (PolyML.exceptionLocation exn) of
1.20 + NONE => NONE
1.21 + | SOME i => if i >= 0 then NONE else SOME (~ i));
1.22 +
1.23 exception Interrupt = SML90.Interrupt;
1.24 val ord = SML90.ord;
1.25 val chr = SML90.chr;
1.26 @@ -61,6 +77,7 @@
1.27 use "General/alist.ML";
1.28 use "General/table.ML";
1.29 use "General/graph.ML";
1.30 +use "General/ord_list.ML";
1.31
1.32 structure Position =
1.33 struct
1.34 @@ -89,6 +106,7 @@
1.35 use "General/markup.ML";
1.36 use "Concurrent/single_assignment.ML";
1.37 use "Concurrent/time_limit.ML";
1.38 +use "Concurrent/par_exn.ML";
1.39 use "Concurrent/task_queue.ML";
1.40 use "Concurrent/future.ML";
1.41 use "Concurrent/lazy.ML";
2.1 --- a/src/Pure/Concurrent/future.ML Wed Aug 17 15:03:30 2011 -0700
2.2 +++ b/src/Pure/Concurrent/future.ML Wed Aug 17 15:12:34 2011 -0700
2.3 @@ -394,8 +394,12 @@
2.4
2.5 (* future jobs *)
2.6
2.7 -fun assign_result group result res =
2.8 +fun assign_result group result raw_res =
2.9 let
2.10 + val res =
2.11 + (case raw_res of
2.12 + Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn))
2.13 + | _ => raw_res);
2.14 val _ = Single_Assignment.assign result res
2.15 handle exn as Fail _ =>
2.16 (case Single_Assignment.peek result of
2.17 @@ -473,9 +477,9 @@
2.18 NONE => Exn.Exn (Fail "Unfinished future")
2.19 | SOME res =>
2.20 if Exn.is_interrupt_exn res then
2.21 - (case Exn.flatten_list (Task_Queue.group_status (Task_Queue.group_of_task (task_of x))) of
2.22 - [] => res
2.23 - | exns => Exn.Exn (Exn.EXCEPTIONS exns))
2.24 + (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of
2.25 + NONE => res
2.26 + | SOME exn => Exn.Exn exn)
2.27 else res);
2.28
2.29 fun join_next deps = (*requires SYNCHRONIZED*)
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Pure/Concurrent/par_exn.ML Wed Aug 17 15:12:34 2011 -0700
3.3 @@ -0,0 +1,63 @@
3.4 +(* Title: Pure/Concurrent/par_exn.ML
3.5 + Author: Makarius
3.6 +
3.7 +Parallel exceptions as flattened results from acyclic graph of
3.8 +evaluations. Interrupt counts as neutral element.
3.9 +*)
3.10 +
3.11 +signature PAR_EXN =
3.12 +sig
3.13 + val serial: exn -> serial * exn
3.14 + val make: exn list -> exn
3.15 + val dest: exn -> exn list option
3.16 + val release_all: 'a Exn.result list -> 'a list
3.17 + val release_first: 'a Exn.result list -> 'a list
3.18 +end;
3.19 +
3.20 +structure Par_Exn =
3.21 +struct
3.22 +
3.23 +(* identification via serial numbers *)
3.24 +
3.25 +fun serial exn =
3.26 + (case get_exn_serial exn of
3.27 + SOME i => (i, exn)
3.28 + | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
3.29 +
3.30 +val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial);
3.31 +
3.32 +
3.33 +(* parallel exceptions *)
3.34 +
3.35 +exception Par_Exn of exn Ord_List.T;
3.36 +
3.37 +fun par_exns (Par_Exn exns) = SOME exns
3.38 + | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (serial exn)];
3.39 +
3.40 +fun make exns =
3.41 + (case map_filter par_exns exns of
3.42 + [] => Exn.Interrupt
3.43 + | e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es)));
3.44 +
3.45 +fun dest (Par_Exn exns) = SOME (rev exns)
3.46 + | dest _ = NONE;
3.47 +
3.48 +
3.49 +(* parallel results *)
3.50 +
3.51 +fun all_res results = forall (fn Exn.Res _ => true | _ => false) results;
3.52 +
3.53 +fun release_all results =
3.54 + if all_res results then map Exn.release results
3.55 + else raise make (map_filter Exn.get_exn results);
3.56 +
3.57 +fun release_first results =
3.58 + if all_res results then map Exn.release results
3.59 + else
3.60 + (case get_first
3.61 + (fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of
3.62 + NONE => Exn.interrupt ()
3.63 + | SOME exn => reraise exn);
3.64 +
3.65 +end;
3.66 +
4.1 --- a/src/Pure/Concurrent/par_list.ML Wed Aug 17 15:03:30 2011 -0700
4.2 +++ b/src/Pure/Concurrent/par_list.ML Wed Aug 17 15:12:34 2011 -0700
4.3 @@ -41,7 +41,7 @@
4.4 handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
4.5 in results end;
4.6
4.7 -fun map_name name f xs = Exn.release_first (managed_results name f xs);
4.8 +fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
4.9 fun map f = map_name "Par_List.map" f;
4.10
4.11 fun get_some f xs =
4.12 @@ -55,7 +55,7 @@
4.13 in
4.14 (case get_first found results of
4.15 SOME y => SOME y
4.16 - | NONE => (Exn.release_first results; NONE))
4.17 + | NONE => (Par_Exn.release_first results; NONE))
4.18 end;
4.19
4.20 fun find_some P = get_some (fn x => if P x then SOME x else NONE);
5.1 --- a/src/Pure/Concurrent/task_queue.ML Wed Aug 17 15:03:30 2011 -0700
5.2 +++ b/src/Pure/Concurrent/task_queue.ML Wed Aug 17 15:12:34 2011 -0700
5.3 @@ -12,7 +12,7 @@
5.4 val eq_group: group * group -> bool
5.5 val cancel_group: group -> exn -> unit
5.6 val is_canceled: group -> bool
5.7 - val group_status: group -> exn list
5.8 + val group_status: group -> exn option
5.9 val str_of_group: group -> string
5.10 val str_of_groups: group -> string
5.11 type task
5.12 @@ -56,12 +56,12 @@
5.13 abstype group = Group of
5.14 {parent: group option,
5.15 id: int,
5.16 - status: exn list Synchronized.var}
5.17 + status: exn option Synchronized.var}
5.18 with
5.19
5.20 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
5.21
5.22 -fun new_group parent = make_group (parent, new_id (), Synchronized.var "group" []);
5.23 +fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE);
5.24
5.25 fun group_id (Group {id, ...}) = id;
5.26 fun eq_group (group1, group2) = group_id group1 = group_id group2;
5.27 @@ -74,17 +74,20 @@
5.28
5.29 fun cancel_group (Group {status, ...}) exn =
5.30 Synchronized.change status
5.31 - (fn exns =>
5.32 - if not (Exn.is_interrupt exn) orelse null exns then exn :: exns
5.33 - else exns);
5.34 + (fn exns => SOME (Par_Exn.make (exn :: the_list exns)));
5.35
5.36 fun is_canceled (Group {parent, status, ...}) =
5.37 - not (null (Synchronized.value status)) orelse
5.38 + is_some (Synchronized.value status) orelse
5.39 (case parent of NONE => false | SOME group => is_canceled group);
5.40
5.41 -fun group_status (Group {parent, status, ...}) =
5.42 - Synchronized.value status @
5.43 - (case parent of NONE => [] | SOME group => group_status group);
5.44 +fun group_exns (Group {parent, status, ...}) =
5.45 + the_list (Synchronized.value status) @
5.46 + (case parent of NONE => [] | SOME group => group_exns group);
5.47 +
5.48 +fun group_status group =
5.49 + (case group_exns group of
5.50 + [] => NONE
5.51 + | exns => SOME (Par_Exn.make exns));
5.52
5.53 fun str_of_group group =
5.54 (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
6.1 --- a/src/Pure/General/exn.ML Wed Aug 17 15:03:30 2011 -0700
6.2 +++ b/src/Pure/General/exn.ML Wed Aug 17 15:12:34 2011 -0700
6.3 @@ -11,7 +11,6 @@
6.4 val get_exn: 'a result -> exn option
6.5 val capture: ('a -> 'b) -> 'a -> 'b result
6.6 val release: 'a result -> 'a
6.7 - val flat_result: 'a result result -> 'a result
6.8 val map_result: ('a -> 'b) -> 'a result -> 'b result
6.9 val maps_result: ('a -> 'b result) -> 'a result -> 'b result
6.10 exception Interrupt
6.11 @@ -21,10 +20,6 @@
6.12 val is_interrupt_exn: 'a result -> bool
6.13 val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
6.14 exception EXCEPTIONS of exn list
6.15 - val flatten: exn -> exn list
6.16 - val flatten_list: exn list -> exn list
6.17 - val release_all: 'a result list -> 'a list
6.18 - val release_first: 'a result list -> 'a list
6.19 end;
6.20
6.21 structure Exn: EXN =
6.22 @@ -47,13 +42,10 @@
6.23 fun release (Res y) = y
6.24 | release (Exn e) = reraise e;
6.25
6.26 -fun flat_result (Res x) = x
6.27 - | flat_result (Exn e) = Exn e;
6.28 -
6.29 fun map_result f (Res x) = Res (f x)
6.30 | map_result f (Exn e) = Exn e;
6.31
6.32 -fun maps_result f = flat_result o map_result f;
6.33 +fun maps_result f = (fn Res x => x | Exn e => Exn e) o map_result f;
6.34
6.35
6.36 (* interrupts *)
6.37 @@ -75,23 +67,10 @@
6.38 Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
6.39
6.40
6.41 -(* nested exceptions *)
6.42 +(* concatenated exceptions *)
6.43
6.44 exception EXCEPTIONS of exn list;
6.45
6.46 -fun flatten (EXCEPTIONS exns) = flatten_list exns
6.47 - | flatten exn = if is_interrupt exn then [] else [exn]
6.48 -and flatten_list exns = List.concat (map flatten exns);
6.49 -
6.50 -fun release_all results =
6.51 - if List.all (fn Res _ => true | _ => false) results
6.52 - then map (fn Res x => x) results
6.53 - else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
6.54 -
6.55 -fun release_first results = release_all results
6.56 - handle EXCEPTIONS [] => interrupt ()
6.57 - | EXCEPTIONS (exn :: _) => reraise exn;
6.58 -
6.59 end;
6.60
6.61 datatype illegal = Interrupt;
7.1 --- a/src/Pure/IsaMakefile Wed Aug 17 15:03:30 2011 -0700
7.2 +++ b/src/Pure/IsaMakefile Wed Aug 17 15:12:34 2011 -0700
7.3 @@ -60,6 +60,7 @@
7.4 Concurrent/lazy.ML \
7.5 Concurrent/lazy_sequential.ML \
7.6 Concurrent/mailbox.ML \
7.7 + Concurrent/par_exn.ML \
7.8 Concurrent/par_list.ML \
7.9 Concurrent/par_list_sequential.ML \
7.10 Concurrent/simple_thread.ML \
8.1 --- a/src/Pure/Isar/runtime.ML Wed Aug 17 15:03:30 2011 -0700
8.2 +++ b/src/Pure/Isar/runtime.ML Wed Aug 17 15:12:34 2011 -0700
8.3 @@ -60,34 +60,38 @@
8.4 fun exn_msgs context exn =
8.5 if Exn.is_interrupt exn then []
8.6 else
8.7 - (case exn of
8.8 - Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
8.9 - | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
8.10 - | EXCURSION_FAIL (exn, loc) =>
8.11 - map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)) (exn_msgs context exn)
8.12 - | TERMINATE => ["Exit"]
8.13 - | TimeLimit.TimeOut => ["Timeout"]
8.14 - | TOPLEVEL_ERROR => ["Error"]
8.15 - | ERROR msg => [msg]
8.16 - | Fail msg => [raised exn "Fail" [msg]]
8.17 - | THEORY (msg, thys) =>
8.18 - [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
8.19 - | Ast.AST (msg, asts) =>
8.20 - [raised exn "AST" (msg ::
8.21 - (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
8.22 - | TYPE (msg, Ts, ts) =>
8.23 - [raised exn "TYPE" (msg ::
8.24 - (if detailed then
8.25 - if_context context Syntax.string_of_typ Ts @
8.26 - if_context context Syntax.string_of_term ts
8.27 - else []))]
8.28 - | TERM (msg, ts) =>
8.29 - [raised exn "TERM" (msg ::
8.30 - (if detailed then if_context context Syntax.string_of_term ts else []))]
8.31 - | THM (msg, i, thms) =>
8.32 - [raised exn ("THM " ^ string_of_int i) (msg ::
8.33 - (if detailed then if_context context Display.string_of_thm thms else []))]
8.34 - | _ => [raised exn (General.exnMessage exn) []]);
8.35 + (case Par_Exn.dest exn of
8.36 + SOME exns => maps (exn_msgs context) exns
8.37 + | NONE =>
8.38 + (case exn of
8.39 + Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
8.40 + | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
8.41 + | EXCURSION_FAIL (exn, loc) =>
8.42 + map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc))
8.43 + (exn_msgs context exn)
8.44 + | TERMINATE => ["Exit"]
8.45 + | TimeLimit.TimeOut => ["Timeout"]
8.46 + | TOPLEVEL_ERROR => ["Error"]
8.47 + | ERROR msg => [msg]
8.48 + | Fail msg => [raised exn "Fail" [msg]]
8.49 + | THEORY (msg, thys) =>
8.50 + [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
8.51 + | Ast.AST (msg, asts) =>
8.52 + [raised exn "AST" (msg ::
8.53 + (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
8.54 + | TYPE (msg, Ts, ts) =>
8.55 + [raised exn "TYPE" (msg ::
8.56 + (if detailed then
8.57 + if_context context Syntax.string_of_typ Ts @
8.58 + if_context context Syntax.string_of_term ts
8.59 + else []))]
8.60 + | TERM (msg, ts) =>
8.61 + [raised exn "TERM" (msg ::
8.62 + (if detailed then if_context context Syntax.string_of_term ts else []))]
8.63 + | THM (msg, i, thms) =>
8.64 + [raised exn ("THM " ^ string_of_int i) (msg ::
8.65 + (if detailed then if_context context Display.string_of_thm thms else []))]
8.66 + | _ => [raised exn (General.exnMessage exn) []]));
8.67 in exn_msgs NONE e end;
8.68
8.69 fun exn_message exn_position exn =
9.1 --- a/src/Pure/ML-Systems/polyml-5.2.1.ML Wed Aug 17 15:03:30 2011 -0700
9.2 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML Wed Aug 17 15:12:34 2011 -0700
9.3 @@ -13,6 +13,8 @@
9.4 end;
9.5
9.6 fun reraise exn = raise exn;
9.7 +fun set_exn_serial (_: int) (exn: exn) = exn;
9.8 +fun get_exn_serial (exn: exn) : int option = NONE;
9.9
9.10 use "ML-Systems/polyml_common.ML";
9.11 use "ML-Systems/multithreading_polyml.ML";
10.1 --- a/src/Pure/ML-Systems/polyml.ML Wed Aug 17 15:03:30 2011 -0700
10.2 +++ b/src/Pure/ML-Systems/polyml.ML Wed Aug 17 15:12:34 2011 -0700
10.3 @@ -17,6 +17,22 @@
10.4 NONE => raise exn
10.5 | SOME location => PolyML.raiseWithLocation (exn, location));
10.6
10.7 +fun set_exn_serial i exn =
10.8 + let
10.9 + val (file, startLine, endLine) =
10.10 + (case PolyML.exceptionLocation exn of
10.11 + NONE => ("", 0, 0)
10.12 + | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
10.13 + val location =
10.14 + {file = file, startLine = startLine, endLine = endLine,
10.15 + startPosition = ~ i, endPosition = 0};
10.16 + in PolyML.raiseWithLocation (exn, location) handle e => e end;
10.17 +
10.18 +fun get_exn_serial exn =
10.19 + (case Option.map #startPosition (PolyML.exceptionLocation exn) of
10.20 + NONE => NONE
10.21 + | SOME i => if i >= 0 then NONE else SOME (~ i));
10.22 +
10.23 use "ML-Systems/polyml_common.ML";
10.24 use "ML-Systems/multithreading_polyml.ML";
10.25 use "ML-Systems/unsynchronized.ML";
11.1 --- a/src/Pure/ML-Systems/smlnj.ML Wed Aug 17 15:03:30 2011 -0700
11.2 +++ b/src/Pure/ML-Systems/smlnj.ML Wed Aug 17 15:12:34 2011 -0700
11.3 @@ -3,10 +3,13 @@
11.4 Compatibility file for Standard ML of New Jersey 110 or later.
11.5 *)
11.6
11.7 +use "ML-Systems/proper_int.ML";
11.8 +
11.9 exception Interrupt;
11.10 fun reraise exn = raise exn;
11.11 +fun set_exn_serial (_: int) (exn: exn) = exn;
11.12 +fun get_exn_serial (exn: exn) : int option = NONE;
11.13
11.14 -use "ML-Systems/proper_int.ML";
11.15 use "ML-Systems/overloading_smlnj.ML";
11.16 use "General/exn.ML";
11.17 use "ML-Systems/single_assignment.ML";
12.1 --- a/src/Pure/PIDE/document.ML Wed Aug 17 15:03:30 2011 -0700
12.2 +++ b/src/Pure/PIDE/document.ML Wed Aug 17 15:12:34 2011 -0700
12.3 @@ -372,7 +372,7 @@
12.4 |> set_result result;
12.5 in ((assigns, execs, [(name, node')]), node') end)
12.6 end))
12.7 - |> Future.join_results |> Exn.release_all |> map #1;
12.8 + |> Future.join_results |> Par_Exn.release_all |> map #1;
12.9
12.10 val state' = state
12.11 |> fold (fold define_exec o #2) updates
13.1 --- a/src/Pure/ROOT.ML Wed Aug 17 15:03:30 2011 -0700
13.2 +++ b/src/Pure/ROOT.ML Wed Aug 17 15:12:34 2011 -0700
13.3 @@ -77,7 +77,7 @@
13.4 then use "Concurrent/bash.ML"
13.5 else use "Concurrent/bash_sequential.ML";
13.6
13.7 -use "Concurrent/mailbox.ML";
13.8 +use "Concurrent/par_exn.ML";
13.9 use "Concurrent/task_queue.ML";
13.10 use "Concurrent/future.ML";
13.11
13.12 @@ -89,6 +89,7 @@
13.13 if Multithreading.available then ()
13.14 else use "Concurrent/par_list_sequential.ML";
13.15
13.16 +use "Concurrent/mailbox.ML";
13.17 use "Concurrent/cache.ML";
13.18
13.19
14.1 --- a/src/Pure/Thy/thy_info.ML Wed Aug 17 15:03:30 2011 -0700
14.2 +++ b/src/Pure/Thy/thy_info.ML Wed Aug 17 15:12:34 2011 -0700
14.3 @@ -207,7 +207,7 @@
14.4 " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
14.5 | Finished thy => Future.value (thy, Future.value (), I)))
14.6 #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
14.7 - #> rev #> Exn.release_all) #> ignore;
14.8 + #> rev #> Par_Exn.release_all) #> ignore;
14.9
14.10 in
14.11
15.1 --- a/src/Pure/thm.ML Wed Aug 17 15:03:30 2011 -0700
15.2 +++ b/src/Pure/thm.ML Wed Aug 17 15:12:34 2011 -0700
15.3 @@ -515,7 +515,7 @@
15.4 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
15.5 Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
15.6 (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
15.7 -and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
15.8 +and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
15.9
15.10 val join_proofs = Proofterm.join_bodies o map fulfill_body;
15.11