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, 12 insertions, 0 deletions

diff --git a/hol-light/TacticRecording/graveyard.ml b/hol-light/TacticRecording/graveyard.ml
new file mode 100644
index 00000000..db5c733d
--- /dev/null
+++ b/hol-light/TacticRecording/graveyard.ml
@@ -0,0 +1,12 @@
+
+
+(* Utility for applying tactic and incorproating results into goal tree.      *)
+(* Takes an "infotactic", i.e. like a normal tactic that works on 'goal' and  *)
+(* returns 'goalstate', but that also returns 'finfo' which summarises the    *)
+(* operation.  These are easily formed by tagging normal tactics.             *)
+
+let infotactic_wrap0 (infotac:goal->(goalstate*finfo)) (gx:xgoal) : xgoalstate =
+  let (g,id) = dest_xgoal gx in
+  let ((meta,gs,just),gst) = infotac g in
+  let gxs = extend_gtree id gst gs in
+  (meta,gxs,just);;