Capability for exporting .dot files added.

10 files changed, 375 insertions, 101 deletions

diff --git a/hol-light/TacticRecording/ex.dot b/hol-light/TacticRecording/ex.dot
new file mode 100644
index 00000000..fbe961bd
--- /dev/null
+++ b/hol-light/TacticRecording/ex.dot
@@ -0,0 +1,13 @@
+digraph G {
+  subgraph cluster0 {
+    label = "process #1"
+    a0->a1->a2->a3
+  }
+  subgraph cluster1 {
+    label = "process #2"
+    b0->b1->b2->b3
+  }
+  b3->23
+  b2->a3
+  a3->23
+}
\ No newline at end of file
diff --git a/hol-light/TacticRecording/examples1.ml b/hol-light/TacticRecording/examples1.ml
index b587c18f..fd0b446c 100644
--- a/hol-light/TacticRecording/examples1.ml
+++ b/hol-light/TacticRecording/examples1.ml
@@ -45,10 +45,11 @@ let th = top_thm ();;
 
 #use"TacticRecording/mlexport.ml";;
 
-print_executed_proof ();;
-print_flat_proof ();;
+print_executed_proof true;;
+print_flat_proof true;;
 print_thenl_proof ();;
-print_optimal_proof ();;
+print_packaged_proof ();;
+print_gv_proof ();;
 
 g `(y:A) = z ==> (x:A) = x /\ y = y /\ z = z`;;
 e (STRIP_TAC);;
diff --git a/hol-light/TacticRecording/examples3.ml b/hol-light/TacticRecording/examples3.ml
index d0e181e2..62a2ef70 100644
--- a/hol-light/TacticRecording/examples3.ml
+++ b/hol-light/TacticRecording/examples3.ml
@@ -42,9 +42,14 @@ let LEMMA_1 = theorem_wrap "LEMMA_1" LEMMA_1;;
 
 top_thm ();;
 print_executed_proof true;;
-print_flat_proof false;;
+print_flat_proof true;;
 print_packaged_proof ();;
 print_thenl_proof ();;
+print_gv_proof ();;
+
+let gtr = !the_goal_tree;;
+let h = gtree_to_hiproof gtr;;
+let h' = (trivsimp_hiproof o dethen_hiproof) h;;
 
 g `!x n. x pow (n + 1) - (&n + &1) * x + &n =
          (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`;;
@@ -82,6 +87,7 @@ let LEMMA_2 = theorem_wrap "LEMMA_2" LEMMA_2;;
 print_executed_proof true;;
 print_flat_proof true;;
 print_packaged_proof ();;
+print_gv_proof ();;
 
 g `!n x. &0 <= x ==> &0 <= x pow (n + 1) - (&n + &1) * x + &n`;;
 
@@ -123,11 +129,68 @@ print_executed_proof true;;
 print_flat_proof true;;
 print_thenl_proof ();;
 print_packaged_proof ();;
+print_gv_proof ();;
 
 g `!n x. 1 <= n /\ (!i. 1 <= i /\ i <= n + 1 ==> &0 <= x i)
          ==> x(n + 1) * (sum(1..n) x / &n) pow n
                 <= (sum(1..n+1) x / (&n + &1)) pow (n + 1)`;;
 
