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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Pp
open Util
open Ast
open Indtypes
open Type_errors
open Pretype_errors
open Lexer
let print_loc loc =
if loc = dummy_loc then
[< 'sTR"<unknown>" >]
else
[< 'iNT (fst loc); 'sTR"-"; 'iNT (snd loc) >]
let guill s = "\""^s^"\""
let where s =
if !Options.debug then [< 'sTR"in "; 'sTR s; 'sTR":"; 'sPC >] else [<>]
let report () = [< 'sTR "."; 'sPC; 'sTR "Please report." >]
(* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)
let rec explain_exn_default = function
| Stream.Failure ->
hOV 0 [< 'sTR "Anomaly: Uncaught Stream.Failure." >]
| Stream.Error txt ->
hOV 0 [< 'sTR "Syntax error: "; 'sTR txt >]
| Token.Error txt ->
hOV 0 [< 'sTR "Syntax error: "; 'sTR txt >]
| Sys_error msg ->
hOV 0 [< 'sTR "Error: OS: "; 'sTR msg >]
| UserError(s,pps) ->
hOV 1 [< 'sTR"Error: "; where s; pps >]
| Out_of_memory ->
hOV 0 [< 'sTR "Out of memory" >]
| Stack_overflow ->
hOV 0 [< 'sTR "Stack overflow" >]
| Ast.No_match s ->
hOV 0 [< 'sTR "Anomaly: Ast matching error: "; 'sTR s; report () >]
| Anomaly (s,pps) ->
hOV 1 [< 'sTR "Anomaly: "; where s; pps; report () >]
| Match_failure(filename,pos1,pos2) ->
hOV 1 [< 'sTR "Anomaly: Match failure in file ";
'sTR (guill filename); 'sTR " from char #";
'iNT pos1; 'sTR " to #"; 'iNT pos2;
report () >]
| Not_found ->
hOV 0 [< 'sTR "Anomaly: Search error"; report () >]
| Failure s ->
hOV 0 [< 'sTR "Anomaly: Failure "; 'sTR (guill s); report () >]
| Invalid_argument s ->
hOV 0 [< 'sTR "Anomaly: Invalid argument "; 'sTR (guill s); report () >]
| Sys.Break ->
hOV 0 [< 'fNL; 'sTR"User Interrupt." >]
| Univ.UniverseInconsistency ->
hOV 0 [< 'sTR "Error: Universe Inconsistency." >]
| TypeError(ctx,te) ->
hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error ctx te >]
| PretypeError(ctx,te) ->
hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_pretype_error ctx te >]
| InductiveError e ->
hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_inductive_error e >]
| Cases.PatternMatchingError (env,e) ->
hOV 0
[< 'sTR "Error:"; 'sPC; Himsg.explain_pattern_matching_error env e >]
| Logic.RefinerError e ->
hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_refiner_error e >]
| Nametab.GlobalizationError q ->
hOV 0 [< 'sTR "Error:"; 'sPC;
'sTR "The reference"; 'sPC; Nametab.pr_qualid q;
'sPC ; 'sTR "was not found";
'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
| Nametab.GlobalizationConstantError q ->
hOV 0 [< 'sTR "Error:"; 'sPC;
'sTR "No constant of this name:"; 'sPC; Nametab.pr_qualid q >]
| Tacmach.FailError i ->
hOV 0 [< 'sTR "Error: Fail tactic always fails (level ";
'iNT i; 'sTR")." >]
| Stdpp.Exc_located (loc,exc) ->
hOV 0 [< if loc = Ast.dummy_loc then [<>]
else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >];
explain_exn_default exc >]
| Lexer.Error Illegal_character ->
hOV 0 [< 'sTR "Syntax error: Illegal character." >]
| Lexer.Error Unterminated_comment ->
hOV 0 [< 'sTR "Syntax error: Unterminated comment." >]
| Lexer.Error Unterminated_string ->
hOV 0 [< 'sTR "Syntax error: Unterminated string." >]
| Lexer.Error Undefined_token ->
hOV 0 [< 'sTR "Syntax error: Undefined token." >]
| Lexer.Error (Bad_token s) ->
hOV 0 [< 'sTR "Syntax error: Bad token"; 'sPC; 'sTR s; 'sTR "." >]
| Assert_failure (s,b,e) ->
hOV 0 [< 'sTR "Anomaly: assert failure"; 'sPC;
if s <> "" then
[< 'sTR ("(file \"" ^ s ^ "\", characters ");
'iNT b; 'sTR "-"; 'iNT e; 'sTR ")" >]
else
[< >];
report () >]
| reraise ->
hOV 0 [< 'sTR "Anomaly: Uncaught exception ";
'sTR (Printexc.to_string reraise); report () >]
let raise_if_debug e =
if !Options.debug then raise e
let explain_exn_function = ref explain_exn_default
let explain_exn e = !explain_exn_function e
|
