Breakpoints in Ltac debugger: new command "r foo" to jump to the next

call to "idtac foo" in Ltac code.

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

2 files changed, 72 insertions, 32 deletions

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 1c2fb2787..7d7688873 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -49,11 +49,12 @@ let db_pr_goal g =
 
 (* Prints the commands *)
 let help () =
-  msgnl (str "Commands: <Enter>=Continue" ++ fnl() ++
-         str "          h/?=Help" ++ fnl() ++
-         str "          r<num>=Run <num> times" ++ fnl() ++
-         str "          s=Skip" ++ fnl() ++
-         str "          x=Exit")
+  msgnl (str "Commands: <Enter> = Continue" ++ fnl() ++
+         str "          h/? = Help" ++ fnl() ++
+         str "          r <num> = Run <num> times" ++ fnl() ++
+         str "          r <string> = Run up to next idtac <string>" ++ fnl() ++
+         str "          s = Skip" ++ fnl() ++
+         str "          x = Exit")
 
 (* Prints the goal and the command to be executed *)
 let goal_com g tac =
@@ -62,37 +63,56 @@ let goal_com g tac =
     msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ())
   end
 
-(* Gives the number of a run command *)
+let skipped = ref 0
+let skip = ref 0
+let breakpoint = ref None
+
+let rec drop_spaces inst i =
+  if String.length inst > i && inst.[i] = ' ' then drop_spaces inst (i+1)
+  else i
+
+(* (Re-)initialize debugger *)
+let db_initialize () =
+  skip:=0;skipped:=0;breakpoint:=None
+
+(* Gives the number of steps or next breakpoint of a run command *)
 let run_com inst =
   if (String.get inst 0)='r' then
-    let num = int_of_string (String.sub inst 1 ((String.length inst)-1)) in
-    if num>0 then num
-    else raise (Invalid_argument "run_com")
+    let i = drop_spaces inst 1 in
+    if String.length inst > i then
+      let s = String.sub inst i (String.length inst - i) in
+      if inst.[0] >= '0' && inst.[0] <= '9' then
+        let num = int_of_string s in
+        if num<0 then raise (Invalid_argument "run_com");
+        skip:=num;skipped:=0
+      else
+        breakpoint:=Some s
+    else
+      raise (Invalid_argument "run_com")
   else
     raise (Invalid_argument "run_com")
 
-let allskip = ref 0
-let skip = ref 0
-
 (* Prints the run counter *)
 let run ini =
   if not ini then
+  begin
     for i=1 to 2 do
       print_char (Char.chr 8);print_char (Char.chr 13)
     done;
-  msg (str "Executed expressions: " ++ int (!allskip - !skip) ++
-       fnl() ++ fnl())
+    msg (str "Executed expressions: " ++ int !skipped ++ fnl() ++ fnl())
+  end;
+  incr skipped
 
 (* Prints the prompt *)
 let rec prompt level =
   begin
     msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
     flush stdout;
-    let exit () = skip:=0;allskip:=0;raise Sys.Break in
+    let exit () = skip:=0;skipped:=0;raise Sys.Break in
     let inst = try read_line () with End_of_file -> exit () in
     match inst with
-    | ""  -> true
-    | "s" -> false
+    | ""  -> DebugOn (level+1)
+    | "s" -> DebugOff
     | "x" -> print_char (Char.chr 8); exit ()
     | "h"| "?" ->
       begin
@@ -100,32 +120,34 @@ let rec prompt level =
         prompt level
       end
     | _ ->
-      (try let ctr=run_com inst in skip:=ctr;allskip:=ctr;run true;true
+      (try run_com inst;run true;DebugOn (level+1)
        with Failure _ | Invalid_argument _ -> prompt level)
   end
 
 (* Prints the state and waits for an instruction *)
 let debug_prompt lev g tac f =
   (* What to print and to do next *)
-  let continue =
-    if !skip = 0 then (goal_com g tac; prompt lev)
-    else (decr skip; run false; if !skip=0 then allskip:=0; true) in
+  let newlevel =
+    if !skip = 0 then
+      if !breakpoint = None then (goal_com g tac; prompt lev)
+      else (run false; DebugOn (lev+1))
+    else (decr skip; run false; if !skip=0 then skipped:=0; DebugOn (lev+1)) in
   (* What to execute *)
-  try f (if continue then DebugOn (lev+1) else DebugOff)
+  try f newlevel
   with e ->
-    skip:=0; allskip:=0;
+    skip:=0; skipped:=0;
     if Logic.catchable_exception e then
       ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
     raise e
 
 (* Prints a constr *)
 let db_constr debug env c =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str "Evaluated term: " ++ print_constr_env env c)
 
 (* Prints the pattern rule *)
 let db_pattern_rule debug num r =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
   begin
     msgnl (str "Pattern rule " ++ int num ++ str ":");
     msgnl (str "|" ++ spc () ++ !prmatchrl r)
@@ -138,38 +160,38 @@ let hyp_bound = function
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,_,c) ido =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str "Hypothesis " ++
            str ((Names.string_of_id id)^(hyp_bound ido)^
                 " has been matched: ") ++ print_constr_env env c)
 
 (* Prints the matched conclusion *)
 let db_matched_concl debug env c =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str "Conclusion has been matched: " ++ print_constr_env env c)
 
 (* Prints a success message when the goal has been matched *)
 let db_mc_pattern_success debug =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str "The goal has been successfully matched!" ++ fnl() ++
            str "Let us execute the right-hand side part..." ++ fnl())
 
 (* Prints a failure message for an hypothesis pattern *)
 let db_hyp_pattern_failure debug env (na,hyp) =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str ("The pattern hypothesis"^(hyp_bound na)^
                 " cannot match: ") ++
            !prmatchpatt env hyp)
 
 (* Prints a matching failure message for a rule *)
 let db_matching_failure debug =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     msgnl (str "This rule has failed due to matching errors!" ++ fnl() ++
            str "Let us try the next one...")
 
 (* Prints an evaluation failure message for a rule *)
 let db_eval_failure debug s =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
     let s = str "message \"" ++ s ++ str "\"" in
     msgnl
       (str "This rule has failed due to \"Fail\" tactic (" ++
@@ -177,9 +199,20 @@ let db_eval_failure debug s =
 
 (* Prints a logic failure message for a rule *)
 let db_logic_failure debug err =
-  if debug <> DebugOff & !skip = 0 then
+  if debug <> DebugOff & !skip = 0 & !breakpoint = None then
   begin
     msgnl (!explain_logic_error err);
     msgnl (str "This rule has failed due to a logic error!" ++ fnl() ++
            str "Let us try the next one...")
   end
+
+let is_breakpoint brkname s = match brkname, s with
+  | Some s, MsgString s'::_ -> s = s'
+  | _ -> false
+
+let db_breakpoint debug s =
+  match debug with
+  | DebugOn lev when s <> [] & is_breakpoint !breakpoint s ->
+      breakpoint:=None
+  | _ ->
+      ()
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index d96f4c746..62c2359b6 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -34,6 +34,9 @@ type debug_info =
 val debug_prompt :
   int -> goal sigma -> glob_tactic_expr -> (debug_info -> 'a) -> 'a
 
+(** Initializes debugger *)
+val db_initialize : unit -> unit
+
 (** Prints a constr *)
 val db_constr : debug_info -> env -> constr -> unit
 
@@ -72,3 +75,7 @@ val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
 
 (** Prints a logic failure message for a rule *)
 val db_logic_failure : debug_info -> exn -> unit
+
+(** Prints a logic failure message for a rule *)
+val db_breakpoint : debug_info ->
+  identifier Util.located message_token list -> unit