+print_flat_proof true;;
+e (STRIP_TAC);;
+e (STRIP_TAC);;
+e (STRIP_TAC);;
+e (ABBREV_TAC `a = sum (1..n + 1) x / (&n + &1)`);;
+e (ABBREV_TAC `b = sum (1..n) x / &n`);;
+e (SUBGOAL_THEN `x (n + 1) = (&n + &1) * a - &n * b` SUBST1_TAC);;
+(* *** Subgoal 1 *** *)
+e (EXPAND_TAC "a");;
+e (EXPAND_TAC "b");;
+e (ASM_SIMP_TAC [REAL_DIV_LMUL; REAL_OF_NUM_EQ; LE_1; REAL_ARITH `~(&n + &1 = &0)`]);;
+e (SIMP_TAC [SUM_ADD_SPLIT; ARITH_RULE `1 <= n + 1`; SUM_SING_NUMSEG]);;
+e (REAL_ARITH_TAC);;
+(* *** Subgoal 2 *** *)
+e (SUBGOAL_THEN `&0 <= a /\ &0 <= b` STRIP_ASSUME_TAC);;
+(* *** Subgoal 2.1 *** *)
+e (EXPAND_TAC "a");;
+e (EXPAND_TAC "b");;
+e (CONJ_TAC);;
+(* *** Subgoal 2.1.1 *** *)
+e (MATCH_MP_TAC REAL_LE_DIV);;
+e (CONJ_TAC);;
+(* *** Subgoal 2.1.1.1 *** *)
+e (MATCH_MP_TAC SUM_POS_LE_NUMSEG);;
+e (ASM_SIMP_TAC [ARITH_RULE `p <= n ==> p <= n + 1`]);;
+(* *** Subgoal 2.1.1.2 *** *)
+e (REAL_ARITH_TAC);;
+(* *** Subgoal 2.1.2 *** *)
+e (MATCH_MP_TAC REAL_LE_DIV);;
+e (CONJ_TAC);;
+(* *** Subgoal 2.1.2.1 *** *)
+e (MATCH_MP_TAC SUM_POS_LE_NUMSEG);;
+e (ASM_SIMP_TAC [ARITH_RULE `p <= n ==> p <= n + 1`]);;
+(* *** Subgoal 2.1.2.2 *** *)
+e (REAL_ARITH_TAC);;
+(* *** Subgoal 2.2 *** *)
+e (ASM_CASES_TAC `b = &0`);;
+(* *** Subgoal 2.2.1 *** *)
+e (ASM_SIMP_TAC [REAL_POW_ZERO;LE_1;REAL_MUL_RZERO;REAL_POW_LE]);;
+(* *** Subgoal 2.2.2 *** *)
+e (ASM_SIMP_TAC [REAL_POW_ZERO;LE_1;REAL_MUL_RZERO;REAL_POW_LE]);;
+e (MP_TAC (ISPECL [`n`;`a / b`] LEMMA_2));;
+e (ASM_SIMP_TAC [REAL_LE_DIV]);;
+e (REWRITE_TAC [REAL_ARITH `&0 <= x - a + b <=> a - b <= x`; REAL_POW_DIV]);;
+e (SUBGOAL_THEN `&0 < b` ASSUME_TAC);;
+(* *** Subgoal 2.2.2.1 *** *)
+e (ASM_REAL_ARITH_TAC);;
+(* *** Subgoal 2.2.2.2 *** *)
+e (ASM_SIMP_TAC [REAL_LE_RDIV_EQ;REAL_POW_LT]);;
+e (MATCH_MP_TAC EQ_IMP);;
+e (AP_THM_TAC);;
+e (AP_TERM_TAC);;
+e (REWRITE_TAC [REAL_POW_ADD]);;
+e (UNDISCH_TAC `~(b = &0)`);;
+e (CONV_TAC REAL_FIELD);;
+
 (* AGM *)
 
 let AGM = prove
diff --git a/hol-light/TacticRecording/examples3_LEMMA1.dot b/hol-light/TacticRecording/examples3_LEMMA1.dot
new file mode 100644
index 00000000..69bc7c4a
--- /dev/null
+++ b/hol-light/TacticRecording/examples3_LEMMA1.dot
@@ -0,0 +1,24 @@
+digraph G {
+  subgraph cluster0 {
+    label = "induction";
+    517->518;
+    517->519;
+  }
+  subgraph cluster1 {
+    label = "base case";
+    528->528
+  }
+  subgraph cluster2 {
+    label = "step case";
+    537->538;
+    538->540;
+    540->542;
+    542->544;
+    544->546;
+    546->548;
+  }
+  512->513;
+  513->517;
+  518->528;
+  519->537;
+}
\ No newline at end of file
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;;
diff --git a/hol-light/TacticRecording/hiproofs.ml b/hol-light/TacticRecording/hiproofs.ml
index 41941cde..4adee607 100644
--- a/hol-light/TacticRecording/hiproofs.ml
+++ b/hol-light/TacticRecording/hiproofs.ml
@@ -27,9 +27,9 @@
 (* indicates a tactic that completes its goal.                                *)
 
 type hiproof =
-    Hactive                             (* Active subgoal *)
-  | Hatomic of (finfo * int)            (* Atomic tactic + arity *)
-  | Hidentity                           (* Null, for wiring *)
+    Hactive of goalid                   (* Active subgoal *)
+  | Hatomic of (goalid * int)           (* Atomic tactic + arity *)
+  | Hidentity of goalid                 (* Null, for wiring *)
   | Hlabelled of (label * hiproof)      (* Box *)
   | Hsequence of (hiproof * hiproof)    (* Serial application *)
   | Htensor of hiproof list             (* Parallel application *)
