From fa9df2efe5666789bf91bb7761567cd53e6c451f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 18 Dec 2016 18:14:58 +0100 Subject: [stm] Break stm/toplevel dependency loop. Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore. --- vernac/explainErr.ml | 129 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 129 insertions(+) create mode 100644 vernac/explainErr.ml (limited to 'vernac/explainErr.ml') diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml new file mode 100644 index 000000000..17897460c --- /dev/null +++ b/vernac/explainErr.ml @@ -0,0 +1,129 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* hov 0 (str "Syntax error: " ++ str txt ++ str ".") + | Compat.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 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 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) ?(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 (CErrors.handled (fst e)) then + let (e, info) = e in + let msg = str "Uncaught exception " ++ str (Printexc.to_string e) 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 + match e' with + | None -> e + | Some (None, loc) -> (fst e, Loc.add_loc (snd e) loc) + | Some (Some msg, loc) -> + (EvaluatedError (msg, Some (fst e)), Loc.add_loc (snd e) loc) -- cgit v1.2.3