%====================================================================
%----This converts input sets in the TPTP Problem Set into a format 
%----acceptable to someother system.
%----
%----Entry point : tptp2X(<TPTP file>,<Format>,<Arrangements>,
%----              <Output directory>,<Shorten flag>).
%----where the <Format> is one of :
%----    setheo
%----    otter(<sos>,<inference rules>), 
%----      where <sos> is one of :
%----          theorem
%----          hypothesis
%----          positive
%----          negative
%----          unit
%----      and <inference rules> is a list of Otter inference rules.
%----    mgtp
%----    pttp
%----    tptp
%----<Arrangements> is a list of arrangements :
%----    none
%----    lr
%----    cr
%----    clr
%----<Shorten flag> is shorten to replace all symbols by short ones.
%----
%----Written by Geoff Sutcliffe, July 1992.
%----Updated by Geoff Sutcliffe, November 1992.
%----Updated by Geoff Sutcliffe, March 1993.
%----
%----Written for SICStus Prolog. Points that may need fixing for
%----other interpreters are not/1 (may be built in) and realRead
%----which uses SICStus specific system calls. A naive alternative
%----to realRead is provided.
%====================================================================
%----These are used in the TPTP. They are also declared at runtime
%----in tptp2X/5
:-op(100,fx,++).
:-op(100,fx,--).
%----Include the code for shortening clauses
:-compile(tptpshort).
%----Use the standard TPTP read code
:-compile(tptpread).
%----Load the format files
:-compile('format.setheo').
:-compile('format.otter').
:-compile('format.mgtp').
:-compile('format.pttp').
:-compile('format.sprfn').
:-compile('format.tptp'). 
%--------------------------------------------------------------------
%----Simple append, required in tptpread
append__([Head|Tail],List,[Head|TailList]):-
    !,
    append__(Tail,List,TailList).

append__([],List,List):-
    !.
%--------------------------------------------------------------------
%----Split (not append Tsang!)
%----This must make the front list short as possible first
split__([],L,L).

split__([H|T],L,[H|T1]):-
    split__(T,L,T1).
%----------------------------------------------------------------------
%----Simple select
select__(Element,[Element|Tail],Tail).

select__(Element,[Head|Tail],[Head|SelectedTail]):-
    select__(Element,Tail,SelectedTail).
%--------------------------------------------------------------------
%----Simple member
member__(Element,[Element|_]).

member__(Element,[_|Tail]):-
    member__(Element,Tail).
%--------------------------------------------------------------------
%----Remove all elements upto the last delimiter
list_tail__([],_,[],not_found):-
    !.
    
%----Check if the delimiter is further down the list
list_tail__([_|List_tail],Delimiter,Tail_tail,found):-
    list_tail__(List_tail,Delimiter,Tail_tail,found),
    !.

%----Check if this is the delimiter
list_tail__([Delimiter|List_tail],Delimiter,List_tail,found):-
    !.

%----Otherwise pass back this list
list_tail__(List,_,List,not_found).
%----------------------------------------------------------------------
%----Clauses to the same as the UNIX basename command
basename__(Full_name,Suffix,Basename):-
    name(Full_name,Full_name_list),
    name(Suffix,Suffix_list),
%----Delete upto last / (ASCII 47)
    list_tail__(Full_name_list,47,Full_name_tail_list,_),
%----Try to delete suffix from list
    (split__(Basename_list,Suffix_list,Full_name_tail_list) ->
        name(Basename,Basename_list);
%----If not possible, then ignore the suffix
        name(Basename,Full_name_tail_list)).
%----------------------------------------------------------------------
%----Clauses the same as the UNIX dirname command
dirname__(Full_name,Dirname):-
    name(Full_name,Full_name_list),
%----Remove the basename
    basename__(Full_name,'',Basename),
    name(Basename,Basename_list),
%----Find what is before the basename, if anything
    (split__(Dirname_list,[47|Basename_list],Full_name_list) ->
        name(Dirname,Dirname_list);
%----If no directory then it's the current one
        Dirname = '.').
%----------------------------------------------------------------------
%----Concatenate a list of atoms into a list of the ASCII
concatenate_atoms_to_list__([],[]):-
    !.

concatenate_atoms_to_list__([First_term|Rest_of_terms],Terms_list):-
    concatenate_atoms_to_list__(Rest_of_terms,Rest_list),
    name(First_term,First_list),
    append__(First_list,Rest_list,Terms_list).
