Altered graph .dot export so that nodes are displayed as their tactic.

3 files changed, 60 insertions, 4 deletions

diff --git a/hol-light/TacticRecording/ex3b.dot b/hol-light/TacticRecording/ex3b.dot
new file mode 100644
index 00000000..5b951b96
--- /dev/null
+++ b/hol-light/TacticRecording/ex3b.dot
@@ -0,0 +1,37 @@
+digraph G {
+  344 [label = "CONV_TAC"];
+  345 [label = "GEN_TAC"];
+  351 [label = "INDUCT_TAC"];
+  352 [label = "REWRITE_TAC"];
+  358 [label = "REAL_ARITH_TAC"];
+  353 [label = "REWRITE_TAC"];
+  367 [label = "REWRITE_TAC"];
+  368 [label = "SIMP_TAC"];
+  370 [label = "REWRITE_TAC"];
+  372 [label = "REWRITE_TAC"];
+  374 [label = "ASM_REWRITE_TAC"];
+  376 [label = "REWRITE_TAC"];
+  378 [label = "REAL_ARITH_TAC"];
+  344 -> 345;
+  345 -> 351;
+  subgraph cluster1 {
+    label = "induction";
+    351 -> 352;
+    351 -> 353;
+    352 -> 358;
+    subgraph cluster2 {
+      label = "base case";
+      358;
+    }
+    353 -> 367;
+    subgraph cluster3 {
+      label = "step case";
+      367 -> 368;
+      368 -> 370;
+      370 -> 372;
+      372 -> 374;
+      374 -> 376;
+      376 -> 378;
+    }
+  }
+}
\ No newline at end of file
diff --git a/hol-light/TacticRecording/gvexport.ml b/hol-light/TacticRecording/gvexport.ml
index 050ef997..952b3ad9 100644
--- a/hol-light/TacticRecording/gvexport.ml
+++ b/hol-light/TacticRecording/gvexport.ml
@@ -23,7 +23,10 @@ let rec print_gv_graphelem d ge =
        -> (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");;
+       -> (print_indent d; print_goalid id; print_string ";\n")
+  | Name (id,x)
+       -> (print_indent d; print_goalid id;
+             print_string " [label = "; print_fstring x; print_string "];\n");;
 
 let print_gv_graph ges =
   let () = (cluster_count := 0) in
diff --git a/hol-light/TacticRecording/hiproofs.ml b/hol-light/TacticRecording/hiproofs.ml
index 4adee607..370e0dc3 100644
--- a/hol-light/TacticRecording/hiproofs.ml
+++ b/hol-light/TacticRecording/hiproofs.ml
@@ -288,13 +288,24 @@ let thenise_hiproof h =
 type graph_elem =
     Box of (label * graph_elem list)
   | Line of (goalid * goalid)
-  | Single of goalid;;
+  | Single of goalid
+  | Name of (goalid * string);;
 
 let is_box ge =
   match ge with Box _ -> true | _ -> false;;
 
 let mk_line id1 id2 = Line (id1,id2);;
 
+let rec graph_elem_nodes ge =
+  match ge with
+    Box (_,ges)    -> graph_nodes ges
+  | Line (id1,id2) -> [id1;id2]
+  | Single id      -> [id]
+  | Name (id,x)    -> [id]
+
+and graph_nodes ges =
+  foldr (fun ge ids -> union (graph_elem_nodes ge) ids) ges [];;
+
 
 (* Utils *)
 
@@ -348,8 +359,13 @@ let rec hiproof_graph0 h =
 
 let hiproof_graph h =
   let ges = hiproof_graph0 h in
-  let (ges1,ges2) = partition is_box ges in
-  ges1 @ ges2;;
+  let ids = graph_nodes ges in
+  let tacname_of_id id =
+     match ((fst o gtree_tactic1 o get_gtree) id) with
+       Some x -> x
+     | None   -> "<tactic>" in
+  let ges' = map (fun id -> Name (id, tacname_of_id id)) ids in
+  ges' @ ges;;