src/Pure/Concurrent/par_list.ML
author wenzelm
Tue Dec 16 16:25:19 2008 +0100 (2008-12-16)
changeset 29120 8a904ff43f28
parent 28980 9d7ea903e877
child 29368 503ce3f8f092
permissions -rw-r--r--
renamed structure TaskQueue to Task_Queue;
     1 (*  Title:      Pure/Concurrent/par_list.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Parallel list combinators.
     6 
     7 Notes:
     8 
     9   * These combinators only make sense if the operator (function or
    10     predicate) applied to the list of operands takes considerable
    11     time.  The overhead of scheduling is significantly higher than
    12     just traversing the list of operands sequentially.
    13 
    14   * The order of operator application is non-deterministic.  Watch out
    15     for operators that have side-effects or raise exceptions!
    16 *)
    17 
    18 signature PAR_LIST =
    19 sig
    20   val map: ('a -> 'b) -> 'a list -> 'b list
    21   val get_some: ('a -> 'b option) -> 'a list -> 'b option
    22   val find_some: ('a -> bool) -> 'a list -> 'a option
    23   val exists: ('a -> bool) -> 'a list -> bool
    24   val forall: ('a -> bool) -> 'a list -> bool
    25 end;
    26 
    27 structure ParList: PAR_LIST =
    28 struct
    29 
    30 fun raw_map f xs =
    31   if Future.enabled () then
    32     let
    33       val group = Task_Queue.new_group ();
    34       val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
    35       val _ = List.app (ignore o Future.join_result) futures;
    36     in Future.join_results futures end
    37   else map (Exn.capture f) xs;
    38 
    39 fun map f xs = Exn.release_first (raw_map f xs);
    40 
    41 fun get_some f xs =
    42   let
    43     exception FOUND of 'b option;
    44     fun found (Exn.Exn (FOUND some)) = some
    45       | found _ = NONE;
    46     val results = raw_map (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
    47   in
    48     (case get_first found results of
    49       SOME y => SOME y
    50     | NONE => (Exn.release_first results; NONE))
    51   end;
    52 
    53 fun find_some P = get_some (fn x => if P x then SOME x else NONE);
    54 
    55 fun exists P = is_some o get_some (fn x => if P x then SOME () else NONE);
    56 fun forall P = not o exists (not o P);
    57 
    58 end;