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