src/Pure/Concurrent/par_exn.ML
author wenzelm
Thu, 18 Aug 2011 15:39:00 +0200
changeset 44266 d9c7bf932eab
parent 44264 c21ecbb028b6
child 44270 3eaad39e520c
permissions -rw-r--r--
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/par_exn.ML
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
     3
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
     4
Parallel exceptions as flattened results from acyclic graph of
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
     5
evaluations.  Interrupt counts as neutral element.
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
     6
*)
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
     7
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
     8
signature PAR_EXN =
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
     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
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    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
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    13
  val release_all: 'a Exn.result list -> 'a list
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    14
  val release_first: 'a Exn.result list -> 'a list
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    15
end;
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    16
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    17
structure Par_Exn =
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    18
struct
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    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
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    30
(* parallel exceptions *)
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    31
44264
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    32
exception Par_Exn of exn list;
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    33
  (*non-empty list with unique identified elements sorted by exn_ord;
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    34
    no occurrences of Par_Exn or Exn.Interrupt*)
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    35
44264
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    36
fun par_exns (Par_Exn exns) = exns
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    37
  | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    38
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    39
fun make exns =
44264
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    40
  (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    41
    [] => Exn.Interrupt
44264
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    42
  | es => Par_Exn es);
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    43
44264
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    44
fun dest (Par_Exn exns) = SOME exns
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    45
  | dest _ = NONE;
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    46
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    47
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    48
(* parallel results *)
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    49
44266
d9c7bf932eab clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents: 44264
diff changeset
    50
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
    51
  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
    52
  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
    53
  else raise make (map_filter Exn.get_exn results);
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    54
44266
d9c7bf932eab clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents: 44264
diff changeset
    55
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
    56
  | 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
    57
  | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn;
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    58
44248
6a3541412b23 clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents: 44247
diff changeset
    59
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
    60
  (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
    61
    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
    62
  | SOME exn => reraise exn);
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    63
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    64
end;
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    65