author wenzelm
Tue, 21 Oct 2008 16:52:59 +0200
changeset 28646 3a8d75c935ce
parent 28645 605a3b1ef6ba
child 28980 9d7ea903e877
permissions -rw-r--r--

(*  Title:      Pure/Concurrent/par_list.ML
    ID:         $Id$
    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: ('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 ParList: PAR_LIST =

fun raw_map f xs =
  if Future.enabled () then
      val group = TaskQueue.new_group ();
      val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
      val _ = (ignore o Future.join_result) futures;
    in Future.join_results futures end
  else map (Exn.capture f) xs;

fun map f xs = Exn.release_first (raw_map f xs);

fun get_some f xs =
    exception FOUND of 'b option;
    fun found (Exn.Exn (FOUND some)) = some
      | found _ = NONE;
    val results = raw_map (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
    (case get_first found results of
      SOME y => SOME y
    | NONE => (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);