I have previously asked about implementing the cut in a simple prolog meta-interpreter: handling the cut with a simple meta-interpreter
A comment pointed me to using the throw(cut)/catch combination: Implementing cut in tracing meta interpreter prolog
This is a simpler program to minimise distraction and help focus on the issue:
fruit(apple).
fruit(orange) :- !.
fruit(banana).
% meta-interpreter
prove(true) :- !.
prove(!) :- !, ( true ; throw(cut) ).
prove((A,B)):- !, prove(A), prove(B).
prove(H) :- clause(H,B),
catch(prove(B), cut, fail),
write(H), write(" <- "), writeln(B).
The desired behaviour is this:
?- fruit(X)
X = apple
X = orange
When using the meta-interpreter, it seem the cut is not implemented correctly:
?- prove(fruit(X)).
fruit(apple) <- true
X = apple ;
fruit(orange) <- !
X = orange ;
fruit(banana) <- true
X = banana.
Question: Why isn't the meta-interpreter implementation of cut working as expected?
I have traced the query (removing the lines related to write/1). The traces for the three fruit appear the same suggesting the prove(!)
is not throwing cut
.
Call:prove(fruit(_6416))
Call:clause(fruit(_504),_722)
Exit:clause(fruit(apple),true)
Call:catch(prove(true),cut,fail)
Exit:catch('5afa3202-4e65-4ba4-b81d-893043450958' :prove(true),cut,'5afa3202-4e65-4ba4-b81d-893043450958' :fail)
Exit:prove(fruit(apple))
X = apple
Redo:clause(fruit(_504),_720)
Exit:clause(fruit(orange),!)
Call:catch(prove(!),cut,fail)
Exit:catch('5afa3202-4e65-4ba4-b81d-893043450958' :prove(!),cut,'5afa3202-4e65-4ba4-b81d-893043450958' :fail)
Exit:prove(fruit(orange))
X = orange
Redo:catch('5afa3202-4e65-4ba4-b81d-893043450958' :prove(!),cut,'5afa3202-4e65-4ba4-b81d-893043450958' :fail)
Exit:clause(fruit(banana),true)
Call:catch(prove(true),cut,fail)
Exit:catch('5afa3202-4e65-4ba4-b81d-893043450958' :prove(true),cut,'5afa3202-4e65-4ba4-b81d-893043450958' :fail)
Exit:prove(fruit(banana))
X = banana
Your problem is that you are catching just one clause at a time instead of the whole rule. You are backtracking over the alternatives given by clause/2
.
So your last clause of prove/1
may be written:
prove(H) :-
catch(
(clause(H,B),
prove(B)
), cut, fail),
write(H), write(" <- "), writeln(B).