%======================================================================
%----The tptp2X  utility is used  to make transformations on the 
%----clauses in TPTP problem, and to output the clauses in formats 
%----accepted  by existing ATP systems. See the associated ReadMe
%----file for details.
%----
%----Written by Geoff Sutcliffe, July 1992.
%----Updated by Geoff Sutcliffe, November 1992.
%----Updated by Geoff Sutcliffe, March 1993.
%----Revised by Geoff Sutcliffe, January, 1994.
%----Updated by Geoff Sutcliffe, April, 1994.
%----Revised by Geoff Sutcliffe, May 1994, with ideas from
%----    Gerd Neugebauer
%======================================================================
%----------------------------------------------------------------------
%----These are used in the TPTP and need to exist before the 
%----transformations and formats are loaded. They are also declared at 
%----runtime in tptp2X/4.
:-op(100,fx,++).
:-op(100,fx,--).
%----------------------------------------------------------------------
%----Here's how files get loaded into Prolog. Fix this if your dialect
%----does not use compile/1 (quite possible, as compile/1 is only a
%----de facto standard). 
tptp2X_load(FileName):-
    compile(FileName).
%----------------------------------------------------------------------
%----tptp2X_module loads transformations and formats. It has an extra
%----argument in which the transformations and formats are specified.
%----At the moment the 2nd argument is not used, but XTPTP uses it from
%----tptp2X.config.
tptp2X_module(FileName,_):-
    tptp2X_load(FileName).
%----------------------------------------------------------------------
%----Load the configuration file
:-tptp2X_load('tptp2X.config').
%----Use the standard TPTP read code. 
:-tptp2X_load(tptpread).
%----------------------------------------------------------------------
%----Simple append, required in tptpread. Renamed to avoid confusion 
%----with builtins.
tptp_append([],List,List).

tptp_append([Head|Tail],List,[Head|TailList]):-
    tptp_append(Tail,List,TailList).
%----------------------------------------------------------------------
%----Simple select. Renamed to avoid confusion with builtins.
tptp_select(Element,[Element|Tail],Tail).

tptp_select(Element,[Head|Tail],[Head|SelectedTail]):-
    tptp_select(Element,Tail,SelectedTail).
%----------------------------------------------------------------------
%----Select the Nth element.
tptp_select_Nth(Element,[Element|Tail],1,Tail).

tptp_select_Nth(Element,[Head|Tail],N,[Head|SelectedTail]):-
    N > 1,
    NewN is N - 1,
    tptp_select_Nth(Element,Tail,NewN,SelectedTail).
%----------------------------------------------------------------------
%----Simple member. Renamed to avoid confusion with builtins.
tptp_member(Element,[Element|_]).

tptp_member(Element,[_|Tail]):-
    tptp_member(Element,Tail).
%----------------------------------------------------------------------
%----Simple length. Renamed to avoid confusion with builtins.
tptp_length([],0).

tptp_length([_|Tail],Length):-
    tptp_length(Tail,TailLength),
    Length is TailLength + 1.
%----------------------------------------------------------------------
%----Remove all elements upto the last delimiter
list_tail([],_,[],not_found):-
    !.
    
%----Check if the delimiter is further down the list
list_tail([_|ListTail],Delimiter,TailTail,found):-
    list_tail(ListTail,Delimiter,TailTail,found),
    !.

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

%----Otherwise pass back this list
list_tail(List,_,List,not_found).
%----------------------------------------------------------------------
%----Generating random integers in a given range
%----Generic version - Integers in range 0 to 4095 (may not be adequate
%----for all uses).
tptp_random_integer_for_dialect(generic,Lowest,Highest,Random):-
%----Seed already saved, use it.
    retract(seed(BigRandom)),
    !,
    NewSeed is (125 * BigRandom + 1) mod 4096,
    asserta(seed(NewSeed)),
    Random is Lowest + (BigRandom mod (Highest - Lowest + 1)).

%----First time - make seed from Lowest and Highest
tptp_random_integer_for_dialect(generic,Lowest,Highest,Random):-
    Seed is Highest - Lowest,
    asserta(seed(Seed)),
    tptp_random_integer_for_dialect(generic,Lowest,Highest,Random).

%----BinProlog version
tptp_random_integer_for_dialect(binprolog,Lowest,Highest,Random):-
%----Integer in some range (not in manual)
    random(BigRandom),
    Random is Lowest + (BigRandom mod (Highest - Lowest + 1)).

%----SICStus 0.7 version - Use generic
tptp_random_integer_for_dialect(sicstus07,Lowest,Highest,Random):-
    tptp_random_integer_for_dialect(generic,Lowest,Highest,Random).

