# HG changeset patch # User huffman # Date 1313619154 25200 # Node ID 355d5438f5fb5091155e3dd10ad9dc6ea6167a94 # Parent e44f465c00a18439e3b6e496fc16823515e78e7f# Parent a93426812ad5ef0765e0dcb980937e759ffb99f4 merged diff -r e44f465c00a1 -r 355d5438f5fb Admin/polyml/future/ROOT.ML --- a/Admin/polyml/future/ROOT.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/Admin/polyml/future/ROOT.ML Wed Aug 17 15:12:34 2011 -0700 @@ -7,6 +7,22 @@ NONE => raise exn | SOME location => PolyML.raiseWithLocation (exn, location)); +fun set_exn_serial i exn = + let + val (file, startLine, endLine) = + (case PolyML.exceptionLocation exn of + NONE => ("", 0, 0) + | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine)); + val location = + {file = file, startLine = startLine, endLine = endLine, + startPosition = ~ i, endPosition = 0}; + in PolyML.raiseWithLocation (exn, location) handle e => e end; + +fun get_exn_serial exn = + (case Option.map #startPosition (PolyML.exceptionLocation exn) of + NONE => NONE + | SOME i => if i >= 0 then NONE else SOME (~ i)); + exception Interrupt = SML90.Interrupt; val ord = SML90.ord; val chr = SML90.chr; @@ -61,6 +77,7 @@ use "General/alist.ML"; use "General/table.ML"; use "General/graph.ML"; +use "General/ord_list.ML"; structure Position = struct @@ -89,6 +106,7 @@ use "General/markup.ML"; use "Concurrent/single_assignment.ML"; use "Concurrent/time_limit.ML"; +use "Concurrent/par_exn.ML"; use "Concurrent/task_queue.ML"; use "Concurrent/future.ML"; use "Concurrent/lazy.ML"; diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/Concurrent/future.ML Wed Aug 17 15:12:34 2011 -0700 @@ -394,8 +394,12 @@ (* future jobs *) -fun assign_result group result res = +fun assign_result group result raw_res = let + val res = + (case raw_res of + Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn)) + | _ => raw_res); val _ = Single_Assignment.assign result res handle exn as Fail _ => (case Single_Assignment.peek result of @@ -473,9 +477,9 @@ NONE => Exn.Exn (Fail "Unfinished future") | SOME res => if Exn.is_interrupt_exn res then - (case Exn.flatten_list (Task_Queue.group_status (Task_Queue.group_of_task (task_of x))) of - [] => res - | exns => Exn.Exn (Exn.EXCEPTIONS exns)) + (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of + NONE => res + | SOME exn => Exn.Exn exn) else res); fun join_next deps = (*requires SYNCHRONIZED*) diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/Concurrent/par_exn.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Concurrent/par_exn.ML Wed Aug 17 15:12:34 2011 -0700 @@ -0,0 +1,63 @@ +(* Title: Pure/Concurrent/par_exn.ML + Author: Makarius + +Parallel exceptions as flattened results from acyclic graph of +evaluations. Interrupt counts as neutral element. +*) + +signature PAR_EXN = +sig + val serial: exn -> serial * exn + val make: exn list -> exn + val dest: exn -> exn list option + val release_all: 'a Exn.result list -> 'a list + val release_first: 'a Exn.result list -> 'a list +end; + +structure Par_Exn = +struct + +(* identification via serial numbers *) + +fun serial exn = + (case get_exn_serial exn of + 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); + + +(* parallel exceptions *) + +exception Par_Exn of exn Ord_List.T; + +fun par_exns (Par_Exn exns) = SOME exns + | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (serial exn)]; + +fun make exns = + (case map_filter par_exns exns of + [] => Exn.Interrupt + | e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es))); + +fun dest (Par_Exn exns) = SOME (rev exns) + | dest _ = NONE; + + +(* parallel results *) + +fun all_res results = forall (fn Exn.Res _ => true | _ => false) results; + +fun release_all results = + if all_res results then map Exn.release results + else raise make (map_filter Exn.get_exn results); + +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); + +end; + diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/Concurrent/par_list.ML --- a/src/Pure/Concurrent/par_list.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/Concurrent/par_list.ML Wed Aug 17 15:12:34 2011 -0700 @@ -41,7 +41,7 @@ handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn); in results end; -fun map_name name f xs = Exn.release_first (managed_results name f xs); +fun map_name name f xs = Par_Exn.release_first (managed_results name f xs); fun map f = map_name "Par_List.map" f; fun get_some f xs = @@ -55,7 +55,7 @@ in (case get_first found results of SOME y => SOME y - | NONE => (Exn.release_first results; NONE)) + | NONE => (Par_Exn.release_first results; NONE)) end; fun find_some P = get_some (fn x => if P x then SOME x else NONE); diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/Concurrent/task_queue.ML Wed Aug 17 15:12:34 2011 -0700 @@ -12,7 +12,7 @@ val eq_group: group * group -> bool val cancel_group: group -> exn -> unit val is_canceled: group -> bool - val group_status: group -> exn list + val group_status: group -> exn option val str_of_group: group -> string val str_of_groups: group -> string type task @@ -56,12 +56,12 @@ abstype group = Group of {parent: group option, id: int, - status: exn list Synchronized.var} + status: exn option Synchronized.var} with fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status}; -fun new_group parent = make_group (parent, new_id (), Synchronized.var "group" []); +fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE); fun group_id (Group {id, ...}) = id; fun eq_group (group1, group2) = group_id group1 = group_id group2; @@ -74,17 +74,20 @@ fun cancel_group (Group {status, ...}) exn = Synchronized.change status - (fn exns => - if not (Exn.is_interrupt exn) orelse null exns then exn :: exns - else exns); + (fn exns => SOME (Par_Exn.make (exn :: the_list exns))); fun is_canceled (Group {parent, status, ...}) = - not (null (Synchronized.value status)) orelse + is_some (Synchronized.value status) orelse (case parent of NONE => false | SOME group => is_canceled group); -fun group_status (Group {parent, status, ...}) = - Synchronized.value status @ - (case parent of NONE => [] | SOME group => group_status group); +fun group_exns (Group {parent, status, ...}) = + the_list (Synchronized.value status) @ + (case parent of NONE => [] | SOME group => group_exns group); + +fun group_status group = + (case group_exns group of + [] => NONE + | exns => SOME (Par_Exn.make exns)); fun str_of_group group = (is_canceled group ? enclose "(" ")") (string_of_int (group_id group)); diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/General/exn.ML --- a/src/Pure/General/exn.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/General/exn.ML Wed Aug 17 15:12:34 2011 -0700 @@ -11,7 +11,6 @@ val get_exn: 'a result -> exn option val capture: ('a -> 'b) -> 'a -> 'b result val release: 'a result -> 'a - val flat_result: 'a result result -> 'a result val map_result: ('a -> 'b) -> 'a result -> 'b result val maps_result: ('a -> 'b result) -> 'a result -> 'b result exception Interrupt @@ -21,10 +20,6 @@ val is_interrupt_exn: 'a result -> bool val interruptible_capture: ('a -> 'b) -> 'a -> 'b result exception EXCEPTIONS of exn list - val flatten: exn -> exn list - val flatten_list: exn list -> exn list - val release_all: 'a result list -> 'a list - val release_first: 'a result list -> 'a list end; structure Exn: EXN = @@ -47,13 +42,10 @@ fun release (Res y) = y | release (Exn e) = reraise e; -fun flat_result (Res x) = x - | flat_result (Exn e) = Exn e; - fun map_result f (Res x) = Res (f x) | map_result f (Exn e) = Exn e; -fun maps_result f = flat_result o map_result f; +fun maps_result f = (fn Res x => x | Exn e => Exn e) o map_result f; (* interrupts *) @@ -75,23 +67,10 @@ Res (f x) handle e => if is_interrupt e then reraise e else Exn e; -(* nested exceptions *) +(* concatenated exceptions *) exception EXCEPTIONS of exn list; -fun flatten (EXCEPTIONS exns) = flatten_list exns - | flatten exn = if is_interrupt exn then [] else [exn] -and flatten_list exns = List.concat (map flatten exns); - -fun release_all results = - if List.all (fn Res _ => true | _ => false) results - then map (fn Res x => x) results - else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results)); - -fun release_first results = release_all results - handle EXCEPTIONS [] => interrupt () - | EXCEPTIONS (exn :: _) => reraise exn; - end; datatype illegal = Interrupt; diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/IsaMakefile Wed Aug 17 15:12:34 2011 -0700 @@ -60,6 +60,7 @@ Concurrent/lazy.ML \ Concurrent/lazy_sequential.ML \ Concurrent/mailbox.ML \ + Concurrent/par_exn.ML \ Concurrent/par_list.ML \ Concurrent/par_list_sequential.ML \ Concurrent/simple_thread.ML \ diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/Isar/runtime.ML Wed Aug 17 15:12:34 2011 -0700 @@ -60,34 +60,38 @@ fun exn_msgs context exn = if Exn.is_interrupt exn then [] else - (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]] - | THEORY (msg, thys) => - [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 []))] - | TYPE (msg, Ts, ts) => - [raised exn "TYPE" (msg :: - (if detailed then - if_context context Syntax.string_of_typ Ts @ - if_context context Syntax.string_of_term ts - else []))] - | TERM (msg, ts) => - [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) []]); + (case Par_Exn.dest exn of + SOME exns => maps (exn_msgs context) exns + | NONE => + (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]] + | THEORY (msg, thys) => + [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 []))] + | TYPE (msg, Ts, ts) => + [raised exn "TYPE" (msg :: + (if detailed then + if_context context Syntax.string_of_typ Ts @ + if_context context Syntax.string_of_term ts + else []))] + | TERM (msg, ts) => + [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; fun exn_message exn_position exn = diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/ML-Systems/polyml-5.2.1.ML --- a/src/Pure/ML-Systems/polyml-5.2.1.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML Wed Aug 17 15:12:34 2011 -0700 @@ -13,6 +13,8 @@ end; fun reraise exn = raise exn; +fun set_exn_serial (_: int) (exn: exn) = exn; +fun get_exn_serial (exn: exn) : int option = NONE; use "ML-Systems/polyml_common.ML"; use "ML-Systems/multithreading_polyml.ML"; diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/ML-Systems/polyml.ML Wed Aug 17 15:12:34 2011 -0700 @@ -17,6 +17,22 @@ NONE => raise exn | SOME location => PolyML.raiseWithLocation (exn, location)); +fun set_exn_serial i exn = + let + val (file, startLine, endLine) = + (case PolyML.exceptionLocation exn of + NONE => ("", 0, 0) + | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine)); + val location = + {file = file, startLine = startLine, endLine = endLine, + startPosition = ~ i, endPosition = 0}; + in PolyML.raiseWithLocation (exn, location) handle e => e end; + +fun get_exn_serial exn = + (case Option.map #startPosition (PolyML.exceptionLocation exn) of + NONE => NONE + | SOME i => if i >= 0 then NONE else SOME (~ i)); + use "ML-Systems/polyml_common.ML"; use "ML-Systems/multithreading_polyml.ML"; use "ML-Systems/unsynchronized.ML"; diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/ML-Systems/smlnj.ML Wed Aug 17 15:12:34 2011 -0700 @@ -3,10 +3,13 @@ Compatibility file for Standard ML of New Jersey 110 or later. *) +use "ML-Systems/proper_int.ML"; + exception Interrupt; fun reraise exn = raise exn; +fun set_exn_serial (_: int) (exn: exn) = exn; +fun get_exn_serial (exn: exn) : int option = NONE; -use "ML-Systems/proper_int.ML"; use "ML-Systems/overloading_smlnj.ML"; use "General/exn.ML"; use "ML-Systems/single_assignment.ML"; diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/PIDE/document.ML Wed Aug 17 15:12:34 2011 -0700 @@ -372,7 +372,7 @@ |> set_result result; in ((assigns, execs, [(name, node')]), node') end) end)) - |> Future.join_results |> Exn.release_all |> map #1; + |> Future.join_results |> Par_Exn.release_all |> map #1; val state' = state |> fold (fold define_exec o #2) updates diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/ROOT.ML Wed Aug 17 15:12:34 2011 -0700 @@ -77,7 +77,7 @@ then use "Concurrent/bash.ML" else use "Concurrent/bash_sequential.ML"; -use "Concurrent/mailbox.ML"; +use "Concurrent/par_exn.ML"; use "Concurrent/task_queue.ML"; use "Concurrent/future.ML"; @@ -89,6 +89,7 @@ if Multithreading.available then () else use "Concurrent/par_list_sequential.ML"; +use "Concurrent/mailbox.ML"; use "Concurrent/cache.ML"; diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/Thy/thy_info.ML Wed Aug 17 15:12:34 2011 -0700 @@ -207,7 +207,7 @@ " (unresolved " ^ commas_quote (map #1 bad) ^ ")") []))) | Finished thy => Future.value (thy, Future.value (), I))) #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn]) - #> rev #> Exn.release_all) #> ignore; + #> rev #> Par_Exn.release_all) #> ignore; in diff -r e44f465c00a1 -r 355d5438f5fb src/Pure/thm.ML --- a/src/Pure/thm.ML Wed Aug 17 15:03:30 2011 -0700 +++ b/src/Pure/thm.ML Wed Aug 17 15:12:34 2011 -0700 @@ -515,7 +515,7 @@ fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) = Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (map #1 promises ~~ fulfill_bodies (map #2 promises)) body -and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures)); +and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures)); val join_proofs = Proofterm.join_bodies o map fulfill_body;