%----------------------------------------------------------------------
%----Concatenate a list of terms into a big atom
concatenate_atoms__(Atoms,Atom):-
    concatenate_atoms_to_list__(Atoms,Atoms_list),
    name(Atom,Atoms_list).
%----------------------------------------------------------------------
%-----Fast reverse a list
fast_reverse_list__([],Reverse_list,Reverse_list):-
    !.

fast_reverse_list__([Head|Tail],Reverse_so_far,Reverse_list):-
    fast_reverse_list__(Tail,[Head|Reverse_so_far],Reverse_list).
%----------------------------------------------------------------------
%----Reverse the literals in each input clause
reverse_literals_in_clauses__([],[]):-
    !.

reverse_literals_in_clauses__([input_clause(Name,Status,Literals)|
Rest_of_input_clauses],[input_clause(Name,Status,Reversed_literals)|
Rest_of_new_input_clauses]):-
    fast_reverse_list__(Literals,[],Reversed_literals),
    reverse_literals_in_clauses__(Rest_of_input_clauses,
Rest_of_new_input_clauses).
%--------------------------------------------------------------------
%----Depending on the option, rearrange the clauses accordingly
rearrange_clauses__(Input_clauses,none,Input_clauses).

rearrange_clauses__(Input_clauses,lr,New_input_clauses):-
    reverse_literals_in_clauses__(Input_clauses,New_input_clauses).

rearrange_clauses__(Input_clauses,cr,New_input_clauses):-
    fast_reverse_list__(Input_clauses,[],New_input_clauses).

rearrange_clauses__(Input_clauses,clr,New_input_clauses):-
    fast_reverse_list__(Input_clauses,[],Reversed_input_clauses),
    reverse_literals_in_clauses__(Reversed_input_clauses,
New_input_clauses).
%----------------------------------------------------------------------
%----Supply comment character for various conversions
format_comment_character__(tptp,'%').

format_comment_character__(otter(_,_),'%').

format_comment_character__(setheo,'#').

format_comment_character__(mgtp,'%').

format_comment_character__(pttp,'%').

format_comment_character__(sprfn,'%').
%----------------------------------------------------------------------
%----Supply preferred extensions for various conversions
format_extension__(tptp,tptp).

format_extension__(otter(_,_),in).

format_extension__(setheo,lop).

format_extension__(mgtp,mgtp).

format_extension__(pttp,pttp).

format_extension__(sprfn,sprfn).
%----------------------------------------------------------------------
%----Supply the arrangement variant extension
arrangement_extension__(none,'').

arrangement_extension__(lr,'-lr').

arrangement_extension__(cr,'-cr').

arrangement_extension__(clr,'-clr').
%----------------------------------------------------------------------
read_line_as_list__(10,[]):-
    !.

read_line_as_list__(Last_character,[Last_character|Rest_of_line]):-
    get0(Next_character),
    read_line_as_list__(Next_character,Rest_of_line).

read_line__(Line):-
    get0(First_character),
    read_line_as_list__(First_character,Line_as_list),
    name(Line,Line_as_list).
%----------------------------------------------------------------------
%----Check if this is a comment line
comment_line__(Line):-
    name(Line,[37,45,45,45,45,45,45,45,45|_]).
%----------------------------------------------------------------------
%----Reset the first character of the line, if not empty
convert_comment_character__('',_,''):-
    !.

convert_comment_character__(Line,Comment_ascii,Translated_line):-
    name(Line,[_|Rest_of_line_list]),
    name(Translated_line,[Comment_ascii|Rest_of_line_list]).
%----------------------------------------------------------------------
%----Keep translating until a full comment line is reached
translate_until_comment_line__(Last_line,_):-
    comment_line__(Last_line),
    !.

translate_until_comment_line__(_,Comment_ascii):-
    read_line__(Line),
    convert_comment_character__(Line,Comment_ascii,Translated_line),
    write(Translated_line),
    nl,
    translate_until_comment_line__(Line,Comment_ascii).
%----------------------------------------------------------------------
%----Read and echo a tptp header, converting the comment character to 
%----that supplied
translate_tptp_header__(Comment_atom):-
    name(Comment_atom,[Comment_ascii]),
%----Get the first line and check it is a comment line
    read_line__(Line),
    comment_line__(Line),
    !,
    convert_comment_character__(Line,Comment_ascii,Translated_line),
    write(Translated_line),
    nl,
    translate_until_comment_line__(dummy_line,Comment_ascii).
    
