equal
deleted
inserted
replaced
|
1 (* Title: Pure/Concurrent/par_exn.ML |
|
2 Author: Makarius |
|
3 |
|
4 Parallel exceptions as flattened results from acyclic graph of |
|
5 evaluations. Interrupt counts as neutral element. |
|
6 *) |
|
7 |
|
8 signature PAR_EXN = |
|
9 sig |
|
10 val make: exn list -> exn |
|
11 val dest: exn -> (serial * exn) list option |
|
12 val release_all: 'a Exn.result list -> 'a list |
|
13 val release_first: 'a Exn.result list -> 'a list |
|
14 end; |
|
15 |
|
16 structure Par_Exn = |
|
17 struct |
|
18 |
|
19 (* parallel exceptions *) |
|
20 |
|
21 exception Par_Exn of (serial * exn) Ord_List.T; |
|
22 |
|
23 fun exn_ord ((i, _), (j, _)) = int_ord (j, i); |
|
24 |
|
25 fun par_exns (Par_Exn exns) = SOME exns |
|
26 | par_exns exn = if Exn.is_interrupt exn then NONE else SOME [(serial (), exn)]; |
|
27 |
|
28 fun make exns = |
|
29 (case map_filter par_exns exns of |
|
30 [] => Exn.Interrupt |
|
31 | e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es))); |
|
32 |
|
33 fun dest (Par_Exn exns) = SOME (rev exns) |
|
34 | dest _ = NONE; |
|
35 |
|
36 |
|
37 (* parallel results *) |
|
38 |
|
39 fun all_res results = forall (fn Exn.Res _ => true | _ => false) results; |
|
40 |
|
41 fun release_all results = |
|
42 if all_res results then map Exn.release results |
|
43 else raise make (map_filter Exn.get_exn results); |
|
44 |
|
45 fun release_first results = release_all results |
|
46 handle Par_Exn ((serial, exn) :: _) => reraise exn; (* FIXME preserve serial in location (?!?) *) |
|
47 |
|
48 end; |
|
49 |