%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                     %
%     Meta-interpreter for Updating programs.         %
%                                                     %
%                    Joao Leite                       %
%                  Vitor Nogueira                     %
%                       1997                          %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

/*

This meta-interpreter implements the semantics of:

J. A. Leite and L. M. Pereira, 
Iterated Logic Program Updates, 
In J. Jaffar (ed.), Procs. of the 1998 Joint 
International Conference and Symposium on Logic 
Programming (JICSLP'98), Manchester, England, 
pages 265-278, MIT Press, June 1998.



The semantics used is WFSX.

 Syntax:

 Rules are of the form:
        Head <- Body.
 where Head is a literal and Body a conjunction of
 literals separated by ','.

 To write facts, simply ommit the body and the <-

 A literal is either an objective literal 'L', or a
 default negated objective literal 'not L'.
 An objective literal is an atom 'A' or an explicit
 negated atom '- A'.

 The initial program is allways empty. To consider
 an initial program P simply update empty by P.

 A file may contain several update programs separated
 by 'newProgram.'(see example).

 Warning: this metainterpreter was conceived for
 ground programs; use predicates with variables at your
 own risk.

 Acknowledgements: This meta-interpreter was based on
 another one developped by Jose Alferes
*/

/*
 Usage:

 clean -> resets the knowledge base (i.e retracts all
          updates made until the present time,
          including the initial program).

 updateF(FileName) -> updates the current knowledge base
                      (that may itself be the result of
                      several updates) with the update
                      program(s) in the file FileName.

 update(List) -> update the current knowledge base with
                 the list of rules List. Here, each
                 rule must be inside parenthesis. One
                 can have t-literals in the head,
                 meaning that that rule is to be added
                 in the refered update level.

 listUp -> Lists the current state of the knowledge
           base, i.e. all update programs.

 listUp(N) -> Lists the update program of level N.

 saveUp(FileName) -> Saves the current state (including
                     all updates made) into the file
                     FileName. The file is saved with
                     the syntax described above,so that
                     it can be used later for updateF/1.

 current(N) -> Returns in N the level of the latest
               update + 1.

 demo(G/T) -> demo of goal G when current time is T.
              G can be an objective literal 'L', or
              its default 'not L'. T can either be a
              number or 'now' (refering to the number
              of the actual update level). demo(G/now)
              proves G at the latest time level.
*/

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                Operators definition                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- op(950,fy , not ).           % Negation as failure
:- op(950,fy , '-' ).           % Expicit Negation
:- op(1110,xfy, '<-' ).         % Rule symbol
:- op(1110,yf , '<-' ).         % Rule symbol
:- op(1110,fy , '<-' ).         % Rule symbol

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                Erasing all updates                  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

clean :-
        retractall(current(_)),
        retractall(( _ <- _)).

:- dynamic current/1.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%    Updating from a file with several programs       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

updateF(FileName) :-
        getNumberOfUpdate(C),
        see(FileName),
        loadClauses(C),
        seen.

loadClauses(CR) :-
        read(C),
   ( C = end_of_file -> true;
   ( processClause(C,CR,NewCR), loadClauses(NewCR) ) ).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                Updating from a list                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

update(L) :-
        getNumberOfUpdate(C),
        update(L,C).

update([],_).
update([R|T], C) :-
        processClause(R,C,NewC), update(T,NewC).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                Processing one clause               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

processClause(newProgram,_,C) :- !,
        getNumberOfUpdate(C).
processClause(R,C,C) :-
        makeRule(R,C,Head,Body),
        assert((Head <- Body)).

makeRule( (H <- B), N, NH, NB ) :- !,
        addArgsH(H,N,C,NH),
        makeBody(B,C,NB).
makeRule( Fact, N, NF, true) :-
        addArgsH(Fact,N,_, NF).

makeBody((A,B),C,(NA,NB)) :- !,
        addArgsB(A,C,C,NA), makeBody(B,C,NB).
makeBody(A,C,NA) :-
        addArgsB(A,C,C,NA).

