:- use_module(library(readutil)).

:-op(140,fy, [~, ?, !, neg]).
:-op(160, yfx, [&, and, or]).
:-op(180, yfx, '!=').
:-op(200, xfy, [imp, =>]).
:-op(200, xfy, [bimp, <=>]).
:-op(160, xfy, :).

is_connective(Op) :-
	member(Op,[~,neg,&,and,'|',or,=>,imp,<=>,bimp]).

% translate_fmla/2 <-- translate TPTP format into internal formula format
%

translate(~,neg).
translate(&,and).
translate('|',or).
translate(=>,imp).
translate(<=>,bimp).

translate_fmla(Frm,TFrm) :-
	Frm =.. [Op|Frms],
	is_connective(Op),
	!,
	translate(Op,TOp),
	translate_fmlas(Frms,TFrms),
	TFrm =..[TOp|TFrms].
translate_fmla(Frm,TFrm) :-
	Frm =.. [:,Vars,Frm0],
	Vars =.. [!,Xs],
	!,
	translate_fmla(Frm0,TFrm0),
	translate_all(Xs,TFrm0,TFrm).
translate_fmla(Frm,TFrm) :-
	Frm =.. [:,Vars,Frm0],
	Vars =.. [?,Xs],
	!,
	translate_fmla(Frm0,TFrm0),
	translate_exists(Xs,TFrm0,TFrm).
translate_fmla(Frm,Frm).

translate_all([X],Frm,all(X,Frm)).
translate_all([X|Xs],Frm,all(X,TFrm)) :-
    translate_all(Xs,Frm,TFrm).

translate_exists([X],Frm,some(X,Frm)).
translate_exists([X|Xs],Frm,some(X,TFrm)) :-
    translate_some(Xs,Frm,TFrm).

:- translate_all([X,Y],p(X,Y),_TFrm).

translate_fmlas([F|Fs],[TF|TFs]) :-
	translate_fmla(F,TF),
	translate_fmlas(Fs,TFs).
translate_fmlas([],[]).

% translate_clause/2 <-- translate TPTP format into internal clause format
%
translate_clause(Disjunction,L or C) :-
	Disjunction =.. ['|',L0,RestDisjunction],
	!,
	translate_fmla(L0,L),
	translate_clause(RestDisjunction,C).
translate_clause(L,L).
%translate_clause(L,L) :-
%	translate_fmla(Literal,L).

% input2formula(File,Input) <-- reads in an Input from File
% where Input is either a negated Formula, or a clause set

is_fof_annotated([fof(_,_,_)|_]).
is_cnf_annotated([cnf(_,_,_)|_]).

input2formula(File,Input) :-
	read_file_to_terms(File,Problem,[]),
	is_fof_annotated(Problem),
	problem2formula(Problem,Input).
input2formula(File,Input) :-
	read_file_to_terms(File,Problem,[]),
	is_cnf_annotated(Problem),
	problem2clauses(Problem,Cs),
	conjunctions(Cs,Input).

% problem2formula(Problem,Formula) <-- transforms a Problem 
% to a (unsatisfiable) Formula
%
problem2formula(Problem,Formula) :-
	is_fof_annotated(Problem),
	p2fmlas(Problem,Axioms,Conjectures),
	fmlas2formula(Axioms,Conjectures,Formula).

p2fmlas([fof(_,axiom,(Axiom0))|Problem],[Axiom1|Axioms],Conjectures) :-
	translate_fmla(Axiom0,Axiom1),
	p2fmlas(Problem,Axioms,Conjectures).
p2fmlas([fof(_,conjecture,(Conjecture0))|Problem],Axioms,[Conjecture1|Conjectures]) :-
	translate_fmla(Conjecture0,Conjecture1),
	p2fmlas(Problem,Axioms,Conjectures).
p2fmlas([],[],[]).

fmlas2formula(Axioms,Conjectures,Formula) :-
	negate_conjectures(Conjectures,NegatedConjectures),
	append(Axioms,NegatedConjectures,Frms),
	conjunctions(Frms,Formula).

negate_conjectures([C|Cs],[neg(C)|NCs]) :-
	negate_conjectures(Cs,NCs).
negate_conjectures([],[]).

conjunctions([F0,F1|Fs],F0 and Formula) :-	
	conjunctions([F1|Fs],Formula).
conjunctions([Formula],Formula).

% problem2clauses(Problem,Clauses) <-- transforms a Problem 
% to a clause set
%
problem2clauses(Problem,Clauses) :-
	is_cnf_annotated(Problem),
	p2clauses(Problem,Clauses).

p2clauses([cnf(_,Role,C0)|Problem],[C|Cs]) :-
	member(Role,[hypothesis,negated_conjecture]),
	translate_clause(C0,C),
	p2clauses(Problem,Cs).
p2clauses([],[]).

/* Dreadbury Mansion */
:- input2formula('PUZ001+1.p',_F).
:- input2formula('PUZ001-1.p',_F).