/*
	Translate TPTP into LLP
*/
:- op(200, fy, (++)).
:- op(200, fy, (--)).

:- op(1200,  fy, (linear)).
:- op(1200,  fy, (forall)).
:- op(1200, xfy, (\)).
:- op(1200, yfx, (<=)).
:- op(1150,  fx, (resource)).
:- op(1060, xfy, (&)).
:- op( 950, xfy, (-<>)).
:- op( 950, xfy, (=>)).
:- op( 900,  fy, (!)).

:- dynamic input_clause/3.

translate(IN, OUT) :-
	see(IN),
	read_tptp(1, Cs),
	seen,
	tell(OUT),
	(ground(Cs) -> Prop = yes ; Prop = no),
	portray_clause(propositional(Prop)),
	nl,
	to_llp_all(Cs),
	told.

%%
%% Read TPTP clauses
%%

read_tptp(N, Clauses) :-
	read(X),
	read_tptp(X, N, Clauses).

read_tptp(end_of_file, _, []) :- !.
read_tptp(input_clause(_,_,C0), N, [clause(N,C)|Cs]) :-
	conv_clause(C0, C),
	N1 is N + 1,
	read_tptp(N1, Cs).

conv_clause([], []).
conv_clause([L0|Ls0], [L|Ls]) :-
	conv_lit(L0, L),
	conv_clause(Ls0, Ls).

conv_lit(++L, +L).
conv_lit(--L, -L).

%%
%% Translate to LLP
%%

to_llp_all(Cs) :-
	generate_query,
	generate_headers(Cs),
	to_llp_clauses(Cs).

generate_query :-
	B = +'BOT',
	trans_head_lit(B, [Lim,Proof], Head),
	trans_head2_lit(B, [Lim,Proof], Head2),
	portray_clause((Head :- Head2)),
	nl.

generate_headers(Cs) :-
	get_all_pred(Cs, Ps),
	member(F/A, Ps),
	functor(H, F, A),
	gen_header(+H),
	gen_header(-H),
	fail.
generate_headers(_).

get_all_pred(Cs, Ps) :-
	setof(FA, get_all_pred0(Cs, FA), Ps).

get_all_pred0(Cs, F/A) :-
	member(C, Cs),
	C = clause(_,Clause),
	member(Lit, Clause),
	arg(1, Lit, P),
	functor(P, F, A).

gen_header(Lit) :-
	complement(Lit, NLit),
	trans_head_lit(Lit, [Lim,Proof], Head),
	trans_head2_lit(Lit, [Lim,Proof], Head2),
	trans_red_lit(Lit, [], Red),
	trans_red_lit(NLit, [], NRed),
	gen_same(Red, Same),
	gen_same(NRed, NSame),
	portray_clause((Head :- Same, !, fail)),
	(ground(Lit) ->
	    portray_clause((Head :- NSame, !, top, Proof=reduction))
	;
%	    portray_clause((Head :- NSame, !, top, Proof=reduction)),
	    portray_clause((Head :- NRed, top, Proof=reduction))
	),
	portray_clause((Head :- Red => Head2)),
	nl.

gen_same(Lit, Same) :-
	copy_term(Lit, Lit1),
	Lit =.. [_|Xs],
	Lit1 =.. [_|Ys],
	(Xs == [] ->
	    Same = (Lit1)
	;
	    gen_eqs(Xs, Ys, Es),
	    Same = (Lit1, Es)
	).

gen_eqs([X], [Y], (X == Y)) :- !.
gen_eqs([X|Xs], [Y|Ys], (X == Y, Es)) :-
	gen_eqs(Xs, Ys, Es).

to_llp_clauses(Cs0) :-
%	reorder_clauses(Cs0, Cs),
%	to_llp_clauses1(Cs).
	to_llp_clauses1(Cs0).

to_llp_clauses1([]).
to_llp_clauses1([C|Cs]) :-
	to_llp(C),
	to_llp_clauses1(Cs).

reorder_clauses(Cs0, Cs) :-
	add_cost(Cs0, Xs),
	keysort(Xs, Ys),
	remove_cost(Ys, Cs).

add_cost([], []).
add_cost([C|Cs], [K-C|Xs]) :-
	C = clause(_,Clause),
	length(Clause, N),
	variables(Clause, Vs),
	length(Vs, V),
	K = k(V,N),
	add_cost(Cs, Xs).

remove_cost([], []).
remove_cost([_-C|Xs], [C|Cs]) :-
	remove_cost(Xs, Cs).

to_llp(clause(N,Clause0)) :-
	(ground(Clause0) ->
	    Ground = yes
	;
	    Ground = no
	),
	number_lit(Clause0, 1, Clause),
	to_horn(Clause, Hs0),
	(member(+_, Clause0) ->
	    Hs = Hs0
	;
	    Hs = [[lit(0,+'BOT')|Clause]|Hs0]
	),
	horn_to_llp_all(Hs, N, Ground, LLP),
	numbervars((Clause0,LLP), 0, _),
	writeq(cl(N,Clause0)), write('.'), nl,
	(Ground == yes ->
	    write('linear ('), nl
	;
	    write('('), nl
	),
	write_llp(LLP), nl,
	write(').'), nl, nl.

number_lit([], _, []).
number_lit([L|Ls0], M, [lit(M,L)|Ls]) :-
	M1 is M + 1,
	number_lit(Ls0, M1, Ls).

to_horn(Clause, Hs) :-
	to_horn(Clause, [], Hs).

