author wenzelm
Wed, 17 Aug 2011 22:14:22 +0200
changeset 44247 270366301bd7
parent 44113 0baa8bbd355a
child 44265 b94951f06e48
permissions -rw-r--r--
more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;

(*  Title:      Pure/Concurrent/par_list.ML
    Author:     Makarius

Parallel list combinators.


  * These combinators only make sense if the operator (function or
    predicate) applied to the list of operands takes considerable
    time.  The overhead of scheduling is significantly higher than
    just traversing the list of operands sequentially.

  * The order of operator application is non-deterministic.  Watch out
    for operators that have side-effects or raise exceptions!

signature PAR_LIST =
  val map_name: string -> ('a -> 'b) -> 'a list -> 'b list
  val map: ('a -> 'b) -> 'a list -> 'b list
  val get_some: ('a -> 'b option) -> 'a list -> 'b option
  val find_some: ('a -> bool) -> 'a list -> 'a option
  val exists: ('a -> bool) -> 'a list -> bool
  val forall: ('a -> bool) -> 'a list -> bool

structure Par_List: PAR_LIST =

fun managed_results name f xs =
  if null xs orelse null (tl xs) orelse
      not (Multithreading.enabled ()) orelse Multithreading.self_critical ()
  then map (Exn.capture f) xs
      val group = Task_Queue.new_group (Future.worker_group ());
      val futures =
        Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
          (map (fn x => fn () => f x) xs);
      val results = Future.join_results futures
        handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
    in results end;

fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
fun map f = map_name "" f;

fun get_some f xs =
    exception FOUND of 'b option;
    fun found (Exn.Exn (FOUND some)) = some
      | found _ = NONE;
    val results =
      managed_results "Par_List.get_some"
        (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
    (case get_first found results of
      SOME y => SOME y
    | NONE => (Par_Exn.release_first results; NONE))

fun find_some P = get_some (fn x => if P x then SOME x else NONE);

fun exists P = is_some o get_some (fn x => if P x then SOME () else NONE);
fun forall P = not o exists (not o P);