:- module( fortprog
         , [ iddfs_assertIfNotExists/1
           , iddfs_maxList/2
           , iddfs_isNewResult/2
           , iddfs_searchDepth/1
           , iddfs_set_step/1 ]
         ).
:- dynamic user:continue_iddfs/0.
:- dynamic user:iddfs_isUserDefined/2.
:- dynamic user:iddfs_step/1.
:- dynamic user:expand_query/4.
:- multifile user:expand_query/4.
:- multifile user:term_expansion/2.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ATTENTION %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The "root" predicates are term_expansion/2 and expand_query/4, at the bottom
% of this file (for technical reasons). Skip to them to understand the other
% predicates.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%% Special queries %%%%%
% Handle the special query of loading a module (determine user defined
% predicates before).
expandQuery([Module], [Module])
    :- absolute_file_name(Module, FileName, [extensions(['.pl'])])
    ,  write(FileName), nl
    ,  preProcess(FileName).



%%%%% The pure term expanding predicates %%%%%
% Expand a query
% `?- <Query>.`
%
% to
%
% `?- iddfs_assertIfNotExists(user:continue_iddfs)
%   , iddfs_searchDepth(MaxDepth)
%   , retract(user:continue_iddfs)
%   , <Query_using_expanded_predicates>
%   , iddfs_maxList(Lvls, Lvl)
%   , iddfs_isNewResult(Lvl, MaxDepth).`
expandQuery(Query, NewQuery)
    :- termAny(isUserDefinedTerm, Query)
    -> ( expandBody(MaxDepth, Query, ExpQuery, Lvls)
       , makeConjTerm([ iddfs_assertIfNotExists(user:continue_iddfs)
                      , iddfs_searchDepth(MaxDepth)
                      , retract(user:continue_iddfs)
                      , ExpQuery
                      , iddfs_maxList(Lvls, Lvl)
                      , iddfs_isNewResult(Lvl, MaxDepth) ]
                     , NewQuery)
        )
    ; Query = NewQuery.

expandRule(Head, Body, NewHead, NewBody)
    :- functor(Head, Functor, Arity)
    ,  user:iddfs_isUserDefined(Functor, Arity)
    -> ( expandPredication(MaxDepth, Head, NewHead, Lvl)
       , expandBody(MaxD1, Body, TempBody0, Lvls)
       , expandBodyByLvlCalc(Lvls, Lvl, TempBody0, TempBody1)
       , expandBodyByDepthCalcAndCut(MaxDepth, MaxD1, TempBody1, NewBody) )
    ;  (Head = NewHead, Body = NewBody).

% Expect term (and not its parts generated by `=..`) as input.
expandPredication(Depth, CompoundTerm, Expansion, Lvl)
    :- CompoundTerm =.. CTParts
    ,  expandCompoundTermParts(Depth, CTParts, ExpCTParts, Lvl)
    ,  Expansion =.. ExpCTParts.

expandCompoundTermParts(Depth, [Functor | Args], [NewFunctor | NewArgs], Lvl)
    :- length(Args, N)
    ,  user:iddfs_isUserDefined(Functor, N)
    -> ( appendArgs([Depth, Lvl], Args, NewArgs)
       , atom_concat(Functor, '_iddfs_expanded', NewFunctor)
       )
    % Don't expand if predicate is not user-defined.
    ;  ( Functor = NewFunctor
       , Args = NewArgs
       , Lvl = 0 ).

% Expect term (and not its parts generated by `=..`) as input.
% If body is just a variable, `=..` does not work.
expandBody(_    , VarBody, VarBody, [0]) :- var(VarBody), !.
expandBody(Depth, Body   , NewBody, Lvls)
    :- Body =.. BodyParts
    ,  expandBodyParts(Depth, BodyParts, ExpBodyParts, Lvls)
    ,  NewBody =.. ExpBodyParts.

expandBodyParts(Depth, [,, Left, Right], [,, ExpLeft, ExpRight], Lvls)
    :- expandBody(Depth, Left, ExpLeft, LvlsLeft)
    ,  expandBody(Depth, Right, ExpRight, LvlsRight)
    ,  append(LvlsLeft, LvlsRight, Lvls).