@@ -47,19 +47,21 @@ let dest_hsequence h =
 
 let is_hsequence h = can dest_hsequence h;;
 
-let dest_atomic_hiproof h =
+let is_hidentity h = match h with Hidentity _ -> true | _ -> false;;
+
+let hiproof_id h =
   match h with
-    Hatomic (info,n) -> (info,n)
-  | _ -> failwith "dest_atomic_hiproof: Not an atomic hiproof";;
+    Hactive id | Hatomic (id,_) | Hidentity id -> id
+  | _  -> failwith "hiproof_id: Not a unit hiproof";;
 
 
 (* Arity *)
 
 let rec hiproof_arity h =
   match h with
-    Hactive           -> 1
+    Hactive _         -> 1
   | Hatomic (_,n)     -> n
-  | Hidentity         -> 1
+  | Hidentity _       -> 1
   | Hlabelled (_,h0)  -> hiproof_arity h0
   | Hsequence (h1,h2) -> hiproof_arity h2
   | Htensor hs        -> sum (map hiproof_arity hs)
@@ -74,6 +76,29 @@ type hitrace =
 
 
 
+(* ** TRANSLATION OF GOAL TREE TO HIPROOF ** *)
+
+
+let rec gtree_to_hiproof gtr =
+  let id = gtree_id gtr in
+  let (_,gtrm) = gtr in
+  match !gtrm with
+    Gactive
+       -> Hactive id
+  | Gexit _
+       -> Hidentity id
+  | Gexecuted (gstp,gtrs)
+       -> let h1 =
+             match gstp with
+               Gatom _ | Gbox (_,_,true)
+                  -> Hatomic (id, length gtrs)
+             | Gbox (l,gtr,false)
+                  -> Hlabelled (l, gtree_to_hiproof gtr) in
+          let h2 = Htensor (map gtree_to_hiproof gtrs) in
+          Hsequence (h1,h2);;
+
+
+
 (* ** REFACTORING OPERATIONS ** *)
 
 
@@ -118,22 +143,27 @@ let collapse_tensor h hs =
 let trivsimp_hiproof h =
   let trivsimp h =
      match h with
-       Hatomic ((Some"ALL_TAC",[]), _) -> Hidentity
-     | Hsequence (h1, Hempty)    -> h1
-     | Hsequence (h1, Hidentity) -> h1
-     | Hsequence (Hidentity, h2) -> h2
-     | Htensor []    -> Hempty
-     | Htensor [h0]  -> h0
-     | Htensor hs0   -> if (forall (fun h0 -> h0 = Hidentity) hs0)
-                          then Hidentity
-                          else Htensor (foldr collapse_tensor hs0 [])
-     | _   -> h in
+       Hatomic (id,_) when (gtree_tactic (get_gtree id) = (Some "ALL_TAC",[]))
+                                   -> Hidentity id
+     | Hsequence (h1, Hempty)      -> h1
+     | Hsequence (h1, Hidentity _) -> h1
+     | Hsequence (h1, Htensor hs2) -> if (forall is_hidentity hs2)
+                                        then h1
+                                        else h
+     | Hsequence (Hidentity _, h2) -> h2
+     | Hsequence (Htensor hs1, h2) -> if (forall is_hidentity hs1)
+                                        then h2
+                                        else h
+     | Htensor []                  -> Hempty
+     | Htensor [h0]                -> h0
+     | Htensor hs0                 -> Htensor (foldr collapse_tensor hs0 [])
+     | _  -> h in
   refactor_hiproof true trivsimp h;;
 
 
 (* Matching up lists of hiproofs *)
 
-let rec matchup_hiproofs hs1 hs2 =
+let rec matchup_hiproofs0 hs1 hs2 =
   match hs1 with
     [] -> []
   | h1::hs01
@@ -144,11 +174,16 @@ let rec matchup_hiproofs hs1 hs2 =
                        then failwith "matchup_hiproofs: unknown arity"
                        else failwith "matchup_hiproofs: Internal error - \
                                                       inconsistent arities" in
