%--------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%--------------------------------------------------%
% Copyright (C) 1997-2008, 2010-2011 The University of Melbourne.
% Copyright (C) 2014-2023 The Mercury team.
% This file is distributed under the terms specified in COPYING.LIB.
%--------------------------------------------------%
%
% 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).

    % A domain error exception, which indicates that the inputs
    % to a predicate or function were outside the domain of that
    % predicate or function. The string indicates where the error occurred.
    %
:- type domain_error
    --->    domain_error(string).

%--------------------------------------------------%

    % throw(Exception):
    %
    % Throw the specified exception.
    %
:- func throw(T) = _ is erroneous.
:- pred throw(T::in) is erroneous.
% The termination analyzer can infer termination of throw/1 itself but
% declaring it to be terminating here means that all of the standard library
% will treat it as terminating as well.
:- pragma terminates(func(throw/1)).
:- pragma terminates(pred(throw/1)).

    % 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.

% 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 for exception_result/1
    --->    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(in(pred(out) is det),       out(cannot_fail)) is cc_multi.
:- mode try(in(pred(out) is semidet),   out)              is cc_multi.
:- mode try(in(pred(out) is cc_multi),  out(cannot_fail)) is cc_multi.
:- mode try(in(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(in(pred(out, di, uo) is det),
    out(cannot_fail), di, uo) is cc_multi.
:- mode try_io(in(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(in(pred(out, di, uo) is det),
    out(cannot_fail), di, uo) is cc_multi.
:- mode try_store(in(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 set MaybeException = yes(E), otherwise set 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(in(pred(out) is det),     out, out(nil_or_singleton_list))
    is cc_multi.
:- mode try_all(in(pred(out) is semidet), out, out(nil_or_singleton_list))
    is cc_multi.
:- mode try_all(in(pred(out) is multi),   out, out) is cc_multi.
:- mode try_all(in(pred(out) is nondet),  out, out) is cc_multi.

:- inst [] for list/1
    --->    [].
:- inst nil_or_singleton_list for list/1
    --->    []
    ;       [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(in(pred(out) is nondet),
    in(pred(in, di, uo) is det), di, uo) is cc_multi.
:- mode incremental_try_all(in(pred(out) is nondet),
    in(pred(in, in, out) is det), in, out) is cc_multi.

    % finally(P, PRes, Cleanup, CleanupRes, !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.
    % An 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(in(pred(out, di, uo) is det), out,
    in(pred(out, di, uo) is det), out, di, uo) is det.
:- mode finally(in(pred(out, di, uo) is cc_multi), out,
    in(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.

%--------------------------------------------------%
%--------------------------------------------------%