author | wenzelm |
Sat, 20 Aug 2011 20:00:55 +0200 | |
changeset 45214 | 605381e7c7c5 |
parent 45171 | 0c4411e2fc90 |
child 48242 | e331c6256a41 |
permissions | -rw-r--r-- |
wenzelm@45125 | 1 |
(* Title: Pure/Concurrent/par_exn.ML |
wenzelm@45125 | 2 |
Author: Makarius |
wenzelm@45125 | 3 |
|
wenzelm@45125 | 4 |
Parallel exceptions as flattened results from acyclic graph of |
wenzelm@45125 | 5 |
evaluations. Interrupt counts as neutral element. |
wenzelm@45125 | 6 |
*) |
wenzelm@45125 | 7 |
|
wenzelm@45125 | 8 |
signature PAR_EXN = |
wenzelm@45125 | 9 |
sig |
wenzelm@45127 | 10 |
val serial: exn -> serial * exn |
wenzelm@45125 | 11 |
val make: exn list -> exn |
wenzelm@45154 | 12 |
val dest: exn -> exn list option |
wenzelm@45125 | 13 |
val release_all: 'a Exn.result list -> 'a list |
wenzelm@45125 | 14 |
val release_first: 'a Exn.result list -> 'a list |
wenzelm@45125 | 15 |
end; |
wenzelm@45125 | 16 |
|
wenzelm@45125 | 17 |
structure Par_Exn = |
wenzelm@45125 | 18 |
struct |
wenzelm@45125 | 19 |
|
wenzelm@45127 | 20 |
(* identification via serial numbers *) |
wenzelm@45127 | 21 |
|
wenzelm@45127 | 22 |
fun serial exn = |
wenzelm@45127 | 23 |
(case get_exn_serial exn of |
wenzelm@45127 | 24 |
SOME i => (i, exn) |
wenzelm@45171 | 25 |
| NONE => |
wenzelm@45171 | 26 |
let |
wenzelm@45171 | 27 |
val i = Library.serial (); |
wenzelm@45171 | 28 |
val exn' = uninterruptible (fn _ => set_exn_serial i) exn; |
wenzelm@45171 | 29 |
in (i, exn') end); |
wenzelm@45127 | 30 |
|
wenzelm@45153 | 31 |
val the_serial = the o get_exn_serial; |
wenzelm@45153 | 32 |
|
wenzelm@45153 | 33 |
val exn_ord = rev_order o int_ord o pairself the_serial; |
wenzelm@45127 | 34 |
|
wenzelm@45127 | 35 |
|
wenzelm@45125 | 36 |
(* parallel exceptions *) |
wenzelm@45125 | 37 |
|
wenzelm@45147 | 38 |
exception Par_Exn of exn list; |
wenzelm@45147 | 39 |
(*non-empty list with unique identified elements sorted by exn_ord; |
wenzelm@45147 | 40 |
no occurrences of Par_Exn or Exn.Interrupt*) |
wenzelm@45125 | 41 |
|
wenzelm@45147 | 42 |
fun par_exns (Par_Exn exns) = exns |
wenzelm@45147 | 43 |
| par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)]; |
wenzelm@45125 | 44 |
|
wenzelm@45125 | 45 |
fun make exns = |
wenzelm@45214 | 46 |
(case Ord_List.unions exn_ord (map par_exns exns) of |
wenzelm@45125 | 47 |
[] => Exn.Interrupt |
wenzelm@45147 | 48 |
| es => Par_Exn es); |
wenzelm@45125 | 49 |
|
wenzelm@45154 | 50 |
fun dest (Par_Exn exns) = SOME exns |
wenzelm@45153 | 51 |
| dest exn = if Exn.is_interrupt exn then SOME [] else NONE; |
wenzelm@45125 | 52 |
|
wenzelm@45125 | 53 |
|
wenzelm@45125 | 54 |
(* parallel results *) |
wenzelm@45125 | 55 |
|
wenzelm@45125 | 56 |
fun release_all results = |
wenzelm@45149 | 57 |
if forall (fn Exn.Res _ => true | _ => false) results |
wenzelm@45149 | 58 |
then map Exn.release results |
wenzelm@45125 | 59 |
else raise make (map_filter Exn.get_exn results); |
wenzelm@45125 | 60 |
|
wenzelm@45149 | 61 |
fun plain_exn (Exn.Res _) = NONE |
wenzelm@45149 | 62 |
| plain_exn (Exn.Exn (Par_Exn _)) = NONE |
wenzelm@45149 | 63 |
| plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn; |
wenzelm@45149 | 64 |
|
wenzelm@45126 | 65 |
fun release_first results = |
wenzelm@45149 | 66 |
(case get_first plain_exn results of |
wenzelm@45149 | 67 |
NONE => release_all results |
wenzelm@45149 | 68 |
| SOME exn => reraise exn); |
wenzelm@45125 | 69 |
|
wenzelm@45125 | 70 |
end; |
wenzelm@45125 | 71 |