trye
Lib.trye : ('a -> 'b) -> 'a -> 'b
Maps exceptions into HOL_ERR
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 [];
Exception- The type of (it) contains a free type variable. Setting it to a unique
monotype.
Empty raised
> trye hd [];
Exception- The type of (it) contains a free type variable. Setting it to a unique
monotype.
HOL_ERR (at Lib.trye: original exn. not a HOL_ERR) raised
> trye (fn _ => raise Interrupt) 1;
Exception- The type of (it) contains a free type variable. Setting it to a unique
monotype.
Interrupt raised