src/HOL/TPTP/lib/Tools/tptp_translate
author blanchet
Mon Jan 23 17:40:32 2012 +0100 (2012-01-23)
changeset 46320 0b8b73b49848
parent 46319 c248e4f1be74
child 46324 e4bccf5ec61e
permissions -rwxr-xr-x
renamed two files to make room for a new file
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Jasmin Blanchette
     4 #
     5 # DESCRIPTION: Translation tool for TPTP formats
     6 
     7 
     8 PRG="$(basename "$0")"
     9 
    10 function usage() {
    11   echo
    12   echo "Usage: isabelle $PRG FORMAT FILE"
    13   echo
    14   echo "  Translates TPTP file to specified TPTP format (\"CNF\", \"FOF\", \"TFF0\", \"TFF1\", or \"THF0\")."
    15   echo
    16   exit 1
    17 }
    18 
    19 [ "$#" -eq 0 -o "$1" = "-?" ] && usage
    20 
    21 SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    22 
    23 for FILE in "$@"
    24 do
    25   echo "theory $SCRATCH imports \"Main\" begin ML {* ATP_Problem_Generate.translate_tptp_file \"$FILE\" *} end;" \
    26     > /tmp/$SCRATCH.thy
    27   "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    28 done