The following is small prolog meta-interpreter that interprets the cut using the catch/throw mechanism[1].
fruit(apple).
fruit(orange) :- !.
fruit(banana).
% meta-interpreter that handles the cut
prove(true) :- !.
prove(!) :- !, ( true ; throw(cut) ).
prove((A,B)):- !, prove(A), prove(B).
prove(H) :-
catch((clause(H,B), prove(B)), cut, fail).
With plain prolog:
?- fruit(X).
X = apple
X = orange
... and with the meta-interpreter, the results are as expected:
?- prove(fruit(X)).
X = apple
X = orange
Question
My question is about retention of choices made within the scope of catch(Goal, ExceptionTag, Handler).
Q1: The SWI-Prolog documentation for catch/3[2] is not clear. But it suggests that all choices made inside Goal are discarded when an exception is raised. This, to me, doesn't accord with the observed behaviour. If all choices are lost, then prove(!):-true would not remain committed to, which would then not result in X=orange as a solution.
What am I misunderstanding about the behaviour of catch/3?
Q2: Even if the choices are retained, the effect of Handler=fail means the entire scope ((clause(H,B), prove(B)) should fail, again disgarding any choices made in that Goal.
Clearly I am misunderstanding something here.
My Attempt At Diagnosis
I changed the meta-interpreter to be more verbose at the areas of interest:
prove(!) :- writeln("111"), true.
prove(!) :- writeln("222"), throw(cut), writeln("333").
The output confirms that the choice associated with prove(!)-writeln("111"),true is retained - apparently in contradiction with the documentation.
?- prove(fruit(X)),
X = apple
111
222
X = orange
In addition to SWI-Prolog I've googled the documentation of implementations and they aren't clear either.
UPDATE:
Given the comments I am highlighting the SWI-Prolog documentation for catch/3:
all choice points generated by Goal are cut, the system backtracks to the start of catch/3
This suggests that all solutions are lost, as if the Goal in catch(Goal, Exception, Handler) was not executed.
At the time your query succeeds with the second solution (X = orange), no exception has been raised yet, and no choices have been discarded.
Only when you then ask for a further solution, does execution fail to the right hand side of ( ... ; throw(cut) ). Only then is the exception raised, discarding any remaining alternatives of the fruit(X) call.
So, this metainterpreted implementation is lazy: it discards alternatives only on failure, while a typical implementation would discard them immediately at cut time. This difference does not affect the semantics, only resource consumption. Either implementation is valid in principle.
EDIT: You seem to slightly misinterpret the documentation. To clarify: catch(Goal,...,...) behaves like call(Goal) up to the moment that a throw is encountered. It may well first succeed with multiple solutions. When the throw is executed, only the remaining choices are cut. And backtracking to the start of catch/3 only means that all of Goal's bindings at throw-time are undone before the recovery goal executes. Earlier successes cannot be undone.