#!/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

#----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 for bulk conversion
if ($#argv >= 1) then
    set FilesToConvert='*/*'
    set Transformations=none
#----Special case for Otter
    if ($1 == otter) then
        set FormatToConvertTo='otter(none,[set(auto)])'
    else
        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=$<
    echo    "Tranformations to apply"
    echo -n "    (e.g., none, or [clr,magic])       : "
    set Transformations=$<
    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)
        echo "tptp2X('$TPTPDirectory/Problems/$Domain/$File',$Transformations,$FormatToConvertTo,'$OutputDirectory/$Domain')." >>$TPTPDirectory/PrologScript
        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
