committing to choices in the scope of catch/3

Question

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.

---

1. Implementing cut in tracing meta interpreter prolog

2. https://www.swi-prolog.org/pldoc/man?predicate=catch/3

Answer 1

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.

Answer 2

This clause creates two choice points:

%   |------- #1 ----------|--- #2 -----|
    prove(!) :- !, ( true ; throw(cut) ).

The first choice point will simply succeed. This is producing the X = orange solution. You can see it in this trace (using trace/0 in SWI):

^  Redo: (14) clause(fruit(_7766), _9820) ? creep
^  Exit: (14) clause(fruit(orange), !) ? creep
   Call: (14) prove(!) ? creep
   Call: (15) true ? creep
   Exit: (15) true ? creep
   Exit: (14) prove(!) ? creep
^  Exit: (12) catch(user:(clause(fruit(orange), !), prove(!)), cut, user:fail) ? creep
   Exit: (11) prove(fruit(orange)) ? creep
X = orange ;

Notice how throw/1 was never called. Next it will redo on prove(!) but from its #2 choice point this time which will throw:

   Redo: (14) prove(!) ? creep
   Call: (15) throw(cut) ? creep
   Exception: (15) throw(cut) ? creep
   Exception: (14) prove(!) ? creep
   Fail: (11) prove(fruit(_18)) ? creep
false.

Now it throws, catches, and fails, emulating the cut behavior.

TL;DR: (true ; throw(foo) ) does not throw immediately, it first succeeds and then only throws upon backtracking.