src/Pure/Concurrent/par_exn.ML
author wenzelm
Fri, 19 Aug 2011 13:32:27 +0200
changeset 44296 0c4411e2fc90
parent 44271 89f40a5939b2
child 44334 605381e7c7c5
permissions -rw-r--r--
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
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
44271
89f40a5939b2 more precise treatment of exception nesting and serial numbers;
wenzelm
parents: 44270
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)
44296
0c4411e2fc90 more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
wenzelm
parents: 44271
diff changeset
    25
  | NONE =>
0c4411e2fc90 more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
wenzelm
parents: 44271
diff changeset
    26
      let
0c4411e2fc90 more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
wenzelm
parents: 44271
diff changeset
    27
        val i = Library.serial ();
0c4411e2fc90 more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
wenzelm
parents: 44271
diff changeset
    28
        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
    29
      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
    30
44270
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44266
diff changeset
    31
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
    32
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44266
diff changeset
    33
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
    34
64620f1d6f87 identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents: 44248
diff changeset
    35
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    36
(* parallel exceptions *)
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    37
44264
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    38
exception Par_Exn of exn list;
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    39
  (*non-empty list with unique identified elements sorted by exn_ord;
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    40
    no occurrences of Par_Exn or Exn.Interrupt*)
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    41
44264
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    42
fun par_exns (Par_Exn exns) = exns
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    43
  | 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
    44
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    45
fun make exns =
44264
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    46
  (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
    47
    [] => Exn.Interrupt
44264
c21ecbb028b6 tune Par_Exn.make: balance merge;
wenzelm
parents: 44249
diff changeset
    48
  | es => Par_Exn es);
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    49
44271
89f40a5939b2 more precise treatment of exception nesting and serial numbers;
wenzelm
parents: 44270
diff changeset
    50
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
    51
  | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    52
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    53
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    54
(* parallel results *)
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    55
44266
d9c7bf932eab clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents: 44264
diff changeset
    56
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
    57
  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
    58
  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
    59
  else raise make (map_filter Exn.get_exn results);
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    60
44266
d9c7bf932eab clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
wenzelm
parents: 44264
diff changeset
    61
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
    62
  | 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
    63
  | 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
    64
44248
6a3541412b23 clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents: 44247
diff changeset
    65
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
    66
  (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
    67
    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
    68
  | SOME exn => reraise exn);
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    69
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    70
end;
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents:
diff changeset
    71