author  wenzelm 
Wed, 17 Aug 2011 22:25:00 +0200  
changeset 44248  6a3541412b23 
parent 44247  270366301bd7 
child 44249  64620f1d6f87 
permissions  rwrr 
44247  1 
(* Title: Pure/Concurrent/par_exn.ML 
2 
Author: Makarius 

3 

4 
Parallel exceptions as flattened results from acyclic graph of 

5 
evaluations. Interrupt counts as neutral element. 

6 
*) 

7 

8 
signature PAR_EXN = 

9 
sig 

10 
val make: exn list > exn 

11 
val dest: exn > (serial * exn) list option 

12 
val release_all: 'a Exn.result list > 'a list 

13 
val release_first: 'a Exn.result list > 'a list 

14 
end; 

15 

16 
structure Par_Exn = 

17 
struct 

18 

19 
(* parallel exceptions *) 

20 

21 
exception Par_Exn of (serial * exn) Ord_List.T; 

22 

23 
fun exn_ord ((i, _), (j, _)) = int_ord (j, i); 

24 

25 
fun par_exns (Par_Exn exns) = SOME exns 

26 
 par_exns exn = if Exn.is_interrupt exn then NONE else SOME [(serial (), exn)]; 

27 

28 
fun make exns = 

29 
(case map_filter par_exns exns of 

30 
[] => Exn.Interrupt 

31 
 e :: es => Par_Exn (Library.foldl (Ord_List.merge exn_ord) (e, es))); 

32 

33 
fun dest (Par_Exn exns) = SOME (rev exns) 

34 
 dest _ = NONE; 

35 

36 

37 
(* parallel results *) 

38 

39 
fun all_res results = forall (fn Exn.Res _ => true  _ => false) results; 

40 

41 
fun release_all results = 

42 
if all_res results then map Exn.release results 

43 
else raise make (map_filter Exn.get_exn results); 

44 

44248
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset

45 
fun release_first results = 
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset

46 
if all_res results then map Exn.release results 
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset

47 
else 
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset

48 
(case get_first 
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset

49 
(fn res => if Exn.is_interrupt_exn res then NONE else Exn.get_exn res) results of 
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset

50 
NONE => Exn.interrupt () 
6a3541412b23
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
wenzelm
parents:
44247
diff
changeset

51 
 SOME exn => reraise exn); 
44247  52 

53 
end; 

54 