|
#!/usr/bin/env bash
#
# Author: Nik Sultana, Cambridge University Computer Lab
#
# DESCRIPTION: TPTP visualisation utility
PRG="$(basename "$0")"
#FIXME inline or move to settings
DOT2TEX=dot2tex
DOT=dot
PERL=perl
PDFLATEX=pdflatex
[ -n "$ISABELLE_PDFLATEX" ] && PDFLATEX=$ISABELLE_PDFLATEX
DOT2TEX_VERSION="$($DOT2TEX -V 2> /dev/null)"
DOT_VERSION="$($DOT -V 2>&1 | grep Graphviz)"
PERL_VERSION="$($PERL -v | grep -e "v[0-9]\+." 2> /dev/null)"
PDFLATEX_VERSION="$($PDFLATEX -version | head -1 2> /dev/null)"
function check_deps()
{
#FIXME how well does this work across different platforms and/or versions of
# the tools?
for DEP in DOT2TEX DOT PERL PDFLATEX
do
eval DEP_VAL=\$${DEP}
eval DEP_VERSION=\$${DEP}_VERSION
if [ -z "$DEP_VERSION" ]; then
echo "$DEP not installed"
else
echo "$DEP ($DEP_VAL) : $DEP_VERSION"
fi
done
}
function usage() {
echo
echo "Usage: isabelle $PRG [OPTIONS] IN_FILE OUT_FILE"
echo
echo " Options are:"
echo " -d probe for dependencies"
echo " -k don't delete temp files, and print their location"
echo " -n print name of the generated file"
echo
echo " Produces a DOT/TeX/PDF from a TPTP problem/proof, depending on whether"
echo " the extension of OUT_FILE is dot/tex/pdf."
echo
exit 1
}
OUTPUT_FORMAT=2
SHOW_TARGET=""
KEEP_TEMP=""
NON_EXEC=""
while getopts "dnkX" OPT
do
#FIXME could add "quiet" mode to send stderr (and some stdout) to /dev/null
case "$OPT" in
n)
SHOW_TARGET=true
;;
k)
KEEP_TEMP=true
;;
X)
NON_EXEC=true
;;
d)
check_deps
exit 0
;;
*)
exit 1
;;
esac
done
shift $(($OPTIND - 1))
[ "$#" -ne 2 -o "$1" = "-?" ] && usage
case "${2##*.}" in
dot)
OUTPUT_FORMAT=0
;;
tex)
OUTPUT_FORMAT=1
;;
pdf)
OUTPUT_FORMAT=2
;;
*)
echo "Unrecognised output file extension \".${2##*.}\"."
exit 1
;;
esac
## set some essential variables, prepare the work directory
WORKDIR=""
while :
do
#FIXME not perfectly reliable method, but probably good enough
WORKDIR="${ISABELLE_TMP_PREFIX}-tptpgraph$RANDOM"
[ ! -d "$WORKDIR" ] && break
done
OUTPUT_FILENAME="$(basename "$2")"
FILEDIR="$(cd "$(dirname "$2")"; cd "$(pwd -P)"; pwd)"
FILENAME="${OUTPUT_FILENAME%.*}"
WD="$(pwd)"
mkdir -p $WORKDIR
function generate_dot()
{
LOADER="tptp_graph_$RANDOM"
echo "theory $LOADER imports \"$TPTP_HOME/TPTP_Parser\" \
begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
> $WORKDIR/$LOADER.thy
isabelle process -T "$WORKDIR/$LOADER" -l Pure
}
function cleanup_workdir()
{
if [ -n "$KEEP_TEMP" ]; then
echo $WORKDIR
else
rm -rf $WORKDIR
fi
}
if [ "$OUTPUT_FORMAT" -eq 0 ]; then
[ -z "$NON_EXEC" ] && generate_dot "$1" "$2"
cleanup_workdir
exit 0
fi
## generate and process files in temporary workdir, then move required
## output file to destination dir
[ -z "$NON_EXEC" ] && generate_dot $1 "$WORKDIR/${FILENAME}.dot"
cd $WORKDIR
if [ -z "$NON_EXEC" ]; then
$DOT -Txdot "${FILENAME}.dot" \
| $DOT2TEX -f pgf -t raw --crop \
| $PERL -w -p -e 's/_/\\_/g' > "${FILENAME}.tex"
fi
if [ "$OUTPUT_FORMAT" -eq 1 ]; then
TARGET=$FILENAME.tex
else
TARGET=$FILENAME.pdf
[ -z "$NON_EXEC" ] && $PDFLATEX "${FILENAME}.tex"
fi
[ -z "$NON_EXEC" ] && mv $TARGET $WD
cd $WD
cleanup_workdir
[ -n "$SHOW_TARGET" ] && echo "$FILEDIR/$TARGET"
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
