%==============================================================================
%----This outputs in CLIF/HYBRID format 
%----
%----Written by Geoff Sutkiffe, March 2008
%----This mistreats constants that look like variables.
%----DANGER - CONSTANTS THAT LOOK LIKE VARIABLES GET TREATED AS VARIABLES
%==============================================================================
%==============================================================================
%----Generic output
%==============================================================================
%----Translate symbols if necessary. Only equal right now
output_kif_symbol('$tptp_equal'):-
    !,
    write('=').

output_kif_symbol('$tptp_not_equal'):-
    !,
    write('/='),
    print_message(warning,"ERROR - SHOULD NOT GET HERE - PLEASE TELL GEOFF").

output_kif_symbol(Reserved):-
    tptp2X_member(Reserved,[forall,exists,iff,implies,if,and,or,not]),
    !,
    write(Reserved),
    write('__kif').

%---All others do as is
output_kif_symbol(Symbol):-
    write(Symbol).
%------------------------------------------------------------------------------
%----Output an atom with variables in KIF format
output_kif_term([OneTerm]):-
    !,
    output_kif_term(OneTerm).

output_kif_term([FirstTerm|RestOfTerms]):-
    !,
    output_kif_term(FirstTerm),
    write(' '),
    output_kif_term(RestOfTerms).

%----Variables look like atoms that start with uppercase. For KIF they
%----need a leading ?.
output_kif_term(Variable):-
    atomic(Variable),
    name(Variable,[FirstASCII|_]),
    FirstASCII >= 65,
    FirstASCII =< 90,
    !,
    write('?'),
    write(Variable).

%----Numbervars variables look like shit.
output_kif_term('$VAR'(Index)):-
    !,
    write('?'),
    write('$VAR'(Index)).

%----Normal atomic things
output_kif_term(Term):-
    atomic(Term),
    !,
    write(Term).

%----Complex terms
output_kif_term(Complex):-
    Complex =.. [Symbol|Arguments],
    write('('),
    output_kif_symbol(Symbol),
    write(' '),
    output_kif_term(Arguments),
    write(')').
%------------------------------------------------------------------------------
%----Output an atom
kif_output_variable(Variable):-
    write('?'),write(Variable).
%------------------------------------------------------------------------------
%----Output an atom
%----Constants
kif_output_atom(_,'$true'):-
    !,
    write('(or)').

kif_output_atom(_,'$false'):-
    !,
    write('(and)').

%----Propositions get ()ed
kif_output_atom(_,Atom):-
    atomic(Atom),
    !,
    write('('),
    writeq(Atom),
    write(')').

kif_output_atom(_,Atom):-
    output_kif_term(Atom).
%------------------------------------------------------------------------------
%==============================================================================
%----FOF output
%==============================================================================
%------------------------------------------------------------------------------
%----Recognise and split up quantified formulae
kif_quantified_formula(QuantifiedFormula,KIFQuantifier,Variables,
Formula):-
    QuantifiedFormula =.. [:,Quantification,Formula],
    !,
    Quantification =.. [Quantifier,Variables],
    tptp2X_member(ct(Quantifier,KIFQuantifier),[ct('!',forall),ct('?',exists)]).
%------------------------------------------------------------------------------
%----Recognise and split up binary formulae
kif_binary_formula(BinaryFormula,KIFConnective,LHS,RHS):-
    BinaryFormula =.. [Connective,LHS,RHS],
    tptp2X_member((Connective)-(KIFConnective),
[('<=>')-('iff'),('<~>')-('xor'),('<=')-('then'),('=>')-('if'),('&')-('and'),
(';')-('or'),('|')-('or')]).
%----Both needed after shorten which sets '|' somewhere - need to check
%----|;BUG
%------------------------------------------------------------------------------
%----Recognise and split up unary formulae
kif_unary_formula(UnaryFormula,KIFConnective,Formula):-
    UnaryFormula =.. [Connective,Formula],
%----Had to use ()s due to some Prolog confusion about -
    tptp2X_member((Connective)-(KIFConnective),[('~')-('not')]).
%------------------------------------------------------------------------------
%----The format for outputing quantified formulae in oscar format
%----FormulaPrefix,VariablesPrefix,VariablesSeparator,VariablesSuffix,
%----FormulaSuffix
kif_quantified_format('(',' (',' ',')',' )').

%----PrefixBracket,ConnectivePrefix,ConnectiveSuffix,SuffixBracket
kif_binary_format('(','','',' )').

