Prolog unbind bound variable

Question

I have a meta trace interpreter. It is written for swi prologue.

trace(Goal):- trace(Goal, 0). trace(true, _Depth):-!, true. trace(fail, _Depth):-!, fail. trace(A > B, _Depth):-!, A > B. trace(A < B, _Depth):-!, A < B. trace(A <= B, _Depth):-!, A <= B. trace(A >= B, _Depth):-!, A >= B. trace(A = B, _Depth):-!, A = B. trace(A is B, _Depth):-!, A is B. trace(!, _Depth):-!, fail. trace(not(A), _Depth):-!, not(A). trace((Goal1, Goal2), Depth):-!, trace(Goal1, Depth), trace(Goal2, Depth). trace(Goal, Depth):- display('Call: ', Goal, Depth), clause(Goal, Body), Depth1 is Depth + 1, trace(Body, Depth1), display('Exit: ', Goal, Depth), display_redo(Goal, Depth). trace(Goal, Depth):- display('Fail: ', Goal, Depth), fail. display(Message, Goal, Depth):- tab(Depth), write(Depth), write(': '), write(Message), write(Goal), nl. display_redo(Goal, Depth):- true ; display('Redo: ', Goal, Depth), fail. just_do_it(In, Out, Query):- consult(In), tell(Out), call_with_depth_limit(findall(Query, trace(Query), _Solutions), 30, _XMessage), writeln(_XMessage), writeln(_Solutions), told, unload_file(In), true. 

It works great and as it should, except for one. When I have a variable in Query in the just_do_it(In, Out, Query) function, the output is from the associated variable. Is there a way to untie the variable in the next steps of the trace so that I can see when it is bound and when not?

Output Example:

 0: Call: a(_G1085,_G1085,_G1087) 0: Exit: a(3,3,7) 0: Redo: a(3,3,7) 1: Call: b(_G1087,_G1085) 1: Exit: b(7,3) 1: Redo: b(7,3) 1: Exit: b(5,1) 1: Redo: b(5,1) 1: Fail: b(_G1087,_G1085) 0: Fail: a(_G1085,_G1085,_G1087) 

Example output I want to have:

 0: Call: a(_G1085,_G1085,_G1087) 0: Exit: a(3,3,7) 0: Redo: a(_G1085,_G1085,_G1087) 1: Call: b(_G1087,_G1085) 1: Exit: b(7,3) 1: Redo: b(_G1087,_G1085) 1: Exit: b(5,1) 1: Redo: b(_G1087,_G1085) 1: Fail: b(_G1087,_G1085) 0: Fail: a(_G1085,_G1085,_G1087) 

Answer 1

There are several problems in your interpreter:

You are using the <= operator, which does not exist. So you should get a syntax error. In Prolog, less than or equal to =< to avoid confusion with the arrow ⇐ / <= .

You define the predicate trace/1 , but the SWI, like many other Prologs, already predicts this predicate. Therefore, it is better to use a different name.

Cut incorrectly.

The rule for not/1 should rather define (\+)/1 and read:

 trace(\+A, Depth):-!, \+trace(A, Depth). 

Evidence variables should lead to instantiation_error . Like in call(_) . Therefore you need as a first rule

 trace(V, _) :- var(V), !, throw(error(instantiation_error, _)). 

---

To display the repeat correctly, you need to replace the clause(Goal, Body), target in a more explicit way. After all, there is no way to unbind variables other than using backtracking. That is, we must find the right moment when the variables are still unreasonable. Replace clause/2 with redo_clause/3 .

 redo_clause(Depth, Goal, Body) :- findall(Goal-Body, clause(Goal, Body), [First|Rest]), ( Goal-Body = First ; length(Rest, RL), length(RestC, RL), member(Goal-Body,RestC), display('Redo: ', Goal, Depth), Rest = RestC ).