-          Hsequence (h1, Htensor hs2a) :: (matchup_hiproofs hs01 hs2b);;
+          (h1,hs2a) :: (matchup_hiproofs0 hs01 hs2b);;
+
+let matchup_hiproofs hs1 hs2 =
+  let hhs = matchup_hiproofs0 hs1 hs2 in
+  map (fun (h1,hs2) -> Hsequence (h1, Htensor hs2)) hhs;;
 
 
 (* Separating out lists of hiproofs *)
 
+(*
 let separate_hiproofs0 h (hs01,hs02) =
   match h with
     Hsequence (h1,h2)
@@ -158,6 +193,7 @@ let separate_hiproofs0 h (hs01,hs02) =
           (h::hs01, h2::hs02);;
 
 let separate_hiproofs hs = foldr separate_hiproofs0 hs ([],[]);;
+*)
 
 
 (* Delabelling *)
@@ -176,6 +212,14 @@ let delabel_hiproof h =
      | _  -> h in
   refactor_hiproof true delabel h;;
 
+let dethen_hiproof h =
+  let dethen h =
+     match h with
+       Hlabelled (Tactical (Some ("THEN" | "THENL"),_), h0)
+          -> h0
+     | _  -> h in
+  refactor_hiproof true dethen h;;
+
 
 (* Right-grouping *)
 
@@ -189,6 +233,8 @@ let rightgroup_hiproof h =
           -> Hsequence (h1, Htensor (matchup_hiproofs hs2 hs3))
      | Hsequence (Hsequence (h1, Htensor hs2), h3)
           -> Hsequence (h1, Htensor (matchup_hiproofs hs2 [h3]))
+     | Hsequence (Hsequence (h1,h2), h3)
+          -> Hsequence (h1, Hsequence (h2,h3))
      | _  -> h in
   refactor_hiproof true rightgroup h;;
 
@@ -234,21 +280,94 @@ let thenise_hiproof h =
 
 
 
