improve the amount of information given by the Ltac tactic debugger

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

4 files changed, 188 insertions, 26 deletions

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 889e06a8b..96df8f641 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -31,6 +31,8 @@ type debug_info =
 (* An exception handler *)
 let explain_logic_error = ref (fun e -> mt())
 
+let explain_logic_error_no_anomaly = ref (fun e -> mt())
+
 (* Prints the goal *)
 let db_pr_goal g =
   msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Refiner.sig_it g))
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index a64965605..6da6dc61c 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -66,5 +66,11 @@ val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit
 (* An exception handler *)
 val explain_logic_error: (exn -> Pp.std_ppcmds) ref
 
+(* For use in the Ltac debugger: some exception that are usually
+   consider anomalies are acceptable because they are caught later in
+   the process that is being debugged.  One should not require
+   from users that they report these anomalies. *)
+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
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 20649674d..cfda82a98 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -48,6 +48,12 @@ open Pretyping
 open Pretyping.Default
 open Pcoq
 
+let safe_msgnl s =
+    try msgnl s with e -> 
+      msgnl 
+	(str "bug in the debugger : " ++
+         str "an exception is raised while printing debug information")
+
 let error_syntactic_metavariables_not_allowed loc =
   user_err_loc 
     (loc,"out_ident",
@@ -1296,11 +1302,39 @@ let interp_may_eval f ist gl = function
 	    user_err_loc (loc, "interp_may_eval",
 	    str "Unbound context identifier" ++ pr_id s))
   | ConstrTypeOf c -> pf_type_of gl (f ist gl c)
-  | ConstrTerm c -> f ist gl c
+  | ConstrTerm c -> 
+     try 
+	f ist gl c
+     with e -> 
+	begin 
+	  match ist.debug with 
+	    DebugOn lev -> 
+	    safe_msgnl (str "Level " ++ int lev ++
+                          str ": interpretation of term " ++ 
+			   Printer.pr_rawconstr_env (pf_env gl) (fst c) ++
+			   str " raised an exception" ++
+			   fnl() ++
+			   !Tactic_debug.explain_logic_error_no_anomaly e)
+	| _ -> ()
+     end;
+     raise e  
 
 (* Interprets a constr expression possibly to first evaluate *)
 let interp_constr_may_eval ist gl c =
-  let csr = interp_may_eval pf_interp_constr ist gl c in
+  let csr = 
+    try
+      interp_may_eval pf_interp_constr ist gl c
+    with e -> 
+      begin match ist.debug with
+	  DebugOn lev -> 
+	    safe_msgnl (str "Level " ++ int lev ++
+                           str ": evaluation of term raised an exception" ++
+			   fnl() ++
+			   !Tactic_debug.explain_logic_error_no_anomaly e)
+	| _ -> ()
+      end;
+      raise e
+  in
   begin
     db_constr ist.debug (pf_env gl) csr;
     csr
@@ -1481,7 +1515,31 @@ and interp_app ist gl fv largs loc =
     | VFun(olfun,var,body) ->
       let (newlfun,lvar,lval)=head_with_value (var,largs) in
       if lvar=[] then
-	let v = val_interp { ist with lfun=newlfun@olfun } gl body in
+	let v = 
+          let res = 
+	    try
+	      val_interp { ist with lfun=newlfun@olfun } gl body
+	    with e ->
+	      begin match ist.debug with
+		  DebugOn lev -> 
+		    safe_msgnl 
+		      (str "Level " ++ int lev ++ 
+			  str ": evaluation raises an exception" ++
+                          fnl() ++
+			  !Tactic_debug.explain_logic_error_no_anomaly e)
+		| _ -> ()
+	      end;
+	      raise e
+	  in
+	    (match ist.debug with
+		DebugOn lev -> 
+		  safe_msgnl (str "Level " ++ int lev ++ 
+				 str ": evaluation returns" ++ fnl() ++
+				 pr_value (Some (pf_env gl)) res)
+	      | _ -> ());
+	    res
+	in
+
         if lval=[] then locate_tactic_call loc v
 	else interp_app ist gl v lval loc
       else
@@ -1706,26 +1764,114 @@ and interp_match ist g lz constr lmr =
         (try eval_with_fail ist lz g t
          with e when is_match_catchable e -> apply_match ist csr [])
     | (Pat ([],Term c,mt))::tl ->
