/*******************************************************************************
*  Wang's Algorithm 
* (c) P. H. Roosen-Runge, 2002.

*  Checks a file of propositions and reports for each proposition
*  whether it is a tautology.  Each proposition is a term constructed from
*  'not', 'and', 'or', 'xor', 'implies', 'iff', 'true', 'false', 
*  and Prolog terms.  Each term must end in '.'.
*
*  The predicate tautology(Term) succeeds if Term represents a tautology. It
*  uses Wang's algorithm for proving theorems in the propositional calculus
*  using sequents.
*
******************************************************************************/
% Ver 1.0, P. H. Roosen-Runge, December 1990.
% Ver 1.2, December 6, 1991:  modified for Quintus Prolog 3.1
%     1.2.2  Feb. 23, 1992: input must be a ground term.
%     1.3.1 July 5: rewritten for optimization, using Prolog's indexing
%	   on the principal functor of the first argument. Tracing removed.
%     1.4   Dec. 12, 1999: shows counter-example

%     1.4GNU November 4, 2002: Gnu Prolog version
%     1.41GNU Dec. 5: fixed counter-example printing
/*****************************************************************************/

:-op(995,xfy,'>>').    % sequent
:-op(990, yfx, iff).  % Left-associative (yfx) for consistency with
                      % commutative arithmetic operators.

:-op(990,yfx,implies). % for consistency with iff
:-op(980,yfx, [or, cor]).
:-op(970,xfx,xor). % xor isn't associative.  force parenthesization.
:-op(960,yfx,[and, cand]).
:-op(950,fy,not).
:-op(700,yfx,['<=','<', '>','=>', '>=', '<>', '!=']). % was right-associative
:-op(400, xfx, [div, mod]).
:-op(200, xfy,'**').
:-op(200, xf, '!').

:- initialization(activate).   % gprolog      

error(X) :- write('!! '), write(X), nl.
activate :- 
      set_linedit_prompt('|:'),
      write('wang: version 1.41GNU, December 5, 2002.'), nl,
      propositions
     ;
      nl, error('Something wrong.'), halt.

propositions :- read(T),
	(  T==end_of_file, halt
	 ; 
            nl, write(T), nl,
	   \+ ground(T) -> nl,  % defined below; not in gprolog.
               error('Prolog variable in input. Use lower-case or quote it.')
	 ; 
	    check(T)
	), 
	propositions.

check(T) :- 
        (
         tautology(T), nl, display('* Valid.'), nl, nl  
        ;
        nl, display('* Not valid.')
        ), 
        nl, nl.

tautology(Term) :- (!), sweepR(Term, ([]>>[]), ([]>>[])).

checkAtoms(S, LAtoms>>RAtoms) :- 
	ok(LAtoms, RAtoms), (!)  % gprolog parser problem?
	;
	S \== ([]>>[]) -> sweep(S, LAtoms>>RAtoms)
	; 
        noLogical(LAtoms), noLogical(RAtoms),
	     showCounterExample(LAtoms, RAtoms),(!), fail
        ;
        RAtoms = [false], noLogical(LAtoms),
        nl, write('Counterexample: '),
        writeSet(LAtoms), write(' is true.'), (!), fail
        ;
        LAtoms = [true], noLogical(RAtoms),
        nl, write('Counterexample: '),
        writeSet(RAtoms), write(' is false.'), (!), fail 
        ; 
        fail. %  no counterexample for [true] >> [false], etc.

ok(LAtoms, RAtoms) :-
	memberchk(false, LAtoms) ; memberchk(true, RAtoms)
        ;
        member(M, LAtoms), member(M, RAtoms).


noLogical([]).
noLogical([First | Rest]) :- 
	 \+ logical(First),
	 noLogical(Rest).

logical(First) :- 
        functor(First, true, 0) ; functor(First, false, 0) ;
	functor(First, not, 1) ;
	functor(First, F, 2), member(F, [and, or, iff, xor, implies]).
	
showCounterExample(Left, Right) :-
	nl, write('Counterexample: '),
	Left = [] -> writeSet(Right), write(' is false.')
	;
        Right = [] -> writeSet(Left), write(' is true.')
        ;
	writeSet(Left), write(' is true and '),
	writeSet(Right), write(' is false.').
       
writeSet([X]) :- write(X).
writeSet(X) :- 
	list_to_set(X, Set),
       (
        Set = [Single], write(Single)
        ;
	write('each of '), write(Set)
       ).

sweep([P | Rest]>>R, Atoms) :- (!), sweepL(P, Rest>>R, Atoms).
sweep(L>>[P | Rest], Atoms) :- (!), sweepR(P, L>>Rest, Atoms).

sweepR(not P, S, Atoms) :- (!), sweepL(P, S, Atoms).
sweepR(C1 or C2, L>> Rest, Atoms) :- (!), sweepR(C1, L>>[C2 | Rest], Atoms).
sweepR(C1 implies C2, L>>R, Atoms) :- 
		(!), sweepR(C2, [C1 | L]>>R, Atoms).		
sweepR(C1 and C2, S, Atoms) :-
		(!), sweepR(C1, S, Atoms), (!),
		sweepR(C2, S, Atoms).
sweepR(C1 iff C2, L>>R, Atoms) :-
		(!), sweepR(C2, [C1 | L]>>R, Atoms), (!),
                sweepR(C1, [C2 | L]>>R, Atoms).
sweepR(C1 xor C2, S, Atoms) :-  (!), sweepL(C1 iff C2, S, Atoms).
sweepR(P, S, LAtoms>>RAtoms) :- checkAtoms(S, LAtoms>>[P | RAtoms]).

sweepL(not P, S, Atoms) :- (!), sweepR(P, S, Atoms).
sweepL(C1 and C2,  Rest>>R, Atoms) :- (!), sweepL(C1, [C2 | Rest] >> R, Atoms).
sweepL(C1 or C2, S, Atoms) :-
                (!), sweepL(C1, S, Atoms), (!), sweepL(C2, S, Atoms).
sweepL(C1 implies C2, S, Atoms) :-
                (!), sweepR(C1, S, Atoms), (!), sweepL(C2, S, Atoms).
sweepL(C1 iff C2, Rest>>R, Atoms) :-
		(!), sweepL(C1 implies C2, [C2 implies C1 | Rest]>>R, Atoms).
sweepL(C1 xor C2, S, Atoms) :-	(!), sweepR(C1 iff C2, S, Atoms).
	
sweepL(P, S, LAtoms>>RAtoms) :- checkAtoms(S, [P | LAtoms]>>RAtoms).

ground(T) :-
    nonvar(T),
   (
     functor(T, _, 0)
    ;
     T =.. [_ | Args], grounds(Args)
   ).

grounds([T]) :- ground(T).
grounds([H | T]) :- ground(H), grounds(T).

%   list_to_set(+List, ?Set)

%   Authors: Lawrence Byrd + Richard A. O'Keefe
%   Updated: 19 Jan 1994

list_to_set([], []).
list_to_set([Head|Tail], Set) :-
    memberchk(Head, Tail),
    (!),
    list_to_set(Tail, Set).
list_to_set([Head|Tail], [Head|Set]) :-
    list_to_set(Tail, Set).
