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

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open CErrors
open Indtypes
open Type_errors
open Pretype_errors
open Indrec

let guill s = str "\"" ++ str s ++ str "\""

(** Invariant : exceptions embedded in EvaluatedError satisfy
    Errors.noncritical *)

exception EvaluatedError of Pp.t * 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 ".")
  | Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
  | CLexer.Error.E err -> hov 0 (str (CLexer.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 ++ CErrors.print reraise
  (* Otherwise, not handled here *)
  | _ -> raise CErrors.Unhandled

let _ = CErrors.register_handler explain_exn_default


(** Pre-explain a vernac interpretation error *)

let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), 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) ->
      let te = Himsg.map_ptype_error EConstr.of_constr te in
      wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
  | PretypeError(ctx,sigma,te) ->
      wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
  | Typeclasses_errors.TypeClassError(env, te) ->
      wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
  | InductiveError e ->
      wrap_vernac_error exn (Himsg.explain_inductive_error e)
  | Modops.ModuleTypingError e ->
      wrap_vernac_error exn (Himsg.explain_module_error e)
  | Modintern.ModuleInternalizationError e ->
      wrap_vernac_error exn (Himsg.explain_module_internalization_error e)
  | RecursionSchemeError 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 exn (Himsg.explain_reduction_tactic_error e)
  | Logic.RefinerError e ->
    let sigma, env = Pfedit.get_current_context () in
    wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e)
  | Nametab.GlobalizationError q ->
      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.")
  | Refiner.FailError (i,s) ->
      let s = Lazy.force s in
      wrap_vernac_error exn
        (str "Tactic failure" ++
         (if Pp.ismt s then s else str ": " ++ s) ++
         if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
  | AlreadyDeclared msg ->
      wrap_vernac_error exn (msg ++ str ".")
  | _ ->
      exn

let rec strip_wrapping_exceptions = function
  | Logic_monad.TacticFailure e ->
    strip_wrapping_exceptions e
  | exc -> exc

let additional_error_info = ref []

let register_additional_error_info f =
  additional_error_info := f :: !additional_error_info

let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) =
  let exc = strip_wrapping_exceptions exc in
  let e = process_vernac_interp_error (exc, info) in
  let () =
    if not allow_uncaught && not (CErrors.handled (fst e)) then
      let (e, info) = e in
      let msg = str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." in
      let err = CErrors.make_anomaly msg in
      Util.iraise (err, info)
  in
  let e' =
    try Some (CList.find_map (fun f -> f e) !additional_error_info)
    with _ -> None
  in
  let add_loc_opt ?loc info = Option.cata (fun l -> Loc.add_loc info l) info loc in
  match e' with
  | None -> e
  | Some (loc, None) -> (fst e, add_loc_opt ?loc (snd e))
  | Some (loc, Some msg) ->
    (EvaluatedError (msg, Some (fst e)), add_loc_opt ?loc (snd e))