1#!/usr/bin/env bash 2# 3# Author: Nik Sultana, Cambridge University Computer Lab 4# 5# DESCRIPTION: TPTP visualisation utility 6 7 8PRG="$(basename "$0")" 9 10#FIXME inline or move to settings 11DOT2TEX=dot2tex 12DOT=dot 13PERL=perl 14PDFLATEX=pdflatex 15[ -n "$ISABELLE_PDFLATEX" ] && PDFLATEX=$ISABELLE_PDFLATEX 16DOT2TEX_VERSION="$($DOT2TEX -V 2> /dev/null)" 17DOT_VERSION="$($DOT -V 2>&1 | grep Graphviz)" 18PERL_VERSION="$($PERL -v | grep -e "v[0-9]\+." 2> /dev/null)" 19PDFLATEX_VERSION="$($PDFLATEX -version | head -1 2> /dev/null)" 20 21function check_deps() 22{ 23 #FIXME how well does this work across different platforms and/or versions of 24 # the tools? 25 for DEP in DOT2TEX DOT PERL PDFLATEX 26 do 27 eval DEP_VAL=\$${DEP} 28 eval DEP_VERSION=\$${DEP}_VERSION 29 if [ -z "$DEP_VERSION" ]; then 30 echo "$DEP not installed" 31 else 32 echo "$DEP ($DEP_VAL) : $DEP_VERSION" 33 fi 34 done 35} 36 37function usage() { 38 echo 39 echo "Usage: isabelle $PRG [OPTIONS] IN_FILE OUT_FILE" 40 echo 41 echo " Options are:" 42 echo " -d probe for dependencies" 43 echo " -k don't delete temp files, and print their location" 44 echo " -n print name of the generated file" 45 echo 46 echo " Produces a DOT/TeX/PDF from a TPTP problem/proof, depending on whether" 47 echo " the extension of OUT_FILE is dot/tex/pdf." 48 echo 49 exit 1 50} 51 52OUTPUT_FORMAT=2 53SHOW_TARGET="" 54KEEP_TEMP="" 55NON_EXEC="" 56 57while getopts "dnkX" OPT 58do 59 #FIXME could add "quiet" mode to send stderr (and some stdout) to /dev/null 60 case "$OPT" in 61 n) 62 SHOW_TARGET=true 63 ;; 64 k) 65 KEEP_TEMP=true 66 ;; 67 X) 68 NON_EXEC=true 69 ;; 70 d) 71 check_deps 72 exit 0 73 ;; 74 *) 75 exit 1 76 ;; 77 esac 78done 79 80shift $(($OPTIND - 1)) 81[ "$#" -ne 2 -o "$1" = "-?" ] && usage 82 83case "${2##*.}" in 84 dot) 85 OUTPUT_FORMAT=0 86 ;; 87 tex) 88 OUTPUT_FORMAT=1 89 ;; 90 pdf) 91 OUTPUT_FORMAT=2 92 ;; 93 *) 94 echo "Unrecognised output file extension \".${2##*.}\"." 95 exit 1 96 ;; 97esac 98 99## set some essential variables, prepare the work directory 100 101WORKDIR="" 102while : 103do 104 #FIXME not perfectly reliable method, but probably good enough 105 WORKDIR="${ISABELLE_TMP_PREFIX}-tptpgraph$RANDOM" 106 [ ! -d "$WORKDIR" ] && break 107done 108OUTPUT_FILENAME="$(basename "$2")" 109FILEDIR="$(cd "$(dirname "$2")"; cd "$(pwd -P)"; pwd)" 110FILENAME="${OUTPUT_FILENAME%.*}" 111WD="$(pwd)" 112mkdir -p $WORKDIR 113 114function generate_dot() 115{ 116 LOADER="tptp_graph_$RANDOM" 117 echo "theory $LOADER imports \"$TPTP_HOME/TPTP_Parser\" \ 118begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \ 119ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \ 120 > $WORKDIR/$LOADER.thy 121 isabelle process -T "$WORKDIR/$LOADER" -l Pure 122} 123 124function cleanup_workdir() 125{ 126 if [ -n "$KEEP_TEMP" ]; then 127 echo $WORKDIR 128 else 129 rm -rf $WORKDIR 130 fi 131} 132 133if [ "$OUTPUT_FORMAT" -eq 0 ]; then 134 [ -z "$NON_EXEC" ] && generate_dot "$1" "$2" 135 cleanup_workdir 136 exit 0 137fi 138 139## generate and process files in temporary workdir, then move required 140## output file to destination dir 141 142[ -z "$NON_EXEC" ] && generate_dot $1 "$WORKDIR/${FILENAME}.dot" 143cd $WORKDIR 144if [ -z "$NON_EXEC" ]; then 145 $DOT -Txdot "${FILENAME}.dot" \ 146 | $DOT2TEX -f pgf -t raw --crop \ 147 | $PERL -w -p -e 's/_/\\_/g' > "${FILENAME}.tex" 148fi 149 150if [ "$OUTPUT_FORMAT" -eq 1 ]; then 151 TARGET=$FILENAME.tex 152else 153 TARGET=$FILENAME.pdf 154 [ -z "$NON_EXEC" ] && $PDFLATEX "${FILENAME}.tex" 155fi 156[ -z "$NON_EXEC" ] && mv $TARGET $WD 157cd $WD 158cleanup_workdir 159 160[ -n "$SHOW_TARGET" ] && echo "$FILEDIR/$TARGET" 161