Restructuration interpréteur de tactique: plus d'évaluation partielle à la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif

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

1 files changed, 32 insertions, 8 deletions

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 43162f05d4..68d1425aa0 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -16,7 +16,7 @@ open Printer
 
 (* Debug information *)
 type debug_info =
-  | DebugOn
+  | DebugOn of int
   | DebugOff
   | Exit
 
@@ -31,20 +31,37 @@ let db_pr_goal = function
 let help () =
   msgnl (str "Commands: <Enter>=Continue, h=Help, s=Skip, x=Exit")
 
+(* Prints raised exceptions *)
+let rec db_print_error = function
+  | Type_errors.TypeError(ctx,te) -> 
+      hov 0 (str "Type error:" ++ spc ())
+  | Pretype_errors.PretypeError(ctx,te) ->
+      hov 0 (str "Pretype error:" ++ spc ())
+  | Logic.RefinerError e -> 
+      hov 0 (str "Refiner error:" ++ spc ())
+  | Stdpp.Exc_located (loc,exc) ->
+      db_print_error exc
+  | Util.UserError(s,pps) -> 
+      hov 1 (str"Error: " ++ pps)
+  | GlobalizationError q ->
+      hov 0 (str "Error: " ++ Libnames.pr_qualid q ++ str " not found") ++ 
+  | _ ->
+      hov 0 (str "Uncaught exception ")
+
 (* Prints the state and waits for an instruction *)
-let debug_prompt goalopt tac_ast =
+let debug_prompt level goalopt tac_ast f exit =
   db_pr_goal goalopt;
   msg (str "Going to execute:" ++ fnl () ++ (pr_raw_tactic tac_ast) ++ fnl ());
 (*         str "Commands: <Enter>=Continue, s=Skip, x=Exit" >];*)
 (*  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 > ");
+    msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
     flush stdout;
     let inst = read_line () in
 (*    mSGNL (mt ());*)
     match inst with
-    | ""  -> DebugOn
+    | ""  -> DebugOn (level+1)
     | "s" -> DebugOff
     | "x" -> Exit
     | "h" ->
@@ -53,20 +70,27 @@ let debug_prompt goalopt tac_ast =
         prompt ()
       end
     | _   -> prompt () in
-  prompt ()
+  match prompt () with
+    | Exit -> exit ()
+    | d ->
+	try f d
+	with e when Logic.catchable_exception e ->
+	  ppnl (str "Level " ++ int level ++ str ": " ++ db_print_error e); 
+	  raise e
 
 (* Prints a constr *)
 let db_constr debug env c =
-  if debug = DebugOn then
+  if debug <> DebugOff & debug <> Exit then
     msgnl (str "Evaluated term --> " ++ prterm_env env c)
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,c) =
-  if debug = DebugOn then
+  if debug <> DebugOff & debug <> Exit then
     msgnl (str "Matched hypothesis --> " ++ str (Names.string_of_id id^": ") ++
            prterm_env env c)
 
 (* Prints the matched conclusion *)
 let db_matched_concl debug env c =
-  if debug = DebugOn then
+  if debug <> DebugOff & debug <> Exit then
     msgnl (str "Matched goal --> " ++ prterm_env env c)
+