to_horn([], _, []).
to_horn([L|Post], Pre, [[L|Rest]|Hs]) :-
	append(Pre, Post, Rest),
	append(Pre, [L], Pre1),
	to_horn(Post, Pre1, Hs).

horn_to_llp_all([], _, _, []).
horn_to_llp_all([H|Hs], N, Ground, [Z|Zs]) :-
	horn_to_llp(H, N, Ground, Z),
	horn_to_llp_all(Hs, N, Ground, Zs).

horn_to_llp(Clause, N, Ground, Z) :-
	Clause = [lit(_,L)|Ls],
	trans_head2_lit(L, [Lim0,Proof0], Head),
	gen_proof(Clause, N, Proof, Ps),
	( Ls == [] ->
	    (Ground == yes ->
		Z = (Head :- top, Proof0=Proof)
	    ;
		Z = (Head :- Lim0>=1, top, Proof0=Proof)
	    )
	;
	    trans_body(Ls, Lim1, Body, Ps),
	    (Ground == yes ->
		Lim0 = Lim1,
		Z = (Head :- Body, Proof0=Proof)
	    ;	
		Z = (Head :- Lim0>=1, Lim1 is Lim0-1, Body, Proof0=Proof)
	    )
	).

gen_proof(Clause, N, Proof, Ps) :-
	length(Clause, M),
	functor(Proof, proof, M),
	gen_lit_list(Clause, [L|Ls]),
	Proof =.. [_,clause(N,L,Ls)|Ps].

gen_lit_list([], []).
gen_lit_list([lit(M,_)|Ls0], [M|Ls]) :-
	gen_lit_list(Ls0, Ls).

trans_body([], _, top, []).
trans_body([lit(_,L)|Ls], Lim1, Body, [P|Ps]) :-
	complement(L, NL),
	trans_head_lit(NL, [Lim1,P], B),
	(Ls == [] ->
	    Body = B
	;
	    Body = (B & Body1),
	    trans_body(Ls, Lim1, Body1, Ps)
	).

trans_head_lit(Lit, As, Atom) :-
	trans_lit(Lit, "p_", Atom0),
	add_args(Atom0, As, Atom).

trans_head2_lit(Lit, As, Atom) :-
	trans_lit(Lit, "q_", Atom0),
	add_args(Atom0, As, Atom).

trans_red_lit(Lit, As, Atom) :-
	trans_lit(Lit, "r_", Atom0),
	add_args(Atom0, As, Atom).

trans_lit(+Lit, Pre, Atom) :-
	Lit =.. [F|As],
	name(F, N),
	append(Pre, N, N1),
	name(F1, N1),
	Atom =.. [F1|As].
trans_lit(-Lit, Pre, Atom) :-
	Lit =.. [F|As],
	name(F, N),
	append("not_", N, N0),
	append(Pre, N0, N1),
	name(F1, N1),
	Atom =.. [F1|As].
	
trans_clause_no(N, X) :-
	name(N, L),
	append("c_", L, L1),
	name(X, L1).

complement(+X, -X).
complement(-X, +X).

add_args(X, As, Z) :-
	X =.. L,
	append(L, As, L1),
	Z =.. L1.

write_llp([]).
write_llp([X|Xs]) :-
	X = (Head :- Body),
	writeq(Head), write(' :-'), nl,
	write_llp_body(Body),
	(Xs = [] ->
	    true
	;
	    nl, write(') & ('), nl
	),
	write_llp(Xs).

write_llp_body((B1, B2)) :- !,
	write_llp_body(B1), write(','), nl,
	write_llp_body(B2).
write_llp_body((B1 & B2)) :- !,
	tab(2), write('('), nl,
	write_llp_with((B1 & B2)), nl,
	tab(2), write(')').
write_llp_body(((forall Xs \ B1) => B2)) :- !,
	tab(2), write_list(['( forall ',Xs,' \\ ']),
	writeq(B1), write_list([' ) => (']), nl,
	write_llp_body(B2), nl,
	tab(2), write(')').
write_llp_body(B) :-
	tab(2), writeq(B).

write_llp_with((B1 & B2)) :- !,
	write_llp_with(B1), write(' &'), nl,
	write_llp_with(B2).
write_llp_with(B) :-
	tab(2), writeq(B).

write_list([]).
write_list([X|Xs]) :-
	write(X),
	write_list(Xs).

variables(X, Vs) :-
	variables(X, [], Vs).

variables(X, Vs, Vs) :-
	var(X), memq(X, Vs), !.
variables(X, Vs, [X|Vs]) :-
	var(X), !.
variables(X, Vs0, Vs0) :-
	atomic(X), !.
variables([X|Xs], Vs0, Vs) :- !,
	variables(X, Vs0, Vs1),
	variables(Xs, Vs1, Vs).
variables(X, Vs0, Vs) :-
	X =.. Xs,
	variables(Xs, Vs0, Vs).

memq(X, [Y|_]) :-
	X==Y, !.
memq(X, [_|Ys]) :-
	memq(X, Ys).

concat_str(As, X) :-
	concat_str0(As, Name),
	name(X, Name).

concat_str0([], []).
concat_str0([A|As], Name) :-
	concat_str0(As, Name0),
	name(A, N),
	append(N, Name0, Name).

append([], Zs, Zs).
append([X|Xs], Ys, [X|Zs]) :-
	append(Xs, Ys, Zs).

member(X, [X|_]).
member(X, [_|L]) :-
	member(X, L).