author | sultana |
Wed, 19 Feb 2014 15:57:02 +0000 | |
changeset 55593 | c67c27f0ea94 |
parent 55592 | 37c1abaf4876 |
child 55594 | eb291b215c73 |
permissions | -rw-r--r-- |
47412 | 1 |
(* Title: HOL/TPTP/TPTP_Parser/tptp_to_dot.ML |
2 |
Author: Nik Sultana, Cambridge University Computer Laboratory |
|
3 |
||
4 |
Translates parsed TPTP proofs into DOT format. This can then be processed |
|
5 |
by an accompanying script to translate the proofs into other formats. |
|
55586 | 6 |
|
7 |
It tries to adhere to the symbols used in IDV, as described in |
|
8 |
"An Interactive Derivation Viewer" by Trac & Puzis & Sutcliffe, UITP 2006. |
|
47412 | 9 |
*) |
10 |
||
11 |
signature TPTP_TO_DOT = |
|
12 |
sig |
|
13 |
(*DOT-drawing function, works directly on parsed TPTP*) |
|
14 |
val tptp_dot_node : bool -> bool -> TPTP_Syntax.tptp_line -> string |
|
15 |
||
16 |
(*Parse a (LEO-II+E) proof and produce a DOT file*) |
|
17 |
val write_proof_dot : string -> string -> unit |
|
18 |
end |
|
19 |
||
20 |
structure TPTP_To_Dot : TPTP_TO_DOT = |
|
21 |
struct |
|
22 |
||
23 |
open TPTP_Syntax |
|
24 |
||
55592
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
25 |
datatype style = |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
26 |
(*Only draw shapes. No formulas or edge labels.*) |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
27 |
Shapes |
55593 | 28 |
(*Don't draw shapes. Only write formulas (as nodes) and inference names (as edge labels).*) |
55592
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
29 |
| Formulas |
55593 | 30 |
(*Draw shapes and write the AF ID inside.*) |
31 |
| IDs |
|
55592
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
32 |
|
55593 | 33 |
(*FIXME this kind of configurability isn't very user-friendly.*) |
55592
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
34 |
(*Determine the require output style form the TPTP_GRAPH environment variable. |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
35 |
Shapes is the default style.*) |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
36 |
val required_style = |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
37 |
if getenv "TPTP_GRAPH" = "formulas" then |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
38 |
Formulas |
55593 | 39 |
else if getenv "TPTP_GRAPH" = "IDs" then |
40 |
IDs |
|
55592
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
41 |
else Shapes |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
42 |
|
47412 | 43 |
(*Draw an arc between two nodes*) |
44 |
fun dot_arc reverse (src, label) target = |
|
55592
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
45 |
let |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
46 |
val edge_label = |
55593 | 47 |
if required_style = Shapes orelse required_style = IDs then "" |
55592
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
48 |
else |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
49 |
case label of |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
50 |
NONE => "" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
51 |
| SOME label => "[label=\"" ^ label ^ "\"];" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
52 |
in |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
53 |
"\"" ^ (if reverse then target else src) ^ |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
54 |
"\" -> \"" ^ (if reverse then src else target) ^ |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
55 |
"\" " ^ edge_label ^ "\n" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
56 |
end |
47412 | 57 |
|
58 |
(*Node shapes indicate the role of the related clauses.*) |
|
59 |
exception NO_ROLE_SHAPE |
|
60 |
fun the_role_shape role = |
|
55592
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
61 |
if role = Role_Fi_Domain orelse |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
62 |
role = Role_Fi_Functors orelse |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
63 |
role = Role_Fi_Predicates orelse |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
64 |
role = Role_Type orelse |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
65 |
role = Role_Unknown then |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
66 |
raise NO_ROLE_SHAPE |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
67 |
else if required_style = Formulas then "plaintext" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
68 |
else |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
69 |
case role of |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
70 |
Role_Axiom => "triangle" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
71 |
| Role_Hypothesis => "invtrapezium" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
72 |
| Role_Definition => "invtriangle" (*NOTE this is not standard wrt IDV*) |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
73 |
| Role_Assumption => "trapezium" (*NOTE this is not standard wrt IDV*) |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
74 |
| Role_Lemma => "hexagon" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
75 |
| Role_Theorem => "star" (*NOTE this is not standard wrt IDV*) |
55590 | 76 |
|
55592
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
77 |
| Role_Conjecture => "house" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
78 |
| Role_Negated_Conjecture => "invhouse" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
79 |
| Role_Plain => "circle" |
55590 | 80 |
|
47412 | 81 |
|
82 |
fun have_role_shape role = |
|
83 |
(the_role_shape role; true) |
|
84 |
handle NO_ROLE_SHAPE => false |
|
85 |
| exc => raise exc |
|
86 |
||
87 |
(*Different styles are applied to nodes relating to clauses written in |
|
88 |
difference languages.*) |
|
89 |
exception NO_LANG_STYLE |
|
90 |
fun the_lang_style lang = |
|
91 |
case lang of |
|
92 |
CNF => "dotted" |
|
93 |
| FOF => "dashed" |
|
55587
5d3db2c626e3
experimenting with improving DOT output, and embedding LaTeX code for formulas (rather than only giving the clause number);
sultana
parents:
55586
diff
changeset
|
94 |
| THF => "" (* "filled" *) |
47412 | 95 |
| _ => raise NO_LANG_STYLE |
96 |
||
97 |
(*Does the formula just consist of "$false"?*) |
|
98 |
fun is_last_line CNF (Pred (Interpreted_Logic False, [])) = true |
|
99 |
| is_last_line THF (Atom (THF_Atom_term |
|
100 |
(Term_Func (Interpreted_Logic False, [])))) = true |
|
101 |
| is_last_line _ _ = false |
|
102 |
||
103 |
fun tptp_dot_node with_label reverse_arrows |
|
55592
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
104 |
(Annotated_Formula (_, lang, n, role, fmla_tptp, annot)) = |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
105 |
let |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
106 |
val node_label = |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
107 |
if required_style = Formulas then |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
108 |
"\", label=\"$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\"];\n" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
109 |
(*FIXME add a parameter to switch to using the following code, which lowers, centers, and horizontally-bounds the label. |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
110 |
(this is useful if you want to keep the shapes but also show formulas)*) |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
111 |
(* "\", label=\"\\\\begin{minipage}{10cm}\\\\vspace{21mm}\\\\centering$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\\\\end{minipage}\"];\n") ^*) |
55593 | 112 |
else if required_style = IDs then |
113 |
"\", label=\"" ^ n ^ "\"];\n" |
|
55592
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
114 |
else |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
115 |
"\", label=\"\"];\n" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
116 |
in |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
117 |
(*don't expect to find 'Include' in proofs*) |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
118 |
if have_role_shape role andalso role <> Role_Definition then |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
119 |
"\"" ^ n ^ |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
120 |
"\" [shape=\"" ^ |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
121 |
(if is_last_line lang fmla_tptp then "doublecircle" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
122 |
else the_role_shape role) ^ |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
123 |
"\", style=\"" ^ the_lang_style lang ^ |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
124 |
node_label ^ |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
125 |
(case TPTP_Proof.extract_source_info annot of |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
126 |
SOME (TPTP_Proof.Inference (rule, _, pinfos)) => |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
127 |
let |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
128 |
fun parent_id (TPTP_Proof.Parent n) = n |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
129 |
| parent_id (TPTP_Proof.ParentWithDetails (n, _)) = n |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
130 |
val parent_ids = map parent_id pinfos |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
131 |
in |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
132 |
map |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
133 |
(dot_arc reverse_arrows |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
134 |
(n, if with_label then SOME rule else NONE)) |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
135 |
parent_ids |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
136 |
|> implode |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
137 |
end |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
138 |
| _ => "") |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
139 |
else "" |
37c1abaf4876
behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not;
sultana
parents:
55591
diff
changeset
|
140 |
end |
47412 | 141 |
|
142 |
(*FIXME add opts to label arcs etc*) |
|
143 |
fun write_proof_dot input_file output_file = |
|
144 |
let |
|
145 |
(*rankdir=\"LR\";\n*) |
|
146 |
val defaults = |
|
55587
5d3db2c626e3
experimenting with improving DOT output, and embedding LaTeX code for formulas (rather than only giving the clause number);
sultana
parents:
55586
diff
changeset
|
147 |
"graph[nodesep=3];\n" ^ |
47412 | 148 |
"node[fixedsize=true];\n" ^ |
55587
5d3db2c626e3
experimenting with improving DOT output, and embedding LaTeX code for formulas (rather than only giving the clause number);
sultana
parents:
55586
diff
changeset
|
149 |
"node[width=0.5];\n" ^ |
47412 | 150 |
"node[shape=plaintext];\n" ^ |
55587
5d3db2c626e3
experimenting with improving DOT output, and embedding LaTeX code for formulas (rather than only giving the clause number);
sultana
parents:
55586
diff
changeset
|
151 |
(* "node[fillcolor=lightgray];\n" ^ *) |
55590 | 152 |
"node[fontsize=50];\n" |
47412 | 153 |
in |
154 |
TPTP_Parser.parse_file input_file |
|
55587
5d3db2c626e3
experimenting with improving DOT output, and embedding LaTeX code for formulas (rather than only giving the clause number);
sultana
parents:
55586
diff
changeset
|
155 |
|> map (tptp_dot_node true true) |
47426 | 156 |
|> implode |
47412 | 157 |
|> (fn str => "digraph ProofGraph {\n" ^ defaults ^ str ^ "}") |
158 |
|> File.write (Path.explode output_file) |
|
159 |
end |
|
160 |
||
161 |
end |