cleaned code used to produce a proof-graph;

--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Feb 19 15:57:02 2014 +0000
@@ -525,38 +525,12 @@
   | string_of_tptp_type (Subtype (symbol1, symbol2)) =
       string_of_symbol symbol1 ^ " << " ^ string_of_symbol symbol2
 
-             
-(*FIXME clean up this code!*)
+(*FIXME formatting details haven't been fully worked out -- don't use this function for anything serious in its current form!*)
 (*TODO Add subscripting*)
 (*infix symbols, including \subset, \cup, \cap*)
 fun latex_of_tptp_term x =
-((*writeln ("term=" ^ PolyML.makestring x);*)
   case x of
-(*
-      Term_Func (Uninterpreted "subset", [tptp_t1, tptp_t2]) =>
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")"
-    | Term_Func (Uninterpreted "union", [tptp_t1, tptp_t2]) =>
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")"
-*)
-(*
-      Term_Func (Interpreted_Logic Apply, [Term_Func (Interpreted_Logic Apply, [Uninterpreted "subset", tptp_t1]), tptp_t2]) =>
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")"
-    | Term_Func (Interpreted_Logic Apply, [Term_Func (Interpreted_Logic Apply, [Uninterpreted "union", tptp_t1]), tptp_t2]) =>
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")"
-*)
-(*
-      Term_Func (Interpreted_ExtraLogic Apply,
-                 [Term_Func (Interpreted_ExtraLogic Apply,
-                             [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "subset", []),
-                                                                             tptp_t1])]), tptp_t2]) =>
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")"
-    | Term_Func (Interpreted_ExtraLogic Apply,
-                 [Term_Func (Interpreted_ExtraLogic Apply,
-                             [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "union", []),
-                                                                             tptp_t1])]), tptp_t2]) =>
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")"
-
-    |*) Term_Func (Interpreted_Logic Equals, [tptp_t1, tptp_t2]) =>
+      Term_Func (Interpreted_Logic Equals, [tptp_t1, tptp_t2]) =>
         "(" ^ latex_of_tptp_term tptp_t1 ^ " = " ^ latex_of_tptp_term tptp_t2 ^ ")"
     | Term_Func (Interpreted_Logic NEquals, [tptp_t1, tptp_t2]) =>
         "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\neq " ^ latex_of_tptp_term tptp_t2 ^ ")"
@@ -576,11 +550,8 @@
     | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*)
     | Term_Num (_, str) => str
     | Term_Distinct_Object str => str (*FIXME*)
-)
+
 and latex_of_symbol (Uninterpreted str) =
-(*    if str = "union" then "\\\\cup"
-    else if str = "subset" then "\\\\subset"
-    else*)
     if str = "emptyset" then "\\\\emptyset"
     else "\\\\mathrm{" ^ str ^ "}"
   | latex_of_symbol (Interpreted_ExtraLogic interpreted_symbol) = latex_of_interpreted_symbol interpreted_symbol
@@ -654,100 +625,48 @@
        NONE => latex_of_symbol symbol
      | SOME tptp_type =>
          latex_of_symbol symbol ^ " : " ^ latex_of_tptp_type tptp_type)
-  | latex_of_tptp_atom (THF_Atom_term tptp_term) = latex_of_tptp_term tptp_term   
+  | latex_of_tptp_atom (THF_Atom_term tptp_term) = latex_of_tptp_term tptp_term
   | latex_of_tptp_atom (THF_Atom_conn_term symbol) = latex_of_symbol symbol
 
