src/Pure/ML-Systems/exn.ML
author wenzelm
Thu Oct 01 23:27:05 2009 +0200 (2009-10-01)
changeset 32843 c8f5a7c8353f
parent 32100 8ac6b1102f16
permissions -rw-r--r--
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
wenzelm@23962
     1
(*  Title:      Pure/ML-Systems/exn.ML
wenzelm@23962
     2
    Author:     Makarius
wenzelm@23962
     3
wenzelm@28444
     4
Extra support for exceptions.
wenzelm@23962
     5
*)
wenzelm@23962
     6
wenzelm@28444
     7
signature EXN =
wenzelm@28444
     8
sig
wenzelm@28444
     9
  datatype 'a result = Exn of exn | Result of 'a
wenzelm@28444
    10
  val get_result: 'a result -> 'a option
wenzelm@28444
    11
  val get_exn: 'a result -> exn option
wenzelm@28444
    12
  val capture: ('a -> 'b) -> 'a -> 'b result
wenzelm@28444
    13
  val release: 'a result -> 'a
wenzelm@28444
    14
  exception Interrupt
wenzelm@28459
    15
  exception EXCEPTIONS of exn list
wenzelm@32100
    16
  val flatten: exn -> exn list
wenzelm@32100
    17
  val flatten_list: exn list -> exn list
wenzelm@28444
    18
  val release_all: 'a result list -> 'a list
wenzelm@28444
    19
  val release_first: 'a result list -> 'a list
wenzelm@28444
    20
end;
wenzelm@28444
    21
wenzelm@28444
    22
structure Exn: EXN =
wenzelm@23962
    23
struct
wenzelm@23962
    24
wenzelm@28444
    25
(* runtime exceptions as values *)
wenzelm@28444
    26
wenzelm@23962
    27
datatype 'a result =
wenzelm@23962
    28
  Result of 'a |
wenzelm@23962
    29
  Exn of exn;
wenzelm@23962
    30
wenzelm@23962
    31
fun get_result (Result x) = SOME x
wenzelm@23962
    32
  | get_result _ = NONE;
wenzelm@23962
    33
wenzelm@23962
    34
fun get_exn (Exn exn) = SOME exn
wenzelm@23962
    35
  | get_exn _ = NONE;
wenzelm@23962
    36
wenzelm@23962
    37
fun capture f x = Result (f x) handle e => Exn e;
wenzelm@23962
    38
wenzelm@23962
    39
fun release (Result y) = y
wenzelm@31427
    40
  | release (Exn e) = reraise e;
wenzelm@23962
    41
wenzelm@28444
    42
wenzelm@28459
    43
(* interrupt and nested exceptions *)
wenzelm@28444
    44
wenzelm@28444
    45
exception Interrupt = Interrupt;
wenzelm@28459
    46
exception EXCEPTIONS of exn list;
wenzelm@28444
    47
wenzelm@32100
    48
fun flatten Interrupt = []
wenzelm@32100
    49
  | flatten (EXCEPTIONS exns) = flatten_list exns
wenzelm@32100
    50
  | flatten exn = [exn]
wenzelm@32100
    51
and flatten_list exns = List.concat (map flatten exns);
wenzelm@23962
    52
wenzelm@28444
    53
fun release_all results =
wenzelm@28444
    54
  if List.all (fn Result _ => true | _ => false) results
wenzelm@28444
    55
  then map (fn Result x => x) results
wenzelm@32100
    56
  else raise EXCEPTIONS (flatten_list (List.mapPartial get_exn results));
wenzelm@28444
    57
wenzelm@28444
    58
fun release_first results = release_all results
wenzelm@31427
    59
  handle EXCEPTIONS (exn :: _) => reraise exn;
wenzelm@28444
    60
wenzelm@23962
    61
end;