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
blanchet@46319
     1
#!/usr/bin/env bash
blanchet@46319
     2
#
blanchet@46319
     3
# Author: Jasmin Blanchette
blanchet@46319
     4
#
blanchet@46319
     5
# DESCRIPTION: Translation tool for TPTP formats
blanchet@46319
     6
blanchet@46319
     7
blanchet@46319
     8
PRG="$(basename "$0")"
blanchet@46319
     9
blanchet@46319
    10
function usage() {
blanchet@46319
    11
  echo
blanchet@46319
    12
  echo "Usage: isabelle $PRG FORMAT FILE"
blanchet@46319
    13
  echo
blanchet@46319
    14
  echo "  Translates TPTP file to specified TPTP format (\"CNF\", \"FOF\", \"TFF0\", \"TFF1\", or \"THF0\")."
blanchet@46319
    15
  echo
blanchet@46319
    16
  exit 1
blanchet@46319
    17
}
blanchet@46319
    18
blanchet@46319
    19
[ "$#" -eq 0 -o "$1" = "-?" ] && usage
blanchet@46319
    20
blanchet@46319
    21
SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
blanchet@46319
    22
blanchet@46319
    23
for FILE in "$@"
blanchet@46319
    24
do
blanchet@46320
    25
  echo "theory $SCRATCH imports \"Main\" begin ML {* ATP_Problem_Generate.translate_tptp_file \"$FILE\" *} end;" \
blanchet@46319
    26
    > /tmp/$SCRATCH.thy
blanchet@46319
    27
  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
blanchet@46319
    28
done