У меня есть мета-интерпретатор трассировки, измененный с предыдущего вопросаПролог unbind связанной переменной.

Я не понимаю, как интерпретировать разрез. Благодаря пользователю @false, который сказал мне, что разрез плохо реализован, у меня вопрос, как мне реализовать разрез в этом мета-интерпретаторе?

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