%========================================================================
%----This outputs TPTP Problem Set clauses and formulae in a format
%----acceptable to the ftprolog system.
%----FOF only
%----Written by Thomas Raths & Jens Otten, April 2005, adapted Nov 2005
%========================================================================

% Syntax von ft:
%
% constant, variable, function ::=
%         sequence of alphabetic, numeric characters and '_' beginning with
%         a lowercase letter
% 
% term ::= constant | variable | function(terms)
%
% terms ::= term | term , terms
%
% let f, f1, f2 be formulae
%
% formula ::= Literal | Var[var list] 
%          neg f | f1 and f2 | f1 or f2 | f1 imp f2 | f1 iff f2 |
%          a(var,f) | e(var,f) | 
%          (f)


%----Print out the connectives, quantifiers, and literals of a formula
%----in ftprolog format.
output_ftprolog_fof(~ A):-
    !, write('( neg '), output_ftprolog_fof(A), write(' )').
output_ftprolog_fof('|'(A,B) ):- 
    !, write('( '), output_ftprolog_fof(A), write(' or '),
    output_ftprolog_fof(B), write(' )').
output_ftprolog_fof((A ; B)):- 
    !, write('( '), output_ftprolog_fof(A), write(' or '),
    output_ftprolog_fof(B), write(' )').
output_ftprolog_fof(A & B):-
    !, write('( '), output_ftprolog_fof(A), write(' and '),
    output_ftprolog_fof(B), write(' )').
output_ftprolog_fof(A => B):-
    !, write('( '), output_ftprolog_fof(A), write(' imp '),
    output_ftprolog_fof(B), write(' )').
output_ftprolog_fof(A <=> B):-
    !, write('( '), output_ftprolog_fof(A), write(' iff '),
    output_ftprolog_fof(B), write(' )').
output_ftprolog_fof(! [] : A):- !, output_ftprolog_fof(A).
output_ftprolog_fof(! [V|L] : A):-
    !, write('( a(x'), write(V), write(','),
    output_ftprolog_fof(! L : A), write(' ))').
output_ftprolog_fof(? [] : A):- !, output_ftprolog_fof(A).
output_ftprolog_fof(? [V|L] : A):-
    !, write('( e(x'), write(V), write(','),
    output_ftprolog_fof(? L : A), write(' ))').
output_ftprolog_fof('$true') :- !, write('(atom___ imp atom___)').
output_ftprolog_fof('$false') :- !, write('(false___)').
output_ftprolog_fof(Atom) :- transpred_ftprolog(Atom).

%%% transform a tptp-variable or constant 'XYZ' into xXYZ
transpred_ftprolog(A) :- atom(A), !, write(A).
transpred_ftprolog(A) :- A=..[B|C], 
                         write(B), write('('), transterms_ftprolog(C), write(')').
transterms_ftprolog([A|T]):- looks_like_a_variable(A), !, write('x'), write(A),
                             (T\=[] -> (write(','), transterms_ftprolog(T)); true).
% A cannot be a variable
transterms_ftprolog([A|T]):- A=..[B|C], 
                             write(B), write('('), transterms_ftprolog(C), write(')'),
                            (T\=[] -> (write(','), transterms_ftprolog(T)); true).

%----------------------------------------------------------------------
%----Print out the formulae in ftprolog format.
output_ftprolog_fo_formulae([]).

% for TPTP-v3.1.0 or later
output_ftprolog_fo_formulae([fof(Name,Status,Formula)|
RestOfFormulae]):-
    write('% '), write(Name), write(', '),
    write(Status), write('.'), nl,
    write('('),
    (Status==conjecture ->
         output_ftprolog_fof(Formula);
         output_ftprolog_fof(Formula)),
    write(')'),
    ( (RestOfFormulae=[fof(_,axiom,_)|_];
       RestOfFormulae=[fof(_,lemma,_)|_];
       RestOfFormulae=[fof(_,definition,_)|_];
       RestOfFormulae=[fof(_,hypothesis,_)|_])  ->
        (nl, nl,
         write(' and '), nl, nl);
         (RestOfFormulae=[fof(_,conjecture,_)|_]  ->
             (nl, nl,
              write(' imp '), nl, nl);
             true)),
    output_ftprolog_fo_formulae(RestOfFormulae).

% for TPTP-v2.7.0 or earlier
output_ftprolog_fo_formulae([input_formula(Name,Status,Formula)|
RestOfFormulae]):-
    write('% '), write(Name), write(', '),
    write(Status), write('.'), nl,
    write('('),
    (Status==conjecture ->
         output_ftprolog_fof(Formula);
         output_ftprolog_fof(Formula)),
    write(')'),
    ( (RestOfFormulae=[input_formula(_,axiom,_)|_];
       RestOfFormulae=[input_formula(_,hypothesis,_)|_])  ->
        (nl, nl,
         write(' and '), nl, nl);
         (RestOfFormulae=[input_formula(_,conjecture,_)|_]  ->
             (nl, nl,
              write(' imp '), nl, nl);
             true)),
    output_ftprolog_fo_formulae(RestOfFormulae).
%----------------------------------------------------------------------
%----Print out the list of input formulae as a first-order formula in
%----ftprolog format.
output_ftprolog_fo_formula([]):-
    !.

output_ftprolog_fo_formula(Formulae):-
    nl,
    write('f(('), nl, nl,
    output_ftprolog_fo_formulae(Formulae), nl, nl,
    write(')).'), nl, nl.

%----------------------------------------------------------------------

%----------------------------------------------------------------------
%----Print out all the clauses in ftprolog format.
ftprolog(ftprolog,Clauses,_):-
    tptp_clauses(Clauses),
    output_ftprolog_formula(Clauses).

%----Print out first-order formula in ftprolog format.
ftprolog(ftprolog,Formulae,_):-
    tptp_formulae(Formulae),
    output_ftprolog_fo_formula(Formulae).
%----------------------------------------------------------------------
%----Provide information about the ftprolog format.
ftprolog_format_information('%','.ftprolog').
%----------------------------------------------------------------------
%----Provide information about the TPTP file.
ftprolog_file_information(format,ftprolog).
%----------------------------------------------------------------------