/*DiaLaw 2.0, 1998, Prolog 2 for Windows*/
clean :-
        retract(teller(_)),
        fail.
clean.

dialaw :-
        clean,
        create_windows,
        first_move(CS, FirstSentence, DialogMoves),
        dialog(CS, FirstSentence, DialogMoves),
        new(@stop, dialog('Stop')),
        send(@stop, append, button(stop, message(@stop, return, doit))),
        send(@stop, default_button, stop),
        send(@stop, open),
        get(@stop, confirm, _),
        send(@mainf, destroy),
        send(@stop, destroy).

first_move([(bert, Sentence)], Sentence, [(bert, (claim, Sentence), (0, dialaw))]) :-
        assert(teller(1)), teller(U),
        send(@sv, print, U),
        send(@sv, print, '. On level 0, move 1 of the dialog game'),
        send(@sv, newline), 
        new(D, dialog('Berts statement:')),
        send(D, width, 500),
        send(D, append, new(TI, text_item(statement, ''))),
        send(TI, geometry,@default,@default,450,@default ),
        send(D, append,
             button(ok, message(D, return,
                                TI?selection))),
        send(D, append,
             button(cancel, message(D, return, @nil))),
        send(D, default_button, ok), % Ok: default button
        get(D, confirm, Answer),     % This blocks!
        send(D, destroy),
        Answer \== @nil,             % canceled
        Sentence = Answer,
        send(@dv, print, '1.  bert: '),
        send(@csb, print, U),
        send(@csb, print, '. '),
        send(@csb, print, Sentence),
        send(@cse, print, U),
        send(@cse, print, '. '),
        send(@cse, print, []).

dialog(_, S, [(_, (accept, S), _)|_]).
dialog(_, S, [(_, (withdraw, S), _)|_]).
dialog(_, S, [(_, (accept, not(S)), _)|_]).
dialog(CS, S, [(_, (withdraw, not(S)), _)|_]):-
                not_inCS((_, S), CS).
dialog(_, _, [(_, (quit, _), _)|_]).

dialog(CS, FS, DM) :-
        move_input(CS, DM, NewPlayer, NewLevels, Move),
        trace,
        valid_move(NewLevels, NewPlayer, CS, DM, ValidMove, Move),
        notrace,
        send(@cse,clear),
        send(@csb,clear),
        update_CS(DM, CS, NewCS, ValidMove, NewPlayer),
        dialog(NewCS, FS, [(NewPlayer, ValidMove, NewLevels)|DM]).

move_input( CS
          , [(P, (accept, il_claim(S)), (L, _))|_]
          , P
          , (L, il_claim(S))
          , (withdraw, S)
          ):-
        otherplayer(P, Op),
        only_inCS_other(CS, Op, S),
        teller,
        write_status([(P, (accept, S), (L, _))|_], P, (L, S)).

move_input( CS
          , [(P, (accept, A), (L, _))|_]
          , P
          , (L, A)
          , ( accept, reason( applicable(rule(A, B))
                            , applies(rule(A, B))
                            )
            )
          ) :-
     inCS((P, valid(rule(A, B))), CS),
     only_inCS_other( CS, P
                    , reason( applicable(rule(A, B))
                            , applies(rule(A, B)))
                    ),
     teller,
     write_status([(P, (accept, A), (L, _))|_], P, (L, A)).

move_input( CS
          , [(P, (accept, valid(rule(A, B))), (L, _))|_]
          , P
          , (L, valid(rule(A, B)))
          , (accept, reason(applicable(rule(A, B)), applies(rule(A, B))))
          ):-
        inCS((P, A), CS),
        only_inCS_other(CS, P, reason(applicable(rule(A, B)), applies(rule(A, B)))),
        teller,
        write_status( [(P, (accept, valid(rule(A, B))), (L, _))|_]
                    , P, (L, valid(rule(A, B))
                    )
          ).
