Implementing cut in tracing meta interpreter prolog

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.

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)