25 exception
%--------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
%--------------------------------------------------%
% Copyright (C) 1997-2008, 2010-2011 The University of Melbourne.
% This file may only be copied under the terms of the GNU Library General
% Public License - see the file COPYING.LIB in the Mercury distribution.
%--------------------------------------------------%
%
% File: exception.m.
% Main author: fjh.
% Stability: medium.
%
% This module defines the Mercury interface for exception handling.
%
% Note that throwing an exception across the C interface won't work.
% That is, if a Mercury procedure that is exported to C using
% `pragma foreign_export' throws an exception which is not caught within that
% procedure, then you will get undefined behaviour.
%
%--------------------------------------------------%
%--------------------------------------------------%
:- module exception.
:- interface.
:- import_module io.
:- import_module list.
:- import_module maybe.
:- import_module store.
:- import_module univ.
%--------------------------------------------------%
% Exceptions of this type are used by many parts of the Mercury
% implementation to indicate an internal error.
%
:- type software_error
---> software_error(string).
% throw(Exception):
% Throw the specified exception.
%
:- func throw(T) = _ is erroneous.
:- pred throw(T::in) is erroneous.
% The following type and inst are used by try/3 and try/5.
:- type exception_result(T)
---> succeeded(T)
; failed
; exception(univ).
:- inst cannot_fail
---> succeeded(ground)
; exception(ground).
% try(Goal, Result):
%
% Operational semantics:
% Call Goal(R).
% If Goal(R) fails, succeed with Result = failed.
% If Goal(R) succeeds, succeed with Result = succeeded(R).
% If Goal(R) throws an exception E, succeed with
% Result = exception(E).
%
% Declarative semantics:
% try(Goal, Result) <=>
% ( Goal(R), Result = succeeded(R)
% ; not Goal(_), Result = failed
% ; Result = exception(_)
% ).
%
:- pred try(pred(T), exception_result(T)).
:- mode try(pred(out) is det, out(cannot_fail)) is cc_multi.
:- mode try(pred(out) is semidet, out) is cc_multi.
:- mode try(pred(out) is cc_multi, out(cannot_fail)) is cc_multi.
:- mode try(pred(out) is cc_nondet, out) is cc_multi.
% try_io(Goal, Result, IO_0, IO):
%
% Operational semantics:
% Call Goal(R, IO_0, IO_1).
% If it succeeds, succeed with Result = succeeded(R)
% and IO = IO_1.
% If it throws an exception E, succeed with Result = exception(E)
% and with the final IO state being whatever state
% resulted from the partial computation from IO_0.
%
% Declarative semantics:
% try_io(Goal, Result, IO_0, IO) <=>
% ( Goal(R, IO_0, IO), Result = succeeded(R)
% ; Result = exception(_)
% ).
%
:- pred try_io(pred(T, io, io), exception_result(T), io, io).
:- mode try_io(pred(out, di, uo) is det,
out(cannot_fail), di, uo) is cc_multi.
:- mode try_io(pred(out, di, uo) is cc_multi,
out(cannot_fail), di, uo) is cc_multi.
% try_store(Goal, Result, Store_0, Store):
%
% Just like try_io, but for stores rather than io.states.
%
:- pred try_store(pred(T, store(S), store(S)),
exception_result(T), store(S), store(S)).
:- mode try_store(pred(out, di, uo) is det,
out(cannot_fail), di, uo) is cc_multi.
:- mode try_store(pred(out, di, uo) is cc_multi,
out(cannot_fail), di, uo) is cc_multi.
% try_all(Goal, MaybeException, Solutions):
%
% Operational semantics:
% Try to find all solutions to Goal(S), using backtracking.
% Collect the solutions found in Solutions, until the goal
% either throws an exception or fails. If it throws an
% exception E then MaybeException = yes(E), otherwise
% MaybeException = no.
%
% Declaratively it is equivalent to:
% all [S] (list.member(S, Solutions) => Goal(S)),
% (
% MaybeException = yes(_)
% ;
% MaybeException = no,
% all [S] (Goal(S) => list.member(S, Solutions))
% ).
%
:- pred try_all(pred(T), maybe(univ), list(T)).
:- mode try_all(pred(out) is det, out, out(nil_or_singleton_list))
is cc_multi.
:- mode try_all(pred(out) is semidet, out, out(nil_or_singleton_list))
is cc_multi.
:- mode try_all(pred(out) is multi, out, out) is cc_multi.
:- mode try_all(pred(out) is nondet, out, out) is cc_multi.
:- inst [] ---> [].
:- inst nil_or_singleton_list ---> [] ; [ground].
% incremental_try_all(Goal, AccumulatorPred, Acc0, Acc):
%
% Declaratively it is equivalent to:
% try_all(Goal, MaybeException, Solutions),
% list.map(wrap_success, Solutions, Results),
% list.foldl(AccumulatorPred, Results, Acc0, Acc1),
% (
% MaybeException = no,
% Acc = Acc1
% ;
% MaybeException = yes(Exception),
% AccumulatorPred(exception(Exception), Acc1, Acc)
% )
%
% where (wrap_success(S, R) <=> R = succeeded(S)).
%
% Operationally, however, incremental_try_all/5 will call
% AccumulatorPred for each solution as it is obtained, rather than
% first building a list of the solutions.
%
:- pred incremental_try_all(pred(T), pred(exception_result(T), A, A), A, A).
:- mode incremental_try_all(pred(out) is nondet,
pred(in, di, uo) is det, di, uo) is cc_multi.
:- mode incremental_try_all(pred(out) is nondet,
pred(in, in, out) is det, in, out) is cc_multi.
% rethrow(ExceptionResult):
% Rethrows the specified exception result (which should be
% of the form `exception(_)', not `succeeded(_)' or `failed'.).
%
:- pred rethrow(exception_result(T)).
:- mode rethrow(in(bound(exception(ground)))) is erroneous.
:- func rethrow(exception_result(T)) = _.
:- mode rethrow(in(bound(exception(ground)))) = out is erroneous.
% finally(P, PRes, Cleanup, CleanupRes, IO0, IO).
% Call P and ensure that Cleanup is called afterwards,
% no matter whether P succeeds or throws an exception.
% PRes is bound to the output of P.
% CleanupRes is bound to the output of Cleanup.
% A exception thrown by P will be rethrown after Cleanup
% is called, unless Cleanup throws an exception.
% This predicate performs the same function as the `finally'
% clause (`try {...} finally {...}') in languages such as Java.
%
:- pred finally(pred(T, io, io), T, pred(io.res, io, io), io.res, io, io).
:- mode finally(pred(out, di, uo) is det, out,
pred(out, di, uo) is det, out, di, uo) is det.
:- mode finally(pred(out, di, uo) is cc_multi, out,
pred(out, di, uo) is cc_multi, out, di, uo) is cc_multi.
% throw_if_near_stack_limits checks if the program is near
% the limits of the Mercury stacks, and throws an exception
% (near_stack_limits) if this is the case.
%
% This predicate works only in low level C grades; in other grades,
% it never throws an exception.
%
% The predicate is impure instead of semipure because its effect
% depends not only on the execution of other impure predicates,
% but all calls.
%
:- type near_stack_limits
---> near_stack_limits.
:- impure pred throw_if_near_stack_limits is det.
%--------------------------------------------------%
%--------------------------------------------------%