-(*
-and latex_of_tptp_formula (Pred (symbol, tptp_term_list)) =
-      "(" ^ latex_of_symbol symbol ^
-      space_implode " " (map latex_of_tptp_term tptp_term_list) ^ ")"
-  | latex_of_tptp_formula (Fmla (symbol, tptp_formula_list)) =
-      "(" ^ latex_of_symbol symbol ^
-      space_implode " " (map latex_of_tptp_formula tptp_formula_list) ^ ")"
-*)
-(*
-and  latex_of_tptp_formula (Pred (Uninterpreted "subset", [tptp_t1, tptp_t2])) =
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")"
-    | latex_of_tptp_formula (Pred (Uninterpreted "union", [tptp_t1, tptp_t2])) =
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")"
-*)
-and  (*latex_of_tptp_formula (
-      Pred (Interpreted_ExtraLogic Apply,
-                 [Term_Func (Interpreted_ExtraLogic Apply,
-                             [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "subset", []),
-                                                                             tptp_t1])]), tptp_t2])) =
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")"
-    | latex_of_tptp_formula (Pred (Interpreted_ExtraLogic Apply,
-                 [Term_Func (Interpreted_ExtraLogic Apply,
-                             [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "union", []),
-                                                                             tptp_t1])]), tptp_t2])) =
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")"
-
-    |*) latex_of_tptp_formula (Pred (Interpreted_Logic Equals, [tptp_t1, tptp_t2])) =
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " = " ^ latex_of_tptp_term tptp_t2 ^ ")"
-    | latex_of_tptp_formula (Pred (Interpreted_Logic NEquals, [tptp_t1, tptp_t2])) =
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\neq " ^ latex_of_tptp_term tptp_t2 ^ ")"
-    | latex_of_tptp_formula (Pred (Interpreted_Logic Or, [tptp_t1, tptp_t2])) =
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\vee " ^ latex_of_tptp_term tptp_t2 ^ ")"
-    | latex_of_tptp_formula (Pred (Interpreted_Logic And, [tptp_t1, tptp_t2])) =
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\wedge " ^ latex_of_tptp_term tptp_t2 ^ ")"
-    | latex_of_tptp_formula (Pred (Interpreted_Logic Iff, [tptp_t1, tptp_t2])) =
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")"
-    | latex_of_tptp_formula (Pred (Interpreted_Logic If, [tptp_t1, tptp_t2])) =
-        "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")"
+and latex_of_tptp_formula (Pred (Interpreted_Logic Equals, [tptp_t1, tptp_t2])) =
+      "(" ^ latex_of_tptp_term tptp_t1 ^ " = " ^ latex_of_tptp_term tptp_t2 ^ ")"
+  | latex_of_tptp_formula (Pred (Interpreted_Logic NEquals, [tptp_t1, tptp_t2])) =
+      "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\neq " ^ latex_of_tptp_term tptp_t2 ^ ")"
+  | latex_of_tptp_formula (Pred (Interpreted_Logic Or, [tptp_t1, tptp_t2])) =
+      "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\vee " ^ latex_of_tptp_term tptp_t2 ^ ")"
+  | latex_of_tptp_formula (Pred (Interpreted_Logic And, [tptp_t1, tptp_t2])) =
+      "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\wedge " ^ latex_of_tptp_term tptp_t2 ^ ")"
+  | latex_of_tptp_formula (Pred (Interpreted_Logic Iff, [tptp_t1, tptp_t2])) =
+      "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")"
+  | latex_of_tptp_formula (Pred (Interpreted_Logic If, [tptp_t1, tptp_t2])) =
+      "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")"
 
   | latex_of_tptp_formula (x as (Pred (symbol, tptp_term_list))) =
-((*writeln ("fmla=" ^ PolyML.makestring x);*)
-      (*"(" ^*) latex_of_symbol symbol ^
-      space_implode "\\\\, " (map latex_of_tptp_term tptp_term_list) (*^ ")"*)
-)
+      latex_of_symbol symbol ^
+       space_implode "\\\\, " (map latex_of_tptp_term tptp_term_list)
 
-(*
-    | latex_of_tptp_formula (Fmla (Uninterpreted "subset", [tptp_f1, tptp_f2])) =
-        "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_f2 ^ ")"
-    | latex_of_tptp_formula (Fmla (Uninterpreted "union", [tptp_f1, tptp_f2])) =
-        "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_f2 ^ ")"
-*)
+  | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "union", []))), tptp_f1]), tptp_f2])) =
+      "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_f2 ^ ")"
+
+  | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "subset", []))), tptp_f1]), tptp_f2])) =
+      "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_f2 ^ ")"
 
