--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Feb 19 15:57:02 2014 +0000
@@ -528,7 +528,8 @@
| NONE => Free (n, dummyT) (*to infer the variable's type*)
)
| NONE =>
- raise MISINTERPRET_TERM ("Could not type variable", tptp_t))
+ Free (n, dummyT)
+ (*raise MISINTERPRET_TERM ("Could not type variable", tptp_t)*))
else (*variables range over individuals*)
Free (n, interpret_type config thy type_map (Defined_type Type_Ind)),
thy)
--- 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
@@ -25,21 +25,26 @@
datatype style =
(*Only draw shapes. No formulas or edge labels.*)
Shapes
- (*Don't draw shapes. Only write formulas (as nodes) and inference names (as edge labels)*)
+ (*Don't draw shapes. Only write formulas (as nodes) and inference names (as edge labels).*)
| Formulas
+ (*Draw shapes and write the AF ID inside.*)
+ | IDs
+(*FIXME this kind of configurability isn't very user-friendly.*)
(*Determine the require output style form the TPTP_GRAPH environment variable.
Shapes is the default style.*)
val required_style =
if getenv "TPTP_GRAPH" = "formulas" then
Formulas
+ else if getenv "TPTP_GRAPH" = "IDs" then
+ IDs
else Shapes
(*Draw an arc between two nodes*)
fun dot_arc reverse (src, label) target =
let
val edge_label =
- if required_style = Shapes then ""
+ if required_style = Shapes orelse required_style = IDs then ""
else
case label of
NONE => ""
@@ -104,6 +109,8 @@
(*FIXME add a parameter to switch to using the following code, which lowers, centers, and horizontally-bounds the label.
(this is useful if you want to keep the shapes but also show formulas)*)
(* "\", label=\"\\\\begin{minipage}{10cm}\\\\vspace{21mm}\\\\centering$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\\\\end{minipage}\"];\n") ^*)
+ else if required_style = IDs then
+ "\", label=\"" ^ n ^ "\"];\n"
else
"\", label=\"\"];\n"
in