1(*  Title:      Pure/Concurrent/par_exn.ML
2    Author:     Makarius
3
4Parallel exceptions as flattened results from acyclic graph of
5evaluations.  Interrupt counts as neutral element.
6*)
7
8signature PAR_EXN =
9sig
10  val make: exn list -> exn
11  val dest: exn -> exn list option
12  val is_interrupted: 'a Exn.result list -> bool
13  val release_all: 'a Exn.result list -> 'a list
14  val release_first: 'a Exn.result list -> 'a list
15end;
16
17structure Par_Exn: PAR_EXN =
18struct
19
20(* parallel exceptions *)
21
22exception Par_Exn of exn list;
23  (*non-empty list with unique identified elements sorted by exn_ord;
24    no occurrences of Par_Exn or Exn.Interrupt*)
25
26fun par_exns (Par_Exn exns) = exns
27  | par_exns exn = if Exn.is_interrupt exn then [] else [exn];
28
29fun make exns =
30  let
31    val exnss = map par_exns exns
32    val exns' = List.concat exnss
33  in if null exns' then Exn.Interrupt else Par_Exn exns' end;
34
35fun dest (Par_Exn exns) = SOME exns
36  | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
37
38
39(* parallel results *)
40
41fun is_interrupted results =
42  List.exists (fn Exn.Exn _ => true | _ => false) results andalso
43    Exn.is_interrupt (make (List.mapPartial Exn.get_exn results));
44
45fun release_all results =
46  if List.all (fn Exn.Res _ => true | _ => false) results
47  then map Exn.release results
48  else raise make (List.mapPartial Exn.get_exn results);
49
50fun plain_exn (Exn.Res _) = NONE
51  | plain_exn (Exn.Exn (Par_Exn _)) = NONE
52  | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn;
53
54fun release_first results =
55  (case Portable.first_opt (fn _ => plain_exn) results of
56    NONE => release_all results
57  | SOME exn => Exn.reraise exn);
58
59end;
60