%----SICStus 2.1 version.
tptp_random_integer_for_dialect(sicstus21,Lowest,Highest,Random):-
    use_module(library(random)),
    HighestPlus1 is Highest + 1,
    random(Lowest,HighestPlus1,Random).

%----Eclipse version
tptp_random_integer_for_dialect(eclipse,Lowest,Highest,Random):-
%----Integer in range 0 to (2^32 - 1)
    random(BigRandom),
    Random is Lowest + (BigRandom mod (Highest - Lowest + 1)).

%----Quintus version - Integer in specified range
tptp_random_integer_for_dialect(quintus,Lowest,Highest,Random):-
    use_module(library(random)),
    HighestPlus1 is Highest + 1,
    random(Lowest,HighestPlus1,Random).

tptp_random_integer(Lowest,Highest,Random):-
    prolog_dialect(Dialect),
    tptp_random_integer_for_dialect(Dialect,Lowest,Highest,Random).
%----------------------------------------------------------------------
%----Clauses to the same as the UNIX basename command
basename(FullName,Suffix,Basename):-
    name(FullName,FullNameList),
    name(Suffix,SuffixList),
%----Delete upto last / (ASCII 47)
    list_tail(FullNameList,47,FullNameTailList,_),
%----Try to delete suffix from list
    (tptp_append(BasenameList,SuffixList,FullNameTailList) ->
        name(Basename,BasenameList);
%----If not possible, then ignore the suffix
        name(Basename,FullNameTailList)).
%----------------------------------------------------------------------
%----Clauses the same as the UNIX dirname command
dirname(FullName,Dirname):-
    name(FullName,FullNameList),
%----Remove the basename
    basename(FullName,'',Basename),
    name(Basename,BasenameList),
%----Find what is before the basename, if anything
    (tptp_append(DirnameList,[47|BasenameList],FullNameList) ->
        name(Dirname,DirnameList);
%----If no directory then it's the current one
        Dirname = '.').
%----------------------------------------------------------------------
%-----Convert from an integer to a list of characters
integer_name(Integer,FinalString):-
    integer_name(Integer,[],FinalString).

integer_name(Integer,StringSoFar,[Character|StringSoFar]):-
    Integer < 10,
    !,
    Character is Integer + 48.

integer_name(Integer,StringSoFar,FinalString):-
    TopHalf is Integer // 10,
    BottomHalf is Integer mod 10,
    Character is BottomHalf + 48,
    integer_name(TopHalf,[Character|StringSoFar],FinalString).
%----------------------------------------------------------------------
%----Do name for atoms and integers
any_name(Atom,AtomList):-
    atom(Atom),
    !,
    name(Atom,AtomList).

any_name(Integer,IntegerList):-
    integer(Integer),
    integer_name(Integer,IntegerList).
%----------------------------------------------------------------------
%----Concatenate a list of atoms into a list of the ASCII
concatenate_atoms_to_list([],[]):-
    !.

concatenate_atoms_to_list([FirstTerm|RestOfTerms],TermsList):-
    any_name(FirstTerm,FirstList),
    concatenate_atoms_to_list(RestOfTerms,RestList),
    tptp_append(FirstList,RestList,TermsList).
%----------------------------------------------------------------------
%----Concatenate a list of terms into a big atom
concatenate_atoms(Atoms,Atom):-
    concatenate_atoms_to_list(Atoms,AtomsList),
    name(Atom,AtomsList).
%----------------------------------------------------------------------
%-----Fast reverse a list
fast_reverse_list([],ReverseList,ReverseList):-
    !.

fast_reverse_list([Head|Tail],ReverseSoFar,ReverseList):-
    fast_reverse_list(Tail,[Head|ReverseSoFar],ReverseList).
%----------------------------------------------------------------------
read_line_as_list(10,[]):-
    !.

read_line_as_list(LastCharacter,[LastCharacter|RestOfLine]):-
    get0(NextCharacter),
    read_line_as_list(NextCharacter,RestOfLine).

read_line(Line):-
    get0(FirstCharacter),
    read_line_as_list(FirstCharacter,LineAsList),
    name(Line,LineAsList).
%----------------------------------------------------------------------
%----Check if this is a comment line
comment_line(Line):-
    name(Line,[37,45,45,45,45,45,45,45,45|_]).
%----------------------------------------------------------------------
%----Keep reading until
read_until_comment_line(HeaderLine,[]):-
    comment_line(HeaderLine),
    !.

