#!/bin/csh
#--------------------------------------------------------------------------
clear
echo "--------------------------------------------------------------------"
echo "                This is the tptp2X installation"
echo ""
echo "Press return to accept the default values in []s"
echo "--------------------------------------------------------------------"
#--------------------------------------------------------------------------
#----TPTP directory
#----Look for being in or below TPTP-v*
set TPTPDirectory=`expr match "$cwd" "\(.*TPTP-v[0-9\.]*\).*"`
#----Look for being below TPTP (for me)
if ("$TPTPDirectory" == "") then
    set TPTPDirectory=`expr match "$cwd" "\(.*TPTP\)\/.*"`
    endif
#----Look for being in TPTP (for me)
if ("$TPTPDirectory" == "") then
    set TPTPDirectory=`expr match "$cwd" "\(.*TPTP\)"`
    endif
#----Look for being above TPTP-v* (for installation)
if ("$TPTPDirectory" == "") then
    set LSOutput=`ls -d TPTP-v?.?.?`
    if ("$LSOutput" != "" && (-d "$LSOutput")) then
        set TPTPDirectory="$cwd/"`expr match "$LSOutput" "\(.*TPTP-v[0-9\.]*\).*"`
        endif
    endif

#----Now ask the user
set LegalResponse=no
echo "The TPTP directory must contain the TPTP2X directory."
while ($LegalResponse != yes)
    echo -n "TPTP directory        [$TPTPDirectory] : "
    set Response=$<
    if ($Response == "") then
        set Response=$TPTPDirectory
        endif
#----Check for non empty response
    if ("$Response" != "") then
#----Check that the TPTP directory exists
        if (!(-d $Response)) then
            echo "Cannot find the TPTP directory."
            continue
            endif
        set TPTP2XDirectory=$Response/TPTP2X
#----Check that the TPTP2X directory exists
        if (!(-d $TPTP2XDirectory)) then
            echo "Cannot find the TPTP2X directory."
            continue
            endif
#----Check that tptp2X.config exists (rough check of the directory)
        if (!(-f $TPTP2XDirectory/tptp2X.config)) then
            echo "Cannot find the tptp2X.config file."
            continue
            endif
        set LegalResponse=yes
        set TPTPDirectory=$Response
        endif
    end
