blob: 050ef997ce5ea30c9af179f643132a2ba417e9b0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
(* ========================================================================== *)
(* GRAPHVIZ EXPORT (HOL LIGHT) *)
(* - Exporting recorded tactics into a Dot file for GraphViz *)
(* *)
(* By Mark Adams *)
(* Copyright (c) Univeristy of Edinburgh, 2012 *)
(* ========================================================================== *)
let cluster_count = ref 0;;
let rec print_gv_graphelem d ge =
match ge with
Box (l,ges)
-> let () = (cluster_count := !cluster_count + 1) in
(print_indent d; print_string "subgraph cluster";
print_int !cluster_count; print_string " "; print_string "{\n";
print_indent (d+2); print_string "label = "; print_label l;
print_string ";\n";
do_list (print_gv_graphelem (d+2)) ges;
print_indent d; print_string "}\n")
| Line (id1,id2)
-> (print_indent d; print_goalid id1; print_string " -> ";
print_goalid id2; print_string ";\n")
| Single id
-> (print_indent d; print_goalid id; print_string ";\n");;
let print_gv_graph ges =
let () = (cluster_count := 0) in
(print_string "digraph G {\n";
do_list (print_gv_graphelem 2) ges;
print_string "}\n");;
let print_hiproof_gv_graph h =
let h' = (trivsimp_hiproof o rightgroup_hiproof o
trivsimp_hiproof o dethen_hiproof) h in
let ges = hiproof_graph h' in
print_gv_graph ges;;
let print_gtree_gv_proof gtr =
let h = gtree_to_hiproof gtr in
print_hiproof_gv_graph h;;
let print_gv_proof () = print_gtree_gv_proof !the_goal_tree;;
|
