[mercury-users] Exceptions (again!)

[Fergus Henderson]

On 16-Jul-1998, Ralph Becket <rwab1 at cam.sri.com> wrote:
> Thanks for the informative reply!
> 
> I wonder if exceptions could be sneakily arranged by preventing
> exception chucking predicates from being det?  Or perhaps having a
> determinism specially for this kind of thing.  Or possibly by
> including the io__state in the exception package?  I'm just throwing
> ideas around here...

The interface I'm planning on is this one.  (Comments welcome.)

I have an implementation of this which I'm happy to make available
if anyone wants to have a play around with this.  But currently
it is not yet tested very well.

%-----------------------------------------------------------------------------%
:- module exception.
:- interface.
:- import_module std_util, list, io.

%
% throw(Exception):
%	Throw the specified exception.
%
:- pred throw(T).
:- mode throw(in) is erroneous.

:- func throw(T) = _.
:- mode throw(in) = out is erroneous.

% The following types are used by try/3 and try/5.

:- type exception_result(T)
	--->	succeeded(T)
	;	failed
	;	exception(univ).

:- inst cannot_fail
	--->	succeeded(ground)
	;	exception(ground).

:- type determinism
	--->	det
	;	semidet
	;	cc_multi
	;	cc_nondet
	;	multi
	;	nondet
	;	erroneous
	;	failure.

%
% try(Determinism, Goal, Result):
%    Operational semantics:
%	Call Goal(R) (which must have the specified Determinism).
%	If Goal(R) fails, succed 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(determinism,      	  pred(T),		  exception_result(T)).
:- mode try(in(bound(det)),	  pred(out) is det,       out(cannot_fail))
							       is cc_multi.
:- mode try(in(bound(semidet)),	  pred(out) is semidet,   out) is cc_multi.
:- mode try(in(bound(cc_multi)),  pred(out) is cc_multi,  out(cannot_fail))
							       is cc_multi.
:- mode try(in(bound(cc_nondet)), pred(out) is cc_nondet, out) is cc_multi.

%
% try_io(Determinism, Goal, Result, IO_0, IO):
%    Operational semantics:
%	Call Goal(R, IO_0, IO_1) (which must have the specified Determinism).
%	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(_, Goal, Result, IO_0, IO) <=>
%		( Goal(R, IO_0, IO), Result = succeeded(R)
%		; Result = exception(_)
%		).
%
:- pred try_io(determinism, 	    pred(T, io__state, io__state),
				    exception_result(T), io__state, io__state).
:- mode try_io(in(bound(det)),      pred(out, di, uo) is det,
				    out(cannot_fail), di, uo) is cc_multi.
:- mode try_io(in(bound(cc_multi)), pred(out, di, uo) is cc_multi,
				    out(cannot_fail), di, uo) is cc_multi.

%
% try_all(Determinism, Goal, ResultList):
%    Operational semantics:
%	Try to find all solutions to Goal(R) (which must have the
%	specified Determinism), using backtracking.
%	Collect the solutions found in the ResultList, until
%	the goal either throws an exception or fails.
%	If it throws an exception, put that exception at the end of
%	the ResultList.
%    Declarative semantics:
%       try_all(_, Goal, ResultList) <=>
%		(if
%			list__reverse(ResultList, [Last | AllButLast]),
%			Last = exception(_)
%		then
%			all [M] (list__member(M, AllButLast) =>
%				(M = succeeded(R), Goal(R))),
%		else
%			all [M] (list__member(M, ResultList) =>
%				(M = succeeded(R), Goal(R))),
%			all [R] (Goal(R) =>
%				list__member(succeeded(R), ResultList)),
%		).

:- pred try_all(determinism,        pred(T), list(exception_result(T))).
:- mode try_all(in(bound(det)),	    pred(out) is det, 
				    	     out(try_all_det)) is cc_multi.
:- mode try_all(in(bound(semidet)), pred(out) is semidet,  
				    	     out(try_all_semidet)) is cc_multi.
:- mode try_all(in(bound(multi)),   pred(out) is multi, 
				    	     out(try_all_multi)) is cc_multi.
:- mode try_all(in(bound(nondet)),  pred(out) is nondet,
				    	     out(try_all_nondet)) is cc_multi.
:- inst [] ---> [].
:- inst try_all_det ---> [cannot_fail].
:- inst try_all_semidet ---> [] ; [cannot_fail].
:- inst try_all_multi ---> [cannot_fail | try_all_nondet].
:- inst try_all_nondet == list_skel(cannot_fail).

%
% 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) is erroneous.

:- func rethrow(exception_result(T)) = _.
:- mode rethrow(in) = out is erroneous.

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

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.