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