read_until_comment_line(TPTPLine,[Line|RestOfHeaderLines]):-
%----Remove TPTP comment character, if any
    (name(TPTPLine,[37|RestOfAscii]) ->
        name(Line,RestOfAscii);
        Line = TPTPLine),
%----Read next line
    read_line(NextLine),
    read_until_comment_line(NextLine,RestOfHeaderLines).
%----------------------------------------------------------------------
%----Read lines between two comment lines
read_header_lines(FileHeader):-
%----Get the first line and check it is a comment line
    read_line(FirstHeaderLine),
    comment_line(FirstHeaderLine),
    !,
    read_line(Line),
    read_until_comment_line(Line,FileHeader).
    
%----If the first line is not a comment then return nothing
read_header_lines([]).
%----------------------------------------------------------------------
%----Read the header from a TPTP file, one line at a time
read_input_file_header(TPTPFileName,FileHeader):-
    tptp_path_name(TPTPFileName,TPTPPathName),
%----Redirect input
    seeing(CurrentInput),
    see(TPTPPathName),
    read_header_lines(FileHeader),
%----Reset input to old input
    seen,
    see(CurrentInput).
%---------------------------------------------------------------------
%----Write a comment line
output_comment_line(CommentAtom):-
    write(CommentAtom),
    write('-------------------------------------'),
    write('-------------------------------------'),
    nl.
%----------------------------------------------------------------------
%----Output the file header using the given comment atom
output_file_header([],_):-
    !.

output_file_header([FirstHeaderLine|RestOfHeaderLines],CommentAtom):-
    write(CommentAtom),
    write(FirstHeaderLine),
    nl,
    output_file_header(RestOfHeaderLines,CommentAtom).
%----------------------------------------------------------------------
%----Make the output file name
%----If the output directory is user, then output to stdout
make_output_file_name(user,_,_,user):-
    !.

make_output_file_name(OutputDirectory,OutputName,FileNameExtension,
OutputFileName):-
    concatenate_atoms([OutputDirectory,'/',OutputName,FileNameExtension],
OutputFileName).
%----------------------------------------------------------------------
%----Allow mulitple output formats (useful for the competition)
output_clauses_in_format(_,_,[],_,_):-
    !.

output_clauses_in_format(FileHEader,OutputClauses,[FirstFormat|
RestOfFormats],OutputName,OutputDirectory):-
    !,
    output_clauses_in_format(FileHEader,OutputClauses,FirstFormat,
OutputName,OutputDirectory),
    output_clauses_in_format(FileHEader,OutputClauses,RestOfFormats,
OutputName,OutputDirectory).

%----Format the clauses and write to file
output_clauses_in_format(FileHeader,OutputClauses,OutputFormat,
OutputName,OutputDirectory):-
%----Extract the main name of the output format
    OutputFormat =.. [FormatName|_],