expandBodyParts(Depth, [;, Left, Right], [;, ExpLeft, ExpRight], Lvls)
    :- expandBody(Depth, Left, ExpLeft, LvlsLeft)
    ,  expandBody(Depth, Right, ExpRight, LvlsRight)
    ,  append(LvlsLeft, LvlsRight, Lvls).
expandBodyParts(Depth, [->, Left, Right], [->, ExpLeft, ExpRight], Lvls)
    :- expandBody(Depth, Left, ExpLeft, LvlsLeft)
    ,  expandBody(Depth, Right, ExpRight, LvlsRight)
    ,  append(LvlsLeft, LvlsRight, Lvls).
expandBodyParts(Depth, [\+, Arg], [\+, ExpArg], Lvls)
    :- expandBody(Depth, Arg, ExpArg, Lvls).
expandBodyParts(Depth, PredicationParts, NewPred, [Lvl])
    :- PredicationTerm =.. PredicationParts
    ,  expandPredication(Depth, PredicationTerm, ExpPredTerm, Lvl)
    ,  ExpPredTerm =.. NewPred.

% Transform
%
% <Body>
%
% to
%
% <Body>, iddfs_maxList(Lvls, MaxLvl), Lvl is MaxLvl + 1
expandBodyByLvlCalc(Lvls, Lvl, Body, NewBody)
    :- makeConjTerm( [ Body
                     , iddfs_maxList(Lvls, MaxLvl)
                     , Lvl is MaxLvl + 1]
                   , NewBody).

% Transform
% <Body>
%
% to
%
% N > 0 -> ( N1 is N - 1, <Body> )
%        ; (iddfs_assertIfNotExists(user:continue_iddfs), fail)
expandBodyByDepthCalcAndCut(MaxDepth, MaxD1, Body, NewBody)
    :- makeConjTerm([MaxD1 is MaxDepth - 1, Body], ThenAction)
    ,  makeDisjTerm([ MaxDepth > 0 -> ThenAction
                    , (iddfs_assertIfNotExists(user:continue_iddfs)
                    , fail)]
                   , NewBody).



%%%%% Specific utility predicates %%%%%
iddfs_assertIfNotExists(Term) :- \+ Term -> asserta(Term) ; true.

% This determines the step used to increase the search depth. It is configurable
% by using `iddfs_set_step/1`.
user:iddfs_step(1).

iddfs_set_step(N) :- retractall(user:iddfs_step(_)), asserta(user:iddfs_step(N)).

% Count from 0 to infinity using global step setting.
iddfs_searchDepth(0).
iddfs_searchDepth(D)
    :- user:continue_iddfs
    ,  iddfs_searchDepth(D1)
    ,  user:iddfs_step(Step)
    ,  D is D1 + Step.

iddfs_maxList([], 0). % For our purpose this is a good choice.
iddfs_maxList([ X | Xs ], Max)
    :- iddfs_maxList(Xs, MaxSoFar)
    , (ground(X) -> Max is max(X, MaxSoFar)
                  ; Max is MaxSoFar).

% A result is considered new, if it is found within a new interval.
iddfs_isNewResult(Lvl, MaxDepth)
    :- user:iddfs_step(Step)
    ,  Lvl >= MaxDepth - Step + 1.

preProcess(Module)
    :- open(Module, read, Stream)
    ,  read_terms(Stream, Terms)
    ,  checkForIllegalOps(Terms)
    ,  getUserDefinedPreds(Terms)
    ,  close(Stream).

read_terms(Stream, [])
    :- at_end_of_stream(Stream).
read_terms(Stream, [T | Ts])
    :- \+ at_end_of_stream(Stream)
    ,  read(Stream, T)
    ,  read_terms(Stream, Ts).

checkForIllegalOps(Terms) :- listAny(termAny(isForbiddenOp), Terms), !.
checkForIllegalOps(_).

