--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML Tue Apr 10 06:45:15 2012 +0100
@@ -0,0 +1,108 @@
+(* Title: HOL/TPTP/TPTP_Parser/tptp_to_dot.ML
+ Author: Nik Sultana, Cambridge University Computer Laboratory
+
+Translates parsed TPTP proofs into DOT format. This can then be processed
+by an accompanying script to translate the proofs into other formats.
+*)
+
+signature TPTP_TO_DOT =
+sig
+ (*DOT-drawing function, works directly on parsed TPTP*)
+ val tptp_dot_node : bool -> bool -> TPTP_Syntax.tptp_line -> string
+
+ (*Parse a (LEO-II+E) proof and produce a DOT file*)
+ val write_proof_dot : string -> string -> unit
+end
+
+structure TPTP_To_Dot : TPTP_TO_DOT =
+struct
+
+open TPTP_Syntax
+
+(*Draw an arc between two nodes*)
+fun dot_arc reverse (src, label) target =
+ "\"" ^ (if reverse then target else src) ^
+ "\" -> \"" ^ (if reverse then src else target) ^
+ "\" " ^ (case label of
+ NONE => ""
+ | SOME label => "[label=\"" ^ label ^ "\"];") ^ "\n"
+
+(*Node shapes indicate the role of the related clauses.*)
+exception NO_ROLE_SHAPE
+fun the_role_shape role =
+ case role of
+ Role_Axiom => "triangle"
+ | Role_Hypothesis => "???"
+ | Role_Definition => raise NO_ROLE_SHAPE
+ | Role_Assumption => "???"
+ | Role_Lemma => "???"
+ | Role_Theorem => "???"
+ | Role_Conjecture => "house"
+ | Role_Negated_Conjecture => "invhouse"
+ | Role_Plain => "circle"
+ | Role_Fi_Domain => raise NO_ROLE_SHAPE
+ | Role_Fi_Functors => raise NO_ROLE_SHAPE
+ | Role_Fi_Predicates => raise NO_ROLE_SHAPE
+ | Role_Type => raise NO_ROLE_SHAPE
+ | Role_Unknown => raise NO_ROLE_SHAPE
+
+fun have_role_shape role =
+ (the_role_shape role; true)
+ handle NO_ROLE_SHAPE => false
+ | exc => raise exc
+
+(*Different styles are applied to nodes relating to clauses written in
+ difference languages.*)
+exception NO_LANG_STYLE
+fun the_lang_style lang =
+ case lang of
+ CNF => "dotted"
+ | FOF => "dashed"
+ | THF => "filled"
+ | _ => raise NO_LANG_STYLE
+
+(*Does the formula just consist of "$false"?*)
+fun is_last_line CNF (Pred (Interpreted_Logic False, [])) = true
+ | is_last_line THF (Atom (THF_Atom_term
+ (Term_Func (Interpreted_Logic False, [])))) = true
+ | is_last_line _ _ = false
+
+fun tptp_dot_node with_label reverse_arrows
+ (Annotated_Formula (_, lang, n, role, fmla_tptp, annot)) =
+ (*don't expect to find 'Include' in proofs*)
+ if have_role_shape role
+ then
+ "\"" ^ n ^
+ "\" [shape=\"" ^
+ (if is_last_line lang fmla_tptp then "doublecircle"
+ else the_role_shape role) ^
+ "\", style=\"" ^ the_lang_style lang ^
+ "\", label=\"" ^ n ^ "\"];\n" ^
+ (case TPTP_Proof.extract_inference_info annot of
+ NONE => ""
+ | SOME (rule, ids) =>
+ map (dot_arc reverse_arrows
+ (n, if with_label then SOME rule else NONE)) ids
+ |> String.concat)
+ else ""
+
+(*FIXME add opts to label arcs etc*)
+fun write_proof_dot input_file output_file =
+ let
+ (*rankdir=\"LR\";\n*)
+ val defaults =
+ "node[fixedsize=true];\n" ^
+ "node[width=.5];\n" ^
+ "node[shape=plaintext];\n" ^
+ "node[fillcolor=lightgray];\n" ^
+ "node[fontsize=40];\n" ^
+ "edge[dir=none];\n"
+ in
+ TPTP_Parser.parse_file input_file
+ |> map (tptp_dot_node false true)
+ |> String.concat
+ |> (fn str => "digraph ProofGraph {\n" ^ defaults ^ str ^ "}")
+ |> File.write (Path.explode output_file)
+ end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph Tue Apr 10 06:45:15 2012 +0100
@@ -0,0 +1,156 @@
+#!/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
+SED=sed
+PDFLATEX=pdflatex
+[ -n "$ISABELLE_PDFLATEX" ] && PDFLATEX=$ISABELLE_PDFLATEX
+DOT2TEX_VERSION="$($DOT2TEX -V 2> /dev/null)"
+DOT_VERSION="$($DOT -V 2> /dev/null)"
+SED_VERSION="$($SED --version | head -1 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_VERSION DOT_VERSION SED_VERSION PDFLATEX_VERSION
+ do
+ eval DEP_VAL=\$$DEP
+ if [ -z "$DEP_VAL" ]; then
+ echo "$DEP not installed"
+ else
+ echo "$DEP_VAL"
+ 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 "dknX" 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
+ ;;
+ 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."
+ exit 1
+ ;;
+esac
+
+function generate_dot()
+{
+ #FIXME using a thy might be more robust
+ LOADER="use \"$TPTP_HOME/TPTP_Parser/ml_yacc_lib.ML\"; \
+ use \"$TPTP_HOME/TPTP_Parser/tptp_syntax.ML\"; \
+ use \"$TPTP_HOME/TPTP_Parser/tptp_lexyacc.ML\"; \
+ use \"$TPTP_HOME/TPTP_Parser/tptp_parser.ML\"; \
+ (*\"$TPTP_HOME/TPTP_Parser/tptp_problem_name.ML\";*) \
+ use \"$TPTP_HOME/TPTP_Parser/tptp_proof.ML\"; \
+ use \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\"; \
+ TPTP_To_Dot.write_proof_dot \"$1\" \"$2\"; exit 0;"
+ "$ISABELLE_PROCESS" -e "$LOADER" Pure
+}
+
+
+if [ "$OUTPUT_FORMAT" -eq 0 ]; then
+ [ -z "$NON_EXEC" ] && generate_dot "$1" "$2"
+ exit 0
+fi
+
+## set some essential variables
+
+[ -z "$TMPDIR" ] && TMPDIR=/tmp
+WORKDIR=""
+while :
+do
+ WORKDIR="$TMPDIR/tptpgraph$RANDOM"
+ if [ ! -d "$WORKDIR" ]; then
+ break
+ fi
+done
+OUTPUT_FILENAME="$(basename "$2")"
+FILEDIR="$(cd "$(dirname "$2")"; cd "$(pwd -P)"; pwd)"
+FILENAME="${OUTPUT_FILENAME%.*}"
+WD="$(pwd)"
+
+## generate and process files in temporary workdir, then move to destination dir
+
+mkdir -p $WORKDIR
+[ -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 > "${FILENAME}.tex"
+ $SED -i '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
+if [ -n "$KEEP_TEMP" ]; then
+ echo $WORKDIR
+else
+ rm -rf $WORKDIR
+fi
+
+[ -n "$SHOW_TARGET" ] && echo "$FILEDIR/$TARGET"