tune Par_Exn.make: balance merge;
clarified Par_Exn.dest: later exceptions first;
(* 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 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) = exns
| par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
fun make exns =
(case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
[] => Exn.Interrupt
| es => Par_Exn es);
fun dest (Par_Exn exns) = SOME 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;