[mercury-users] exceptions and cc_multi

[Fergus Henderson]

On 30-Nov-2000, Michael Day <mikeday at corplink.com.au> wrote:
> 
> > It would be OK to use `promise_only_solution' here, provided that
> > `risky_operation' is det or semidet (not cc_multi or cc_nondet),
> > and that `do something impure' and `undo the impure thing' are both det.
> 
> Right. However, I can't seem to use promise_only_solution, as
> risky_operation returns a unique io__state, which appears to mess things
> up (the error messages are fairly impenetrable).

That's a good point.  It's possible to define a `promise_only_solution_io'
that works like `promise_only_solution' but which also handles I/O
procedures or other procedures with di/uo modes.

	% `promise_only_solution_io' is like `promise_only_solution',
	% but for procedures with unique modes (e.g. those that do IO).
	% 
	% A call to `promise_only_solution_io(P, X, IO0, IO)'
	% constitutes a promise on the part of the caller that for
	% the given IO0, there is only one value of `X' and `IO0' for
	% which P(X, IO0, IO) is true.  `promise_only_solution_io(P,
	% X, IO0, IO)' presumes that this assumption is satisfied, and
	% returns the X and IO for which `Pred(X, IO0, IO)' is true.
	% 
	% Note that misuse of this predicate may lead to unsound
	% results: if the assumption is not satisfied, the behaviour
	% is undefined.  (If you lie to the compiler, the compiler
	% will get its revenge!)

	:- pred promise_only_solution_io(pred(T, IO, IO), T, IO, IO).
	:- mode promise_only_solution_io(pred(out, di, uo) is cc_multi,
			out, di, uo) is det.

This can be implemented using a fairly simple hack:

	promise_only_solution_io(Pred, X) -->
		call(cc_cast_io(Pred), X).

	:- func cc_cast_io(pred(T, IO, IO)) = pred(T, IO, IO).
	:- mode cc_cast_io(pred(out, di, uo) is cc_multi) =
		out(pred(out, di, uo) is det) is det.

	:- pragma c_code(cc_cast_io(X :: (pred(out, di, uo) is cc_multi)) =
				(Y :: out(pred(out, di, uo) is det)),
			[will_not_call_mercury, thread_safe],
			"Y = X;").

I think this is a good candidate for inclusion in the standard library.

> > Proof:
> 
> <snipped>
> 
> That's a very clear proof. However... does the same proof apply for
> try_io?

No, it doesn't.  For `try_io', the final io__state is unspecified, and
in general can have more than one possible value.  The "risky_operation"
might be something like

	risky_operation -->
		print("Hello,\n"),
		{ more_risky_stuff },
		print("world!\n").

	more_risk_stuff :-
		throw("oops!").

and the compiler could potentially move the call to risk_stuff before
the call to `print("Hello,\n")' or after the call to `print("World\n")',
or run it in parallel with either of those.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------