diff options
Diffstat (limited to 'hol-light/TacticRecording/gvexport.ml')
| -rw-r--r-- | hol-light/TacticRecording/gvexport.ml | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/hol-light/TacticRecording/gvexport.ml b/hol-light/TacticRecording/gvexport.ml new file mode 100644 index 00000000..050ef997 --- /dev/null +++ b/hol-light/TacticRecording/gvexport.ml @@ -0,0 +1,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;; |