move_input( CS
          , [( P
             , (claim, reason(applicable(rule(A, B)), applies(rule(A,B))))
             , (L, _)
             )|_
            ]
          , Op
          , ( L
            , reason(applicable(rule(A, B)), applies(rule(A, B)))
            )
          , (accept, reason(applicable(rule(A, B)), applies(rule(A, B))))
          ):-
        otherplayer(P, Op),
        inCS((Op, A), CS),
        inCS((Op, valid(rule(A, B))), CS),
        teller,
        write_status( [(P, (claim, reason(applicable(rule(A, B))
                      , applies(rule(A, B)))), (L, _))|_
                      ]
                    , Op
                    , (L, reason( applicable(rule(A, B))
                                , applies(rule(A, B))
                                )
                      )
                    ).

move_input( CS
          , [(P, (accept, applies(rule(A, B))), (L, _))|_]
          , P
          , (L, applies(rule(A, B)))
          , (accept, reason(A, B))
          ):-
        only_inCS_other(CS, P, reason(A, B)),
        teller,
        write_status([(P, (accept, applies(rule(A, B))), (L, _))|_],
                P, (L, applies(rule(A, B)))).

move_input( CS
          , [(P, (accept, excluded(rule(A, B))), (L, _))|_]
          , P
          , (L, excluded(rule(A, B)))
          , (withdraw, applies(rule(A, B)))
          ):-
        otherplayer(P, Op),
        only_inCS_other(CS, Op, applies(rule(A, B))),
        teller,
        write_status([(P, (accept, applies(rule(A, B))), (L, _))|_], P, (L, applies(rule(A, B)))).

move_input( CS
          , [(P, (accept, outweighs(Pro, Con, S)), (L, _))|_]
          , P
          , (L, outweighs(Pro, Con, S))
          , (withdraw, not(S))
          ):-
        inCS((P, not(S)), CS),
        teller,
        write_status( [(P, (accept, outweighs(Pro, Con, S)), (L,_))|_]
                    , P
                    , (L, outweighs(Pro, Con, S))
                    ).

move_input( CS
          , [(P, (withdraw, not(S)), (L, _))|_]
          , P
          , (L, not(S))
          , (accept, S)
          ):-
        inCS((P, outweighs(Pro, Con, S)), CS),
        teller,
        write_status( [(P, (withdraw, not(S)), (L, _))|_]
                    , P
                    , (L, outweighs(Pro, Con, S))
                    )
.
move_input( _
          , [(P, (accept, outweighs(Pro, Con, S)), (L, _))|_]
          , P
          , (L, outweighs(Pro, Con, S))
          , (accept, S)
          ):-
        teller,
        write_status( [(P, (accept, outweighs(Pro, Con, S)), (L,_))|_]
                    , P
                    , (L, outweighs(Pro, Con, S))
                    )
.
move_input(CS
          , [(P, (accept, reason(R, not(S))), (L, _))|_]
          , P
          , (L, reason(R, not(S)))
          , (withdraw, outweighs(Pro, Con, S))
          ):-
        otherplayer(P, Op),
        only_inCS_other(CS, Op, outweighs(Pro, Con, S)),
        teller,
        write_status([(P, (accept, reason(R, not(S))), (L, _))|_], P,
                (L, reason(R, not(S)))).

move_input(CS, DM, NewPlayer, NewLevels, Move):-
        teller,
        next_move(DM, CS, NewPlayer, NewLevels),
        write_status(DM, NewPlayer, NewLevels),
        read_move(NewPlayer, Move).

next_move( [(P, (claim, B), (L, _))|_]
         , _
         , NewPlayer
         , (L, B)
         ) :-
        otherplayer(P, NewPlayer).

next_move( [(P, (question, _), (L, B))|_]
         , _
         , NewPlayer
         , (LL, B)
         ) :-
        otherplayer(P, NewPlayer),
        LL is L +1.

next_move( [(P, (withdraw, B), _)|Rest]
         , CS
         , P
         , (L, not(B))
         ) :-
        only_inCS_other(CS, P, not(B)),
        find_move(Rest, not(B), (L, _)).

