equal
deleted
inserted
replaced
7 |
7 |
8 PRG="$(basename "$0")" |
8 PRG="$(basename "$0")" |
9 |
9 |
10 function usage() { |
10 function usage() { |
11 echo |
11 echo |
12 echo "Usage: isabelle $PRG FORMAT IN_FILE OUT_FILE" |
12 echo "Usage: isabelle $PRG FORMAT FILE" |
13 echo |
13 echo |
14 echo " Translates TPTP input file to the specified format (\"FOF\", \"TFF0\", \"THF0\", or \"DFG\")." |
14 echo " Translates TPTP input file to the specified format (\"FOF\", \"TFF0\", \"THF0\", or \"DFG\")." |
|
15 echo " Emits the result to standard output." |
15 echo |
16 echo |
16 exit 1 |
17 exit 1 |
17 } |
18 } |
18 |
19 |
19 [ "$#" -ne 3 -o "$1" = "-?" ] && usage |
20 [ "$#" -ne 2 -o "$1" = "-?" ] && usage |
20 |
21 |
21 SCRATCH="Scratch_${PRG}_$$_${RANDOM}" |
22 SCRATCH="Scratch_${PRG}_$$_${RANDOM}" |
22 |
23 |
23 args=("$@") |
24 args=("$@") |
24 |
25 |
25 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
26 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
26 ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" \"${args[2]}\" *} end;" \ |
27 ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end;" \ |
27 > /tmp/$SCRATCH.thy |
28 > /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 \|^Loading theory" |
29 "$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 \|^Loading theory" |