translate_tptp_header__(_).
%----------------------------------------------------------------------
%----Call the required output formatter, according to argument.
output_clauses_in_format__(tptp,Input_clauses):-
    output_tptp_clauses__(Input_clauses).

output_clauses_in_format__(mgtp,Input_clauses):-
    output_mgtp_clauses__(Input_clauses).

output_clauses_in_format__(pttp,Input_clauses):-
    output_pttp_clauses__(Input_clauses).

output_clauses_in_format__(otter(SoS,Inference_rules),Input_clauses):-
    output_otter_clauses__(Input_clauses,SoS,Inference_rules).

output_clauses_in_format__(sprfn,Input_clauses):-
    output_sprfn_clauses__(Input_clauses).

output_clauses_in_format__(setheo,Input_clauses):-
    output_setheo_clauses__(Input_clauses).
%----------------------------------------------------------------------
%----Write a comment line
output_comment_line__(Comment_atom):-
    write(Comment_atom),
    write('-------------------------------------'),
    write('---------------------------------'),
    nl.
%----------------------------------------------------------------------
%----Output the clauses to file in the specified format
output_clauses_to_file_for_each_arrangement__(_,[],_,_,_):-
    !.

output_clauses_to_file_for_each_arrangement__(Format,
[First_arrangement|Rest_of_arrangements],Input_clauses,TPTP_file_name,
Base_output_file_name):-
%----Rearrange the clause as requested
    rearrange_clauses__(Input_clauses,First_arrangement,
New_input_clauses),
%----Create the output file name
    format_extension__(Format,Format_extension),
    arrangement_extension__(First_arrangement,Arrangement_extension),
    concatenate_atoms__([Base_output_file_name,Arrangement_extension,
'.',Format_extension],Output_file_name),
%----Redirect output
    telling(Current_output),
    tell(Output_file_name),
%----Convert the header field across
    format_comment_character__(Format,Comment_atom),
    seeing(Current_input),
    tptp_path_name__(TPTP_file_name,TPTP_path_name),
    see(TPTP_path_name),
    translate_tptp_header__(Comment_atom),
    seen,
    see(Current_input),
%----Output the clause in the required format
    output_clauses_in_format__(Format,New_input_clauses),
%----Put a comment line
    output_comment_line__(Comment_atom),
%----Restore output direction
    told,
    tell(Current_output),
%----Do rest of arrangments
    output_clauses_to_file_for_each_arrangement__(Format,
Rest_of_arrangements,Input_clauses,TPTP_file_name,Base_output_file_name).
%---------------------------------------------------------------------
%----The entry point to convert a TPTP file to other formats
tptp2X(TPTP_file_name,Format,Arrangements,Output_directory,Shorten):-
%----These operators are used in the TPTP. They must be declared here
%----so that they are declared at run, rather than compile time. If 
%----they are only done as :-op(100,fx,++)., then compiled versions of 
%----this code will not work
    op(100,fx,++),
    op(100,fx,--),
%----Read in the clauses
    read_input_clauses_from_file__(TPTP_file_name,Input_clauses,_,
Dictionary),
%----If shorten is defined, then shorten rather than make meaningful
    (Shorten == shorten ->
        shorten_clauses__(Input_clauses,New_input_clauses);
        (instantiate_variables_from_dictionary__(Dictionary),
            New_input_clauses = Input_clauses)),
%----Make the new file name
    basename__(TPTP_file_name,'.p',Basename),
    concatenate_atoms__([Output_directory,'/',Basename],
Base_output_file_name),
    output_clauses_to_file_for_each_arrangement__(Format,Arrangements,
New_input_clauses,TPTP_file_name,Base_output_file_name).

tptp2X:-
    write('Enter TPTP file name         : '),
    read(TPTP_file_name),
    write('Available formats are setheo, mgtp, pttp, tptp, otter(<sos>,<inference rules>),
    where <sos> is one of theorem, hypothesis, positive, negative, unit,
    and <inference rules> is a list of Otter inference rules.'),
    nl,
    write('Enter format                 : '),
    read(Format),
    write('Available arrangements are none, lr, cr, clr'),
    nl,
    write('Enter a list of arrangements : '),
    read(Arrangements),
    write('Enter output directory       : '),
    read(Output_directory),
    write('Enter "shorten" to do so     : '),
    read(Shorten),
    tptp2X(TPTP_file_name,Format,Arrangements,Output_directory,Shorten).
%---------------------------------------------------------------------
