1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Errors
open Indtypes
open Type_errors
open Pretype_errors
open Indrec
let print_loc loc =
if Loc.is_ghost loc then
(str"<unknown>")
else
let loc = Loc.unloc loc in
(int (fst loc) ++ str"-" ++ int (snd loc))
let guill s = str "\"" ++ str s ++ str "\""
(** Invariant : exceptions embedded in EvaluatedError satisfy
Errors.noncritical *)
exception EvaluatedError of std_ppcmds * exn option
(** Registration of generic errors
Nota: explain_exn does NOT end with a newline anymore!
*)
let explain_exn_default = function
(* Basic interaction exceptions *)
| Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
| Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
| 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.")
(* Exceptions with pre-evaluated error messages *)
| EvaluatedError (msg,None) -> msg
| EvaluatedError (msg,Some reraise) -> msg ++ Errors.print reraise
(* Otherwise, not handled here *)
| _ -> raise Errors.Unhandled
let _ = Errors.register_handler explain_exn_default
(** Pre-explain a vernac interpretation error *)
let wrap_vernac_error with_header (exn, info) strm =
if with_header then
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)
else
(EvaluatedError (strm, None), info)
let process_vernac_interp_error with_header 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 with_header exn (str "Universe inconsistency" ++ msg ++ str ".")
| TypeError(ctx,te) ->
wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te)
| PretypeError(ctx,sigma,te) ->
wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te)
| Typeclasses_errors.TypeClassError(env, te) ->
wrap_vernac_error with_header exn (Himsg.explain_typeclass_error env te)
| InductiveError e ->
wrap_vernac_error with_header exn (Himsg.explain_inductive_error e)
| Modops.ModuleTypingError e ->
wrap_vernac_error with_header exn (Himsg.explain_module_error e)
| Modintern.ModuleInternalizationError e ->
wrap_vernac_error with_header exn (Himsg.explain_module_internalization_error e)
| RecursionSchemeError e ->
wrap_vernac_error with_header exn (Himsg.explain_recursion_scheme_error e)
| Cases.PatternMatchingError (env,sigma,e) ->
wrap_vernac_error with_header exn (Himsg.explain_pattern_matching_error env sigma e)
| Tacred.ReductionTacticError e ->
wrap_vernac_error with_header exn (Himsg.explain_reduction_tactic_error e)
| Logic.RefinerError e ->
wrap_vernac_error with_header exn (Himsg.explain_refiner_error e)
| Nametab.GlobalizationError q ->
wrap_vernac_error with_header exn
(str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
spc () ++ str "was not found" ++
spc () ++ str "in the current" ++ spc () ++ str "environment.")
| Refiner.FailError (i,s) ->
let s = Lazy.force s in
wrap_vernac_error with_header exn
(str "Tactic failure" ++
(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 with_header 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 ?(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
let () =
if not allow_uncaught && not (Errors.handled (fst e)) then
let (e, info) = e in
let msg = str "Uncaught exception " ++ str (Printexc.to_string e) in
let err = Errors.make_anomaly msg in
Util.iraise (err, 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 (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))))
|
