/*
				APPENDIX A
			Section A.1:  An Interpreter
*/
/************************************************************************/
/*        Golog Interpreter With A Simple Execution Monitor.            */
/*        This version does not keep trace of program states.           */
/*     Based on Trans-interpreter by DeGiacomo, Lespérance, Levesque.   */
/************************************************************************/
:- set_flag(print_depth,100).
:- pragma(debug).
:- set_flag(all_dynamic, on).

:- op(800, xfy, [&]).   /* Conjunction */ 
:- op(850, xfy, [v]).   /* Disjunction */ 
:- op(870, xfy, [=>]).  /* Implication */
:- op(880,xfy, [<=>]).  /* Equivalence */
:- op(950, xfy, [:]).   /* Action sequence.*/
:- op(960, xfy, [#]).   /* Nondeterministic action choice.*/
 
/* trans(Prog,Sit,Prog_r,Sit_r) */

trans(A,S,nil,do(A,S)) :- primitive_action(A), poss(A,S).

trans(?(C),S,nil,S) :- holds(C,S).

trans(P1 : P2,S,P2r,Sr) :- final(P1,S),trans(P2,S,P2r,Sr).
trans(P1 : P2,S, P1r : P2,Sr) :- trans(P1,S,P1r,Sr).

trans(P1 # P2,S,Pr,Sr) :- trans(P1,S,Pr,Sr) ; trans(P2,S,Pr,Sr).

trans(pi(V,P),S,Pr,Sr) :- sub(V,_,P,PP), trans(PP,S,Pr,Sr).

trans(star(P),S,PP : star(P),Sr) :- trans(P,S,PP,Sr).

trans(if(C,P1,P2),S,Pr,Sr) :- 
     trans(((?(C) : P1) # (?(-C) : P2)),S,Pr,Sr).

trans(while(C,P),S,Pr,Sr) :- 
     trans(star(?(C) : P) : ?(-C), S,Pr,Sr).

trans(P,S,Pr,Sr) :- proc(P,Pbody), trans(Pbody,S,Pr,Sr).


/* final(Prog,Sit) */

final(nil,S).

final(P1 : P2,S) :- final(P1,S),final(P2,S).

final(P1 # P2,S) :- final(P1,S) ; final(P2,S).

final(pi(V,P),S) :- final(P,S).

final(star(P),S).

final(if(C,P1,P2),S) :- 
      final(( (?(C) : P1) # (?(-C) : P2) ),  S).

final(while(C,P),S) :- 
      final( star(?(C) : P) : ?(-C) ,S).

final(pcall(P_Args),S) :- proc(P_Args,P),final(P,S).

/* transCL(Prog,S,Prog_r,S_r) is the transitive closure 
                                of trans(Prog,S,Prog_r,S_r) */
transCL(P,S,P,S).
transCL(P,S,Pr,Sr) :- trans(P,S,PP,SS), transCL(PP,SS,Pr,Sr).

/* offline(Prog,S,Sr): Sr is the situation resulting after doing Prog */
offline(Prog,S0,Sf) :- final(Prog,S0), S0=Sf;
               trans(Prog,S0,Prog1,S1), 
               offline(Prog1,S1,Sf). 

doEM(Prog,S0,Sf) :-  final(Prog,S0), S0=Sf;
                   trans(Prog,S0,Prog1,S1), 
                  offline(Prog1,S1,Sg), /*  Prog1 leads to the goal */
                    !,
                   monitor(Prog1,S1,Prog2,S2), !, 
                   doEM(Prog2,S2,Sf).

/* sub(Name,New,Term1,Term2): Term2 is Term1 with Name replaced by New. */

sub(X1,X2,T1,T2) :- var(T1), T2 = T1.
sub(X1,X2,T1,T2) :- not var(T1), T1 = X1, T2 = X2.
sub(X1,X2,T1,T2) :- not T1 = X1, T1 =..[F|L1], sub_list(X1,X2,L1,L2),
                    T2 =..[F|L2].
sub_list(X1,X2,[],[]).
sub_list(X1,X2,[T1|L1],[T2|L2]) :- sub(X1,X2,T1,T2), sub_list(X1,X2,L1,L2).


/* The holds predicate implements the revised Lloyd-Topor
   transformations on test conditions.  */

holds(P & Q,S) :- holds(P,S), holds(Q,S).
holds(P v Q,S) :- holds(P,S); holds(Q,S).
holds(P => Q,S) :- holds(-P v Q,S).
holds(P <=> Q,S) :- holds((P => Q) & (Q => P),S).
holds(-(-P),S) :- holds(P,S).
holds(-(P & Q),S) :- holds(-P v -Q,S).
holds(-(P v Q),S) :- holds(-P & -Q,S).
holds(-(P => Q),S) :- holds(-(-P v Q),S).
holds(-(P <=> Q),S) :- holds(-((P => Q) & (Q => P)),S).
holds(-all(V,P),S) :- holds(some(V,-P),S).
holds(-some(V,P),S) :- not holds(some(V,P),S).  /* Negation */
holds(-P,S) :- isAtom(P), not holds(P,S).     /* by failure */
holds(all(V,P),S) :- holds(-some(V,-P),S).
holds(some(V,P),S) :- sub(V,_,P,P1), holds(P1,S).

/* The following clause treats the holds predicate for non fluents, including
   Prolog system predicates. For this to work properly, the GOLOG programmer
   must provide, for all fluents, a clause giving the result of restoring
   situation arguments to situation-suppressed terms, for example:
         restoreSitArg(ontable(X),S,ontable(X,S)).             */

holds(A,S) :- restoreSitArg(A,S,F), F ;
              not restoreSitArg(A,S,F), isAtom(A), A.

isAtom(A) :- not (A = -W ; A = (W1 & W2) ; A = (W1 => W2) ;
    A = (W1 <=> W2) ; A = (W1 v W2) ; A = some(X,W) ; A = all(X,W)).

restoreSitArg(poss(A),S,poss(A,S)).