What is wrong with this version of trace?

Question

I have this tracing meta interpreter. It is written for swi-prolog.

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 is working fine and how it should except one thing. When I have variable in Query in function just_do_it(In, Out, Query), the output is with binded variable. Is there some way to unbind the variable in further steps of tracing so I could see when it is binded and when not?

Example output :

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 wish 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)

Dorpat

Sequel: #27235648 – Petua

Answer 1

There are several issues with your interpreter:

You are using an operator <= which does not exist. So you must get a syntax error on this. In Prolog less-then-or-equal is =< to avoid confusion with an arrow ⇐ / <= .

You are defining a predicate trace/1, but SWI as many other Prologs have this predicate already predefined. So better use another name.

The cut is not correctly implemented.

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

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

Proving variables should result in an instantiation_error. Like in call(_). So you need as first rule

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

---

To display redo correctly, you need to replace the goal clause(Goal, Body), by a more explicit way. After all, there is no way to unbind variables, except via backtracking. That is, we have to find the right moment where the variables are still uninstantiated. Replace clause/2 by 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
   ).

Petua

I took your advice and I altered the interpreter with naming and operator. Yet this does not solve my problem. I edited my question and added example output and output I wish to have. – Mckown

I marked it as answer, it really helped me because you can say I am prolog noob. You mentioned that cut is not implemented correctly, can you tell me what is wrong with it? – Mckown

I found out, that now it does not display Calls and Redos with Depth 0 only Exits. I tryied to trace in swipl and there are some failures which I was not able to resolve. This happens when redo_clause/3 is there. Do you know why this happens? – Mckown

@Đrakenus: Give the query! I do see Redo at level 0. – Petua

My misstake, this should be in question with cut. – Mckown