Tactiques utilisateur + debugger

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@786 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 47 insertions, 0 deletions

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
new file mode 100644
index 0000000000..d9c5d528a7
--- /dev/null
+++ b/proofs/tactic_debug.ml
@@ -0,0 +1,47 @@
+open Ast
+open Pp
+open Printer
+
+(* This module intends to be a beginning of debugger for tactic expressions.
+   Currently, it is quite simple and we can hope to have, in the future, a more
+   complete panel of commands dedicated to a proof assistant framework *)
+
+(* Debug information *)
+type debug_info =
+  | DebugOn
+  | DebugOff
+  | Exit
+
+(* Prints the goal if it exists *)
+let db_pr_goal = function
+  | None -> mSGNL [< 'sTR "No goal" >]
+  | Some g ->
+    mSGNL [<'sTR ("Goal:"); 'fNL; Proof_trees.pr_goal (Tacmach.sig_it g) >]
+
+(* Prints the state and waits for an instruction *)
+let debug_prompt goalopt tac_ast =
+  db_pr_goal goalopt;
+  mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL; 'fNL;
+         'sTR "----<Enter>=Continue----s=Skip----x=Exit----" >];
+  let rec prompt () =
+    mSG [<'fNL; 'sTR "TcDebug> " >];
+    flush stdout;
+    let inst = read_line () in
+    mSGNL [<>];
+    match inst with
+    | ""  -> DebugOn
+    | "s" -> DebugOff
+    | "x" -> Exit
+    | _   -> prompt () in
+  prompt ()
+
+(* Prints a matched hypothesis *)
+let db_matched_hyp debug env (id,c) =
+  if debug = DebugOn then
+    mSGNL [< 'sTR "Matched hypothesis --> "; 'sTR (id^": ");
+             prterm_env env c >]
+
+(* Prints the matched conclusion *)
+let db_matched_concl debug env c =
+  if debug = DebugOn then
+    mSGNL [< 'sTR "Matched goal --> "; prterm_env env c >]