Implementing cut in tracing meta interpreter prolog

Question

I have this tracing meta interpreter, altered from previous question Prolog unbind bound variable.

I don't understand how to interpret cut. Thanks to user @false who told me that the cut is badly implemented, my question is, how should I implement cut in this meta-interpreter?

%tracer
mi_trace(Goal):-
    mi_trace(Goal, 0).

mi_trace(V, _):-
    var(V), !, throw(error(instantiation_error, _)).
mi_trace(true, _Depth):-!, true.
mi_trace(fail, _Depth):-!, fail.
mi_trace(A > B, _Depth):-!, A > B.
mi_trace(A < B, _Depth):-!, A < B.
mi_trace(A =< B, _Depth):-!, A =< B.
mi_trace(A >= B, _Depth):-!, A >= B.
mi_trace(A = B, _Depth):-!, A = B.
mi_trace(A is B, _Depth):-!, A is B.
mi_trace(\+A, _Depth):-!, \+mi_trace(A, _Depth).
mi_trace(!, _Depth):-!, fail. % <- this is wrong
mi_trace((Goal1, Goal2), Depth):-
    !,
    mi_trace(Goal1, Depth),
    mi_trace(Goal2, Depth).
mi_trace(Goal, Depth):-
    display('Call: ', Goal, Depth),
    redo_clause(Depth, Goal, Body),
    Depth1 is Depth + 1,
    mi_trace(Body, Depth1),
    display('Exit: ', Goal, Depth).
mi_trace(Goal, Depth):-
    display('Fail: ', Goal, Depth),
    fail.

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

display(Message, Goal, Depth):-
    tab(Depth), write(Depth), write(': '), write(Message),
    write(Goal), nl.

trace_query(In, Out, Query):-
    consult(In),
    tell(Out),
    call_with_depth_limit(findall(Query, mi_trace(Query), _Solutions), 30, _XMessage),
    writeln(_XMessage),
    writeln(_Solutions),
    told,
    unload_file(In),
    true.

Glue

Answer 1

Let me start with a simple implementation that works for many programs, but not all of them.

Using catch/3 and throw/1

This method is definitely the simplest way to implement the cut in ISO Prolog. However, it is not very efficient. The basic idea is that cut simply succeeds, and only on backtracking it will fail up to the last invocation of mi_call/1. Note that only mi_call/1 constructs will be able to catch those cuts. As a consequence, all user defined goals have to be wrapped with mi_call/1. Same accordingly for built-ins like setof/3.

A naive implementation is:

mi_cut.
mi_cut :- throw(cut).

mi_call(Goal) :-
   catch(Goal, cut, fail).

In your meta-interpreter, exchange two rules to:

mi_trace(!, _Depth):-!, ( true ; throw(cut) ).
...
mi_trace(Goal, Depth):-
    display('Call: ', Goal, Depth),
    Depth1 is Depth + 1,
    catch(
       ( redo_clause(Depth, Goal, Body),
         mi_trace(Body, Depth1)
       ),
       cut,
       fail),
    display('Exit: ', Goal, Depth).

This works for almost every program. Except those, that throw(cut) themselves. Or want to catch all exceptions. It is these tiny little things that makes a general implementation much more complex.

In your tracer, you have not implemented call/1, catch/3, throw/1 for the moment, so these problems will not show - you simply get an error for those. (Maybe TBC)

Caesarism

This is purely amazing. Thank you very much. I just want to ask that if it is necessary to implement call/1, catch/3, throw/1? It seems to work fine with swi-prolog defined call, catch and throw. – Jehovah

@Đrakenus: If the programs you are tracing are not using these constructs, there is no need for them. Currently, trace(throw(xx)) produces permission_error(access,private_procedure,throw/1) and that's fine. – Caesarism

I have simple program in file v(X):-p(X),s(X). v(n). p(m). p(o). s(o). s(p). (sorry about formating), and it does not display Redo at level 0, currently it do Exit at level 0 but not displaying Redo when there should be. You can look at it here - http://pastebin.com/Wgq2R7DF – Jehovah

@Đrakenus: There is a redo for v(X)! But in line 26. Compare this to SWI's trace! – Caesarism

Oh. You are right! Thanks for clarification, I'm just little stressed and doing stupid misstakes. – Jehovah

hi @Caesarism - ive not seen this solution anywhere else. is this a standard pattern or is this something you've invented? I'd like to use this pattern in a guide in preparing - how would you like to be credited, if at all? – Nonunion

No, not my invention. It has been around for some time. See 7.8.4.1 NOTE 1 c. You really need to look at the literature, first. Also note that this here is not a meta-circular version. – Caesarism

hi @Caesarism what is the reference 7.8.4.1 NOTE 1 c ? I google it and didn't locate anything (ISO reference?) Bratoko doesn't have a 7,8.4 and neither does Shapiro, nor LPN. – Nonunion

iso-prolog – Caesarism

what happens if instead of (true ; throw(cut)) we have throw(cut) ? What happens if we remove the disjunctive true? My testing shows it doesn't work as expected, but I can't put into words why. – Nonunion

If you throw(cut) directly, you will get failure immediately. – Caesarism