diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:01:07 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:01:07 +0200 |
commit | 095eac936751bab72e3c6bbdfa3ede51f7198721 (patch) | |
tree | 44cf2859ba6b8486f056efaaf7ee6c2d855f2aae /toplevel/cerrors.ml | |
parent | 4e6d6dab2ef2de6c1ad7972fc981e55a4fde7ae3 (diff) | |
parent | 0b14713e3efd7f8f1cc8a06555d0ec8fbe496130 (diff) |
Merge branch 'experimental/master'
Diffstat (limited to 'toplevel/cerrors.ml')
-rw-r--r-- | toplevel/cerrors.ml | 152 |
1 files changed, 43 insertions, 109 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 095f50c6..3b6f0f7c 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -1,20 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) (************************************************************************) -(* $Id: cerrors.ml 15025 2012-03-09 14:27:07Z glondu $ *) - +open Compat open Pp open Util open Indtypes open Type_errors open Pretype_errors open Indrec -open Lexer let print_loc loc = if loc = dummy_loc then @@ -25,86 +23,37 @@ let print_loc loc = let guill s = "\""^s^"\"" -let where s = - if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) exception EvaluatedError of std_ppcmds * exn option -(* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *) - -let rec explain_exn_default_aux anomaly_string report_fn = function - | Stream.Failure -> - hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") - | Stream.Error txt -> - hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | Token.Error txt -> - hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | Sys_error msg -> - hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ()) - | UserError(s,pps) -> - hov 0 (str "Error: " ++ where s ++ pps) - | Out_of_memory -> - hov 0 (str "Out of memory.") - | Stack_overflow -> - hov 0 (str "Stack overflow.") - | Timeout -> - hov 0 (str "Timeout!") - | Anomaly (s,pps) -> - hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ()) - | AnomalyOnError (s,exc) -> - hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++ - fnl() ++ explain_exn_default_aux anomaly_string report_fn exc) - | Match_failure(filename,pos1,pos2) -> - hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ - if Sys.ocaml_version = "3.06" then - (str " from character " ++ int pos1 ++ - str " to " ++ int pos2) - else - (str " at line " ++ int pos1 ++ - str " character " ++ int pos2) - ++ report_fn ()) - | Not_found -> - hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report_fn ()) - | Failure s -> - hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report_fn ()) - | Invalid_argument s -> - hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ()) - | Sys.Break -> - hov 0 (fnl () ++ str "User interrupt.") - | 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 ".") - | Compat.Exc_located (loc,exc) -> +(** 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 ^ ".")) + | 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 ())) - ++ explain_exn_default_aux anomaly_string report_fn exc) - | Assert_failure (s,b,e) -> - hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ - (if s <> "" then - if Sys.ocaml_version = "3.06" then - (str ("(file \"" ^ s ^ "\", characters ") ++ - int b ++ str "-" ++ int e ++ str ")") - else - (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ - str ", characters " ++ int e ++ str "-" ++ - int (e+6) ++ str ")") - else - (mt ())) ++ - report_fn ()) - | EvaluatedError (msg,None) -> - msg - | EvaluatedError (msg,Some reraise) -> - msg ++ explain_exn_default_aux anomaly_string report_fn reraise - | reraise -> - hov 0 (anomaly_string () ++ str "Uncaught exception " ++ - str (Printexc.to_string reraise) ++ report_fn ()) + ++ 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) @@ -120,13 +69,17 @@ let rec process_vernac_interp_error = function mt() in wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> - wrap_vernac_error (Himsg.explain_type_error ctx te) - | PretypeError(ctx,te) -> - wrap_vernac_error (Himsg.explain_pretype_error 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) -> @@ -145,10 +98,10 @@ let rec process_vernac_interp_error = function (str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q ++ str ".") | Refiner.FailError (i,s) -> - EvaluatedError (hov 0 (str "Error: 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")."), - None) + wrap_vernac_error + (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").") | AlreadyDeclared msg -> wrap_vernac_error (msg ++ str ".") | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () -> @@ -156,32 +109,13 @@ let rec process_vernac_interp_error = function | Proof_type.LtacLocated (s,exc) -> EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()), Some (process_vernac_interp_error exc)) - | Compat.Exc_located (loc,exc) -> - Compat.Exc_located (loc,process_vernac_interp_error exc) + | Loc.Exc_located (loc,exc) -> + Loc.Exc_located (loc,process_vernac_interp_error exc) | exc -> exc -let anomaly_string () = str "Anomaly: " - -let report () = (str "." ++ spc () ++ str "Please report.") - -let explain_exn_default = - explain_exn_default_aux anomaly_string report - -let raise_if_debug e = - if !Flags.debug then raise e - let _ = Tactic_debug.explain_logic_error := - (fun e -> explain_exn_default (process_vernac_interp_error e)) + (fun e -> Errors.print (process_vernac_interp_error e)) let _ = Tactic_debug.explain_logic_error_no_anomaly := - (fun e -> - explain_exn_default_aux (fun () -> mt()) (fun () -> str ".") - (process_vernac_interp_error e)) - -let explain_exn_function = ref explain_exn_default - -let explain_exn e = !explain_exn_function e - -let explain_exn_no_anomaly e = - explain_exn_default_aux (fun () -> raise e) mt e + (fun e -> Errors.print_no_report (process_vernac_interp_error e)) |