1(* Title: Pure/Concurrent/par_exn.ML 2 Author: Makarius 3 4Parallel exceptions as flattened results from acyclic graph of 5evaluations. Interrupt counts as neutral element. 6*) 7 8signature PAR_EXN = 9sig 10 val make: exn list -> exn 11 val dest: exn -> exn list option 12 val is_interrupted: 'a Exn.result list -> bool 13 val release_all: 'a Exn.result list -> 'a list 14 val release_first: 'a Exn.result list -> 'a list 15end; 16 17structure Par_Exn: PAR_EXN = 18struct 19 20(* parallel exceptions *) 21 22exception Par_Exn of exn list; 23 (*non-empty list with unique identified elements sorted by exn_ord; 24 no occurrences of Par_Exn or Exn.Interrupt*) 25 26fun par_exns (Par_Exn exns) = exns 27 | par_exns exn = if Exn.is_interrupt exn then [] else [exn]; 28 29fun make exns = 30 let 31 val exnss = map par_exns exns 32 val exns' = List.concat exnss 33 in if null exns' then Exn.Interrupt else Par_Exn exns' end; 34 35fun dest (Par_Exn exns) = SOME exns 36 | dest exn = if Exn.is_interrupt exn then SOME [] else NONE; 37 38 39(* parallel results *) 40 41fun is_interrupted results = 42 List.exists (fn Exn.Exn _ => true | _ => false) results andalso 43 Exn.is_interrupt (make (List.mapPartial Exn.get_exn results)); 44 45fun release_all results = 46 if List.all (fn Exn.Res _ => true | _ => false) results 47 then map Exn.release results 48 else raise make (List.mapPartial Exn.get_exn results); 49 50fun plain_exn (Exn.Res _) = NONE 51 | plain_exn (Exn.Exn (Par_Exn _)) = NONE 52 | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn; 53 54fun release_first results = 55 (case Portable.first_opt (fn _ => plain_exn) results of 56 NONE => release_all results 57 | SOME exn => Exn.reraise exn); 58 59end; 60