-(*
-    | latex_of_tptp_formula (
-      Fmla (Interpreted_ExtraLogic Apply,
-                 [Fmla (Interpreted_ExtraLogic Apply,
-                             [Fmla (Interpreted_ExtraLogic Apply, [Fmla (Uninterpreted "subset", []),
-                                                                             tptp_t1])]), tptp_t2])) =
-        "(" ^ latex_of_tptp_formula tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_t2 ^ ")"
-    | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply,
-                 [Fmla (Interpreted_ExtraLogic Apply,
-                             [Fmla (Interpreted_ExtraLogic Apply, [Fmla (Uninterpreted "union", []),
-                                                                             tptp_t1])]), tptp_t2])) =
-        "(" ^ latex_of_tptp_formula tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_t2 ^ ")"
-*)
-
-    | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "union", []))), tptp_f1]), tptp_f2])) =
-        "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_f2 ^ ")"
-
-    | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "subset", []))), tptp_f1]), tptp_f2])) =
-        "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_f2 ^ ")"
-
-
-    | latex_of_tptp_formula (Fmla (Interpreted_Logic Equals, [tptp_f1, tptp_f2])) =
-        "(" ^ latex_of_tptp_formula tptp_f1 ^ " = " ^ latex_of_tptp_formula tptp_f2 ^ ")"
-    | latex_of_tptp_formula (Fmla (Interpreted_Logic NEquals, [tptp_f1, tptp_f2])) =
-        "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\neq " ^ latex_of_tptp_formula tptp_f2 ^ ")"
-    | latex_of_tptp_formula (Fmla (Interpreted_Logic Or, [tptp_f1, tptp_f2])) =
-        "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\vee " ^ latex_of_tptp_formula tptp_f2 ^ ")"
-    | latex_of_tptp_formula (Fmla (Interpreted_Logic And, [tptp_f1, tptp_f2])) =
-        "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\wedge " ^ latex_of_tptp_formula tptp_f2 ^ ")"
-    | latex_of_tptp_formula (Fmla (Interpreted_Logic Iff, [tptp_f1, tptp_f2])) =
-        "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_formula tptp_f2 ^ ")"
-    | latex_of_tptp_formula (Fmla (Interpreted_Logic If, [tptp_f1, tptp_f2])) =
-        "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\longrightarrow " ^ latex_of_tptp_formula tptp_f2 ^ ")"
+  | latex_of_tptp_formula (Fmla (Interpreted_Logic Equals, [tptp_f1, tptp_f2])) =
+      "(" ^ latex_of_tptp_formula tptp_f1 ^ " = " ^ latex_of_tptp_formula tptp_f2 ^ ")"
+  | latex_of_tptp_formula (Fmla (Interpreted_Logic NEquals, [tptp_f1, tptp_f2])) =
+      "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\neq " ^ latex_of_tptp_formula tptp_f2 ^ ")"
+  | latex_of_tptp_formula (Fmla (Interpreted_Logic Or, [tptp_f1, tptp_f2])) =
+      "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\vee " ^ latex_of_tptp_formula tptp_f2 ^ ")"
+  | latex_of_tptp_formula (Fmla (Interpreted_Logic And, [tptp_f1, tptp_f2])) =
+      "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\wedge " ^ latex_of_tptp_formula tptp_f2 ^ ")"
+  | latex_of_tptp_formula (Fmla (Interpreted_Logic Iff, [tptp_f1, tptp_f2])) =
+      "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_formula tptp_f2 ^ ")"
+  | latex_of_tptp_formula (Fmla (Interpreted_Logic If, [tptp_f1, tptp_f2])) =
+      "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\longrightarrow " ^ latex_of_tptp_formula tptp_f2 ^ ")"
 
   | latex_of_tptp_formula (x as (Fmla (symbol, tptp_formula_list))) =
-(writeln ("fmla=" ^ PolyML.makestring x);
-      (*"(" ^*) latex_of_symbol symbol ^
-      space_implode "\\\\, " (map latex_of_tptp_formula tptp_formula_list) (*^ ")"*)
-)
+      latex_of_symbol symbol ^
+        space_implode "\\\\, " (map latex_of_tptp_formula tptp_formula_list)
 
   | latex_of_tptp_formula (Sequent (tptp_formula_list1, tptp_formula_list2)) = "" (*FIXME*)
   | latex_of_tptp_formula (Quant (quantifier, varlist, tptp_formula)) =

--- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Feb 19 15:57:02 2014 +0000
@@ -30,7 +30,8 @@
     (*Draw shapes and write the AF ID inside.*)
   | IDs
 
-(*FIXME this kind of configurability isn't very user-friendly.*)
+(*FIXME this kind of configurability isn't very user-friendly.
+  Ideally we'd accept a parameter from the tptp_graph script.*)
 (*Determine the require output style form the TPTP_GRAPH environment variable.
   Shapes is the default style.*)
 val required_style =
@@ -78,7 +79,6 @@
     | Role_Negated_Conjecture => "invhouse"
     | Role_Plain => "circle"
 
-
 fun have_role_shape role =
   (the_role_shape role; true)
   handle NO_ROLE_SHAPE => false
@@ -91,10 +91,11 @@
   case lang of
       CNF => "dotted"
     | FOF => "dashed"
-    | THF => "" (* "filled" *)
+    | THF => "" (*NOTE could use "filled" to contrast with first-order languages*)
     | _ => raise NO_LANG_STYLE
 
-(*Does the formula just consist of "$false"?*)
+(*Check if the formula just consists of "$false"?
+  which we interpret to be the last line of the proof.*)
 fun is_last_line CNF (Pred (Interpreted_Logic False, [])) = true
   | is_last_line THF (Atom (THF_Atom_term
       (Term_Func (Interpreted_Logic False, [])))) = true
@@ -142,13 +143,13 @@
 (*FIXME add opts to label arcs etc*)
 fun write_proof_dot input_file output_file =
   let
-    (*rankdir=\"LR\";\n*)
+    (*NOTE sometimes useful to include: rankdir=\"LR\";\n*)
     val defaults =
       "graph[nodesep=3];\n" ^
       "node[fixedsize=true];\n" ^
       "node[width=0.5];\n" ^
       "node[shape=plaintext];\n" ^
-      (* "node[fillcolor=lightgray];\n" ^ *)
+      (*NOTE sometimes useful to include: "node[fillcolor=lightgray];\n" ^ *)
       "node[fontsize=50];\n"
   in
     TPTP_Parser.parse_file input_file