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