wenzelm@45125: (*  Title:      Pure/Concurrent/par_exn.ML
wenzelm@45125:     Author:     Makarius
wenzelm@45125: 
wenzelm@45125: Parallel exceptions as flattened results from acyclic graph of
wenzelm@45125: evaluations.  Interrupt counts as neutral element.
wenzelm@45125: *)
wenzelm@45125: 
wenzelm@45125: signature PAR_EXN =
wenzelm@45125: sig
wenzelm@45127:   val serial: exn -> serial * exn
wenzelm@45125:   val make: exn list -> exn
wenzelm@45154:   val dest: exn -> exn list option
wenzelm@45125:   val release_all: 'a Exn.result list -> 'a list
wenzelm@45125:   val release_first: 'a Exn.result list -> 'a list
wenzelm@45125: end;
wenzelm@45125: 
wenzelm@45125: structure Par_Exn =
wenzelm@45125: struct
wenzelm@45125: 
wenzelm@45127: (* identification via serial numbers *)
wenzelm@45127: 
wenzelm@45127: fun serial exn =
wenzelm@45127:   (case get_exn_serial exn of
wenzelm@45127:     SOME i => (i, exn)
wenzelm@45171:   | NONE =>
wenzelm@45171:       let
wenzelm@45171:         val i = Library.serial ();
wenzelm@45171:         val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
wenzelm@45171:       in (i, exn') end);
wenzelm@45127: 
wenzelm@45153: val the_serial = the o get_exn_serial;
wenzelm@45153: 
wenzelm@45153: val exn_ord = rev_order o int_ord o pairself the_serial;
wenzelm@45127: 
wenzelm@45127: 
wenzelm@45125: (* parallel exceptions *)
wenzelm@45125: 
wenzelm@45147: exception Par_Exn of exn list;
wenzelm@45147:   (*non-empty list with unique identified elements sorted by exn_ord;
wenzelm@45147:     no occurrences of Par_Exn or Exn.Interrupt*)
wenzelm@45125: 
wenzelm@45147: fun par_exns (Par_Exn exns) = exns
wenzelm@45147:   | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
wenzelm@45125: 
wenzelm@45125: fun make exns =
wenzelm@45147:   (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
wenzelm@45125:     [] => Exn.Interrupt
wenzelm@45147:   | es => Par_Exn es);
wenzelm@45125: 
wenzelm@45154: fun dest (Par_Exn exns) = SOME exns
wenzelm@45153:   | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
wenzelm@45125: 
wenzelm@45125: 
wenzelm@45125: (* parallel results *)
wenzelm@45125: 
wenzelm@45125: fun release_all results =
wenzelm@45149:   if forall (fn Exn.Res _ => true | _ => false) results
wenzelm@45149:   then map Exn.release results
wenzelm@45125:   else raise make (map_filter Exn.get_exn results);
wenzelm@45125: 
wenzelm@45149: fun plain_exn (Exn.Res _) = NONE
wenzelm@45149:   | plain_exn (Exn.Exn (Par_Exn _)) = NONE
wenzelm@45149:   | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn;
wenzelm@45149: 
wenzelm@45126: fun release_first results =
wenzelm@45149:   (case get_first plain_exn results of
wenzelm@45149:     NONE => release_all results
wenzelm@45149:   | SOME exn => reraise exn);
wenzelm@45125: 
wenzelm@45125: end;
wenzelm@45125: