1 files changed, 61 insertions, 0 deletions
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>";;