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
139
140
141
142
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
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 = "\""^s^"\""
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: " ^ 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.is_ghost loc then (mt ())
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
++ Errors.print_no_anomaly exc)
| Compat.Exc_located (loc, exc) ->
let loc = Compat.to_coqloc loc in
hov 0 ((if Loc.is_ghost loc then (mt ())
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
++ Errors.print_no_anomaly exc)
| EvaluatedError (msg,None) -> msg
| EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly 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 strm =
EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)
let is_mt t =
Pervasives.(=) (Lazy.force t) (mt ()) (* FIXME *)
let rec process_vernac_interp_error = function
| Univ.UniverseInconsistency (o,u,v,p) ->
let pr_rel r =
match r with
Univ.Eq -> str"=" | Univ.Lt -> str"<" | Univ.Le -> str"<=" in
let reason = match p with
[] -> mt()
| _::_ ->
str " because" ++ spc() ++ Univ.pr_uni v ++
prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ Univ.pr_uni v)
p ++
(if Univ.Universe.equal (snd (List.last p)) u then mt() else
(spc() ++ str "= " ++ Univ.pr_uni u)) in
let msg =
if !Constrextern.print_universes then
spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
pr_rel o ++ spc() ++ Univ.pr_uni v ++ reason ++ str")"
else
mt() in
wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
| TypeError(ctx,te) ->
wrap_vernac_error (Himsg.explain_type_error ctx Evd.empty te)
| PretypeError(ctx,sigma,te) ->
wrap_vernac_error (Himsg.explain_pretype_error ctx sigma te)
| Typeclasses_errors.TypeClassError(env, te) ->
wrap_vernac_error (Himsg.explain_typeclass_error env te)
| InductiveError e ->
wrap_vernac_error (Himsg.explain_inductive_error e)
| Modops.ModuleTypingError e ->
wrap_vernac_error (Himsg.explain_module_error e)
| Modintern.ModuleInternalizationError e ->
wrap_vernac_error (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)
| Tacred.ReductionTacticError e ->
wrap_vernac_error (Himsg.explain_reduction_tactic_error e)
| Logic.RefinerError e ->
wrap_vernac_error (Himsg.explain_refiner_error e)
| Nametab.GlobalizationError q ->
wrap_vernac_error
(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
(str "Tactic failure" ++
(if not (is_mt s) then str ":" ++ Lazy.force s else mt ()) ++ (* FIXME *)
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 not (is_mt s) ->
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)
| Compat.Exc_located (loc, exc) ->
let loc = Compat.to_coqloc loc in
Loc.Exc_located (loc, process_vernac_interp_error exc)
| exc ->
exc
let _ = Tactic_debug.explain_logic_error :=
(fun e -> Errors.print (process_vernac_interp_error e))
let _ = Tactic_debug.explain_logic_error_no_anomaly :=
(fun e -> Errors.print_no_report (process_vernac_interp_error e))
|