addArgsH(not - P/before,N,C, NP) :- !,
        Bef is N - 1,
        addArgs(P,Bef,C,n,u, neg,NP).
addArgsH(- P/before,N,C,NP) :- !,
        Bef is N - 1,
        addArgs(P,Bef,C,n, u, pos,NP).
addArgsH(not P/before,N,C, NP) :- !,
        Bef is N - 1,
        addArgs(P,Bef,C,p,u, neg, NP).
addArgsH(P/before,N,C,NP) :- !,
        Bef is N - 1,
        addArgs(P,Bef,C,p,u, pos, NP).

addArgsH(not - P/T,_,C, NP) :- !,
        addArgs(P,T,C,n, u, neg, NP).
addArgsH(- P/T,_,C,NP) :- !,
        addArgs(P,T,C,n, u, pos,NP).
addArgsH(not P/T,_,C, NP) :- !,
        addArgs(P,T,C,p, u, neg, NP).
addArgsH(P/T,_,C,NP) :- !,
        addArgs(P,T,C,p,u, pos, NP).

addArgsH(not - P,N,C, NP) :-
        addArgs(P,N,C,n, u, neg, NP).
addArgsH(- P,N,C,NP) :-
        addArgs(P,N,C,n,u, pos,NP).
addArgsH(not P,N,C, NP) :-
        addArgs(P,N,C,p, u, neg, NP).
addArgsH(P,N,C,NP) :-
        addArgs(P,N,C,p,u, pos, NP).

addArgsB(P/now,_,_,NP) :- !,
        current(N), C is N - 1,
        addArgs(P,C,C,0,0,pos,NP).
addArgsB(P/before,_,_,NP) :- !,
        current(N), Bef is N - 2,
        addArgs(P,Bef,Bef,0,0,pos,NP).
addArgsB(P/T,_,_,NP) :- !,
        addArgs(P,T,T,0,0,pos,NP).
addArgsB(P,N,C,NP) :-
        addArgs(P,N,C,0,0,pos,NP).

addArgs(not -P,N,C,X, Y, Z, not -NP) :- !,
        addArgs(P, N, C, X, Y, Z,NP).
addArgs( -P,N,C,X, Y, Z, -NP) :- !,
        addArgs(P, N, C, X, Y, Z,NP).
addArgs(not P,N,C,X, Y, Z, not NP) :- !,
        addArgs(P, N, C, X, Y, Z,NP).
addArgs(P, N, C, X, Y, Z, NP) :-
        P =.. [Pred|Arguments],
        NP =.. [Pred,N, C, X,Y,Z|Arguments].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%   Getting the number of the next update program     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

getNumberOfUpdate(1) :-
        \+ current(_), assert(current(2)).
getNumberOfUpdate(C) :-
   retract(current(C)), C1 is C+1, assert(current(C1)).

/* ------------- demo predicate -------------- */
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%               demo( Goal/Time )                     %
% use Time = now if you want to use the most recent   %
% update program.                                     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

demo(not -G/now):-
        current(C), T is C-1,
        addArgs(G,T,T,n,0, neg, NG),
        demo(NG, [],[],t),!.
demo(not - G/now) :-
        current(C), T is C-1,
        addArgs(G,T,T,n,0,pos,NG), !,
        demo(not NG,[],[],t).
demo(- G/now) :-
        current(C), T is C-1,
        addArgs(G,T,T,n,0,pos,NG), !,
        demo(NG,[],[],t).
demo(not G/now):-
        current(C), T is C-1,
        addArgs(G,T,T,p,0,neg, NG),
        demo(NG, [],[],t),!.
demo(not G/now) :-
        current(C), T is C-1,
        addArgs(G,T,T,p,0,pos,NG), !,
        demo(not NG,[],[],t).
demo(G/now) :-
        current(C), T is C-1,
        addArgs(G,T,T,p,0,pos,NG),!,
        demo(NG,[],[],t).

% T stands for any time-stamp
demo(not -G/T):-
        addArgs(G,T,T,n,0, neg, NG),
        demo(NG, [],[],t),!.