-        (try
-	  let lm = matches c csr in
-	  let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
-          eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt
-         with e when is_match_catchable e -> apply_match ist csr tl)
+        (try let lm = 
+              (try matches c csr with 
+                e -> 
+                  (match ist.debug with
+                    DebugOn lev ->
+                      safe_msgnl (str "Level " ++ int lev ++
+                             str ": matching with pattern" ++ fnl() ++
+                         Printer.pr_constr_pattern_env (pf_env g) c ++ fnl() ++
+                         str "raised the exception" ++ fnl() ++
+                         !Tactic_debug.explain_logic_error_no_anomaly e)
+                  | _ -> ()); raise e) in
+            (try let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
+               eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt
+            with e ->
+               (match ist.debug with
+                  DebugOn lev -> 
+                    safe_msgnl (str "rule body for pattern" ++ fnl() ++
+                    Printer.pr_constr_pattern_env (pf_env g) c ++ fnl() ++
+                    str "raised the exception" ++ fnl() ++
+                    !Tactic_debug.explain_logic_error_no_anomaly e)
+                | _ -> ()); raise e)
+         with e when is_match_catchable e ->
+            (match ist.debug with
+               DebugOn lev ->
+                 safe_msgnl (str "Level " ++ int lev ++ 
+                       str ":switching to the next rule");
+             | DebugOff -> ());
+            apply_match ist csr tl)
+
     | (Pat ([],Subterm (id,c),mt))::tl ->
         (try apply_match_subterm ist 0 (id,c) csr mt
          with PatternMatchingFailure -> apply_match ist csr tl)
     | _ ->
       errorlabstrm "Tacinterp.apply_match" (str
         "No matching clauses for match") in
-  let csr = interp_ltac_constr ist g constr in
+  let csr = 
+      try interp_ltac_constr ist g constr with
+        e -> (match ist.debug with
+               DebugOn lev ->
+               safe_msgnl (str "Level " ++ int lev ++ 
+                      str ": evaluation of the matched expression raised " ++
+                      str "the exception" ++ fnl() ++
+                      !Tactic_debug.explain_logic_error e)
+             | _ -> ()); raise e in
   let ilr = read_match_rule (fst (constr_list ist (pf_env g))) lmr in
-  apply_match ist csr ilr
+  let res = 
+     try apply_match ist csr ilr with
+       e -> 
+           begin match ist.debug with
+             DebugOn lev ->
+                safe_msgnl (str "Level " ++ int lev ++ 
+                        str ": match expression failed with error" ++ fnl() ++
+                    !Tactic_debug.explain_logic_error e)
+           | _ -> ()
+           end;
+           raise e in
+     (if ist.debug <> DebugOff then
+     safe_msgnl (str "match expression returns " ++
+            pr_value (Some (pf_env g)) res));
+     res
 
 (* Interprets tactic expressions : returns a "constr" *)
 and interp_ltac_constr ist gl e =
-  try constr_of_value (pf_env gl) (val_interp ist gl e)
+  let result = 
+  try (val_interp ist gl e) with Not_found -> 
+    begin match ist.debug with
+      DebugOn lev ->
+       safe_msgnl (str "Level " ++ int lev ++ 
+                   str ": evaluation failed for" ++ fnl() ++
+                       Pptactic.pr_glob_tactic (pf_env gl) e)
+    | _ -> ()
+    end;
+    raise Not_found in
+  try let cresult = constr_of_value (pf_env gl) result in
+    (if !debug <> DebugOff then 
+        safe_msgnl (Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++
+        str " has value " ++ fnl() ++ print_constr_env (pf_env gl) cresult);
+     cresult)
+        
   with Not_found ->
-    errorlabstrm "" (str "Must evaluate to a term")
+    errorlabstrm ""
+      (str "Must evaluate to a term" ++ fnl() ++ 
+	  str "offending expression: " ++ fnl() ++
+          Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ str "this is a " ++
+          (match result with
+              VTactic _ -> str "VTactic"
+            | VRTactic _ -> str "VRTactic"
+            | VFun (il,ul,b) ->
+                (str "VFun with body " ++ fnl() ++
+                    Pptactic.pr_glob_tactic (pf_env gl) b ++ fnl() ++
+		    str "instantiated arguments " ++ fnl() ++
+                    List.fold_right 
+                    (fun p s ->
+                      let (i,v) = p in str (string_of_id i) ++ str ", " ++ s)
+                    il (str "") ++
+                    str "uninstantiated arguments " ++ fnl() ++
+                    List.fold_right
+                    (fun opt_id s ->
+                      (match opt_id with
+                          Some id -> str (string_of_id id)
+                        | None -> str "_") ++ str ", " ++ s)
+                    ul (str ""))
+            | VVoid -> str "VVoid"
+            | VInteger _ -> str "VInteger"
+            | VConstr _ -> str "VConstr"
+            | VIntroPattern _ -> str "VIntroPattern"
+            | VConstr_context _ -> str "VConstrr_context"
+            | VRec _ -> str "VRec"))
 
 (* Interprets tactic expressions : returns a "tactic" *)
 and interp_tactic ist tac gl =
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 35725c5bf..a1ac9f184 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -28,19 +28,21 @@ let guill s = "\""^s^"\""
 let where s =
   if !Options.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
 