`next_move( [(P, (accept, not(S)), _)|Rest]
         , _
         , P
         , (L, B)
         ) :-
        find_move(Rest, S, (L, B)).

next_move( [(P, (withdraw, not(S)), _)|Rest]
         , _
         , NewPlayer
         , (L, B)
         ) :-
        find_move(Rest, S, (L, B)),
        otherplayer(P, NewPlayer).

next_move( [(P, (withdraw, il_claim(S)), _)|Rest]
         , CS
         , P
         , (L, S)
         ) :-
        not_inCS((_, not(il_claim(S))), CS),
        find_move(Rest, S, (L, _)).

next_move( [(P, (withdraw, not(il_claim(S))), _)|Rest]
         , CS
         , Op
         , (L, S)
         ) :-
        not_inCS((_, il_claim(S)), CS),
        otherplayer(P, Op),
        find_move(Rest, S, (L, _)).

next_move( [(P, (accept, not(il_claim(S))), _)|Rest]
         , _
         , P
         , (L, S)
         ) :-
        find_move(Rest, S, (L, _)).

next_move( [(P, (withdraw, outweighs(_, _, S)), _)|Rest]
         , CS
         , P
         , (L, reason(R, not(S)))
         ) :-
        only_inCS_other(P, reason(R, not(S)), CS),
        find_move(Rest, reason(R, not(S)), (L, _)).

next_move( [(P, (accept, reason(R, not(S))), _)|Rest]
         , CS
         , P
         , (L, B)
         ) :-
        find_move(Rest, reason(R, not(S)), (L, outweighs(_, _, S))),
        inCS((_, outweighs(_, _, S)), CS),
        find_move(Rest, outweighs(_, _, S), (_, B)).

next_move( [(P, (withdraw, reason(R, not(S))), _)|Rest]
         , CS
         , NewPlayer
         , (L, B)
         ) :-
        find_move(Rest, reason(R, not(S)), (L, outweighs(_, _, S))),
        inCS((_, outweighs(_, _, S)), CS),
        find_move(Rest, outweighs(_, _, S), (_, B)),
        otherplayer(P, NewPlayer).

next_move( [(P, (accept, S), _)|Rest]
         , _
         , NewPlayer
         , (L, B)
         ) :-
        find_move(Rest, S, (L, B)),
        otherplayer(P, NewPlayer).

next_move( [(P, (withdraw, B), _)|Rest]
         , _
         , P
         , NewLevels
         ) :-
        find_move(Rest, B, NewLevels).

next_move([(P, (withdraw, reason(_, not(S))), _)|Rest], CS, P, (L, B)) :-
        inCS((_, outweighs(_, _, S)), CS),
        find_move(Rest, outweighs(_, _, S), (L, B)).

find_move([( _, (claim, S), (L, B))|_], S, (L, B)).

find_move([_|Rest], S, NL) :-
        find_move(Rest, S, NL).

write_status([(_, (A, S), _)|_], P, (L, N)) :-
                teller(U),
                send(@sv, print,U),
                send(@sv, print, '. The level is: '),
                send(@sv, print, L),
                send(@sv, print, '; the move is about '),
                send(@sv, print, N),
                send(@sv, newline),
                send(@dv, clear),
                send(@dv, print, A),
                send(@dv, print, ', '),
                send(@dv, print, S),
                send(@dv, newline),
                send(@dv, print, U),
                send(@dv, print, '. '),
                send(@dv, print, P),
                write_levelmark(L).

read_move(P, (A, S)) :-
    new(@act, frame(P)),
    send(@act, append, new(D, dialog(P))),
    send(D, width, 500),
    send(D, append, new(TI, text_item(sentence, ''))),
    send(TI, geometry,@default,@default,450,@default ),
    send(D, append, button(accept, message(D, return, accept))),
    send(D, append, button(withdraw, message(D, return, withdraw))),
    send(D, append, button(question, message(D, return, question))),
    send(D, append, button(claim, message(D, return, claim))),
    get(D, confirm, A),     % This blocks!
    set_act_type(A),
    get(TI, selection, S),
    act_type(A),
    send(@act, destroy).

set_act_type(Value) :-
    retractall(act_type(_)),
    assert(act_type(Value)).

write_dialog([]).
write_dialog([K|T]):-
     send(@dv, print, K),
     write_dialog(T).

read_again(P, (A, S)) :-
  new(@wrong, dialog('Wrong move')),
  send(@wrong, append, new(@wm, view)),
  send(@wm, newline),
  send(@wrong, append, button(ok, message(@wrong, destroy))),
  send(@wrong, open),
  read_move(P, (A, S)),
  send(@wm, destroy),
  send(@wrong, destroy).

valid_move(_, _, _, _, (quit, _), (quit, _)).
valid_move(_, NP, CS, _, (accept, S), (accept, S)) :-
        only_inCS_other(CS, NP, S),
        not_inCS((_, not(S)), CS).

/* valid moves in case of withdraw*/
valid_move(_, NP, CS, _, (withdraw, S), (withdraw, S)) :-
        otherplayer(NP, P),
        only_inCS_other(CS, P, S).

valid_move(_, P, CS, [(P, (withdraw, S), _)|_],
                (question, not(S)), (question, not(S))) :-
        otherplayer(P, Op),
        inCS((Op, not(S)), CS).

valid_move(NL, NP, CS, DM, ValidMove, (question, outweighs([_], [], _))):-
        read_again(NP, Move),
        valid_move(NL, NP, CS, DM, ValidMove, Move).

valid_move(NL, NP, CS, [(P, (question, S), L)|Rest], ValidMove, (question, S)):-
        read_again(NP, Move),
        valid_move(NL, NP, CS, [(P, (question, S), L)|Rest], ValidMove, Move).

valid_move(NL, NP, CS, _, ValidMove,
                (question, reason(applicable(rule(A, B)), applies(rule(A, B))))):-
        inCS((NP, A), CS),
        inCS((NP, valid(rule(A, B))), CS),
        read_again(NP, Move),
        valid_move(NL, NP, CS, [(_, (question, _), _)|_], ValidMove, Move).

valid_move(_, _, _, [(_, (claim, S), _)|_], (question, S), (question, S)).

valid_move(_, _, CS, [(_, (withdraw, il_claim(S)), _)|_],
                (question, S), (question, S)):-
        not_inCS((_, not(il_claim(S))), CS).

valid_move(_, _, CS, [(_, (withdraw, not(il_claim(S))), _)|_],
                (question, S), (question, S)):-
        not_inCS((_, il_claim(S)), CS).

valid_move(_, _, _, [(_, (accept, not(il_claim(S))), _)|_],
                (question, S), (question, S)).

valid_move(_, NP, CS, [(_, (withdraw, reason(_, not(S))), _)|_],
                (question, outweighs(_, _, S)), (question, outweighs(_, _, S))):-
        otherplayer(NP, P),
        only_inCS_other(CS, P, outweighs(_, _, S)).

valid_move(NL, NP, CS, DM, ValidMove, (claim, S)) :-
        previous_withdraw(NP, S, DM),
        read_again(NP, Move),
        valid_move(NL, NP, CS, DM, ValidMove, Move).

valid_move(NL, NP, CS, [(P, (withdraw, S), Levels)|Rest],
                ValidMove, (claim, _)) :-
        otherplayer(P, Op),
        inCS((Op, not(S)), CS),
        read_again(NP, Move),
        valid_move(NL, NP, CS, [(P, (withdraw, S), Levels)|Rest], ValidMove, Move).

valid_move(NL, NP, CS, [(P, (withdraw, il_claim(S)), Levels)|Rest],
                ValidMove, (claim, _)) :-
        read_again(NP, Move),
        valid_move(NL, NP, CS, [(P, (withdraw, il_claim(S)), Levels)|Rest],
                ValidMove, Move).

valid_move(NL, NP, CS, [(P, (withdraw, not(il_claim(S))), Levels)|Rest],
                ValidMove, (claim, _)) :-
        read_again(NP, Move),
        valid_move(NL, NP, CS, [(P, (withdraw, il_claim(S)), Levels)|Rest],
                ValidMove, Move).

valid_move(NL, NP, CS, [(P, (accept, not(il_claim(S))), Levels)|Rest],
                ValidMove, (claim, _)) :-
        read_again(NP, Move),
        valid_move(NL, NP, CS, [(P, (withdraw, il_claim(S)), Levels)|Rest],
                ValidMove, Move).

valid_move(_, NP, CS, _, (claim, applies(rule(A, B))),
                (claim, applies(rule(A, B)))) :-
        not_inCS((_, applies(rule(A, B))), CS),
        not_inCS((NP, excluded(rule(A, B))), CS).

valid_move(NL, NP, CS, DM, ValidMove, (claim, applies(rule(_, _)))) :-
        read_again(NP, Move),
        valid_move(NL, NP, CS, DM, ValidMove, Move).

valid_move((_, applies(rule(A, B))), NP, CS, _,
                (claim, reason(applicable(rule(A, B)), applies(rule(A, B)))),
                (claim, reason(applicable(rule(A, B)), applies(rule(A, B))))) :-
        not_inCS((_, reason(applicable(rule(A, B)), applies(rule(A, B)))), CS),
        not_inCS((NP, not(A)), CS),
        not_inCS((NP, not(valid(rule(A, B)))), CS).

valid_move(NL, NP, CS, DM, ValidMove,
                (claim, reason(applicable(rule(A, B)), applies(rule(A, B))))) :-
        read_again(NP, Move),
        valid_move(NL, NP, CS, DM, ValidMove, Move).

valid_move(_, _, _, [(_, (claim, B), _)|_], (claim, il_claim(B)),
                (claim, il_claim(B))) :-
        B \= il_claim(_).

valid_move(NL, NP, CS, DM, ValidMove, (claim, il_claim(_))) :-
        read_again(NP, Move),
        valid_move(NL, NP, CS, DM, ValidMove, Move).

valid_move((_, B), _, CS, _, (claim, reason(A, B)),
                (claim, reason(A, B))):-
        not_inCS((_, reason(A, B)), CS).

valid_move((_, B), _, CS, _, (claim, reason(A, not(B))),
                (claim, reason(A, not(B)))) :-
        not_inCS((_, reason(A, not(B))), CS).

valid_move(_, _, CS, [(_, (claim, outweighs(_, _, B)), _)|_],
                (claim, reason(A, not(B))), (claim, reason(A, not(B)))) :-
        not_inCS((_, reason(A, not(B))), CS).

valid_move(NL, NP, CS, DM, ValidMove, (claim, reason(_, _))) :-
        read_again(NP, Move),
        valid_move(NL, NP, CS, DM, ValidMove, Move).

valid_move((_, B), _, CS, _, (claim, outweighs(Proset, Conset, B)),
                (claim, outweighs(Proset, Conset, B))) :-
        not_inCS((_, outweighs(Proset, Conset, B)), CS),
        check_reasonsets(CS, Proset, Conset, B).

valid_move(_, _, _, [(_, (claim, S), _)|_], (claim, not(S)), (claim, not(S))):-
        S \= not(_).

valid_move(_, _, CS, [(_, (question, _), _)|_], (claim, S), (claim, S)):-
        not_inCS((_, S), CS),
        not_inCS((_, not(S)), CS).

valid_move(_, _, CS, [(_, (withdraw, _), _)|_], (claim, S), (claim, S)):-
        not_inCS((_, S), CS),
        not_inCS((_, not(S)), CS).

valid_move(_, _, CS, [(_, (accept, _), _)|_], (claim, S), (claim, S)):-
        not_inCS((_, S), CS),
        not_inCS((_, not(S)), CS).

valid_move(NL, NP, CS, DM, ValidMove, _) :-
        read_again(NP, Move),
        valid_move(NL, NP, CS, DM, ValidMove, Move).

check_reasonsets(_, [], _, _):- fail.

check_reasonsets(CS, Proset, Conset, B) :-
        peel(CS, Proset, Conset, B, _, _).

peel([(bert, reason(R, B))|Rest], Proset, Conset, B, Checkpro, Checkcon) :-
        peel(Rest, Proset, Conset, B, [R|Checkpro], Checkcon).

peel([(bert, reason(R, not(B)))|Rest], Proset, Conset, B, Checkpro, Checkcon) :-
        peel(Rest, Proset, Conset, B, Checkpro, [R|Checkcon]).

peel([_|Rest], Proset, Conset, B, Checkpro, Checkcon) :-
        peel(Rest, Proset, Conset, B, Checkpro, Checkcon).

peel([], Proset, Conset, _, Proset, Conset).

update_CS(_, CS, [(NP, S)|CS], (claim, S), NP):-
        write_CS([(NP, S)|CS]).

update_CS(DM, CS, NewCS, (accept, S), NP) :-
        bigupdate_CS(DM, CS, NewCS, (accept, S), NP),
        write_CS(NewCS).

update_CS(DM, CS, NewCS, (withdraw, S), NP) :-
        bigupdate_CS(DM, CS, NewCS, (withdraw, S), NP),
        write_CS(NewCS).

update_CS(_, CS, CS, _, _):-
        write_CS(CS).

bigupdate_CS([(_, (claim, S), _)|_], CS, [(NP, S)|CS], (accept, S), NP).

bigupdate_CS([X|Rest], CS, NewCS, (accept, S), NP) :-
        bigupdate_CS(Rest, CS, NextCS, (accept, S), NP),
        realupdate_CS([X|Rest], NextCS , NewCS , (accept, S), NP).

bigupdate_CS([(_, (claim, S), _)|_], CS, NewCS, (withdraw, S), NP) :-
        del((NP, S), CS, NewCS).

bigupdate_CS([X|Rest], CS, NewCS, (withdraw, S), NP) :-
        bigupdate_CS(Rest, CS, NextCS, (withdraw, S), NP),
        realupdate_CS([X|Rest], NextCS, NewCS, (withdraw, S), NP).

realupdate_CS([(P, (claim, not(S)), _)|_], CS, CS, (withdraw, S), _) :-
        inCS((P, not(S)), CS).

realupdate_CS([(P, (claim, S), _)|_], CS, NewCS, _, _) :-
        inCS((P, S), CS),
        otherplayer(P, Op),
        not_inCS((Op, S), CS),
        del((_, S), CS, NewCS).

realupdate_CS(_, CS, CS, _, _).

write_CS([(bert, S)|Rest]) :-
        teller(U),
        send(@csb, newline),
        send(@csb, print, U),
        send(@csb, print, '. '),
        send(@csb, print, S),
        write_CS(Rest).

write_CS([(ernie, S)|Rest]) :-
        teller(U),
        send(@cse, newline),
        send(@cse, print, U),
        send(@cse, print, '. '),
        send(@cse, print, S),
        write_CS(Rest).

write_CS([]).

otherplayer(bert, ernie).
otherplayer(ernie, bert).

/*previous_withdraw(Player, S, DM)*/
previous_withdraw(_, _, []):-fail.

previous_withdraw(P, S, [(P, (withdraw, S), _)|_]).

previous_withdraw(P, S, [_|Rest]):-
        previous_withdraw(P, S, Rest).

only_inCS_other(CS, P, S) :-
        otherplayer(P, Op),
        inCS((Op, S), CS),
        not_inCS((P, S), CS).

inCS(_, []):-fail.

inCS(Element, [Element|_]).

inCS(Element, [_|Rest]) :-
        inCS(Element, Rest).

not_inCS(_, []).

not_inCS(Element, [OtherElement|Rest]) :-
        Element \= OtherElement,
        not_inCS(Element, Rest).

del(X, [X|Tail], Tail).

del(X, [Y|Tail], [Y|Tail1]) :-
        del(X, Tail, Tail1).

create_windows :-
  new(@mainf, frame('Dialaw Window')),
  send(@mainf, append, new(@csb, view('Berts commitments', size(25,10)))),
  send(new(@cse, view('Ernies commitments', size(25,10))), right, @csb),
  send(new(@dv, view('Dialog', size(@default,10))), above, @csb),
  send(new(@sv, view('status', size(@default,10))), above, @dv),
  send(@mainf, open).

delete_windows :-
        send(@mainf, destroy).

teller :-
        retract(teller(Umin1)),
        U is Umin1 + 1,
        assert(teller(U)).

write_levelmark(0) :-!.

write_levelmark(L) :-
        send(@dv, print, '>'),
        LL is L-1,
        write_levelmark(LL).

printreeks([]).

printreeks([K|S]) :- put(K), printreeks(S).