#!/bin/csh
#----A shell script for starting Prolog and doing TPTP2X conversions.
#----tptp2X must be configured before using this.

#----Check arguments
if ($#argv >= 1 && $1 != meteor && $1 != mgtp && $1 != otter && $1 != pttp && $1 != setheo && $1 != sprfn && $1 != tptp) then
    echo " "
    echo "The single argument must be one of :"
    echo "    meteor, mgtp, otter, pttp, setheo, sprfn, tptp"
    echo " "
    exit
    endif

#----Get directories information
echo -n "Absolute name of TPTP2X directory      : "
set TPTP2XDirectory=$<

#----Check that tptp2X.config exists (rough check of the directory)
if (!(-f $TPTP2XDirectory/tptp2X.config)) then
    echo " "
    echo "Cannot find the tptp2X.config file there."
    echo " "
    exit
    endif

#----Check that ReadMe exists for help
if (!(-f $TPTP2XDirectory/ReadMe)) then
    echo " "
    echo "Cannot find the ReadMe file there."
    echo " "
    exit
    endif

#----Get the TPTP directory from tptpread
set PrologFact=`grep "^tptp_directory(" $TPTP2XDirectory/tptp2X.config`
set TPTPDirectory=`expr match $PrologFact "tptp_directory('\(.*\)'). *"`

#----Check that the Problems directory is there
if (!(-d $TPTPDirectory/Problems)) then
    echo " "
    echo "Cannot find the Problems directory."
    echo "Check the tptp_directory fact in tptp2X.config"
    echo " "
    exit
    endif

#----Get Prolog name
echo -n "Name of your Prolog interpreter        : "
set PrologInterpreter=$<

#----Check that it can be found
set PrologExecutable=`which $PrologInterpreter`
#----Have to do this in two steps so -x check lives
if ($#PrologExecutable != 1) then
    set PrologExecutable=very_unlikely_file_name
    endif
if (!(-x $PrologExecutable)) then
    echo " "
    echo "Cannot find Prolog executable."
    echo " "
    exit
    endif

#----Check for bulk conversion
if ($#argv >= 1) then
    set FilesToConvert='*/*'
#----Special case for Otter
    if ($1 == otter) then
        set Transformations='equality([s,t,f,p])'
        set FormatToConvertTo='otter(none,[set(auto)])'
    else
        set Transformations=none
        set FormatToConvertTo=$1
        endif
    set OutputDirectory=$TPTPDirectory/$1
else
#----Get the required information from the user
    echo    "Names of files to convert, relative to $TPTPDirectory/Problems "
    echo -n "    (e.g., S??/*)                      : "
    set FilesToConvert=$<
    sed -n -e '/^+ <Transformation>/,/^+ <Format>/p' $TPTP2XDirectory/ReadMe | sed -e '$d'
    echo    "Tranformations to apply"
    echo -n "    (e.g., none, or [clr,magic])       : "
    set Transformations=$<
    sed -n -e '/^+ <Format>/,/^+ <Output directory>/p' $TPTP2XDirectory/ReadMe | sed -e '$d'
    echo    "Formats to convert to "
    echo -n "    (e.g., setheo)                     : "
    set FormatToConvertTo=$<
    echo    "Absolute name of output directory"
    echo -n "    (e.g., ~/ATP/TPTPProblems)         : "
    set OutputDirectory=$<
    endif

#----Ensure that the output directory exists
set HigherDirectory=$OutputDirectory
set ToMake=
@ ToMakeIndex=0
#----Find a higher directory that exists
while ((!(-d $HigherDirectory)) && ($HigherDirectory != ""))
    @ ToMakeIndex++
    set ToMake=($ToMake `basename $HigherDirectory`)
    set HigherDirectory=`dirname $HigherDirectory`
    end
cd $HigherDirectory
#----Make all the subdirectories
while ($ToMakeIndex > 0)
    mkdir $ToMake[$ToMakeIndex]
    cd $ToMake[$ToMakeIndex]
    @ ToMakeIndex--
#----Tell user if directories have been made
    if ($ToMakeIndex == 0) then
        echo Made the directory $OutputDirectory
        endif
    end

# echo "TPTP2X directory      = $TPTP2XDirectory"
# echo "TPTP directory        = $TPTPDirectory"
# echo "Prolog interpreter    = $PrologInterpreter"
# echo "Files to convert      = $FilesToConvert"
# echo "Transformations       = $Transformations"
# echo "Format to convert to  = $FormatToConvertTo"
# echo "Output directory      = $OutputDirectory"

#----Make an input file for Prolog
echo "Preparing Prolog input script"
echo "compile(tptp2X)." >$TPTPDirectory/PrologScript
cd $TPTPDirectory/Problems
#----Separate the domains so that foreach copes
set DomainPart=`expr match "$FilesToConvert" "\(.*\)\/.*"`
foreach Domain ($DomainPart)
#----Make the domain directory if it does not exist
    if (!(-d $OutputDirectory/$Domain)) then
        echo Made the directory $OutputDirectory/$Domain
        mkdir $OutputDirectory/$Domain
        endif
#----Look for the files from this directory
    cd $TPTPDirectory/Problems/$Domain
    set FilePart=`expr match "$FilesToConvert" ".*\/\(.*\)"`
    foreach File ($FilePart)
#----Check that it's a .p, .ax or .eq file
        set Suffix=`expr match "$File" ".*\.\(.*\)"`
        if ($Suffix == "p" || $Suffix == "ax" || Suffix == "eq") then
            echo "tptp2X('$TPTPDirectory/Problems/$Domain/$File',$Transformations,$FormatToConvertTo,'$OutputDirectory/$Domain')." >>$TPTPDirectory/PrologScript
        else
            echo "$File ignored (not a clause file)"
            endif
        end
    end
echo "halt." >>$TPTPDirectory/PrologScript

#----Invoke the Prolog interpreter with this input
echo "Invoking Prolog"
cd $TPTP2XDirectory
$PrologInterpreter <$TPTPDirectory/PrologScript

#----Delete script file
rm $TPTPDirectory/PrologScript
