%========================================================================
%----This outputs TPTP Problem Set clauses in a format acceptable to 
%----the leanCoP system.
%----
%----Written by Jens Otten, March 2000
%----Based on format.leantap
%========================================================================
%----Print out a literal with - for negative, nothing for positive.
%----Use positive representation
output_leancop_signed_literal(--Atom):-
    !,
    write(' '),
    write(Atom).

output_leancop_signed_literal(++Atom):-
    write('-'),
    write(Atom).
%----------------------------------------------------------------------
%----Print out the literals of a clause in leanCoP format.
%----Special case of an empty clause
output_leancop_literals([]):-
    !,
    write('[]').

output_leancop_literals([OneLiteral]):-
    !,
    output_leancop_signed_literal(OneLiteral).

output_leancop_literals([FirstLiteral|RestOfLiterals]):-
    output_leancop_signed_literal(FirstLiteral),
    write('  ,'),
    nl,
    write(' '),
    output_leancop_literals(RestOfLiterals).
%----------------------------------------------------------------------
%----Print out the clauses in leanCoP format.
output_leancop_clauses([]):-
    !.

output_leancop_clauses([input_clause(Name,Status,Literals)|
RestOfClauses]):-
    write('% '),
    write(Name),
    write(', '),
    write(Status),
    write('.'),
    nl,
    write('['),
    output_leancop_literals(Literals),
    write(']'),
    (RestOfClauses \== []  ->
        (nl,
         nl,
         write('  ,'),
         nl,
         nl);
         true),
    output_leancop_clauses(RestOfClauses).
%----------------------------------------------------------------------
%----Print out the list of input clauses as a formula in leanCoP format.
output_leancop_formula([]):-
    !.

output_leancop_formula(Clauses):-
    nl,
    write('f(['),
    nl,
    nl,
    output_leancop_clauses(Clauses),
    nl,
    nl,
    write(']).'),
    nl,
    nl.    
%----------------------------------------------------------------------
%----Print out all the clauses in leanCoP format.
leancop(leancop,Clauses,_):-
    tptp_clauses(Clauses),
    output_leancop_formula(Clauses).

%----Do nothing for FOF - just leave a comment
leancop(leancop,Formulae,_):-
    tptp_formulae(Formulae),
    write('%----No FOF format available in leanCoP'),
    nl.
%----------------------------------------------------------------------
%----Provide information about the leanCoP format.
leancop_format_information('%','.leancop').
%----------------------------------------------------------------------
%----Provide information about the TPTP file
leancop_file_information(format,leancop).
%----------------------------------------------------------------------