% iterative deepening meta-interpreter for Prolog, this version Sicstus.
% using straight comma separated lists for clause bodies.
% Does not deal with built-ins.

% iterative deepening metainterpreter.
idsolve(Query) :- idsolve(Query,0).
idsolve(Query,N) :- tag(Query,N,QQ), solve(QQ),
                    write('Solution found during search to depth '), write(N).
idsolve(Query,N) :- M is N+1, write('Searching at depth '),
                    write(M),nl, idsolve(Query,M).

solve( true/_) :- !.                 %% base case
solve( (A,B) ) :- solve(A), solve(B). %% comma separated pair of goals
solve(  Q/N ) :-   0<N, M is N-1,    %% resolution step, atomic goal
	                             %% unifies with head of a clause;
	                             %% note change of depth.
	           clause( Q, Body ), 
                   tag(Body,M,Tagged),
                   solve( Tagged ).

% tag(+,+,?) distributes depth label to subgoals
tag( (A,B), N, (AA,BB) ) :- tag(A,N,AA), tag(B,N,BB), !.
tag(   A, N, A/N ) :- \+ A = (_,_).

%% some testing data

:- dynamic app/3.
:- dynamic test/2.
:- dynamic foo/1.
:- dynamic mem/2.
:- dynamic p1/1.
:- dynamic p2/1.

app([],Y,Y).
app([H|T],Y,[H|TT]) :- app(T,Y,TT).

mem(X,[X|_]).
mem(X,[_|T]) :- mem(X,T).

test(X,_):- app([1,2,3,4,5,6,7,8,9],[],X),app([1],[],[]).
test(1,1).

foo(X) :- foo(X).
foo(34).

p1(5) :- p1(0).
p1(5) :- p1(3), p2(4).
p1(3) :- p1(2).
p1(2) :- p1(1).
p1(1).
p2(_).




%% queries:  compare:
%% ?- foo(X).                % loops
%% ?- idsolve(foo(X)).       % finds solution.
%%
%% ?- p1(X).                 % solutions in different order
%% ?- idsolve(p1(X)).        %  here, find shortes derivations first
%%
%% ?- test(X,Y).             %% succeeds after going down a longish dead end
%% ?- id_solve(test(X,Y)).   %% faster 