+let anomaly_string () = str "Anomaly: "
+
 let report () = (str "." ++ spc () ++ str "Please report.")
 
 (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)
 
-let rec explain_exn_default = function
+let rec explain_exn_default_aux anomaly_string report_fn = function
   | Stream.Failure -> 
-      hov 0 (str "Anomaly: uncaught Stream.Failure.")
+      hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
   | Stream.Error txt -> 
       hov 0 (str "Syntax error: " ++ str txt)
   | Token.Error txt -> 
       hov 0 (str "Syntax error: " ++ str txt)
   | Sys_error msg -> 
-      hov 0 (str "Anomaly: uncaught exception Sys_error " ++ str (guill msg) ++ report ())
+      hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
   | UserError(s,pps) -> 
       hov 1 (str "User error: " ++ where s ++ pps)
   | Out_of_memory -> 
@@ -48,22 +50,22 @@ let rec explain_exn_default = function
   | Stack_overflow -> 
       hov 0 (str "Stack overflow")
   | Anomaly (s,pps) -> 
-      hov 1 (str "Anomaly: " ++ where s ++ pps ++ report ())
+      hov 1 (anomaly_string () ++ where s ++ pps ++ report_fn ())
   | Match_failure(filename,pos1,pos2) ->
-      hov 1 (str "Anomaly: Match failure in file " ++ str (guill filename) ++ 
+      hov 1 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ 
       if Sys.ocaml_version = "3.06" then
 		   (str " from character " ++ int pos1 ++ 
                     str " to " ++ int pos2)
 		 else
 		   (str " at line " ++ int pos1 ++
 		    str " character " ++ int pos2)
-	           ++ report ())
+	           ++ report_fn ())
   | Not_found -> 
-      hov 0 (str "Anomaly: uncaught exception Not_found" ++ report ())
+      hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report_fn ())
   | Failure s -> 
-      hov 0 (str "Anomaly: uncaught exception Failure " ++ str (guill s) ++ report ())
+      hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report_fn ())
   | Invalid_argument s -> 
-      hov 0 (str "Anomaly: uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
+      hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ())
   | Sys.Break -> 
       hov 0 (fnl () ++ str "User Interrupt.")
   | Univ.UniverseInconsistency -> 
@@ -97,7 +99,7 @@ let rec explain_exn_default = function
   | Stdpp.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
-               ++ explain_exn_default exc)
+               ++ explain_exn_default_aux anomaly_string report_fn exc)
   | Lexer.Error Illegal_character -> 
       hov 0 (str "Syntax error: Illegal character.")
   | Lexer.Error Unterminated_comment -> 
@@ -109,7 +111,7 @@ let rec explain_exn_default = function
   | Lexer.Error (Bad_token s) -> 
       hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".")
   | Assert_failure (s,b,e) ->
-      hov 0 (str "Anomaly: assert failure" ++ spc () ++
+      hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
 	       (if s <> "" then 
 		 if Sys.ocaml_version = "3.06" then
 		   (str ("(file \"" ^ s ^ "\", characters ") ++ 
@@ -120,16 +122,22 @@ let rec explain_exn_default = function
 		    int (e+6) ++ str ")")
 	       else
 		 (mt ())) ++
-	       report ())
+	       report_fn ())
   | reraise ->
-      hov 0 (str "Anomaly: Uncaught exception " ++ 
-	       str (Printexc.to_string reraise) ++ report ())
+      hov 0 (anomaly_string () ++ str "Uncaught exception " ++ 
+	       str (Printexc.to_string reraise) ++ report_fn ())
+
+let explain_exn_default =
+    explain_exn_default_aux (fun () -> str "Anomaly: ") report
 
 let raise_if_debug e =
   if !Options.debug then raise e
 
 let _ = Tactic_debug.explain_logic_error := explain_exn_default
 
+let _ = Tactic_debug.explain_logic_error_no_anomaly :=
+          explain_exn_default_aux (fun () -> mt()) (fun () -> mt())
+
 let explain_exn_function = ref explain_exn_default
 
 let explain_exn e = !explain_exn_function e