%----Get the file name extension (don't like this yet)
    concatenate_atoms([FormatName,'_format_information'],
ExtensionQueryPredicate),
    ExtensionQuery =.. [ExtensionQueryPredicate,FileNameExtension,
CommentAtom],
    ExtensionQuery,
%----Make the output file name
    make_output_file_name(OutputDirectory,OutputName,FileNameExtension,
OutputFileName),
%----Make the output query
    Query =.. [FormatName,OutputClauses,OutputFormat],
%----Redirect the output
    telling(CurrentOutput),
    tell(OutputFileName),
%----Output the file header
    output_comment_line(CommentAtom),
    output_file_header(FileHeader,CommentAtom),
    output_comment_line(CommentAtom),
%----Output the clauses in the required format
    Query,
%----Put a comment line
    output_comment_line(CommentAtom),
%----Restore output direction
    told,
    tell(CurrentOutput).
%---------------------------------------------------------------------
%----Control of a single transformation, including output.
do_transformation(InputClauses,InputName,Dictionary,Transformation,
OutputClauses,OutputName,NewDictionary):-
%----Extract the main name of the transformation
    Transformation =.. [TransformationName|_],
    Query =.. [TransformationName,InputClauses,Dictionary,
Transformation,OutputClauses,NewDictionary,TransformationSuffix],
    Query,
    !,
    concatenate_atoms([InputName,TransformationSuffix],OutputName).

do_transformation(_,_,_,Transformation,_,_,_):-
    write('The tranformation '),
    write(Transformation),
    write(' failed'),
    nl,
    fail.
%---------------------------------------------------------------------
%----Do one transformation that is a sequence in the transformations
%----list.
%----When no more transformation to do, then copy to output
transform_clauses(Clauses,Name,Dictionary,[],Clauses,Name,
Dictionary):-
    !.
    
%----If a list of transformations, then do each one. Use member due
%----to backtracking approach
transform_clauses(InputClauses,InputName,Dictionary,
[[OneTransformation|OtherTransformations]|RestOfTransformations],
OutputClauses,OutputName,NewDictionary):-
    !,
    tptp_member(Transformation,[OneTransformation|OtherTransformations]),
    do_transformation(InputClauses,InputName,Dictionary,
Transformation,IntermediateClauses,IntermediateName,
IntermediateDictionary),
    transform_clauses(IntermediateClauses,IntermediateName,
IntermediateDictionary,RestOfTransformations,OutputClauses,
OutputName,NewDictionary).

%----If a definite transformation, then do it
transform_clauses(InputClauses,InputName,Dictionary,[Transformation|
RestOfTransformations],OutputClauses,OutputName,NewDictionary):-
    !,
    do_transformation(InputClauses,InputName,Dictionary,
Transformation,IntermediateClauses,IntermediateName,
IntermediateDictionary),
    transform_clauses(IntermediateClauses,IntermediateName,
IntermediateDictionary,RestOfTransformations,OutputClauses,OutputName,
NewDictionary).

%----If a single transformation, then do it
transform_clauses(InputClauses,InputName,Dictionary,Transformation,
OutputClauses,OutputName,NewDictionary):-
    do_transformation(InputClauses,InputName,Dictionary,
Transformation,OutputClauses,OutputName,NewDictionary).
%---------------------------------------------------------------------
%----Do a transformation by combination from the transformation list.
%----Done by backtracking over the transformations.
do_all_transformations_and_output(InputClauses,BaseInputName,
Transformations,FileHeader,OutputFormat,OutputDirectory,Dictionary):-
    write(Transformations),
    write('...'),
    transform_clauses(InputClauses,BaseInputName,Dictionary,
Transformations,OutputClauses,BaseOutputName,NewDictionary),
    instantiate_variables_from_dictionary(NewDictionary),
    write(OutputFormat),
    write('...'),
    output_clauses_in_format(FileHeader,OutputClauses,OutputFormat,
BaseOutputName,OutputDirectory),
    write('Done'),
    nl,
    fail.

%----Succeed when all transformation have been backtracked over
do_all_transformations_and_output(_,_,_,_,_,_,_).
%---------------------------------------------------------------------
%----The entry point to convert a TPTP file to other formats
tptp2X(TPTPFileName,Transformations,OutputFormat,OutputDirectory):-
%----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,--),
%----Extract the base file name
    basename(TPTPFileName,'.p',BaseInputName),
    write(BaseInputName),
    write('...'),
%----Read in the file header
    read_input_file_header(TPTPFileName,FileHeader),
%----Read in the clauses
    read_input_clauses_from_file(TPTPFileName,InputClauses,_,
Dictionary),
%----Do each transformation and output the clauses in the required
%----format. 
    do_all_transformations_and_output(InputClauses,BaseInputName,
Transformations,FileHeader,OutputFormat,OutputDirectory,Dictionary).

%----tptp2X interactive with help. Notice that the help messages are broken
%----into small bits, to tolerate those Prolog dialects that have limit
%----atom lengths.
tptp2X:-
    tptp2X_help("+ <TPTP file>","+ <Transformation>"),
    write('Enter TPTP file name         : '),
    read(TPTPFileName),
    tptp2X_help("+ <Transformation>","+ <Format>"),
    write('Enter transformations list   : '),
    read(Transformations),
    tptp2X_help("+ <Format>","+ <Output directory>"),
    write('Enter output format          : '),
    read(OutputFormat),
    tptp2X_help("+ <Output directory>","    "),
    write('Enter output directory       : '),
    read(OutputDirectory),
    tptp2X(TPTPFileName,Transformations,OutputFormat,OutputDirectory).
%---------------------------------------------------------------------
%----Get help from the ReadMe file
tptp2X_help(FirstLineAsciiPrefix,LastLineAsciiPrefix):-
    tptp2X_directory(TPTP2XDirectory),
    concatenate_atoms([TPTP2XDirectory,'/','ReadMe'],ReadMeFile),
    seeing(OldInput),
%----Close the file in case it got left open somehow
    see(ReadMeFile),
    seen,
    see(ReadMeFile),
    !,