isForbiddenOp(Term)
    :- \+ var(Term)
    -> functor(Term, '!', 0)
    ,  syntax_error('IDDFS is not compatible with the cut (!) operator!').
isForbiddenOp(Term)
    :- \+ var(Term)
    -> functor(Term, \+, 1)
    ,  syntax_error('IDDFS is not compatible with the negation (\\+) operator!').

getUserDefinedPreds(Terms)
    :- retractall(user:iddfs_isUserDefined(_,_))
    ,  dispatch_terms(Terms).

isUserDefinedTerm(Term)
    :- \+ var(Term) -> functor(Term, F, A), user:iddfs_isUserDefined(F, A).

markAsUserDefined(Term)
    :- functor(Term, F, A)
    ,  F \= end_of_file
    -> iddfs_assertIfNotExists(user:iddfs_isUserDefined(F, A))
    ;  true.

% Transform terms from argument list to an right associative conjunction term.
% For example: `[true, false, true, false]` becomes `true, (false, (true, false))`
makeConjTerm(Args, Result) :- makeOpTerm(,, Args, Result).

% See `makeConjTerm`, but with `;` instead of `,`
makeDisjTerm(Args, Result) :- makeOpTerm(;, Args, Result).

appendArgs(Args, OldArgs, NewArgs) :- append(OldArgs, Args, NewArgs).



%%%%% Generic utility predicates %%%%%
% True if Goal can successfully be applied on root term, or if termAny(Goal, ST)
% can can successfully be applied on any subterm ST of the root term.
% Mind that the root term could also be a variable or an atom.
termAny(Goal, Term) :- call(Goal, Term), !.
termAny(Goal, Term)
    :- \+ var(Term)
    -> Term =.. [ _ | Args ], listAny(termAny(Goal), Args).

% True if Goal can successfully be applied on any element of List
listAny(Goal, [X | _ ]) :- call(Goal, X), !.
listAny(Goal, [_ | Xs]) :- listAny(Goal, Xs).

% Contruct term using given binary op. For example:
% makeOpTerm( op, [x1, ..., xn], x1 op (x2 op (...( xn-1 op xn)...)) ).
makeOpTerm(_ , [Arg0], Result) :- Result = Arg0.
makeOpTerm(Op, [Arg0, Arg1 | Args], Result)
    :- makeOpTerm(Op, [Arg1 | Args], TempRes)
    ,  Result =.. [Op, Arg0, TempRes].


%%%%% The Dispatching of terms %%%%%
%%% Dispatching needed during term expansion
dispatch([:-, Directive], [:-, Directive]) :- !.
dispatch([?-, Query], [?-, NewQuery]) :- expandQuery(Query, NewQuery), !.
dispatch([:-, Head, Body], [:-, NewHead, NewBody])
    :- expandRule(Head, Body, NewHead, NewBody), !.
dispatch(PredicationParts, NewPred)
    :- PredicationTerm =.. PredicationParts
    ,  expandPredication(_, PredicationTerm, ExpPredTerm, 0)
    ,  ExpPredTerm =.. NewPred.

%%% Dispatching needed during query expansion
dispatch_terms([]).
dispatch_terms([T | Ts]) :- T =.. TParts, dispatch(TParts), dispatch_terms(Ts).

dispatch([:-, _]) :- !.
dispatch([?-, _]) :- !.
dispatch([:-, Head, _]) :- markAsUserDefined(Head), !.
dispatch(PredParts) :- Pred =.. PredParts,  markAsUserDefined(Pred).

%%%%% The hooks which initiate term expansion %%%%%
:- asserta((user:expand_query(Q1,Q2,B,B) :- expandQuery(Q1, Q2))).
:- asserta((user:term_expansion(Term, Expansion) :- Term =.. Parts, dispatch(Parts, ProcessedParts), Expansion =.. ProcessedParts)).

%%% Greeting message:
:- write('Welcome to SWI-Prolog (extended WITH COMPLETE SEARCH for FortProg, 20/01/17).'),
   nl.