demo(not - G/T) :-
        addArgs(G,T,T,n,0,pos,NG), !,
        demo(not NG,[],[],t).
demo(- G/T) :-
        addArgs(G,T,T,n,0,pos,NG), !,
        demo(NG,[],[],t).
demo(not G/T):-
        addArgs(G,T,T,p,0,neg, NG),
        demo(NG, [],[],t),!.
demo(not G/T) :-
        addArgs(G,T,T,p,0,pos,NG), !,
        demo(not NG,[],[],t).
demo(G/T) :-
        addArgs(G,T,T,p,0,pos,NG),
        demo(NG,[],[],t).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%        demo( Goal, Ancestors lists, Mode)           %
%                                                     %
% If Mode=true then tests if Goal is true             %
%     otherwise tests if Goal is true or undef.       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

demo( true, _, _, _ ) :- !.

demo( (G,Cont), AnsL, AnsG, M ) :-
        !, demo(G, AnsL, AnsG,M),
        demo(Cont, AnsL, AnsG,M).

demo( not G, _ , AnsG, t ) :-
           !, \+ demo(G,[],AnsG,tu).

demo( not G, _ , AnsG, tu ) :-
           !, \+ demo(G,AnsG,AnsG,t).

demo( G, Ans, _,  _ ) :-
       loop_detect( G, Ans ), !, fail.

demo( G, AnsL, AnsG, t ) :-
        (G <- Body),
        demo( Body, [G|AnsL], [G|AnsG], t ).

demo( G, AnsL, AnsG, tu ) :-
        compl_neg(G, NG),
        (G <- Body),
        demo( (Body,not NG), [G|AnsL], [G|AnsG], tu ).

%%%%%%  rules specific to the update semantics %%%%%%%%

demo( - G, AnsL, AnsG, M ) :-
        checkIndex(G,0,n_p_0), !,
        insertIndex(G,NG,n, n_p_0),
        demo(NG, AnsL, AnsG, M ).

demo( G, AnsL, AnsG, M ) :-
        checkIndex(G,0, n_p_0), !,
        insertIndex(G,NG,p,n_p_0),
        demo(NG, AnsL, AnsG, M ).

demo(G, AnsL, AnsG, M):-
        checkIndex(G, 0, u_0),
        \+ checkIndex(G, 0, n_p_0),
        checkIndex(G, T, t_undef),
        nonvar(T),
        insertIndex(G, NG, u, u_0),
        demo(NG, AnsL, AnsG, M).

demo(G, AnsL, AnsG, M):-
        checkIndex(G, u, u_0),
        checkIndex(G, neg, pos_neg_0),
        checkIndex(G, T, t_undef),
        nonvar(T),
        checkIndex(G, I, n_p_0),
        inverse(I, InvI),
        insertIndex(G,NG, InvI, n_p_0),
        insertIndex(NG, NNG, pos, pos_neg_0),
        demo(NNG, AnsL, AnsG, M).

%%%%%%%%%%%%%%%%% Defining rules %%%%%%%%%%%%%%%%%%%%%%%

demo(G, AnsL, AnsG, M):-
        checkIndex(G, pos, pos_neg_0),
        \+ checkIndex(G, 0, n_p_0),
        checkIndex(G, 0, u_0),
        decreaseTime(G, NG, T),
        T >=0,
        demo(NG, AnsL, AnsG, M),
        insertIndex(G, NG1, u, u_0),
        insertIndex(NG1, NG2, neg, pos_neg_0),
        demo(not NG2, AnsL, AnsG, M).

demo(G, AnsL, AnsG, M):-
        checkIndex(G, neg, pos_neg_0),
        \+ checkIndex(G, 0, n_p_0),
        checkIndex(G, 0, u_0),
        decreaseTime(G, NG, T),
        T >=0,
        demo(NG, AnsL, AnsG, M),
        insertIndex(G, NG1, u, u_0),
        insertIndex(NG1, NG2, pos, pos_neg_0),
        demo(not NG2, AnsL, AnsG, M).

