----------------------------------------------------------------------
trye                                                             (Lib)
----------------------------------------------------------------------
trye : ('a -> 'b) -> 'a -> 'b

SYNOPSIS
Maps exceptions into {HOL_ERR}

KEYWORDS
exception, error handling.

DESCRIBE
The standard exception for HOL applications to raise is {HOL_ERR}. The
use of a single exception simplifies the writing of exception handlers
and facilities for decoding and printing error messages. However, ML
functions that raise exceptions, such as {hd} and many others, are often
used to implement HOL programs. In such cases, {trye} may be used to
coerce exceptions into applications of {HOL_ERR}. Note however, that the
{Interrupt} exception is not coerced by {trye}.

The application {trye f x} evaluates {f x}; if this evaluates to {y},
then {y} is returned. However, if evaluation raises an exception {e},
there are three cases: if {e} is {Interrupt}, then it is raised; if {e}
is {HOL_ERR}, then it is raised; otherwise, {e} is mapped to an
application of {HOL_ERR} and then raised.

FAILURE
Fails if the function application fails.

EXAMPLE

- hd [];
! Uncaught exception:
! Empty

- trye hd [];
! Uncaught exception:
! HOL_ERR

- trye (fn _ => raise Interrupt) 1;
> Interrupted




SEEALSO
Lib, Feedback.Raise, Lib.try.

----------------------------------------------------------------------