src/Pure/Concurrent/par_list.ML
author wenzelm
Tue, 21 Oct 2008 16:52:59 +0200
changeset 28646 3a8d75c935ce
parent 28645 605a3b1ef6ba
child 28980 9d7ea903e877
permissions -rw-r--r--
Future.join_result;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28199
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/par_list.ML
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
     4
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
     5
Parallel list combinators.
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
     6
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
     7
Notes:
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
     8
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
     9
  * These combinators only make sense if the operator (function or
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    10
    predicate) applied to the list of operands takes considerable
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    11
    time.  The overhead of scheduling is significantly higher than
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    12
    just traversing the list of operands sequentially.
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    13
28358
5d79c5d68459 tuned comments;
wenzelm
parents: 28357
diff changeset
    14
  * The order of operator application is non-deterministic.  Watch out
28199
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    15
    for operators that have side-effects or raise exceptions!
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    16
*)
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    17
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    18
signature PAR_LIST =
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    19
sig
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    20
  val map: ('a -> 'b) -> 'a list -> 'b list
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    21
  val get_some: ('a -> 'b option) -> 'a list -> 'b option
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    22
  val find_some: ('a -> bool) -> 'a list -> 'a option
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    23
  val exists: ('a -> bool) -> 'a list -> bool
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    24
  val forall: ('a -> bool) -> 'a list -> bool
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    25
end;
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    26
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    27
structure ParList: PAR_LIST =
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    28
struct
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    29
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    30
fun raw_map f xs =
28645
605a3b1ef6ba added Future.enabled check;
wenzelm
parents: 28549
diff changeset
    31
  if Future.enabled () then
28549
78affc7d4d0f subject to Multithreading.enabled;
wenzelm
parents: 28443
diff changeset
    32
    let
78affc7d4d0f subject to Multithreading.enabled;
wenzelm
parents: 28443
diff changeset
    33
      val group = TaskQueue.new_group ();
78affc7d4d0f subject to Multithreading.enabled;
wenzelm
parents: 28443
diff changeset
    34
      val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
28646
3a8d75c935ce Future.join_result;
wenzelm
parents: 28645
diff changeset
    35
      val _ = List.app (ignore o Future.join_result) futures;
28549
78affc7d4d0f subject to Multithreading.enabled;
wenzelm
parents: 28443
diff changeset
    36
    in Future.join_results futures end
78affc7d4d0f subject to Multithreading.enabled;
wenzelm
parents: 28443
diff changeset
    37
  else map (Exn.capture f) xs;
28199
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    38
28443
de653f1ad78b more robust treatment of Interrupt (cf. exn.ML);
wenzelm
parents: 28383
diff changeset
    39
fun map f xs = Exn.release_first (raw_map f xs);
28199
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    40
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    41
fun get_some f xs =
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    42
  let
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    43
    exception FOUND of 'b option;
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    44
    fun found (Exn.Exn (FOUND some)) = some
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    45
      | found _ = NONE;
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    46
    val results = raw_map (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    47
  in
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    48
    (case get_first found results of
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    49
      SOME y => SOME y
28443
de653f1ad78b more robust treatment of Interrupt (cf. exn.ML);
wenzelm
parents: 28383
diff changeset
    50
    | NONE => (Exn.release_first results; NONE))
28199
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    51
  end;
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    52
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    53
fun find_some P = get_some (fn x => if P x then SOME x else NONE);
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    54
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    55
fun exists P = is_some o get_some (fn x => if P x then SOME () else NONE);
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    56
fun forall P = not o exists (not o P);
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    57
e63d05ceec24 Parallel list combinators.
wenzelm
parents:
diff changeset
    58
end;