/*
   The "true" predicate takes a positive literal (represented as
a structure) and a state and determines whether the literal
is true in the state.  The literal is assumed to be a ground
literal.  The state may be represented as an atom 
or as a structure whose functor is "result".
   In the first case, the atom is interpreted as the name of 
the state, and the state description of that state is simply
searched for the literal.
   In the second case, the arguments of the functor are assumed
to be an atom and a list of permitted actions for the state
represented by that atom.  The actions are represented as ground
literals (i.e., as structures with no variables).  In this case,
the state for which we are checking the literal's truth is the
state resulting from applying the actions, in order, to the 
state represented by the atom.
   In this second case, the literal will be true iff
     (1) the list is empty, and the literal is true in the 
state represented by the atom
     (2) the literal becomes true as a result of the final
action
     (3) the literal does not become false as a result
of the final action, and it was true before that action.


% This is the case where the state has a description.
% We assume that it is represented as an atom, although
%   other representations are possible, depending on 
%   what's allowed for the first argument of the
%   "state_description" predicate.

true(Literal, State) :-
  state_description(State, Description), 
  member(Literal, Description).

% This is subcase (1) above.
true(Literal, result(State, [])) :-
  true(Literal, State).

% This covers cases 2 and 3.  The last action is 
%   extracted, the addlists and delete lists for
%   that action are found (with variables in these
%   lists bound to the arguments of the last action).
% An auxiliary predicate "true_helper" checks these
%   lists and then proceeds appropriately for cases
%   (2) and (3).  This predicate needs the literal
%   to be checked, the addlist and deletelist, the
%   state to which the list of actions is applied,
%   and the list of all the actions except for the
%   last one.

true(Literal, result(State, ActionList)) :-
  last_and_butlast(ActionList, Last, ButLast),
  Last =.. [Functor | Args],
  action(Functor, Args, _, AddList, DeleteList),  
  true_helper(Literal, AddList, DeleteList, State, ButLast).

% Case (2) above

true_helper(Literal, AddList, _, _, _) :-
  member(Literal, AddList).

% Case (3) above

true_helper(Literal, _, DeleteList, State, ButLast) :-
  not(member(Literal, DeleteList)),
  true(Literal, result(State, ButLast)).



% This predicate is true if when the second argument
%   is added to the end of the third argument (which
%   must be a list), the first argument results.
  
last_and_butlast([Head], Head, []).

last_and_butlast([Head | Tail], Last, [Head | List]):-
  last_and_butlast(Tail, Last, List). 


% Descriptions of individual states

state_description(
  state0,
  [on(c,a), clear(b), clear(c), ontable(a), ontable(b),
   red(a), yellow(b), green(c)]).

state_description(
  state1,
  [clear(a), on(a,c), on(c,e), ontable(e), 
   clear(f), on(f,d), on(d,b), ontable(b),
   red(a), yellow(b), green(c)]).


% Actions are represented by a structure whose 
%   components are the action name, the list of
%   parameters, the precondition list, the addlist,
%   and the delete list.

% an action that moves a block X from some other block Y
%   to the table

action(
  move_to_table,
  [X,Y],
  [on(X,Y), clear(X)],
  [ontable(X), clear(Y)], 
  [on(X,Y)]).

% an action that moves a block X from the table 
%   to the top of a block Y

action(
  move_from_table,
  [X,Y],
  [ontable(X), clear(X), clear(Y)],
  [on(X,Y)],
  [ontable(X), clear(Y)]).

% an action that moves a block x from the top of block y
%   to the top of block z

action(
  move,
  [X,Y,Z],
  [on(X,Y), clear(X), clear(Z)],
  [on(X,Z), clear(Y)], 
  [on(X,Y), clear(Z)]).


%%%%%%%%%%%% The test "program" %%%%%%%%%%%%%%%

test_case(true(on(c,a), result(state0, []))).
test_case(true(ontable(a), result(state0, []))).
test_case(true(clear(b), result(state0, []))).
test_case(true(red(a), result(state0, []))).
test_case(true(on(c,b), result(state0, []))).
test_case(true(on(a,c), result(state0, []))).
test_case(true(ontable(c), result(state0, []))).
test_case(true(clear(a), result(state0, []))).
test_case(true(green(b), result(state0, []))).

test_case(true(on(c,a), result(state0, [move(c,a,b)]))).
test_case(true(ontable(a), result(state0, [move(c,a,b)]))).
test_case(true(clear(b), result(state0, [move(c,a,b)]))).
test_case(true(red(a), result(state0, [move(c,a,b)]))).
test_case(true(on(c,b), result(state0, [move(c,a,b)]))).
test_case(true(on(a,c), result(state0, [move(c,a,b)]))).
test_case(true(ontable(c), result(state0, [move(c,a,b)]))).
test_case(true(clear(a), result(state0, [move(c,a,b)]))).
test_case(true(green(b), result(state0, [move(c,a,b)]))).

test_case(true(on(c,a), result(state0, [move(c,a,b), move_from_table(a,c)]))).
test_case(true(ontable(a), result(state0, [move(c,a,b), move_from_table(a,c)]))).
test_case(true(clear(b), result(state0, [move(c,a,b), move_from_table(a,c)]))).
test_case(true(red(a), result(state0, [move(c,a,b), move_from_table(a,c)]))).
test_case(true(on(c,b), result(state0, [move(c,a,b), move_from_table(a,c)]))).
test_case(true(on(a,c), result(state0, [move(c,a,b), move_from_table(a,c)]))).
test_case(true(ontable(c), result(state0, [move(c,a,b), move_from_table(a,c)]))).
test_case(true(clear(a), result(state0, [move(c,a,b), move_from_table(a,c)]))).
test_case(true(green(b), result(state0, [move(c,a,b), move_from_table(a,c)]))).


test:-
  test1, nl,
  test2.

test1:-
  test_case(X), X, print(X), nl, fail.

test1.

test2:-
  member(X, [on(a,b), on(b,c), on(c,e), on(e,f),
             clear(a), clear(b), clear(c), clear(d),
             ontable(a), ontable(c), ontable(e), ontable(f),
             yellow(a), yellow(b), yellow(c), yellow(d)]),
  true(X, result(state1, [move_to_table(a,c), move_to_table(f,d), 
                          move_to_table(c,e), move_from_table(e,f), 
                          move(d,b,e), move_from_table(c,d),
                          move_from_table(b,c), move_from_table(a,b)])),
  print(X),nl,fail.

test2.