echo "--------------------------------------------------------------------"
#--------------------------------------------------------------------------
#----PrologDialect
#----Look for a reasonable default 
set PrologDialect=""
if ("`which sicstus`" =~ /*) then
    set PrologDialect=sicstus
else 
    if ("`which quintus`" =~ /*) then
        set PrologDialect=quintus
    else 
        if ("`which eclipse`" =~ /*) then
            set PrologDialect=eclipse
        else 
            if ("`which bp`" =~ /*) then
                set PrologDialect=binprolog
            else 
                set PrologDialect=generic
                endif
            endif
        endif
    endif
#----Check with the user
set LegalResponse=no
echo "The Prolog dialect must be one of :"
echo "    generic, binprolog, sicstus, quintus, eclipse"
while ($LegalResponse != yes)
    echo -n "Prolog dialect        [$PrologDialect] : "
    set Response=$<
    if ($Response == "") then
        set Response=$PrologDialect
        endif
    if (_generic_binprolog_sicstus_quintus_eclipse_ =~ *_${Response}_*) then
        set LegalResponse=yes
        set PrologDialect=$Response
    else
        echo $Response is not a valid Prolog dialect.
        endif
    end
echo "--------------------------------------------------------------------"
#--------------------------------------------------------------------------
#----PrologInterpreter
#----Look for a reasonable default executable
set PrologInterpreter=""
switch ($PrologDialect)
    case generic:
        set AbsolutePath=`which prolog`
        breaksw
    case binprolog:
        set AbsolutePath=`which bp`
        breaksw
    case sicstus:
        set AbsolutePath=`which sicstus`
        breaksw
    case quintus:
        set AbsolutePath=`which quintus`
        breaksw
    case eclipse
        set AbsolutePath=`which eclipse`
        breaksw
    endsw
#----Check that the Prolog interpreter can be found
    if ("$AbsolutePath" =~ /*) then
#----Found, use this as default
        set PrologInterpreter=$AbsolutePath
    else
#----Not found, no default
        set PrologInterpreter=""
        endif
set LegalResponse=no
echo "The Prolog interpreter must be an executable."
while ($LegalResponse != yes)
    echo -n "Prolog interpreter    [$PrologInterpreter] : "
    set Response=$<
    if ("$Response" == "") then
        set Response=$PrologInterpreter
        endif
#----An empty default is possible, so check that is was not taken
    if ("$Response" != "") then
#----Check that the Prolog interpreter can be found
        set AbsolutePath=`which $Response`
#----Have to do this in two steps so -x check lives
        if ("$AbsolutePath" !~ /*) then
            set AbsolutePath=very_unlikely_file_name
            endif
        if (-x $AbsolutePath) then
            set LegalResponse=yes
            set PrologInterpreter=$AbsolutePath
        else
            echo $Response does not lead to an executable.
            endif
        endif
    end
#----Set flags to keep things quiet, etc
switch ($PrologDialect)
    case generic:
        set PrologArguments=''
        breaksw
    case binprolog:
#----Larger heap (required for generators) and larger trail and larger
#----hash table (for doing many files in batch)
        set PrologArguments='-h15000 -t5000 -d20'
        breaksw
    case sicstus:
        set PrologArguments=''
        breaksw
    case quintus:
        set PrologArguments=''
        breaksw
    case eclipse
        set PrologArguments=''
        breaksw
    endsw
echo "--------------------------------------------------------------------"
#--------------------------------------------------------------------------
#----Shell
#----Check that the Prolog interpreter can be found
set Shell=tcsh
set AbsolutePath=`which $Shell`
#----If no default shell, use csh
if ("$AbsolutePath" !~ /*) then
    echo "         Your site does not appear to have the "$Shell" shell."
    echo "         -------------------------------------------------"
    echo "This means that the tptp2X script will not be able to  deal with very"
    echo "large numbers of files. In particular, it will not be able to convert"
    echo "all TPTP files to another format in one go.  You can convert a domain"
    echo "at a time.  See the  tptp2X section of  the TPTP technical report for"
    echo "details."
    echo ""
    echo "You should check with your system administrator to see if $Shell can be"
    echo "made available, after which you can reinstall tptp2X."
    echo "--------------------------------------------------------------------"
    set Shell=`which csh`
else
    set Shell=$AbsolutePath
    echo "tcsh shell path is $Shell"
    endif
echo "--------------------------------------------------------------------"
#--------------------------------------------------------------------------
#----Gawk/awk
#----Check that gawk or awk can be found
set GawkPath=`which gawk`
#----If no gawk look for awk
if ("$GawkPath" !~ /*) then
    set GawkPath=`which awk`
    if ("$GawkPath" !~ /*) then
        set GawkPath=""
        endif
    endif
set LegalResponse=no
echo "gawk or awk is required for quietness modes 1 and 2."
while ($LegalResponse != yes)
    echo -n "gawk or awk path      [$GawkPath] : "
    set Response=$<
    if ("$Response" == "") then
        set Response=$GawkPath
        endif
#----An empty default is possible, so check that is was not taken
    if ("$Response" != "") then
#----Check that gawk/awk can be found
        set AbsolutePath=`which $Response`
#----Have to do this in two steps so -x check lives
        if ("$AbsolutePath" !~ /*) then
            set AbsolutePath=very_unlikely_file_name
            endif
        if (-x $AbsolutePath) then
            set LegalResponse=yes
            set GawkPath=$AbsolutePath
        else
            echo $Response does not lead to an executable.
            endif
    else
#----Accept the empty string
        set LegalResponse=yes
        endif
    end
echo "--------------------------------------------------------------------"
#--------------------------------------------------------------------------
#----Install tptp2X.config: 
echo Installing tptp2X.config
#----Any line that starts not with % and has in it %%, stick % at the start.
#----Remove the leading % in lines that refer to the specific dialect.
#----Set the tptp_directory/1 fact
sed -e "/^[^\%].*\%\%.*/s/\(.*\)/% \1/" -e "/\%\%$PrologDialect/s/^\% //" -e "/\%\%$PrologDialect/s/^\%//" -e "/^tptp_directory/s?.*?tptp_directory('$TPTPDirectory').?" $TPTP2XDirectory/tptp2X.config >$TPTP2XDirectory/tptp2X.config.new

#----Move the new file into place
#mv $TPTP2XDirectory/tptp2X.config $TPTP2XDirectory/tptp2X.config.old
mv -f $TPTP2XDirectory/tptp2X.config.new $TPTP2XDirectory/tptp2X.config
#--------------------------------------------------------------------------
#----Install tptp2X.main
echo Installing tptp2X.main
#----Set all loading back to using []/1
sed -e "/:-compile(/s/compile(\(.*\))/[\1]/" $TPTP2XDirectory/tptp2X.main >$TPTP2XDirectory/tptp2X.main.consult
#----If a dialect that supports compile in a "normal" way (in the sense 
#----that it does a consult) then convert the [] loads to compiles.
if (_binprolog_sicstus_quintus_eclipse_ =~ *_${PrologDialect}_*) then
    sed -e "/:-\[/s/\[\(.*\)\]/compile(\1)/" $TPTP2XDirectory/tptp2X.main.consult >$TPTP2XDirectory/tptp2X.main.new
    rm -f $TPTP2XDirectory/tptp2X.main.consult
#    mv $TPTP2XDirectory/tptp2X.main $TPTP2XDirectory/tptp2X.main.old
    mv -f $TPTP2XDirectory/tptp2X.main.new $TPTP2XDirectory/tptp2X.main
else
    echo "It is unknown if $PrologDialect Prolog supports compile/1."
    echo "Source files will be loaded using []/1, in tptp2X.main"
#    mv $TPTP2XDirectory/tptp2X.main $TPTP2XDirectory/tptp2X.main.old
    mv -f $TPTP2XDirectory/tptp2X.main.consult $TPTP2XDirectory/tptp2X.main
    endif

#--------------------------------------------------------------------------
#----Install tptp2X: 
echo Installing tptp2X
#----Have to use ? as the separator as there are /s in the substitutions
sed -e "1s?.*?#\!$Shell?" -e "/set TPTPDirectory/s?.*?set TPTPDirectory=$TPTPDirectory?" -e "/set PrologInterpreter/s?.*?set PrologInterpreter='$PrologInterpreter'?" -e "/set PrologArguments/s/.*/set PrologArguments='$PrologArguments'/" -e "/set Gawk=/s?.*?set Gawk=$GawkPath?" $TPTP2XDirectory/tptp2X >$TPTP2XDirectory/tptp2X.new

#----Move the new file into place
#mv $TPTP2XDirectory/tptp2X $TPTP2XDirectory/tptp2X.old
mv -f $TPTP2XDirectory/tptp2X.new $TPTP2XDirectory/tptp2X

#----Set the mode to executable
chmod 755 $TPTP2XDirectory/tptp2X
#--------------------------------------------------------------------------
echo "--------------------------------------------------------------------"
echo "                tptp2X installation complete"
echo "--------------------------------------------------------------------"
#--------------------------------------------------------------------------