+(* ** HIPROOF GRAPH ** *)
+
+
+(* Graph element datatype *)
+
+type graph_elem =
+    Box of (label * graph_elem list)
+  | Line of (goalid * goalid)
+  | Single of goalid;;
+
+let is_box ge =
+  match ge with Box _ -> true | _ -> false;;
+
+let mk_line id1 id2 = Line (id1,id2);;
+
+
+(* Utils *)
+
+let rec hiproof_ins h =
+  match h with
+    Hactive id        -> [id]
+  | Hatomic (id,n)    -> [id]
+  | Hidentity id      -> [-1]
+  | Hlabelled (l,h0)  -> hiproof_ins h0
+  | Hsequence (h1,h2) -> hiproof_ins h1
+  | Htensor hs        -> flat (map hiproof_ins hs)
+  | Hempty            -> [];;
+
+let rec hiproof_outs (h:hiproof) : goalid list =
+  match h with
+    Hactive id        -> [id]
+  | Hatomic (id,n)    -> copy n id
+  | Hidentity id      -> [id]
+  | Hlabelled (l,h0)  -> hiproof_outs h0
+  | Hsequence (h1, Htensor hs2)
+       -> let nhs2 = enumerate hs2 in
+          let ids1 = hiproof_outs h1 in
+          let foo (n2,h2) =
+             if (is_hidentity h2) then [el (n2-1) ids1]
+                                  else hiproof_outs h2 in
+          flat (map foo nhs2)
+  | Hsequence (h1,h2) -> hiproof_outs h2
+  | Htensor hs        -> flat (map hiproof_outs hs)
+  | Hempty            -> [];;
+
+
+(* Graph production *)
+
+let rec hiproof_graph0 h =
+  match h with
+    Hactive _      -> []
+  | Hatomic _      -> []
+  | Hidentity _    -> []
+  | Hlabelled (l,Hatomic (id,_))
+       -> [Box (l, [Single id])]
+  | Hlabelled (l,h0)
+       -> [Box (l, hiproof_graph0 h0)]
+  | Hsequence (h1,h2)
+       -> let idids = zip (hiproof_outs h1) (hiproof_ins h2) in
+          let idids' = filter (fun (_,id2) -> (id2 > 0)) idids in
+          (hiproof_graph0 h1) @
+          (map (fun idid -> Line idid) idids') @
+          (hiproof_graph0 h2)
+  | Htensor hs     -> flat (map hiproof_graph0 hs)
+  | Hempty         -> [];;
+
+let hiproof_graph h =
+  let ges = hiproof_graph0 h in
+  let (ges1,ges2) = partition is_box ges in
+  ges1 @ ges2;;
+
+
+
 (* ** OTHER OPERATIONS ** *)
 
 
 (* Tactic trace *)
 
-(* Gives a trace of the basic tactics used in the proof, ignoring how they    *)
-(* were combined by tacticals.                                                *)
+(* Gives a linear trace of the basic tactics used in the proof, ignoring how  *)
+(* they were combined by tacticals.                                           *)
 
 let rec hiproof_tactic_trace0 h =
   match h with
-    Hactive
+    Hactive _
        -> [active_info]
-  | Hatomic (info, _)
-       -> [info]
-  | Hidentity
+  | Hatomic (id, _)
+       -> [gtree_tactic (get_gtree id)]
+  | Hidentity _
        -> []
   | Hlabelled (_,h0)
        -> hiproof_tactic_trace0 h0
@@ -264,7 +383,7 @@ let hiproof_tactic_trace h = (hiproof_tactic_trace0 o delabel_hiproof) h;;
 
 (* Block trace *)
 
-(* Gives a trace of the hiproofs used in the proof, stopping at boxes.        *)
+(* Gives a linear trace of the hiproofs used in the proof, stopping at boxes. *)
 
 let rec hiproof_block_trace0 ns0 h =
   match h with
diff --git a/hol-light/TacticRecording/lib.ml b/hol-light/TacticRecording/lib.ml
index ae66892e..b1309f84 100644
--- a/hol-light/TacticRecording/lib.ml
+++ b/hol-light/TacticRecording/lib.ml
@@ -4,6 +4,13 @@ let rec copy n x =
              else [];;
 
 
+let rec enumerate0 n xs =
+  match xs with
+    []     -> []
+  | x::xs0 -> (n,x)::enumerate0 (n+1) xs0;;
+let enumerate xs = enumerate0 1 xs;;
+
+
 (* foldr : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b                            *)
 
 let rec foldr f xs a =
diff --git a/hol-light/TacticRecording/main.ml b/hol-light/TacticRecording/main.ml
index 44c01951..bfdc1488 100644
--- a/hol-light/TacticRecording/main.ml
+++ b/hol-light/TacticRecording/main.ml
@@ -15,9 +15,14 @@
 
 #use "TacticRecording/prooftree.ml";;
 
-(* Hiproofs, refactoring and export *)
+(* Hiproofs & refactoring *)
 
 #use "TacticRecording/hiproofs.ml";;
+
+(* Export *)
+
+#use "TacticRecording/printutils.ml";;
+#use "TacticRecording/gvexport.ml";;
 #use "TacticRecording/mlexport.ml";;
 
 (* Overwriting the existing HOL Light objects *)
diff --git a/hol-light/TacticRecording/mlexport.ml b/hol-light/TacticRecording/mlexport.ml
index d790deee..429cb770 100644
--- a/hol-light/TacticRecording/mlexport.ml
+++ b/hol-light/TacticRecording/mlexport.ml
@@ -8,74 +8,11 @@
 
 
 (* Routines for exporting an ML tactic proof script from the recorded tactic  *)
-(* proof tree.                                                                *)
+(* proof tree, via a hiproof representation.                                  *)
 
 
 
-(* Translation to hiproof *)
-
-let rec gtree_to_hiproof gtr =
-  let (_,gtrm) = gtr in
-  match !gtrm with
-    Gactive
-       -> Hactive
-  | Gexit id
-       -> Hidentity
-  | Gexecuted (gstp,gtrs)
-       -> let h1 =
-             match gstp with
-               Gatom info | Gbox (Tactical info, _, true)
-                  -> Hatomic (info, length gtrs)
-             | Gbox (l,gtr,false)
-                  -> Hlabelled (l, gtree_to_hiproof gtr) in
-          let h2 = Htensor (map gtree_to_hiproof gtrs) in
-          Hsequence (h1,h2);;
-
-
-
-(* ** PRINT UTILITIES ** *)
-
-
-(* Basics *)
-
-let print_string_if b x = if b then print_string x;;
-
-let print_fstring x = print_string ("\"" ^ String.escaped x ^ "\"");;
-
-let print_fterm tm = print_string ("`" ^ string_of_term tm ^ "`");;
-
-let print_ftype ty = print_string ("`" ^ string_of_type ty ^ "`");;
-
-
-(* Printer for 'finfo' *)
-
-let rec print_farg x0 br arg =
-  match arg with
-    Fint n       -> print_int n
-  | Fstring x    -> print_fstring x
-  | Fterm tm     -> print_fterm tm
-  | Ftype ty     -> print_ftype ty
-  | Fthm prf     -> print_finfo "<rule>" br prf
-  | Fpair (arg1,arg2)
-       -> let sep = if (forall is_atomic_farg [arg1;arg2]) then "," else ", " in
-          (print_string_if br "(";
-           print_farg x0 false arg1;
-           print_string sep;
-           print_farg x0 false arg2;
-           print_string_if br ")")
-  | Flist args 
-       -> let sep = if (forall is_atomic_farg args) then ";" else "; " in
-          (print_string "[";
-           print_seplist (print_farg x0 false) sep args;
-           print_string "]")
-  | Ffn f
-       -> (print_finfo x0 br f)
-
-and print_finfo x0 br ((x_,args):finfo) =
-  (print_string_if (br & not (is_empty args)) "(";
-   print_option x0 x_;
-   do_list (fun arg -> print_string " "; print_farg x0 true arg) args;
-   print_string_if (br & not (is_empty args)) ")");;
+(* ** UTILS ** *)
 
 
 (* Printer for tactic 'finfo' *)
@@ -116,11 +53,11 @@ let print_hitrace_line_with fl pr htr =
 
 let print_hiproof0 pr br h =
   match h with
-    Hactive
+    Hactive _
        -> print_string "..."
-  | Hatomic (info,_)
-       -> print_tactic br info
-  | Hidentity
+  | Hatomic (id,_)
+       -> print_tactic br (gtree_tactic (get_gtree id))
+  | Hidentity _
        -> print_string "ALL_TAC"
   | Hlabelled (_,h0)
        -> pr br h0
diff --git a/hol-light/TacticRecording/printutils.ml b/hol-light/TacticRecording/printutils.ml
new file mode 100644
index 00000000..9131e18d
--- /dev/null
+++ b/hol-light/TacticRecording/printutils.ml
@@ -0,0 +1,61 @@
+(* ========================================================================== *)
+(* PRINTER UTILITIES (HOL LIGHT)                                              *)
+(* - Various basic utilities used in writing the exporters                    *)
+(*                                                                            *)
+(* By Mark Adams                                                              *)
+(* Copyright (c) Univeristy of Edinburgh, 2012                                *)
+(* ========================================================================== *)
+
+
+(* Basics *)
+
+let print_string_if b x = if b then print_string x;;
+
+let print_fstring x = print_string ("\"" ^ String.escaped x ^ "\"");;
+
+let print_fterm tm = print_string ("`" ^ string_of_term tm ^ "`");;
+
+let print_ftype ty = print_string ("`" ^ string_of_type ty ^ "`");;
+
+let print_goalid id = print_int id;;
+
+let print_indent d = print_string (String.make d ' ');;
+
+
+(* Printer for 'finfo' *)
+
+let rec print_farg x0 br arg =
+  match arg with
+    Fint n       -> print_int n
+  | Fstring x    -> print_fstring x
+  | Fterm tm     -> print_fterm tm
+  | Ftype ty     -> print_ftype ty
+  | Fthm prf     -> print_finfo "<rule>" br prf
+  | Fpair (arg1,arg2)
+       -> let sep = if (forall is_atomic_farg [arg1;arg2]) then "," else ", " in
+          (print_string_if br "(";
+           print_farg x0 false arg1;
+           print_string sep;
+           print_farg x0 false arg2;
+           print_string_if br ")")
+  | Flist args 
+       -> let sep = if (forall is_atomic_farg args) then ";" else "; " in
+          (print_string "[";
+           print_seplist (print_farg x0 false) sep args;
+           print_string "]")
+  | Ffn f
+       -> (print_finfo x0 br f)
+
+and print_finfo x0 br ((x_,args):finfo) =
+  (print_string_if (br & not (is_empty args)) "(";
+   print_option x0 x_;
+   do_list (fun arg -> print_string " "; print_farg x0 true arg) args;
+   print_string_if (br & not (is_empty args)) ")");;
+
+
+(* Printer for labels *)
+
+let print_label l =
+  match l with
+    Tactical (Some x, _) | Label x  -> print_fstring x
+  | Tactical (None, _)              -> print_fstring "<tactical>";;