% Loop Detection
loop_detect(X,[Y|_]) :- X == Y, !.
loop_detect(X,[_|T]) :- loop_detect(X,T).

% Explicit negation
compl_neg( - G, G ) :- !.
compl_neg( G, - G ).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                 Auxiliary predicates                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

decreaseTime(G,NG,T) :-
        G =.. [Name,TT|Args],
        T is TT - 1,
        NG =.. [Name,T|Args].

inverse(n,p).
inverse(p,n).

checkIndex(G,I,n_p_0) :-
        G =.. [_,_,_,I|_].
checkIndex(G,I,u_0) :-
        G =.. [_,_,_,_, I|_].
checkIndex(G,I,pos_neg_0) :-
        G =.. [_,_,_,_,_,I|_].
checkIndex(G, T, t_undef):-
        G =.. [_,T|_].

dropIndex(G,NG,n_p_0) :-
     G =.. [Name,A,B,_|Args],
     NG =.. [Name,A,B,0|Args].
dropIndex(G,NG,u_0) :-
     G =.. [Name,A,B,C,_|Args],
     NG =.. [Name,A,B,C,0|Args].
dropIndex(G,NG,pos_neg_0) :-
     G =.. [Name,A,B,C,D,_|Args],
     NG =.. [Name,A,B,C,D,0|Args].

insertIndex(G,NG,I,n_p_0) :-
     G =.. [Name,A,B,_|Args],
     NG =.. [Name,A,B,I|Args].
insertIndex(G,NG,I,u_0) :-
     G =.. [Name,A,B,C,_|Args],
     NG =.. [Name,A,B,C,I|Args].
insertIndex(G,NG,I, pos_neg_0) :-
     G =.. [Name,A,B,C,D,_|Args],
     NG =.. [Name,A,B,C,D,I|Args].

/* ------------- listing and saving states --------- */
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                listing of update programs           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

listUp :-
        current(T), C is T - 1,
        write('Current level is '), write(C), nl,
        listUpUntil(C).

listUpUntil(0) :- !.
listUpUntil(N) :-
        listUp(N),
        N1 is N - 1,
        listUpUntil(N1).

listUp(N) :-
        nl, write('%Program of level '), write(N), nl,
        findall(C,clauseLevel(C,N),L),
        processList(L).

processList([]).
processList([(H <- true)|L]) :- !,
        writeHead(H), write('.'), nl,
        processList(L).
processList([(H <- B)|L]) :-
        writeHead(H), write(' <- '),
        writeBody(B), write('.'), nl,
        processList(L).

writeBody((A,B)) :- !,
        writeElem(A), write(', '), writeBody(B).
writeBody(A) :- writeElem(A).

writeHead(- H) :- !,
        write('not '), writeHead(H).
writeHead(H):-
        checkIndex(H,n,n_p_0),!,
        write('- '),
        writeElem(H).
writeHead(H):-
        writeElem(H).

writeElem(not H) :- !,
        write('not '), writeElem(H).
writeElem(H):-
        H =.. [Name,_,C,_|Args],
        HH =.. [Name|Args],
        writeTime(HH,C).

writeTime(G,C) :- var(C), !, write(G).
writeTime(G,C) :- write(G/C).

%getting one clause of level N
clauseLevel((H <- B),N) :-
        (H <- B), H =.. [_,N,_|_].
clauseLevel((- H <- B),N) :-
        (- H <- B), H =.. [_,N,_|_].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%           saving the state into a file              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

saveUp(File) :-
        tell(File),
        saveLevels,
        told.

saveLevels :-
        current(T), C is T - 1,
        write('% This file was generated by saveUp.'),
        nl, nl, write('% There are '), write(C),
        write(' levels'), nl,
        listUpUntil(1,C).

listUpUntil(C,C) :- !,
        listUp(C).
listUpUntil(N,C) :-
        listUp(N), N1 is N + 1, nl,
        write('newProgram.'), nl,
        listUpUntil(N1,C).