:- op(1050,xfy,<->).
:- op(1050,xfy,<-).
:- op(1005,xfy,v).
:- op(1000,xfy,&).
:- op(900,xfy,:).
:- op(800,fy,all).
:- op(800,fy,exists).

main :- unix(argv(Argv)),
	Argv=[_ExecutableName|Args],
	readfiles([],Args,Fs),
	predicates(Fs,Ps),
	writeaxioms(Ps),
	star(Fs,Gs),
	write('formulas(goals).\n'),
	repeat,
	  ( member(G,Gs),
	    writeformula(G),write('.'),nl,fail
	  ;!),
	write('end_of_list.\n').

readfiles(Fs,[],Fs).
readfiles(Fs0,[File|Files],Fs):-
	see(File),read_clauses(Fs1),seen,
	append(Fs0,Fs1,Fs2),readfiles(Fs2,Files,Fs).

read_clauses(Fs):-
	read(F),(
	   F=end_of_file,!,Fs=[]
	 ; read_clauses(Gs),Fs=[F|Gs]
	).

%--- The '*' transformation
star([],[]):-!.
star([F|Fs],[G|Gs]):-!, star(F,G), star(Fs,Gs).

star(F,F):- F=.. [P|_], member(P,[all,exists,true,false]),!.	

star(F,G):-
	F =.. [Op|Args],
	member(Op,[(&), (v), (:), true, false]),!,
	star(Args,Args1),
	G =.. [Op|Args1].

star( -A , -A & -A1 ):-!,star(A,A1).

star( (A -> B) , ( (A -> B) & (A1 -> B1) ) ):-!,star(A,A1),nl, star(B,B1).
star( (A <- B) , ( (A <- B) & (A1 <- B1) ) ):-!,star(A,A1),nl, star(B,B1).
star( (A <-> B) , ( (A <-> B) & (A1 <-> B1) ) ):-!,star(A,A1),nl, star(B,B1).
	
star(F,G):-	F =.. [P|Args],	concat_atom([P,'_star'],P1), G =.. [P1|Args].
	
%--- Get the list of predicates
predicates([],[]):-!.
predicates([F|Fs],Rs):- !,predicates(F,Ps),predicates(Fs,Qs),merge_set(Ps,Qs,Rs).

predicates(F,Ps):-
	F =.. [Op|Args], 
	member(Op,[(&), (v), (-), (->), (<->), (<-), (:)]),!,
	predicates(Args,Ps).
	
predicates(T,[]):- T=.. [P|_], member(P, [all,exists,true,false]), !.	

predicates(T,[P/N]):- T =.. [P|Args], length(Args,N).
	
%--- Print prover9 output

vartuple(0,[]):-!.
vartuple(I,Xs):- J is I-1, vartuple(J,Xs0), concat_atom([x,J],XJ), append(Xs0,[XJ],Xs).
	
writeformula(Quant : F):-
	Quant =.. [Q,_X],member(Q,[all,exists]),!,
	write(Quant),write(' '),
	F=..[Op|_],current_op(N,_,all),
	(current_op(N1,_,Op),N1>N,!,write('('),writeformula(F),write(')');writeformula(F)).

% binary connectives

writeformula(F):-
	F=..[Op,Arg1,Arg2],member(Op,[(&), (v), (->), (<->), (<-)]),!,
	current_op(N,_,Op),!,
	Arg1 =.. [Op1|_],
	(current_op(N1,_,Op1),(N1>N,!; N1=N,\+ member(Op1,[(&), (v)])),!,write('('),Parenth=yes; Parenth=no),
	writeformula(Arg1),
	(Parenth=yes,!,write(')'); true),
	write(' '),(Op=(v),!,write('|');write(Op)),write(' '),
	Arg2 =.. [Op2|_],
	(current_op(_,_,Op2),!,write('('),Parenth2=yes; Parenth2=no),
	writeformula(Arg2),
	(Parenth2=yes,!,write(')'); true).

writeformula(-F):-
	!,F =.. [Op1|_],
	current_op(N,fy,(-)),
	write('-'),
	(current_op(N1,_,Op1),N1>N,!,write('('),Parenth=yes; Parenth=no),
	writeformula(F),
	(Parenth=yes,!,write(')'); true).	
		
writeformula(F):-write(F).

writeaxioms(Ps):-
	write('formulas(assumptions).'),nl,
	repeat,
	  ( member(P/N,Ps),
	    vartuple(N,Xs),
		A =.. [P|Xs],
		concat_atom([P,'_star'],Pstar),
		Astar =.. [Pstar|Xs],
		write( Astar -> A),write('.'),nl,
		fail
	  ;!),write('end_of_list.\n').
