diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 03:10:54 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 21:26:40 +0100 |
commit | f39543a752d05e5661749bbc3f221d75e525b3b4 (patch) | |
tree | 63f0b0a9f9339a0b1e0b1086afa0346216a1f4d5 | |
parent | 6afe572a4448e50f18e408097dd9ed03cc432d39 (diff) |
Moving Tactic_debug to Hightactic.
-rw-r--r-- | dev/printers.mllib | 1 | ||||
-rw-r--r-- | tactics/hightactics.mllib | 1 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
-rw-r--r-- | tactics/tactic_debug.ml | 20 | ||||
-rw-r--r-- | tactics/tactic_debug.mli | 4 | ||||
-rw-r--r-- | tactics/tactics.mllib | 1 | ||||
-rw-r--r-- | toplevel/cerrors.ml | 28 | ||||
-rw-r--r-- | toplevel/cerrors.mli | 1 |
8 files changed, 34 insertions, 24 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index a3ba42ba7..aad56f586 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -201,7 +201,6 @@ Egramml Egramcoq Tacsubst Tacenv -Tactic_debug Trie Dn Btermdn diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 468b938b6..76455f4ac 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,3 +1,4 @@ +Tactic_debug Tacintern Tacentries Tacinterp diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 6bf0e2aa7..5dab244af 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -365,7 +365,7 @@ let debugging_exception_step ist signal_anomaly e pp = if signal_anomaly then explain_logic_error else explain_logic_error_no_anomaly in debugging_step ist (fun () -> - pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ !explain_exc e) + pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e) let error_ltac_variable loc id env v s = user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ diff --git a/tactics/tactic_debug.ml b/tactics/tactic_debug.ml index e991eb86d..d661f9677 100644 --- a/tactics/tactic_debug.ml +++ b/tactics/tactic_debug.ml @@ -14,6 +14,7 @@ open Termops open Nameops open Proofview.Notations + let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () let prtac x = @@ -34,9 +35,11 @@ type debug_info = | DebugOff (* An exception handler *) -let explain_logic_error = ref (fun e -> mt()) +let explain_logic_error e = + Errors.print (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) -let explain_logic_error_no_anomaly = ref (fun e -> mt()) +let explain_logic_error_no_anomaly e = + Errors.print_no_report (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl()) let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) @@ -202,7 +205,7 @@ let debug_prompt lev tac f = (Proofview.tclLIFT begin (skip:=0) >> (skipped:=0) >> if Logic.catchable_exception reraise then - msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise) + msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ explain_logic_error reraise) else return () end) (Proofview.tclZERO ~info reraise) @@ -304,7 +307,7 @@ let db_logic_failure debug err = is_debug debug >>= fun db -> if db then begin - msg_tac_debug (Pervasives.(!) explain_logic_error err) >> + msg_tac_debug (explain_logic_error err) >> msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++ str "Let us try the next one...") end @@ -398,3 +401,12 @@ let extract_ltac_trace trace eloc = | [] -> Loc.ghost in aux trace in None, best_loc + +let get_ltac_trace (_, info) = + let ltac_trace = Exninfo.get info ltac_trace_info in + let loc = Option.default Loc.ghost (Loc.get_loc info) in + match ltac_trace with + | None -> None + | Some trace -> Some (extract_ltac_trace trace loc) + +let () = Cerrors.register_additional_error_info get_ltac_trace diff --git a/tactics/tactic_debug.mli b/tactics/tactic_debug.mli index 523398e75..520fb41ef 100644 --- a/tactics/tactic_debug.mli +++ b/tactics/tactic_debug.mli @@ -61,13 +61,13 @@ val db_matching_failure : debug_info -> unit Proofview.NonLogical.t val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t (** An exception handler *) -val explain_logic_error: (exn -> Pp.std_ppcmds) ref +val explain_logic_error: exn -> Pp.std_ppcmds (** 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 +val explain_logic_error_no_anomaly : exn -> Pp.std_ppcmds (** Prints a logic failure message for a rule *) val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index b495a885f..c290ce228 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -20,5 +20,4 @@ Tacenv Hints Auto Tactic_matching -Tactic_debug Term_dnet diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 0b8edd91c..4f3ffbcae 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -110,6 +110,11 @@ let rec strip_wrapping_exceptions = function strip_wrapping_exceptions e | exc -> exc +let additional_error_info = ref [] + +let register_additional_error_info f = + additional_error_info := f :: !additional_error_info + let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) = let exc = strip_wrapping_exceptions exc in let e = process_vernac_interp_error with_header (exc, info) in @@ -120,19 +125,12 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, let err = Errors.make_anomaly msg in Util.iraise (err, info) in - let ltac_trace = Exninfo.get info Tactic_debug.ltac_trace_info in - let loc = Option.default Loc.ghost (Loc.get_loc info) in - match ltac_trace with + let e' = + try Some (CList.find_map (fun f -> f e) !additional_error_info) + with _ -> None + in + match e' with | None -> e - | Some trace -> - let (e, info) = e in - match Tactic_debug.extract_ltac_trace trace loc with - | None, loc -> (e, Loc.add_loc info loc) - | Some msg, loc -> - (EvaluatedError (msg, Some e), Loc.add_loc info loc) - -let _ = Tactic_debug.explain_logic_error := - (fun e -> Errors.print (fst (process_vernac_interp_error (e, Exninfo.null)))) - -let _ = Tactic_debug.explain_logic_error_no_anomaly := - (fun e -> Errors.print_no_report (fst (process_vernac_interp_error (e, Exninfo.null)))) + | Some (None, loc) -> (fst e, Loc.add_loc (snd e) loc) + | Some (Some msg, loc) -> + (EvaluatedError (msg, Some (fst e)), Loc.add_loc (snd e) loc) diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 68c46010b..a0e3e3c19 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -19,3 +19,4 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> U val explain_exn_default : exn -> Pp.std_ppcmds +val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option * Loc.t) option) -> unit |