equal
deleted
inserted
replaced
|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Jasmin Blanchette |
|
4 # |
|
5 # DESCRIPTION: translate between TPTP formats |
|
6 |
|
7 |
|
8 PRG="$(basename "$0")" |
|
9 |
|
10 function usage() { |
|
11 echo |
|
12 echo "Usage: isabelle $PRG FORMAT IN_FILE OUT_FILE" |
|
13 echo |
|
14 echo " Translates TPTP input file to specified TPTP format (\"FOF\", \"TFF0\", \"TFF1\", or \"THF0\")." |
|
15 echo |
|
16 exit 1 |
|
17 } |
|
18 |
|
19 [ "$#" -ne 3 -o "$1" = "-?" ] && usage |
|
20 |
|
21 SCRATCH="Scratch_${PRG}_$$_${RANDOM}" |
|
22 |
|
23 args=("$@") |
|
24 |
|
25 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
|
26 ML {* ATP_Problem_Import.translate_tptp_file \"${args[0]}\" \"${args[1]}\" \"${args[2]}\" *} end;" \ |
|
27 > /tmp/$SCRATCH.thy |
|
28 "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit" |