author | wenzelm |
Wed, 17 Aug 2011 23:37:23 +0200 | |
changeset 44249 | 64620f1d6f87 |
parent 44248 | 6a3541412b23 |
child 44264 | c21ecbb028b6 |
permissions | -rw-r--r-- |
44247 | 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 |
|
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
10 |
val serial: exn -> serial * exn |
44247 | 11 |
val make: exn list -> exn |
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
12 |
val dest: exn -> exn list option |
44247 | 13 |
val release_all: 'a Exn.result list -> 'a list |
14 |
val release_first: 'a Exn.result list -> 'a list |
|
15 |
end; |
|
16 |
||
17 |
structure Par_Exn = |
|
18 |
struct |
|
19 |
||
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
20 |
(* identification via serial numbers *) |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
21 |
|
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
22 |
fun serial exn = |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
23 |
(case get_exn_serial exn of |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
24 |
SOME i => (i, exn) |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
25 |
| NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end); |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
26 |
|
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
27 |
val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial); |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
28 |
|
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
29 |
|
44247 | 30 |
(* parallel exceptions *) |
31 |
||
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
32 |
exception Par_Exn of exn Ord_List.T; |
44247 | 33 |
|
34 |
fun par_exns (Par_Exn exns) = SOME exns |
|
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
35 |
| par_exns exn = if Exn.is_interrupt exn then NONE else SOME [#2 (serial exn)]; |
44247 | 36 |
|
37 |
fun make exns = |
|
38 |
(case map_filter par_exns exns of |
|
39 |
[] => Exn.Interrupt |
|
40 |
| e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es))); |
|
41 |
||
42 |
fun dest (Par_Exn exns) = SOME (rev exns) |
|
43 |
| dest _ = NONE; |
|
44 |
||
45 |
||
46 |
(* parallel results *) |
|
47 |
||
48 |
fun all_res results = forall (fn Exn.Res _ => true | _ => false) results; |
|
49 |
||
50 |
fun release_all results = |
|
51 |
if all_res results then map Exn.release results |
|
52 |
else raise make (map_filter Exn.get_exn results); |
|
53 |
||
44248
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset
|
54 |
fun release_first results = |
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset
|
55 |
if all_res results then map Exn.release results |
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset
|
56 |
else |
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset
|
57 |
(case get_first |
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset
|
58 |
(fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of |
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset
|
59 |
NONE => Exn.interrupt () |
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset
|
60 |
| SOME exn => reraise exn); |
44247 | 61 |
|
62 |
end; |
|
63 |