| author | wenzelm |
| Sat, 13 Feb 2016 20:01:48 +0100 | |
| changeset 62295 | 4f2fb9adfae5 |
| parent 60546 | dcb0b9b42fcb |
| child 62573 | 27f90319a499 |
| permissions | -rwxr-xr-x |
| 54433 | 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 |
|
|
54472
073f041d83ae
send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
blanchet
parents:
54434
diff
changeset
|
12 |
echo "Usage: isabelle $PRG FORMAT FILE" |
| 54433 | 13 |
echo |
|
54547
c999e2533487
renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy
blanchet
parents:
54472
diff
changeset
|
14 |
echo " Translates TPTP input file to the specified format (\"FOF\", \"TF0\", \"TH0\", or \"DFG\")." |
|
54472
073f041d83ae
send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
blanchet
parents:
54434
diff
changeset
|
15 |
echo " Emits the result to standard output." |
| 54433 | 16 |
echo |
17 |
exit 1 |
|
18 |
} |
|
19 |
||
|
54472
073f041d83ae
send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
blanchet
parents:
54434
diff
changeset
|
20 |
[ "$#" -ne 2 -o "$1" = "-?" ] && usage |
| 54433 | 21 |
|
22 |
SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
|
|
23 |
||
24 |
args=("$@")
|
|
25 |
||
| 60546 | 26 |
isabelle build -b HOL-TPTP |
27 |
||
| 54433 | 28 |
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
|
60544
3daf5eacec05
removed (now illegal) semicolons in generated theory files
blanchet
parents:
54547
diff
changeset
|
29 |
ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \
|
| 54433 | 30 |
> /tmp/$SCRATCH.thy |
|
60545
bcd11dcd0d90
filter out more Poly/ML messages from (ad hoc) TPTP toools
blanchet
parents:
60544
diff
changeset
|
31 |
"$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\|^Warning-The type of\|^ monotype.$" |