%----FormulaPrefix,ConnectiveSuffix,FormulaSuffix
kif_unary_format('(',' ',' )').
%------------------------------------------------------------------------------
%----If the formulae has an acceptable status then output
output_kif_formulae([]).

output_kif_formulae([fof(Name,Role,Formula)|RestOfFormulae]):-
    write('(cl:comment '),
    write('"'),
    write(Name),
    write(', '),
    write(Role),
    write('"'),
    nl,
%----To do by negating conjecture
%    (Role==conjecture -> 
%        (   write('//----This is the conjecture with negated conjecture'),
%            nl,
%            output_generic_prefix_formula(kif,~Formula)
%        )
%    ;   output_generic_prefix_formula(kif,Formula)),
    output_generic_prefix_formula(kif,Formula),
    write(' )'),
    nl,
    nl,
    output_kif_formulae(RestOfFormulae).
%------------------------------------------------------------------------------
output_kif_formulae_by_roles(Formulae):-
    tptp2X_findall_setof1(Role,tptp2X_member(fof(_,Role,_),Formulae),Roles),
    tptp2X_member(Role,Roles),
    findall(fof(Name,Role,Formula),tptp2X_member(fof(Name,Role,Formula),
Formulae),FormulaeWithRole),
    write('(cl:text '),
    write(Role),
    nl,
    nl,
    output_kif_formulae(FormulaeWithRole),
    write(')'),
    nl,
    nl,
    fail.

output_kif_formulae_by_roles(_).
%------------------------------------------------------------------------------
%==============================================================================
%----CNF output
%==============================================================================
%------------------------------------------------------------------------------
output_kif_signed_literal(++'$tptp_not_equal'(LHS,RHS)):-
    !,
    output_kif_signed_literal(--'$tptp_equal'(LHS,RHS)).

output_kif_signed_literal(--Atom):-
    !,
    write('(not '),
    kif_output_atom(cnf,Atom),
    write(')').

output_kif_signed_literal(++Atom):-
    kif_output_atom(cnf,Atom).
%------------------------------------------------------------------------------
%----Output the literals of the clause in KIF format
%----Special case of an empty clause
output_kif_clause([]):-
    !.

output_kif_clause([OneLiteral]):-
    !,
    output_kif_signed_literal(OneLiteral).

output_kif_clause([FirstLiteral|RestOfLiterals]):-
    output_kif_signed_literal(FirstLiteral),
    nl,
    write('        '),
    output_kif_clause(RestOfLiterals).
%------------------------------------------------------------------------------
%----Output the clauses selected by status
output_kif_clauses([]):-
    !.

%----If the clause has an acceptable status then output
output_kif_clauses([input_clause(Name,Role,Literals)|RestOfClauses]):-
    write('(cl:comment '),
    write('"'),
    write(Name),
    write(', '),
    write(Role),
    write('"'),
    nl,
    % write('    (or '),
%----DANGER - CONSTANTS THAT LOOK LIKE VARIABLES GET TREATED AS VARIABLES
    fofify_literals(Literals,Disjunction),
    universally_quantify(Disjunction,QuantifiedDisjunction),
    output_generic_prefix_formula(kif,QuantifiedDisjunction),
    % output_kif_clause(Literals),
    % write(' ) )'),
    write(' )'),
    nl,
    nl,
    output_kif_clauses(RestOfClauses).
%------------------------------------------------------------------------------
output_kif_clauses_by_roles(Clauses):-
    tptp2X_findall_setof1(Role,tptp2X_member(input_clause(_,Role,_),Clauses),
Roles),
    tptp2X_member(Role,Roles),
    findall(input_clause(Name,Role,Clause),tptp2X_member(input_clause(Name,
Role,Clause),Clauses),ClausesWithRole),
    write('(cl:text '),
    write(Role),
    nl,
    nl,
    output_kif_clauses(ClausesWithRole),
    write(')'),
    nl,
    nl,
    fail.

output_kif_clauses_by_roles(_).
%------------------------------------------------------------------------------
%----Output all the clauses in kif format
kif(kif,Clauses,_):-
    tptp_clauses(Clauses),
    output_kif_clauses_by_roles(Clauses).

%----Output all the formulae in kif format
kif(kif,Formulae,_):-
    tptp_formulae(Formulae),
    output_kif_formulae_by_roles(Formulae).
%------------------------------------------------------------------------------
%----Provide information about the kif format
kif_format_information(';; ','.kif').
%------------------------------------------------------------------------------
%----Provide information about the kif file
kif_file_information(format,kif,'KIF format').
%------------------------------------------------------------------------------