:-op(100,fy,~).        % negation
:-op(110,yfx,&).       % conjunction
:-op(120,yfx,v).       % disjunction
:-op(1070,yfx,/->).    % NNF transformations
:-op(1070,yfx,/=>).    % Rule transformations
:-op(1090,xfx,::).     % Labels

:- dynamic show_steps/0.

write_transform(A -> B) :- 
        !,nnf(A,A1),nnf(B,B1),
        t([  [A1] & [] -> [B1] v []  ],G),
        nl,write('Final program:'),nl,show_rules(G).

write_transform(F) :- 
        !,nnf(F,F1),
        t([[] & [] -> [F1] v []],G),
        nl,write('Final program'),nl,show_rules(G).

% t(Rs,Ts) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% transforms Rs into Ts. Both Rs and Ts are lists of expressions like:
%   Bs & BLits -> Hs v HLits
% with Bs, Hs lists of arbitrary formulas and BLits,HLits lists of 
% default literals.

t(Rs,Ts):- append(PreRs,[R|SufRs],Rs),
           unsolved(R),!,                    % pick an unsolved implication R
           (Label :: R /=> RRules),
           (show_steps, Label \= '()',!,
            write('--------------------'),nl,
            show_rules(PreRs),
            show_rule(R),write(' '),write(Label),nl,
            show_rules(SufRs)
           ; true),
           append(PreRs,RRules,Rs2),
           append(Rs2,SufRs,Rs3),
           t(Rs3,Ts).
t(Rs,Rs).

unsolved([_|_] & _ -> _):-!.
unsolved(_ -> [_|_] v _).

is_literal(~ A):-atom(A),!.
is_literal(A):-atom(A).


% Left rules
'(L1)'::	[true|Bs] & BLs -> H	   /=> [ Bs & BLs -> H ]	:-!.

'(L2)'::	[false|_Bs] & _BLs -> _H   /=> []			:-!.

'()'::	        [F|Bs] & BLs -> H	   /=> [ Bs & [F|BLs] -> H ]
							:- is_literal(F),!.

'()'::		[F & G | Bs] & BLs -> H    /=> [ [F,G|Bs] & BLs -> H ]	:-!.
 
'(L3)'::	[~ ~ F | Bs] & BLs -> Hs v HLs
			   		   /=> [ Bs & BLs -> [~ F|Hs] v HLs ]											:-!.

'(L4)'::	[F v G | Bs] & BLs -> H    /=> [ [F|Bs] & BLs -> H,
			         		 [G|Bs] & BLs -> H 
					       ]			:-!.

			   
'(L5)'::	[F -> G | Bs] & BLs -> Hs v HLs
			   		   /=> [ [G|Bs] & BLs -> Hs v HLs,
				               [NOTF|Bs] & BLs -> Hs v HLs,
					       Bs & BLs -> [F,NOTG|Hs] v HLs ]
					   :-!,nnf(~ F,NOTF),nnf(~ G,NOTG).
			   
% Right rules
'(R1)'::	Bs -> [false|Hs] v HLs     /=> [ Bs -> Hs v HLs ]	:-!.

'(R2)'::	_B -> [true|_Hs] v _HLs    /=> []			:-!.

'()'::	     	B -> [F|Hs] v HLs	   /=> [ B -> Hs v [F|HLs] ]
							:-is_literal(F),!.

'()'::		B -> [F v G | Hs] v HLs    /=> [ B -> [F,G|Hs] v HLs ]	:-!.

'(R3)'::	Bs & BLs -> [~ ~ F | Hs] v HLs
			   		   /=> [ [~ F|Bs] & BLs  -> Hs v HLs ]
					  				:-!.

'(R4)'::	B -> [F & G | Hs] v HLs    /=> [ B -> [F|Hs] v HLs,
                                 		 B -> [G|Hs] v HLs 
					       ]			:-!.

'(R5)'::	Bs & BLs -> [F -> G|Hs] v HLs
			   	/=> [ [F|Bs] & BLs -> [G|Hs] v HLs,
			              [NOTG|Bs] & BLs -> [NOTF|Hs] v HLs
				    ]	
				    :-!,nnf(~ F,NOTF),nnf(~ G,NOTG).

% nnf: unfolds applications of 'not' to nonliteral formulas
% and simplifies some trivial cases of truth constants.

nnf(F,G):-subterms(F,F2),(F2=F,!,G=F; nnf(F2,G)).

subterms(F,F):-atom(F),!.
subterms(F,G):-
	F =.. [Func|Args],
	maplist(subterms,Args,Args2),
	F2 =.. [Func|Args2],
	((F2 /-> G),! ; G=F2).

% Simplifications for 'not'
~ ~ ~ A     /->  ~ A			:-!.
~ true      /->  false			:-!.
~ false     /->  true			:-!.
~ (A & B)   /->  ~ A v ~ B		:-!.
~ (A v B)   /->  ~ A & ~ B		:-!.
~ (A -> B)  /->  ~ ~ A & ~ B		:-!.

% Ruling out some truth constants
A & true      /-> A			:-!.
true & A      /-> A			:-!.
_A & false    /-> false			:-!.
false & _A    /-> false			:-!.
_A v true     /-> true			:-!.
true v _A     /-> true			:-!.
A v false     /-> A			:-!.
false v A     /-> A			:-!.
false ->_A    /-> true			:-!.
_A -> true    /-> true			:-!.


show_rules(Rs):-
	repeat, (
	  member(R,Rs),
	  show_rule(R),nl,
	  fail
	;true),!.
show_rule( Bs & BLs -> Hs v HLs ):-
	append(Bs,BLs,B),
	writeall(' & ',B),
	write(' -> '),
	append(Hs,HLs,H),
	writeall(' v ',H).

writeall(nl,[]):-!,nl.
writeall(nl,[X|L]):-!,write(X),nl,writeall(nl,L).
writeall(_Sep,[]):-!.
writeall(_Sep,[X]):-!,write(X).
writeall(Sep,[X|L]):-write(X),write(Sep),writeall(Sep,L).

:-  assert(debug),
    write_transform((~ p -> q) -> ~ (p -> r)).
    
    
