%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% the GoFlux interpreter for executing Golog Programs in Flux
% written by: Stephan Schiffel (stephan.schiffel@inf.tu-dresden.de)
% available at http://www.fluxagent.org
%
% based on the IndiGolog interpreter from
% http://www.cs.toronto.edu/cogrobo/Legolog/index.html
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- ['special_flux2'].

:- set_flag(all_dynamic,on). % ECLiPSe can't deal with predicates not being
                              % listed contiguously
 
% assertz(X) :- assert(X).
% retractall(X) :- retract_all(X).


interpret(D, Z, Zr):-
	trans(D, Z, D1, Z1, H1) ->
		execute(H1, Z, Z1), interpret(D1, Z1, Zr)
	;
	final(D, Z) -> Zr=Z
	.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% operators
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- 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 and FINAL
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%% makros for if and while

makro( if(P, D1, D2) , (?(P) : D1) # (?(-P) : D2) ).
makro( while(P, D) , star(?(P) : D) : ?(-P) ).

%%%%% makros for compatibility with other golog versions (other syntax)
% makro for sequences as lists
makro([], nil).
makro([D|L], D:Ds) :- makro(L, Ds).
% makro for nondeterministic choice
makro(ndet(D1, D2), (D1 # D2)).
% makros for prefix operators
makro(and(X,Y), (X & Y)).
makro(or(X,Y), (X v Y)).
makro(neg(X), -X).

%%%% final(D, Z)

final(nil, _).

final(D1 : D2, Z) :-
    final(D1, Z) , final(D2, Z).

final(D1 # D2, Z) :-
    final(D1, Z) ; final(D2, Z).


final(star(_), _).

final(D, Z) :-
	makro(D, D1), !,
	final(D1, Z).

final(pi(V, D), Z) :-
    sub(V, _, D, D2), !,
    final(D2, Z).

final(D, Z) :-
    proc(D, D2), !,
    final(D2, Z).

%%%% trans(D, Z, Dr, Zr, Hr)

trans(D1 : D2, Z, Dr, Zr, Hr) :-
    final(D1, Z), trans(D2, Z, Dr, Zr, Hr)
		;
		trans(D1, Z, D1r, Zr, Hr), Dr = (D1r : D2)
		.

trans(?(P), Z, nil, Z, []) :-
    holdscond(P, Z).

trans(D1 # D2, Z, Dr, Zr, Hr) :-
    trans(D1, Z, Dr, Zr, Hr) ; trans(D2, Z, Dr, Zr, Hr).


trans(star(D), Z, Dr : star(D), Zr, Hr) :-
    trans(D, Z, Dr, Zr, Hr).

trans(D, Z, Dr, Zr, Hr) :-
	makro(D, D1), !,
	trans(D1, Z, Dr, Zr, Hr).

trans(pi(V, D), Z, Dr, Zr, Hr) :-
    sub(V, _, D, D2), !,
    trans(D2, Z, Dr, Zr, Hr).

trans(D, Z, Dr, Zr, Hr) :-
    proc(D, D2), !,
    trans(D2, Z, Dr, Zr, Hr).

trans(D, Z, nil, Zr, [D]) :-
    prim_action(D),
    poss(D, P),
    holdscond(P, Z),
	state_update(Z,D,Zr).

% SEARCH

final(search(D), Z) :-
	final(D, Z).
 
trans(search(D), Z, followpath(P), Zr, Hr) :-
    trans(D, Z, Dr, Zr, Hr),
    findpath(Dr, Zr, P).

findpath(D, Z, [final(D, Z)]) :-
	final(D, Z).
		 
findpath(D, Z, [trans(D, Z, Dr, Zr, Hr)|P]) :-
	trans(D, Z, Dr, Zr, Hr),
	findpath(Dr, Zr, P).

final(followpath([final(D, Z)]), Z).

trans(followpath([trans(D, Z, Dr, Zr, Hr)|P]), Z, followpath(P), Zr, Hr).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% holdscond
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

holdscond(P & Q, Z) :- !, holdscond(P, Z), holdscond(Q, Z).
holdscond(P v Q, Z) :- !, (holdscond(P, Z) ; holdscond(Q, Z)).
holdscond(P => Q, Z) :- !, holdscond(-P v Q, Z).
holdscond(P <=> Q, Z) :- !, holdscond((P => Q) & (Q => P), Z).
holdscond(-(-P), Z) :- !, holdscond(P, Z).
holdscond(-(P & Q), Z) :- !, holdscond(-P v -Q, Z).
holdscond(-(P v Q), Z) :- !, holdscond(-P & -Q, Z).
holdscond(-(P => Q), Z) :- !, holdscond(-(-P v Q), Z).
holdscond(-(P <=> Q), Z) :- !, holdscond(-((P => Q) & (Q => P)), Z).
holdscond(-all(V, P), Z) :- !, holdscond(some(V, -P), Z).
holdscond(-some(V, P), Z) :- !, \+ holdscond(some(V, P), Z).
holdscond(all(V, P), Z) :- !, holdscond(-some(V, -P), Z).
holdscond(some(V, P), Z) :- !, sub(V, _, P, P1), holdscond(P1, Z).

% complex conditions (condition procedures)
holdscond(P, Z) :- proc(P, P1), !, holdscond(P1, Z).
holdscond(-P, Z) :- proc(P, P1), !, holdscond(-P1, Z).
% makros for different syntax in other golog versions
holdscond(P, Z) :- makro(P, P1), !, holdscond(P1, Z).
holdscond(-P, Z) :- makro(P, P1), !, holdscond(-P1, Z).

holdscond(-P, Z) :- !, \+ holdscond(P, Z).
holdscond(P, Z) :- decode(P, P1, Z), call(P1).


/* sub(Name,New,Term1,Term2): Term2 is Term1 with Name replaced by New. */
sub(_, _, T1, T2) :- var(T1), !, T2 = T1.
sub(X1, X2, T1, T2) :- T1 = X1, !, T2 = X2.
sub(X1, X2, T1, T2) :- 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).

% decode(P1, P2, Z): P2 is P1 with all fluents replaced by their values in Z
decode(P1, P2, _) :- var(P1), !, P2 = P1.

decode(P1, P2, Z) :- P1 =..[F|L1], decode_list(L1, L2, Z), P3 =..[F|L2],
    (
			prim_fluent(P3), has_val(P3, P2, Z)
			;
			\+ prim_fluent(P3), P2=P3
		)
		.

decode_list([], [], _).
decode_list([T1|L1], [T2|L2], Z) :- decode(T1, T2, Z), decode_list(L1, L2, Z).

% true if F has value V in state Z
has_val(F,V,Z) :- func_fluent_to_rel(F,V,Frel), holds(Frel,Z).

% transform f(a,b)=c to f(a,b,c)
func_fluent_to_rel(Ffunc,Value,Frel) :- Ffunc =.. [Fn|L], append(L,[Value],L2), Frel =.. [Fn|L2].