First version of HOL Light tactic recording.

See INSTRUCTIONS and LIMITATIONS files for more details.
Currently works for flattening "packaged-up" tactic proofs into g/e commands.
Won't work for most proofs because most tactics/thms haven't been promoted.
Support for exporting proof graph as a series of goal pairs.
Support for displaying extra information to be intercepter by PG for Prooftree.

1 files changed, 75 insertions, 0 deletions

diff --git a/hol-light/TacticRecording/lib.ml b/hol-light/TacticRecording/lib.ml
new file mode 100644
index 00000000..ae66892e
--- /dev/null
+++ b/hol-light/TacticRecording/lib.ml
@@ -0,0 +1,75 @@
+
+let rec copy n x =
+  if (n > 0) then x::(copy (n-1) x)
+             else [];;
+
+
+(* foldr : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b                            *)
+
+let rec foldr f xs a =
+  match xs with
+    x1::xs2 -> f x1 (foldr f xs2 a)
+  | []      -> a;;
+
+
+(* foldl : ('b -> 'a -> 'b) -> 'b -> 'a list -> 'b                            *)
+
+let rec foldl f a xs =
+  match xs with
+    x1::xs2 -> foldl f (f a x1) xs2
+  | []      -> a;;
+
+
+(* is_empty *)
+
+let is_empty xs =
+  match xs with
+    [] -> true
+  | _  -> false;;
+
+
+(* front *)
+
+let rec front xs =
+  match xs with
+    _::[]   -> []
+  | x0::xs0 -> x0::(front xs0)
+  | []      -> failwith "front: Empty list";;
+
+
+(* string_option *)
+
+let string_option x0 x_ =
+  match x_ with
+    Some x -> x
+  | None   -> x0;;
+
+
+(* print_option *)
+
+let print_option x0 x_ =
+  match x_ with
+    Some x -> print_string x
+  | None   -> print_string x0;;
+
+
+(* seplists *)
+
+let print_seplist p sep xs =
+  if (xs = [])
+    then ()
+    else (p (hd xs);
+          do_list (fun x -> print_string sep; p x) (tl xs));;
+
+let print_string_seplist sep xs =
+  print_seplist print_string sep xs;;
+
+
+(* sum *)
+
+let sum ns = foldl (+) 0 ns;;
+
+
+(* snd_map *)
+
+let snd_map f xys = map (fun (x,y) -> (x, f y)) xys;;