src/Pure/Concurrent/par_exn.ML

identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;

(*  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;