% ITERATIVE-DEEPENING META-INTERPRETER   June 2001, by Kazunori Ueda
%
% To execute a goal with iterative deepening, read the meta-level
% representation (see below) of a program and say:
%     ?- id Goal1 & Goal2 & ... .
%
% --base level representation--   --meta-level representation--
% (variable)          X           (variable)          X
% (function symbol)   f           (function symbol)   f 
% (predicate symbol)  p           (function symbol)   p 
% (logical operator)  ,           (predicate symbol)  &
% (logical operator)  :-          (predicate symbol)  <=
% (clause)  H :- G1, ..., Gn      (atomic formula)  H <= G1 & ... & Gn. 
% (clause)  H.                    (atomic formula)  H <= true.

:- op(1150, xfx, <=).
:- op(950,xfy, &).
:- op(1150,fx,id).

(id A) :- retractall(cutoff),
    solve_id(A,true,30,D), write('Solved in '),
    N is 30-D, write(N), write(' step(s):').
(id A) :- cutoff, write('Depth bound reached.'), nl, fail.

solve_id(A, A,N, N).
solve_id(A0,A,N0,N) :-
    N0>0, N1 is N0-1, solve_id(A0,A1,N1,N), reduce(A1,A).
solve_id(A0,_,0, _) :- \+cutoff, assert(cutoff), fail.

reduce((true & B),C) :- reduce(B,C).
reduce((A0 & B), (A & B)) :- reduce(A0,A).
reduce(A, true) :- builtin(A), call(A).
reduce(A, B)    :- (A <= B).

% built-in predicates, could be added.
builtin(is(_,_)).
builtin(dif(_,_)).