%----Read until first line is found (lucky read doen't backtrack!)
    repeat,
        read_line(FirstLine),
        name(FirstLine,FirstLineAscii),
        tptp_append(FirstLineAsciiPrefix,_,FirstLineAscii),
%----Write the first line
    write(FirstLine),
    nl,
%----Read and write all other lines
    repeat,
        read_line(NextLine),
        name(NextLine,NextLineAscii),
        (tptp_append(LastLineAsciiPrefix,_,NextLineAscii) ->
            true;
            (
                write(NextLine),
                nl,
                fail)),
%----Close the file
    seen,
    see(OldInput).

tptp2X_help(_,_):-
    write('Cannot open ReadMe file to get help'),
    nl.
%---------------------------------------------------------------------
%----Execute the tptp2X/0 entry point, then quite
execute_tptp2X:-
    tptp2X,
    halt.
%---------------------------------------------------------------------
%----Make an interactive executable
%----There is no generic version, but the SICStus version is common
make_tptp2X_interactive_for_dialect(generic):-
    write('Interactive tptp2X cannot be made for generic Prolog'),
    nl.

%----BinProlog version
make_tptp2X_interactive_for_dialect(binprolog):-
    write('Interactive tptp2X cannot be made for BinProlog'),
    nl.
%----Still some problems with this
%    binprolog(BinPrologExecutable),
%    make_executable_unix_appl(BinPrologExecutable,tptp2X,tptp2X_interactive).

%----SICStus 0.7 version
make_tptp2X_interactive_for_dialect(sicstus07):-
    write('Interactive tptp2X cannot be made for SICStus 0.7 Prolog'),
    nl.

%----SICStus 2.1 version.
make_tptp2X_interactive_for_dialect(sicstus21):-
    nofileerrors,
    save(tptp2X_interactive),
    execute_tptp2X.

%----Eclipse version
make_tptp2X_interactive_for_dialect(eclipse):-
    nofileerrors,
    save(tptp2X_interactive),
    execute_tptp2X.

%----Quintus version
make_tptp2X_interactive_for_dialect(quintus):-
    save_program(tptp2X_interactive,execute_tptp2X).

%----Redirect the interactive making according to dialect
make_tptp2X_interactive:-
    prolog_dialect(Dialect),
    !,
    make_tptp2X_interactive_for_dialect(Dialect).

make_tptp2X_interactive:-
    write('No Prolog dialect installed, interactive not made'),
    nl,
    fail.
%---------------------------------------------------------------------
%----Get the Transformations and output format from tptp2Xrc file
%----First look locally
get_transformation_and_output_directory(Transformations,OutputFormat):-
    see(tptp2Xrc),
    read(Transformations),
    read(OutputFormat),
    seen,
    !.
    
%----Second look in tptp2X directory
get_transformation_and_output_directory(Transformations,OutputFormat):-
    tptp_path_name('TPTP2X/tptp2Xrc',PathName),
    see(PathName),
    read(Transformations),
    read(OutputFormat),
    seen,
    !.

%----Default is TPTP format with no transformation
get_transformation_and_output_directory([],tptp).
%---------------------------------------------------------------------
%----This executes tptp2X as a filter, with the tptp2Xrc file
execute_filter:-
    get_transformation_and_output_directory(Transformations,
OutputFormat),
    tptp2X(user,Transformations,OutputFormat,user),
    halt.
%---------------------------------------------------------------------
%----Make a saved state filter.
%----There is no generic version, but the SICStus version is common
make_tptp2X_filter_for_dialect(generic):-
    write('The filter cannot be made for generic Prolog'),
    nl.

%----BinProlog version
make_tptp2X_filter_for_dialect(binprolog):-
    write('The filter cannot be made for BinProlog'),
    nl.
%----Still some problems with this
%    binprolog(BinPrologExecutable),
%    make_executable_unix_appl(BinPrologExecutable,tptp2X,tptp2X_filter).

%----SICStus 0.7 version
make_tptp2X_filter_for_dialect(sicstus07):-
    write('The filter cannot be made for SICStus 0.7 Prolog'),
    nl.

%----SICStus 2.1 version.
make_tptp2X_filter_for_dialect(sicstus21):-
    nofileerrors,
    save(tptp2X_filter),
    execute_filter.

%----Eclipse version
make_tptp2X_filter_for_dialect(eclipse):-
    nofileerrors,
    save(tptp2X_filter),
    execute_filter.

%----Quintus version
make_tptp2X_filter_for_dialect(quintus):-
    save_program(tptp2X_filter,execute_filter).

%----Redirect the filter making according to dialect
make_tptp2X_filter:-
    prolog_dialect(Dialect),
    !,
    make_tptp2X_filter_for_dialect(Dialect).

make_tptp2X_filter:-
    write('No Prolog dialect installed, filter not made'),
    nl,
    fail.
%---------------------------------------------------------------------
