author | wenzelm |
Wed, 16 Jan 2013 11:25:26 +0100 | |
changeset 50909 | b2fb1ab1475d |
parent 49061 | 7449b804073b |
child 50911 | ee7fe4230642 |
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 |
50909 | 11 |
val set_serial: exn -> exn |
44247 | 12 |
val make: exn list -> exn |
44271
89f40a5939b2
more precise treatment of exception nesting and serial numbers;
wenzelm
parents:
44270
diff
changeset
|
13 |
val dest: exn -> exn list option |
49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
47338
diff
changeset
|
14 |
val is_interrupted: 'a Exn.result list -> bool |
44247 | 15 |
val release_all: 'a Exn.result list -> 'a list |
16 |
val release_first: 'a Exn.result list -> 'a list |
|
17 |
end; |
|
18 |
||
47338 | 19 |
structure Par_Exn: PAR_EXN = |
44247 | 20 |
struct |
21 |
||
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
22 |
(* identification via serial numbers *) |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
23 |
|
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
24 |
fun serial exn = |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
25 |
(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
|
26 |
SOME i => (i, exn) |
44296
0c4411e2fc90
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
wenzelm
parents:
44271
diff
changeset
|
27 |
| NONE => |
0c4411e2fc90
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
wenzelm
parents:
44271
diff
changeset
|
28 |
let |
0c4411e2fc90
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
wenzelm
parents:
44271
diff
changeset
|
29 |
val i = Library.serial (); |
0c4411e2fc90
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
wenzelm
parents:
44271
diff
changeset
|
30 |
val exn' = uninterruptible (fn _ => set_exn_serial i) exn; |
0c4411e2fc90
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
wenzelm
parents:
44271
diff
changeset
|
31 |
in (i, exn') end); |
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
32 |
|
50909 | 33 |
fun set_serial exn = #2 (serial exn); |
34 |
||
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44266
diff
changeset
|
35 |
val the_serial = the o get_exn_serial; |
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44266
diff
changeset
|
36 |
|
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44266
diff
changeset
|
37 |
val exn_ord = rev_order o int_ord o pairself the_serial; |
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
38 |
|
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44248
diff
changeset
|
39 |
|
44247 | 40 |
(* parallel exceptions *) |
41 |
||
44264 | 42 |
exception Par_Exn of exn list; |
43 |
(*non-empty list with unique identified elements sorted by exn_ord; |
|
44 |
no occurrences of Par_Exn or Exn.Interrupt*) |
|
44247 | 45 |
|
44264 | 46 |
fun par_exns (Par_Exn exns) = exns |
50909 | 47 |
| par_exns exn = if Exn.is_interrupt exn then [] else [set_serial exn]; |
44247 | 48 |
|
49 |
fun make exns = |
|
44334 | 50 |
(case Ord_List.unions exn_ord (map par_exns exns) of |
44247 | 51 |
[] => Exn.Interrupt |
44264 | 52 |
| es => Par_Exn es); |
44247 | 53 |
|
44271
89f40a5939b2
more precise treatment of exception nesting and serial numbers;
wenzelm
parents:
44270
diff
changeset
|
54 |
fun dest (Par_Exn exns) = SOME exns |
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44266
diff
changeset
|
55 |
| dest exn = if Exn.is_interrupt exn then SOME [] else NONE; |
44247 | 56 |
|
57 |
||
58 |
(* parallel results *) |
|
59 |
||
49061
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
47338
diff
changeset
|
60 |
fun is_interrupted results = |
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
47338
diff
changeset
|
61 |
exists (fn Exn.Exn _ => true | _ => false) results andalso |
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
47338
diff
changeset
|
62 |
Exn.is_interrupt (make (map_filter Exn.get_exn results)); |
7449b804073b
central management of forked goals wrt. transaction id;
wenzelm
parents:
47338
diff
changeset
|
63 |
|
44266
d9c7bf932eab
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents:
44264
diff
changeset
|
64 |
fun release_all results = |
d9c7bf932eab
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents:
44264
diff
changeset
|
65 |
if forall (fn Exn.Res _ => true | _ => false) results |
d9c7bf932eab
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents:
44264
diff
changeset
|
66 |
then map Exn.release results |
d9c7bf932eab
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents:
44264
diff
changeset
|
67 |
else raise make (map_filter Exn.get_exn results); |
44247 | 68 |
|
44266
d9c7bf932eab
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents:
44264
diff
changeset
|
69 |
fun plain_exn (Exn.Res _) = NONE |
d9c7bf932eab
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents:
44264
diff
changeset
|
70 |
| plain_exn (Exn.Exn (Par_Exn _)) = NONE |
d9c7bf932eab
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents:
44264
diff
changeset
|
71 |
| plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn; |
44247 | 72 |
|
44248
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset
|
73 |
fun release_first results = |
44266
d9c7bf932eab
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents:
44264
diff
changeset
|
74 |
(case get_first plain_exn results of |
d9c7bf932eab
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents:
44264
diff
changeset
|
75 |
NONE => release_all results |
d9c7bf932eab
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents:
44264
diff
changeset
|
76 |
| SOME exn => reraise exn); |
44247 | 77 |
|
78 |
end; |
|
79 |