28199

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 

28358

14 
* The order of operator application is nondeterministic. Watch out

28199

15 
for operators that have sideeffects 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 =

28549

31 
if ! future_scheduler andalso Multithreading.enabled () then


32 
let


33 
val group = TaskQueue.new_group ();


34 
val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;


35 
val _ = List.app (ignore o Future.join_results o single) futures;


36 
in Future.join_results futures end


37 
else map (Exn.capture f) xs;

28199

38 

28443

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

28199

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

28443

50 
 NONE => (Exn.release_first results; NONE))

28199

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;
