summaryrefslogtreecommitdiff
path: root/toplevel/cerrors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/cerrors.ml')
-rw-r--r--toplevel/cerrors.ml120
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))))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 02:07:53 +0000