diff options
Diffstat (limited to 'toplevel/cerrors.ml')
| -rw-r--r-- | toplevel/cerrors.ml | 120 |
1 files changed, 64 insertions, 56 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 76f020dd..22ea09c5 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -1,28 +1,30 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat -open Pp open Util +open Pp +open Errors open Indtypes open Type_errors open Pretype_errors open Indrec let print_loc loc = - if loc = dummy_loc then + if Loc.is_ghost loc then (str"<unknown>") else - let loc = unloc loc in + let loc = Loc.unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) let guill s = "\""^s^"\"" +(** Invariant : exceptions embedded in EvaluatedError satisfy + Errors.noncritical *) exception EvaluatedError of std_ppcmds * exn option @@ -33,20 +35,16 @@ exception EvaluatedError of std_ppcmds * exn option let explain_exn_default = function (* Basic interaction exceptions *) | Stream.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ ".")) - | Token.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ ".")) + | Compat.Token.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ ".")) | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err)) | Sys_error msg -> hov 0 (str ("System error: " ^ guill msg)) | Out_of_memory -> hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") | Timeout -> hov 0 (str "Timeout!") | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") - (* Meta-exceptions *) - | Loc.Exc_located (loc,exc) -> - hov 0 ((if loc = dummy_loc then (mt ()) - else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) - ++ Errors.print_no_anomaly exc) + (* Exceptions with pre-evaluated error messages *) | EvaluatedError (msg,None) -> msg - | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise + | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print reraise (* Otherwise, not handled here *) | _ -> raise Errors.Unhandled @@ -55,67 +53,77 @@ let _ = Errors.register_handler explain_exn_default (** Pre-explain a vernac interpretation error *) -let wrap_vernac_error strm = - EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None) - -let rec process_vernac_interp_error = function - | Univ.UniverseInconsistency (o,u,v) -> - let msg = - if !Constrextern.print_universes then - spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++ - str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=") - ++ spc() ++ Univ.pr_uni v ++ str")" - else - mt() in - wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".") +let wrap_vernac_error (exn, info) strm = + let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in + let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in + (e, info) + +let process_vernac_interp_error exn = match fst exn with + | Univ.UniverseInconsistency i -> + let msg = + if !Constrextern.print_universes then + str "." ++ spc() ++ + Univ.explain_universe_inconsistency Universes.pr_with_global_universes i + else + mt() in + wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> - wrap_vernac_error (Himsg.explain_type_error ctx Evd.empty te) + wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te) | PretypeError(ctx,sigma,te) -> - wrap_vernac_error (Himsg.explain_pretype_error ctx sigma te) + wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) | Typeclasses_errors.TypeClassError(env, te) -> - wrap_vernac_error (Himsg.explain_typeclass_error env te) + wrap_vernac_error exn (Himsg.explain_typeclass_error env te) | InductiveError e -> - wrap_vernac_error (Himsg.explain_inductive_error e) + wrap_vernac_error exn (Himsg.explain_inductive_error e) | Modops.ModuleTypingError e -> - wrap_vernac_error (Himsg.explain_module_error e) + wrap_vernac_error exn (Himsg.explain_module_error e) | Modintern.ModuleInternalizationError e -> - wrap_vernac_error (Himsg.explain_module_internalization_error e) + wrap_vernac_error exn (Himsg.explain_module_internalization_error e) | RecursionSchemeError e -> - wrap_vernac_error (Himsg.explain_recursion_scheme_error e) - | Cases.PatternMatchingError (env,e) -> - wrap_vernac_error (Himsg.explain_pattern_matching_error env e) + wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e) + | Cases.PatternMatchingError (env,sigma,e) -> + wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> - wrap_vernac_error (Himsg.explain_reduction_tactic_error e) + wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) | Logic.RefinerError e -> - wrap_vernac_error (Himsg.explain_refiner_error e) + wrap_vernac_error exn (Himsg.explain_refiner_error e) | Nametab.GlobalizationError q -> - wrap_vernac_error + wrap_vernac_error exn (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ spc () ++ str "was not found" ++ spc () ++ str "in the current" ++ spc () ++ str "environment.") - | Nametab.GlobalizationConstantError q -> - wrap_vernac_error - (str "No constant of this name:" ++ spc () ++ - Libnames.pr_qualid q ++ str ".") | Refiner.FailError (i,s) -> - wrap_vernac_error + let s = Lazy.force s in + wrap_vernac_error exn (str "Tactic failure" ++ - (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++ - if i=0 then str "." else str " (level " ++ int i ++ str").") + (if Pp.is_empty s then s else str ": " ++ s) ++ + if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").") | AlreadyDeclared msg -> - wrap_vernac_error (msg ++ str ".") - | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () -> - process_vernac_interp_error exc - | Proof_type.LtacLocated (s,exc) -> - EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()), - Some (process_vernac_interp_error exc)) - | Loc.Exc_located (loc,exc) -> - Loc.Exc_located (loc,process_vernac_interp_error exc) - | exc -> - exc + wrap_vernac_error exn (msg ++ str ".") + | _ -> + exn + +let rec strip_wrapping_exceptions = function + | Logic_monad.TacticFailure e -> + strip_wrapping_exceptions e + | exc -> exc + +let process_vernac_interp_error (exc, info) = + let exc = strip_wrapping_exceptions exc in + let e = process_vernac_interp_error (exc, info) in + let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in + let loc = Option.default Loc.ghost (Loc.get_loc info) in + match ltac_trace with + | None -> e + | Some trace -> + let (e, info) = e in + match Himsg.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 (process_vernac_interp_error e)) + (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 (process_vernac_interp_error e)) + (fun e -> Errors.print_no_report (fst (process_vernac_interp_error (e, Exninfo.null)))) |