diff options
77 files changed, 476 insertions, 443 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index b4757c8f7..3d2676f14 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -322,7 +322,7 @@ let about () = { Interface.compile_date = Coq_config.compile_date; } -let handle_exn e = +let handle_exn (e, info) = let dummy = Stateid.dummy in let loc_of e = match Loc.get_loc e with | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) @@ -332,9 +332,9 @@ let handle_exn e = | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!" | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!" | e -> - match Stateid.get e with - | Some (valid, _) -> valid, loc_of e, mk_msg e - | None -> dummy, loc_of e, mk_msg e + match Stateid.get info with + | Some (valid, _) -> valid, loc_of info, mk_msg e + | None -> dummy, loc_of info, mk_msg e let init = let initialized = ref false in @@ -421,7 +421,7 @@ let print_xml = fun oc xml -> Mutex.lock m; try Xml_printer.print oc xml; Mutex.unlock m - with e -> let e = Errors.push e in Mutex.unlock m; raise e + with e -> let e = Errors.push e in Mutex.unlock m; iraise e let slave_logger xml_oc level message = diff --git a/ide/interface.mli b/ide/interface.mli index 77a875b7d..cbaa02750 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -200,7 +200,7 @@ type init_rty = state_id type about_sty = unit type about_rty = coq_info -type handle_exn_sty = exn +type handle_exn_sty = Exninfo.iexn type handle_exn_rty = state_id * location * string (* Retrocompatibility stuff *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index da0bcaf0b..0cd7e7b81 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -578,6 +578,7 @@ let abstract_eval_call handler (c : 'a call) : 'a value = | PrintAst x -> mkGood (handler.print_ast x) | Annotate x -> mkGood (handler.annotate x) with any -> + let any = Errors.push any in Fail (handler.handle_exn any) (** brain dead code, edit if protocol messages are added/removed *) diff --git a/interp/notation.ml b/interp/notation.ml index de7eca352..cf1dec848 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1001,4 +1001,4 @@ let with_notation_protection f x = with reraise -> let reraise = Errors.push reraise in let () = unfreeze fs in - raise reraise + iraise reraise diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 7dcaf9b13..c13dd3a92 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -213,7 +213,7 @@ and val_of_constr env c = let reraise = Errors.push reraise in let () = print_string "can not compile \n" in let () = Format.print_flush () in - raise reraise + iraise reraise in eval_to_patch env (to_memory ccfv) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index bef72340c..bd44b3967 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -752,7 +752,7 @@ let export ?except senv dir = try join_safe_environment ?except senv with e -> let e = Errors.push e in - Errors.errorlabstrm "export" (Errors.print e) + Errors.errorlabstrm "export" (Errors.iprint e) in assert(senv.future_cst = []); let () = check_current_library dir senv in diff --git a/lib/backtrace.ml b/lib/backtrace.ml index 19b07d876..b3b8bdea2 100644 --- a/lib/backtrace.ml +++ b/lib/backtrace.ml @@ -84,18 +84,23 @@ let get_backtrace e = let add_backtrace e = if !is_recording then + (** This must be the first function call, otherwise the stack may be + destroyed *) let current = get_exception_backtrace () in + let info = Exninfo.info e in begin match current with - | None -> e + | None -> (e, info) | Some fragment -> - let bt = match get_backtrace e with + let bt = match get_backtrace info with | None -> [] | Some bt -> bt in let bt = fragment :: bt in - Exninfo.add e backtrace bt + (e, Exninfo.add info backtrace bt) end - else e + else + let info = Exninfo.info e in + (e, info) let app_backtrace ~src ~dst = if !is_recording then diff --git a/lib/backtrace.mli b/lib/backtrace.mli index ecd046b54..dd82165b6 100644 --- a/lib/backtrace.mli +++ b/lib/backtrace.mli @@ -56,10 +56,10 @@ val record_backtrace : bool -> unit (** Whether to activate the backtrace recording mechanism. Note that it will only work whenever the program was compiled with the [debug] flag. *) -val get_backtrace : exn -> t option +val get_backtrace : Exninfo.info -> t option (** Retrieve the optional backtrace coming with the exception. *) -val add_backtrace : exn -> exn +val add_backtrace : exn -> Exninfo.iexn (** Add the current backtrace information to the given exception. The intended use case is of the form: {[ @@ -88,7 +88,7 @@ val add_backtrace : exn -> exn *) -val app_backtrace : src:exn -> dst:exn -> exn +val app_backtrace : src:Exninfo.info -> dst:Exninfo.info -> Exninfo.info (** Append the backtrace from [src] to [dst]. The returned exception is [dst] except for its backtrace information. This is targeted at container exceptions, that is, exceptions that contain exceptions. This way, one can diff --git a/lib/control.ml b/lib/control.ml index cce9d3a9f..04d176092 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -41,7 +41,7 @@ let unix_timeout n f e = with e -> let e = Backtrace.add_backtrace e in restore_timeout (); - raise e + Exninfo.iraise e let windows_timeout n f e = let killed = ref false in @@ -78,7 +78,7 @@ let windows_timeout n f e = | e -> let () = killed := true in let e = Backtrace.add_backtrace e in - raise e + Exninfo.iraise e type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a } diff --git a/lib/errors.ml b/lib/errors.ml index 45e0f9fdf..ab331d6a4 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -91,8 +91,10 @@ let print_anomaly askreport e = hov 0 (raw_anomaly e) (** The standard exception printer *) -let print e = - print_gen (print_anomaly true) !handle_stack e ++ print_backtrace e +let print ?(info = Exninfo.null) e = + print_gen (print_anomaly true) !handle_stack e ++ print_backtrace info + +let iprint (e, info) = print ~info e (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) diff --git a/lib/errors.mli b/lib/errors.mli index 7e296e45e..e4096a7ef 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -13,7 +13,7 @@ open Pp (** {6 Error handling} *) -val push : exn -> exn +val push : exn -> Exninfo.iexn (** Alias for [Backtrace.add_backtrace]. *) (** {6 Generic errors.} @@ -74,7 +74,8 @@ exception Unhandled val register_handler : (exn -> Pp.std_ppcmds) -> unit (** The standard exception printer *) -val print : exn -> Pp.std_ppcmds +val print : ?info:Exninfo.info -> exn -> Pp.std_ppcmds +val iprint : Exninfo.iexn -> Pp.std_ppcmds (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) diff --git a/lib/exninfo.ml b/lib/exninfo.ml index 845b8d190..2eca5f4a7 100644 --- a/lib/exninfo.ml +++ b/lib/exninfo.ml @@ -14,89 +14,44 @@ module Store = Store.Make(struct end) type 'a t = 'a Store.field -let token = Obj.repr "HACK" -(** Unique token used to recognize enriched exceptions. *) +type info = Store.t -let make = Store.field - -(** Discriminate normal data w.r.t enriched exceptions *) -let is_data obj = - Obj.is_block obj && Obj.size obj = 2 && Obj.field obj 0 == token - -(** As [Array.blit] *) -let blit obj1 off1 obj2 off2 len = - for i = 0 to len - 1 do - let data = Obj.field obj1 (off1 + i) in - Obj.set_field obj2 (off2 + i) data - done - -(** Retrieve the optional backtrace set in an exception. *) -let get (e : exn) i = - let obj = Obj.repr e in - let len = Obj.size obj in - let lst = Obj.field obj (len - 1) in - if is_data lst then - let data = Obj.obj (Obj.field lst 1) in - Store.get data i - else None +type iexn = exn * info -(** Add data to any exception *) -let add e i v : exn = - let obj = Obj.repr e in - let len = Obj.size obj in - let lst = Obj.field obj (len - 1) in - if is_data lst then - (** The exception was already enriched *) - let data = Obj.obj (Obj.field lst 1) in - (** We retrieve the old information and update it *) - let data = Store.set data i v in - let ans = Obj.dup obj in - let data = Obj.repr (token, data) in - let () = Obj.set_field ans (len - 1) data in - Obj.obj ans +let make = Store.field +let add = Store.set +let get = Store.get +let null = Store.empty + +exception Unique + +let dummy = (Unique, Store.empty) + +let current = ref dummy + +let iraise e = + let () = current := e in + raise (fst e) + +let raise ?info e = match info with +| None -> raise e +| Some i -> current := (e, i); raise e + +let info e = + let (src, data) = !current in + if src == e then + (** Slightly unsound, some exceptions may not be unique up to pointer + equality. Though, it should be quite exceptional to be in a situation + where the following holds: + + 1. An argument-free exception is raised through the enriched {!raise}; + 2. It is not captured by any enriched with-clause (which would reset + the current data); + 3. The same exception is raised through the standard raise, accessing + the wrong data. + . *) + let () = current := dummy in + data else - (** This was a plain exception *) - let ans = Obj.new_block 0 (succ len) in - (** We build the new enriched exception from scratch *) - let () = blit obj 0 ans 0 len in - let data = Store.set Store.empty i v in - let data = Obj.repr (token, data) in - let () = Obj.set_field ans len data in - Obj.obj ans - -let clear e = - let obj = Obj.repr e in - let len = Obj.size obj in - let lst = Obj.field obj (len - 1) in - if is_data lst then - let ans = Obj.new_block 0 (pred len) in - let () = blit obj 0 ans 0 (pred len) in - Obj.obj ans - else e - -let copy (src : exn) (dst : exn) = - let obj = Obj.repr src in - let len = Obj.size obj in - let lst = Obj.field obj (len - 1) in - if is_data lst then - (** First object has data *) - let src_data = Obj.obj (Obj.field lst 1) in - let obj = Obj.repr dst in - let len = Obj.size obj in - let lst = Obj.field obj (len - 1) in - if is_data lst then - (** second object has data *) - let dst_data = Obj.obj (Obj.field lst 1) in - let ans = Obj.dup obj in - let data = Obj.repr (token, Store.merge src_data dst_data) in - let () = Obj.set_field ans len data in - Obj.obj ans - else - (** second object has no data *) - let ans = Obj.new_block 0 (succ len) in - (** We build the new enriched exception from scratch *) - let () = blit obj 0 ans 0 len in - let data = Obj.repr (token, src_data) in - let () = Obj.set_field ans len data in - Obj.obj ans - else dst + let () = current := dummy in + Store.empty diff --git a/lib/exninfo.mli b/lib/exninfo.mli index 844ff0f96..c960ac7c0 100644 --- a/lib/exninfo.mli +++ b/lib/exninfo.mli @@ -11,20 +11,29 @@ type 'a t (** Information containing a given type. *) +type info +(** All information *) + +type iexn = exn * info +(** Information-wearing exceptions *) + val make : unit -> 'a t (** Create a new piece of information. *) -val add : exn -> 'a t -> 'a -> exn +val null : info +(** No information *) + +val add : info -> 'a t -> 'a -> info (** Add information to an exception. *) -val get : exn -> 'a t -> 'a option +val get : info -> 'a t -> 'a option (** Get information worn by an exception. Returns [None] if undefined. *) -(* val remove : exn -> 'a t -> exn *) -(** TODO: Remove a given piece of information. *) +val info : exn -> info +(** Retrieve the information of the last exception raised. *) -val clear : exn -> exn -(** Remove any information. *) +val iraise : iexn -> 'a +(** Raise the given enriched exception. *) -val copy : exn -> exn -> exn -(** [copy src dst] adds the additional info from [src] to [dst]. *) +val raise : ?info:info -> exn -> 'a +(** Raise the given exception with additional information. *) diff --git a/lib/flags.ml b/lib/flags.ml index 31b40dc53..0c6fef8be 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -12,7 +12,7 @@ let with_option o f x = with reraise -> let reraise = Backtrace.add_backtrace reraise in let () = o := old in - raise reraise + Exninfo.iraise reraise let with_options ol f x = let vl = List.map (!) ol in @@ -23,7 +23,7 @@ let with_options ol f x = with reraise -> let reraise = Backtrace.add_backtrace reraise in let () = List.iter2 (:=) ol vl in - raise reraise + Exninfo.iraise reraise let without_option o f x = let old = !o in o:=false; @@ -31,7 +31,7 @@ let without_option o f x = with reraise -> let reraise = Backtrace.add_backtrace reraise in let () = o := old in - raise reraise + Exninfo.iraise reraise let with_extra_values o l f x = let old = !o in o:=old@l; @@ -39,7 +39,7 @@ let with_extra_values o l f x = with reraise -> let reraise = Backtrace.add_backtrace reraise in let () = o := old in - raise reraise + Exninfo.iraise reraise let boot = ref false let load_init = ref true diff --git a/lib/future.ml b/lib/future.ml index b851f912c..52a060c93 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -26,7 +26,7 @@ let _ = Errors.register_handler (function "asynchronous script processing.") | _ -> raise Errors.Unhandled) -type fix_exn = exn -> exn +type fix_exn = Exninfo.iexn -> Exninfo.iexn let id x = prerr_endline "Future: no fix_exn.\nYou have probably created a Future.computation from a value without passing the ~fix_exn argument. You probably want to chain with an already existing future instead."; x module UUID = struct @@ -43,7 +43,7 @@ end module UUIDMap = Map.Make(UUID) module UUIDSet = Set.Make(UUID) -type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation] +type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] (* Val is not necessarily a final state, so the computation restarts from the state stocked into Val *) @@ -51,7 +51,7 @@ and 'a comp = | Delegated of (unit -> unit) | Closure of (unit -> 'a) | Val of 'a * Dyn.t option - | Exn of exn (* Invariant: this exception is always "fixed" as in fix_exn *) + | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) and 'a comput = | Ongoing of (UUID.t * fix_exn * 'a comp ref) Ephemeron.key @@ -66,9 +66,10 @@ let get x = | Finished v -> UUID.invalid, id, ref (Val (v,None)) | Ongoing x -> try Ephemeron.get x - with Ephemeron.InvalidKey -> UUID.invalid, id, ref (Exn NotHere) + with Ephemeron.InvalidKey -> + UUID.invalid, id, ref (Exn (NotHere, Exninfo.null)) -type 'a value = [ `Val of 'a | `Exn of exn ] +type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ] let is_over kx = let _, _, x = get kx in match !x with | Val _ | Exn _ -> true @@ -116,7 +117,7 @@ let rec compute ~pure ck : 'a value = let _, fix_exn, c = get ck in match !c with | Val (x, _) -> `Val x - | Exn e -> `Exn e + | Exn (e, info) -> `Exn (e, info) | Delegated wait -> wait (); compute ~pure ck | Closure f -> try @@ -127,12 +128,12 @@ let rec compute ~pure ck : 'a value = let e = Errors.push e in let e = fix_exn e in match e with - | NotReady -> `Exn e + | (NotReady, _) -> `Exn e | _ -> c := Exn e; `Exn e let force ~pure x = match compute ~pure x with | `Val v -> v - | `Exn e -> raise e + | `Exn e -> Exninfo.iraise e let chain ~pure ck f = let uuid, fix_exn, c = get ck in @@ -167,12 +168,14 @@ let purify f x = let v = f x in !unfreeze state; v - with e -> let e = Errors.push e in !unfreeze state; raise e + with e -> + let e = Errors.push e in !unfreeze state; Exninfo.iraise e let transactify f x = let state = !freeze () in try f x - with e -> let e = Errors.push e in !unfreeze state; raise e + with e -> + let e = Errors.push e in !unfreeze state; Exninfo.iraise e let purify_future f x = if is_over x then f x else purify f x let compute x = purify_future (compute ~pure:false) x @@ -214,4 +217,4 @@ let print f kx = | Closure _ -> str "Closure" ++ uid | Val (x, None) -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x) | Val (x, Some _) -> str "StateVal" ++ uid ++ spc () ++ hov 0 (f x) - | Exn e -> str "Exn" ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e)) + | Exn (e, _) -> str "Exn" ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e)) diff --git a/lib/future.mli b/lib/future.mli index bae4fa751..d97b46382 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -66,8 +66,8 @@ module UUIDSet : Set.S with type elt = UUID.t exception NotReady type 'a computation -type 'a value = [ `Val of 'a | `Exn of exn ] -type fix_exn = exn -> exn +type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ] +type fix_exn = Exninfo.iexn -> Exninfo.iexn (* Build a computation, no snapshot of the global state is taken. If you need to grab a copy of the state start with from_here () and then chain. @@ -98,7 +98,7 @@ val fix_exn_of : 'a computation -> fix_exn (* Run remotely, returns the function to assign. If not blocking (the default) it raises NotReady if forced before the delage assigns it. *) -type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation] +type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] val create_delegate : ?blocking:bool -> fix_exn -> 'a computation * ('a assignement -> unit) diff --git a/lib/loc.ml b/lib/loc.ml index 8f133ce0d..5ca345fd2 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -74,4 +74,6 @@ let add_loc e loc = Exninfo.add e location loc let get_loc e = Exninfo.get e location -let raise loc e = raise (Exninfo.add e location loc) +let raise loc e = + let info = Exninfo.add Exninfo.null location loc in + Exninfo.iraise (e, info) diff --git a/lib/loc.mli b/lib/loc.mli index a0b99c689..e9bf946a8 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -40,10 +40,10 @@ val represent : t -> (string * int * int * int * int) (** {5 Located exceptions} *) -val add_loc : exn -> t -> exn +val add_loc : Exninfo.info -> t -> Exninfo.info (** Adding location to an exception *) -val get_loc : exn -> t option +val get_loc : Exninfo.info -> t option (** Retrieving the optional location of an exception *) val raise : t -> exn -> 'a @@ -360,7 +360,7 @@ let pp_dirs ?pp_tag ft = with reraise -> let reraise = Backtrace.add_backtrace reraise in let () = Format.pp_print_flush ft () in - raise reraise + Exninfo.iraise reraise diff --git a/lib/stateid.mli b/lib/stateid.mli index 341544a67..2c12c30c3 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -31,8 +31,8 @@ val of_xml : xml -> t * state id that is a valid state id before the error. * Backtracking to the valid id is safe. * The initial_state_id is assumed to be safe. *) -val add : exn -> ?valid:t -> t -> exn -val get : exn -> (t * t) option +val add : Exninfo.info -> ?valid:t -> t -> Exninfo.info +val get : Exninfo.info -> (t * t) option type ('a,'b) request = { exn_info : t * t; diff --git a/lib/system.ml b/lib/system.ml index 0c4e892b9..1d1968a7c 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -200,7 +200,7 @@ let extern_intern ?(warn=true) magic = with reraise -> let reraise = Errors.push reraise in let () = try_remove filename in - raise reraise + iraise reraise with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try diff --git a/lib/util.ml b/lib/util.ml index 531e4fe7d..a8c25f745 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -128,3 +128,7 @@ type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a let map_union f g = function | Inl a -> Inl (f a) | Inr b -> Inr (g b) + +type iexn = Exninfo.iexn + +let iraise = Exninfo.iraise diff --git a/lib/util.mli b/lib/util.mli index 86720fe47..66f4c9aff 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -95,6 +95,12 @@ type 'a delayed = unit -> 'a val delayed_force : 'a delayed -> 'a +(** {6 Enriched exceptions} *) + +type iexn = Exninfo.iexn + +val iraise : iexn -> 'a + (** {6 Misc. } *) type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b @@ -104,4 +110,3 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a (** Used for browsable-until structures. *) - diff --git a/library/declaremods.ml b/library/declaremods.ml index 30cac7771..33d37ef62 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -796,7 +796,7 @@ let protect_summaries f = (* Something wrong: undo the whole process *) let reraise = Errors.push reraise in let () = Summary.unfreeze_summaries fs in - raise reraise + iraise reraise let start_module interp export id args res = protect_summaries (RawModOps.start_module interp export id args res) diff --git a/library/impargs.ml b/library/impargs.ml index d88d6f106..1a3b88405 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -77,7 +77,7 @@ let with_implicits flags f x = with reraise -> let reraise = Errors.push reraise in let () = implicit_args := oflags in - raise reraise + iraise reraise let set_maximality imps b = (* Force maximal insertion on ending implicits (compatibility) *) diff --git a/library/library.ml b/library/library.ml index 4fea6b836..343588652 100644 --- a/library/library.ml +++ b/library/library.ml @@ -731,7 +731,7 @@ let save_library_to ?todo dir f otab = let () = msg_warning (str ("Removed file "^f')) in let () = close_out ch in let () = Sys.remove f' in - raise reraise + iraise reraise let save_library_raw f lib univs proofs = let (f',ch) = raw_extern_library (f^"o") in diff --git a/library/states.ml b/library/states.ml index 031222c7d..200b14517 100644 --- a/library/states.ml +++ b/library/states.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open System type state = Lib.frozen * Summary.frozen @@ -38,6 +39,6 @@ let with_state_protection f x = let a = f x in unfreeze st; a with reraise -> let reraise = Errors.push reraise in - (unfreeze st; raise reraise) + (unfreeze st; iraise reraise) let with_state_protection_on_exception = Future.transactify diff --git a/library/summary.ml b/library/summary.ml index 96b9d0691..7a0064a1f 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -105,8 +105,8 @@ let unfreeze_summaries fs = with e when Errors.noncritical e -> let e = Errors.push e in Printf.eprintf "Error unfrezing summay %s\n%s\n%!" - (name_of_summary id) (Pp.string_of_ppcmds (Errors.print e)); - raise e + (name_of_summary id) (Pp.string_of_ppcmds (Errors.iprint e)); + iraise e in (** We rely on the order of the frozen list, and the order of folding *) ignore (Int.Map.fold_left fold !summaries fs.summaries) @@ -147,7 +147,7 @@ let unfreeze_summary datas = with e -> let e = Errors.push e in prerr_endline ("Exception unfreezing " ^ name); - raise e) + iraise e) datas (** All-in-one reference declaration + registration *) diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index f872c4a2d..ce0390e1d 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -193,7 +193,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct let entry_create = Entry.create let entry_parse e p = try Entry.parse e p - with Exc_located (loc,e) -> raise (Loc.add_loc e (to_coqloc loc)) + with Exc_located (loc,e) -> Loc.raise (to_coqloc loc) e IFDEF CAMLP5_6_02_1 THEN let entry_print ft x = Entry.print ft x ELSE diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index a0384faf8..9f4963861 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -355,7 +355,7 @@ let with_grammar_rule_protection f x = with reraise -> let reraise = Errors.push reraise in let () = unfreeze fs in - raise reraise + iraise reraise (**********************************************************************) (** Ltac quotations *) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 858c80f29..b74b1faca 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -504,8 +504,8 @@ let f_equal = end | _ -> Proofview.tclUNIT () end - begin function + begin function (e, info) -> match e with | Type_errors.TypeError _ -> Proofview.tclUNIT () - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end end diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 43fefc4c6..c8214ada8 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -74,9 +74,10 @@ let do_observe_tac s tac g = ignore(Stack.pop debug_queue); v with reraise -> + let reraise = Errors.push reraise in if not (Stack.is_empty debug_queue) - then print_debug_queue true (Cerrors.process_vernac_interp_error reraise); - raise reraise + then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise)); + iraise reraise let observe_tac_stream s tac g = if do_observe () diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 71da59c49..1051cae75 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -186,7 +186,7 @@ END let warning_error names e = - let e = Cerrors.process_vernac_interp_error e in + let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> Pp.msg_warning diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2ce9f4f61..6dbd61cfd 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -217,6 +217,8 @@ let prepare_body ((name,_,args,types,_),_) rt = let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') +let process_vernac_interp_error e = + fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)) let derive_inversion fix_names = try @@ -243,23 +245,23 @@ let derive_inversion fix_names = fix_names ) with e when Errors.noncritical e -> - let e' = Cerrors.process_vernac_interp_error e in + let e' = process_vernac_interp_error e in msg_warning (str "Cannot build inversion information" ++ if do_observe () then (fnl() ++ Errors.print e') else mt ()) with e when Errors.noncritical e -> () let warning_error names e = - let e = Cerrors.process_vernac_interp_error e in + let e = process_vernac_interp_error e in let e_explain e = match e with | ToShow e -> - let e = Cerrors.process_vernac_interp_error e in + let e = process_vernac_interp_error e in spc () ++ Errors.print e | _ -> if do_observe () then - let e = Cerrors.process_vernac_interp_error e in + let e = process_vernac_interp_error e in (spc () ++ Errors.print e) else mt () in @@ -277,7 +279,7 @@ let warning_error names e = | _ -> raise e let error_error names e = - let e = Cerrors.process_vernac_interp_error e in + let e = process_vernac_interp_error e in let e_explain e = match e with | ToShow e -> spc () ++ Errors.print e diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e07bce69c..8a6c8430f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -68,10 +68,11 @@ let do_observe_tac s tac g = let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v with reraise -> + let reraise = Errors.push reraise in let e = Cerrors.process_vernac_interp_error reraise in msgnl (str "observation "++ s++str " raised exception " ++ - Errors.print e ++ str " on goal " ++ goal ); - raise reraise;; + Errors.iprint e ++ str " on goal " ++ goal ); + iraise reraise;; let observe_tac_strm s tac g = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index a38764c5b..a466e1089 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -236,9 +236,10 @@ let do_observe_tac s tac g = ignore(Stack.pop debug_queue); v with reraise -> + let reraise = Errors.push reraise in if not (Stack.is_empty debug_queue) - then print_debug_queue true (Cerrors.process_vernac_interp_error reraise); - raise reraise + then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise)); + iraise reraise let observe_tac s tac g = if do_observe () diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index dfe018c33..07cc36815 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -77,7 +77,9 @@ let search_guard loc env possible_indexes fixdefs = let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with reraise -> - let e = Errors.push reraise in Loc.raise loc e); + let (e, info) = Errors.push reraise in + let info = Loc.add_loc info loc in + iraise (e, info)); indexes else (* we now search recursively amoungst all combinations *) @@ -176,7 +178,7 @@ let apply_heuristics env evdref fail_evar = try evdref := consider_remaining_unif_problems ~ts:(Typeclasses.classes_transparent_state ()) env !evdref with e when Errors.noncritical e -> - let e = Errors.push e in if fail_evar then raise e + let e = Errors.push e in if fail_evar then iraise e let check_typeclasses_instances_are_solved env current_sigma pending = (* Naive way, call resolution again with failure flag *) @@ -542,7 +544,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let cofix = (i,(names,ftys,fdefs)) in (try check_cofix env cofix with reraise -> - let e = Errors.push reraise in Loc.raise loc e); + let (e, info) = Errors.push reraise in + let info = Loc.add_loc info loc in + iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env evdref fixj tycon @@ -672,7 +676,10 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let resj = try judge_of_product env name j j' - with TypeError _ as e -> let e = Errors.push e in Loc.raise loc e in + with TypeError _ as e -> + let (e, info) = Errors.push e in + let info = Loc.add_loc info loc in + iraise (e, info) in inh_conv_coerce_to_tycon loc env evdref resj tycon | GLetIn(loc,name,c1,c2) -> diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml index 55eb434d3..5bad5f0f5 100644 --- a/proofs/logic_monad.ml +++ b/proofs/logic_monad.ml @@ -80,22 +80,23 @@ struct (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) - let raise = fun e -> (); fun () -> raise (Exception e) + let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e) (** [try ... with ...] but restricted to {!Exception}. *) let catch = fun s h -> (); fun () -> try s () with Exception e as src -> - let src = Errors.push src in - let e = Backtrace.app_backtrace ~src ~dst:e in - h e () + let (src, info) = Errors.push src in + h (e, info) () - let read_line = fun () -> try Pervasives.read_line () with e -> let e = Errors.push e in raise e () + let read_line = fun () -> try Pervasives.read_line () with e -> + let (e, info) = Errors.push e in raise ~info e () let print_char = fun c -> (); fun () -> print_char c (** {!Pp.pp}. The buffer is also flushed. *) - let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> let e = Errors.push e in raise e () + let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> + let (e, info) = Errors.push e in raise ~info e () let timeout = fun n t -> (); fun () -> Control.timeout n t (Exception Timeout) @@ -103,14 +104,13 @@ struct let make f = (); fun () -> try f () with e when Errors.noncritical e -> - let e = Errors.push e in - Pervasives.raise (Exception e) + let (e, info) = Errors.push e in + Util.iraise (Exception e, info) let run = fun x -> try x () with Exception e as src -> - let src = Errors.push src in - let e = Backtrace.app_backtrace ~src ~dst:e in - Pervasives.raise e + let (src, info) = Errors.push src in + Util.iraise (e, info) end (** {6 Logical layer} *) @@ -136,7 +136,7 @@ end (** A view type for the logical monad, which is a form of list, hence we can decompose it with as a list. *) type ('a, 'b) list_view = - | Nil of exn + | Nil of Exninfo.iexn | Cons of 'a * 'b module type Param = sig @@ -205,9 +205,11 @@ struct In that vision, [bind] is simply [concat_map] (though the cps version is significantly simpler), [plus] is concatenation, and [split] is pattern-matching. *) + type rich_exn = Exninfo.iexn + type 'a iolist = - { iolist : 'r. (exn -> 'r NonLogical.t) -> - ('a -> (exn -> 'r NonLogical.t) -> 'r NonLogical.t) -> + { iolist : 'r. (rich_exn -> 'r NonLogical.t) -> + ('a -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) -> 'r NonLogical.t } include Monad.Make(struct @@ -277,7 +279,7 @@ struct let m = m s in { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) } - let break (f : exn -> exn option) (m : 'a t) : 'a t = (); fun s -> + let break (f : rich_exn -> rich_exn option) (m : 'a t) : 'a t = (); fun s -> let m = m s in { iolist = fun nil cons -> m.iolist nil (fun x next -> cons x (fun e -> match f e with None -> next e | Some e -> nil e)) @@ -285,7 +287,7 @@ struct (** For [reflect] and [split] see the "Backtracking, Interleaving, and Terminating Monad Transformers" paper. *) - type 'a reified = ('a, exn -> 'a reified) list_view NonLogical.t + type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t let rec reflect (m : 'a reified) : 'a iolist = { iolist = fun nil cons -> @@ -296,7 +298,7 @@ struct NonLogical.(m >>= next) } - let split (m : 'a t) : ('a, exn -> 'a t) list_view t = (); fun s -> + let split (m : 'a t) : ('a, rich_exn -> 'a t) list_view t = (); fun s -> let m = m s in let rnil e = NonLogical.return (Nil e) in let rcons p l = NonLogical.return (Cons (p, l)) in diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli index 46cab18d2..0d05a2181 100644 --- a/proofs/logic_monad.mli +++ b/proofs/logic_monad.mli @@ -60,9 +60,9 @@ module NonLogical : sig (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) - val raise : exn -> 'a t + val raise : ?info:Exninfo.info -> exn -> 'a t (** [try ... with ...] but restricted to {!Exception}. *) - val catch : 'a t -> (exn -> 'a t) -> 'a t + val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t val timeout : int -> 'a t -> 'a t (** Construct a monadified side-effect. Exceptions raised by the argument are @@ -98,7 +98,7 @@ end (** A view type for the logical monad, which is a form of list, hence we can decompose it with as a list. *) type ('a, 'b) list_view = -| Nil of exn +| Nil of Exninfo.iexn | Cons of 'a * 'b (** The monad is parametrised in the types of state, environment and @@ -140,17 +140,17 @@ module Logical (P:Param) : sig val local : P.e -> 'a t -> 'a t val update : (P.u -> P.u) -> unit t - val zero : exn -> 'a t - val plus : 'a t -> (exn -> 'a t) -> 'a t - val split : 'a t -> (('a,(exn->'a t)) list_view) t + val zero : Exninfo.iexn -> 'a t + val plus : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t + val split : 'a t -> (('a,(Exninfo.iexn->'a t)) list_view) t val once : 'a t -> 'a t - val break : (exn -> exn option) -> 'a t -> 'a t + val break : (Exninfo.iexn -> Exninfo.iexn option) -> 'a t -> 'a t val lift : 'a NonLogical.t -> 'a t type 'a reified - val repr : 'a reified -> ('a, exn -> 'a reified) list_view NonLogical.t + val repr : 'a reified -> ('a, Exninfo.iexn -> 'a reified) list_view NonLogical.t val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 8e0f3accb..f4747c0d0 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -142,7 +142,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo with reraise -> let reraise = Errors.push reraise in delete_current_proof (); - raise reraise + iraise reraise let build_by_tactic env ctx ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 8dd739686..1a13edf17 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -91,7 +91,7 @@ val start_dependent_proof : (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : (exn -> exn) -> closed_proof +val close_proof : Future.fix_exn -> closed_proof (* Intermediate step necessary to delegate the future. * Both access the current proof state. The formes is supposed to be diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 01bb41ad3..f1d10bbe5 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -230,7 +230,7 @@ let apply env t sp = let ans = Proof.repr (Proof.run t false (sp,env)) in let ans = Logic_monad.NonLogical.run ans in match ans with - | Nil e -> raise (TacticFailure e) + | Nil (e, info) -> iraise (TacticFailure e, info) | Cons ((r, (state, _), status, info), _) -> r, state, status, Trace.to_tree info @@ -260,7 +260,12 @@ module Monad = Proof (** [tclZERO e] fails with exception [e]. It has no success. *) -let tclZERO = Proof.zero +let tclZERO ?info e = + let info = match info with + | None -> Exninfo.null + | Some info -> info + in + Proof.zero (e, info) (** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever the successes of [t1] have been depleted and it failed with [e], @@ -312,17 +317,17 @@ let tclEXACTLY_ONCE e t = let open Logic_monad in let open Proof in split t >>= function - | Nil e -> tclZERO e + | Nil (e, info) -> tclZERO ~info e | Cons (x,k) -> - Proof.split (k e) >>= function + Proof.split (k (e, Exninfo.null)) >>= function | Nil _ -> tclUNIT x | _ -> tclZERO MoreThanOneSuccess (** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *) type 'a case = -| Fail of exn -| Next of 'a * (exn -> 'a tactic) +| Fail of iexn +| Next of 'a * (iexn -> 'a tactic) let tclCASE t = let open Logic_monad in let map = function @@ -745,12 +750,12 @@ let tclTIMEOUT n t = | Logic_monad.Nil e -> return (Util.Inr e) | Logic_monad.Cons (r, _) -> return (Util.Inl r) end - begin let open Logic_monad.NonLogical in function - | Logic_monad.Timeout -> return (Util.Inr Timeout) - | Logic_monad.TacticFailure e as src -> - let e = Backtrace.app_backtrace ~src ~dst:e in - return (Util.Inr e) - | e -> Logic_monad.NonLogical.raise e + begin let open Logic_monad.NonLogical in function (e, info) -> + match e with + | Logic_monad.Timeout -> return (Util.Inr (Timeout, info)) + | Logic_monad.TacticFailure e -> + return (Util.Inr (e, info)) + | e -> Logic_monad.NonLogical.raise ~info e end end >>= function | Util.Inl (res,s,m,i) -> @@ -758,7 +763,7 @@ let tclTIMEOUT n t = Proof.put m >> Proof.update (fun _ -> i) >> return res - | Util.Inr e -> tclZERO e + | Util.Inr (e, info) -> tclZERO ~info e let tclTIME s t = let pr_time t1 t2 n msg = @@ -775,11 +780,11 @@ let tclTIME s t = tclUNIT () >>= fun () -> let tstart = System.get_time() in Proof.split t >>= let open Logic_monad in function - | Nil e -> + | Nil (e, info) -> begin let tend = System.get_time() in pr_time tstart tend n "failure"; - tclZERO e + tclZERO ~info e end | Cons (x,k) -> let tend = System.get_time() in @@ -894,8 +899,8 @@ module Goal = struct let (gl, sigma) = nf_gmake env sigma goal in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl)) with e when catchable_exception e -> - let e = Errors.push e in - tclZERO e + let (e, info) = Errors.push e in + tclZERO ~info e end end @@ -917,8 +922,8 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> - let e = Errors.push e in - tclZERO e + let (e, info) = Errors.push e in + tclZERO ~info e end end @@ -1082,8 +1087,8 @@ module V82 = struct InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >> Pv.set { solution = evd; comb = sgs; } with e when catchable_exception e -> - let e = Errors.push e in - tclZERO e + let (e, info) = Errors.push e in + tclZERO ~info e (* normalises the evars in the goals, and stores the result in @@ -1141,9 +1146,8 @@ module V82 = struct let (_,final,_,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = final.comb } with Logic_monad.TacticFailure e as src -> - let src = Errors.push src in - let e = Backtrace.app_backtrace ~src ~dst:e in - raise e + let (_, info) = Errors.push src in + iraise (e, info) let put_status = Status.put @@ -1151,6 +1155,7 @@ module V82 = struct let wrap_exceptions f = try f () - with e when catchable_exception e -> let e = Errors.push e in tclZERO e + with e when catchable_exception e -> + let (e, info) = Errors.push e in tclZERO ~info e end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index eb54ba3ae..25f4547a9 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -12,6 +12,7 @@ ['a tactic] is the (abstract) type of tactics modifying the proof state and returning a value of type ['a]. *) +open Util open Term (** Main state of tactics *) @@ -172,24 +173,24 @@ module Monad : Monad.S with type +'a t = 'a tactic (** {7 Failure and backtracking} *) (** [tclZERO e] fails with exception [e]. It has no success. *) -val tclZERO : exn -> 'a tactic +val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic (** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever the successes of [t1] have been depleted and it failed with [e], then it behaves as [t2 e]. In other words, [tclOR] inserts a backtracking point. *) -val tclOR : 'a tactic -> (exn -> 'a tactic) -> 'a tactic +val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic (** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one success or [t2 e] if [t1] fails with [e]. It is analogous to [try/with] handler of exception in that it is not a backtracking point. *) -val tclORELSE : 'a tactic -> (exn -> 'a tactic) -> 'a tactic +val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic (** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a] succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a] fails with [e], then it behaves as [f e]. *) -val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (exn -> 'b tactic) -> 'b tactic +val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic (** [tclONCE t] behave like [t] except it has at most one success: [tclONCE t] stops after the first success of [t]. If [t] fails @@ -211,8 +212,8 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic continuation. It is the most general primitive to control backtracking. *) type 'a case = - | Fail of exn - | Next of 'a * (exn -> 'a tactic) + | Fail of iexn + | Next of 'a * (iexn -> 'a tactic) val tclCASE : 'a tactic -> 'a case tactic (** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of @@ -220,7 +221,7 @@ val tclCASE : 'a tactic -> 'a case tactic failure with an exception [e] such that [p e = Some e'] is raised. At which point it drops the remaining successes, failing with [e']. [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *) -val tclBREAK : (exn -> exn option) -> 'a tactic -> 'a tactic +val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic (** {7 Focusing tactics} *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 391a78b34..e443ce077 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -218,14 +218,14 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) rslt;; -let catch_failerror e = +let catch_failerror (e, info) = if catchable_exception e then Control.check_for_interrupt () else match e with | FailError (0,_) -> Control.check_for_interrupt () | FailError (lvl,s) -> - raise (Exninfo.copy e (FailError (lvl - 1, s))) - | e -> raise e + iraise (FailError (lvl - 1, s), info) + | e -> iraise (e, info) (** FIXME: do we need to add a [Errors.push] here? *) (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) @@ -233,7 +233,8 @@ let tclORELSE0 t1 t2 g = try t1 g with (* Breakpoint *) - | e when Errors.noncritical e -> catch_failerror e; t2 g + | e when Errors.noncritical e -> + let e = Errors.push e in catch_failerror e; t2 g (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) @@ -245,7 +246,8 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 let tclORELSE_THEN t1 t2then t2else gls = match try Some(tclPROGRESS t1 gls) - with e when Errors.noncritical e -> catch_failerror e; None + with e when Errors.noncritical e -> + let e = Errors.push e in catch_failerror e; None with | None -> t2else gls | Some sgl -> @@ -270,16 +272,17 @@ let ite_gen tcal tac_if continue tac_else gl= success:=true;result in let tac_else0 e gl= if !success then - raise e + iraise e else try tac_else gl with - e' when Errors.noncritical e' -> raise e in + e' when Errors.noncritical e' -> iraise e in try tcal tac_if0 continue gl with (* Breakpoint *) - | e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl + | e when Errors.noncritical e -> + let e = Errors.push e in catch_failerror e; tac_else0 e gl (* Try the first tactic and, if it succeeds, continue with the second one, and if it fails, use the third one *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index ea1677f06..744843fc9 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -102,7 +102,7 @@ exception FailError of int * Pp.std_ppcmds Lazy.t (** Takes an exception and either raise it at the next level or do nothing. *) -val catch_failerror : exn -> unit +val catch_failerror : Exninfo.iexn -> unit val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 80aaf9f2a..b25f37b36 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -138,9 +138,9 @@ let rec prompt level = Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line - begin function + begin function (e, info) -> match e with | End_of_file -> exit - | e -> raise e + | e -> raise ~info e end >>= fun inst -> match inst with @@ -154,9 +154,9 @@ let rec prompt level = end | _ -> Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1))) - begin function + begin function (e, info) -> match e with | Failure _ | Invalid_argument _ -> prompt level - | e -> raise e + | e -> raise ~info e end end @@ -189,7 +189,7 @@ let debug_prompt lev tac f = (* What to execute *) Proofview.tclOR (f newlevel) - begin fun reraise -> + begin fun (reraise, info) -> Proofview.tclTHEN (Proofview.tclLIFT begin (skip:=0) >> (skipped:=0) >> @@ -197,7 +197,7 @@ let debug_prompt lev tac f = msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise) else return () end) - (Proofview.tclZERO reraise) + (Proofview.tclZERO ~info reraise) end let is_debug db = diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 298fa8237..a527675f6 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -359,7 +359,7 @@ module Make(T : Task) = struct let with_n_workers n f = let q = create n in try let rc = f q in destroy q; rc - with e -> let e = Errors.push e in destroy q; raise e + with e -> let e = Errors.push e in destroy q; iraise e let n_workers { active; parking } = Pool.n_workers active, Pool.n_workers parking diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 903b31b8f..4bc6f4ee6 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -38,7 +38,7 @@ let call_hook fix_exn hook l c = try hook l c with e when Errors.noncritical e -> let e = Errors.push e in - raise (fix_exn e) + iraise (fix_exn e) (* Support for mutually proved theorems *) @@ -206,7 +206,7 @@ let save id const cstrs do_guard (locality,poly,kind) hook = call_hook (fun exn -> exn) hook l r with e when Errors.noncritical e -> let e = Errors.push e in - raise (fix_exn e) + iraise (fix_exn e) let default_thm_id = Id.of_string "Unnamed_thm" diff --git a/stm/stm.ml b/stm/stm.ml index 6babc3e42..5b7642f53 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -85,7 +85,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr)) with e -> let e = Errors.push e in - raise Hooks.(call process_error e) + iraise Hooks.(call process_error e) end (* Wrapper for Vernac.parse_sentence to set the feedback id *) @@ -101,10 +101,10 @@ let vernac_parse ?newtip ?route eid s = | None -> raise (Invalid_argument "vernac_parse") | Some ast -> ast with e when Errors.noncritical e -> - let e = Errors.push e in - let loc = Option.default Loc.ghost (Loc.get_loc e) in - Hooks.(call parse_error feedback_id loc (print e)); - raise e) + let (e, info) = Errors.push e in + let loc = Option.default Loc.ghost (Loc.get_loc info) in + Hooks.(call parse_error feedback_id loc (iprint (e, info))); + iraise (e, info)) () let pr_open_cur_subgoals () = @@ -576,7 +576,7 @@ module State : sig val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool - val exn_on : Stateid.t -> ?valid:Stateid.t -> exn -> exn + val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn (* to send states across worker/master *) type frozen_state val get_cached : Stateid.t -> frozen_state @@ -637,13 +637,14 @@ end = struct (* {{{ *) try if VCS.get_state id = None then VCS.set_state id s with VCS.Expired -> () - let exn_on id ?valid e = - match Stateid.get e with - | Some _ -> e + let exn_on id ?valid (e, info) = + match Stateid.get info with + | Some _ -> (e, info) | None -> - let loc = Option.default Loc.ghost (Loc.get_loc e) in - Hooks.(call execution_error id loc (print e)); - Stateid.add Hooks.(call process_error e) ?valid id + let loc = Option.default Loc.ghost (Loc.get_loc info) in + Hooks.(call execution_error id loc (iprint (e, info))); + let (e, info) = Hooks.(call process_error (e, info)) in + (e, Stateid.add info ?valid id) let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) f id @@ -666,16 +667,16 @@ end = struct (* {{{ *) if Proof_global.there_are_pending_proofs () then VCS.goals id (Proof_global.get_open_goals ()); with e -> - let e = Errors.push e in + let (e, info) = Errors.push e in let good_id = !cur_id in cur_id := Stateid.dummy; VCS.reached id false; Hooks.(call unreachable_state id); - match Stateid.get e, safe_id with - | None, None -> raise (exn_on id ~valid:good_id e) - | None, Some good_id -> raise (exn_on id ~valid:good_id e) - | Some _, None -> raise e - | Some (_,at), Some id -> raise (Stateid.add e ~valid:id at) + match Stateid.get info, safe_id with + | None, None -> iraise (exn_on id ~valid:good_id (e, info)) + | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info)) + | Some _, None -> iraise (e, info) + | Some (_,at), Some id -> iraise (e, Stateid.add info ~valid:id at) end (* }}} *) @@ -986,7 +987,8 @@ end = struct (* {{{ *) | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> Pp.feedback (Feedback.InProgress ~-1); - let e = Stateid.add ~valid (RemoteException e_msg) e_error_at in + let info = Stateid.add ~valid Exninfo.null e_error_at in + let e = (RemoteException e_msg, info) in t_assign (`Exn e); List.iter (fun (id,s) -> State.assign id s) e_safe_states; if !Flags.async_proofs_always_delegate then `Park t_states else `Reset @@ -996,7 +998,8 @@ end = struct (* {{{ *) | None | Some (Querys _) | Some (States _) -> () | Some (BuildProof { t_start = start; t_assign }) -> let s = "Worker cancelled by the user" in - let e = Stateid.add ~valid:start (RemoteException (strbrk s)) start in + let info = Stateid.add ~valid:start Exninfo.null start in + let e = (RemoteException (strbrk s), info) in t_assign (`Exn e); Hooks.(call execution_error start Loc.ghost (strbrk s)); Pp.feedback (Feedback.InProgress ~-1) @@ -1023,13 +1026,14 @@ end = struct (* {{{ *) RespBuiltProof(rc,time) with | e when Errors.noncritical e -> + let (e, info) = Errors.push e in (* This can happen if the proof is broken. The error has also been * signalled as a feedback, hence we can silently recover *) - let e_error_at, e_safe_id = match Stateid.get e with + let e_error_at, e_safe_id = match Stateid.get info with | Some (safe, err) -> err, safe | None -> Stateid.dummy, Stateid.dummy in prerr_endline "failed with the following exception:"; - prerr_endline (string_of_ppcmds (print e)); + prerr_endline (string_of_ppcmds (iprint (e, info))); prerr_endline ("last safe id is: " ^ Stateid.to_string e_safe_id); prerr_endline ("cached? " ^ string_of_bool (State.is_cached e_safe_id)); let prog old_v n = @@ -1049,7 +1053,7 @@ end = struct (* {{{ *) | Some id -> aux (n+1) m id in (if is_cached e_safe_id then [e_safe_id,get_cached e_safe_id] else []) @ aux 1 (prog 1 1) e_safe_id in - RespError { e_error_at; e_safe_id; e_msg = print e; e_safe_states } + RespError { e_error_at; e_safe_id; e_msg = iprint (e, info); e_safe_states } let perform_query q = try Future.purify (fun { t_at; t_report_at; t_text; t_route = route } -> @@ -1168,12 +1172,12 @@ end = struct (* {{{ *) expr = (VernacEndProof (Proved (true,None))) }; Some proof with e -> - let e = Errors.push e in - (try match Stateid.get e with + let (e, info) = Errors.push e in + (try match Stateid.get info with | None -> Pp.pperrnl Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ - spc () ++ print e) + spc () ++ iprint (e, info)) | Some (_, cur) -> match VCS.visit cur with | { step = `Cmd { cast = { loc } } } @@ -1184,11 +1188,11 @@ end = struct (* {{{ *) Pp.pperrnl Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ str ": chars " ++ int start ++ str "-" ++ int stop ++ - spc () ++ print e) + spc () ++ iprint (e, info)) | _ -> Pp.pperrnl Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ - spc () ++ print e) + spc () ++ iprint (e, info)) with e -> Pp.msg_error (str"unable to print error message: " ++ str (Printexc.to_string e))); None @@ -1381,7 +1385,8 @@ end = struct (* {{{ *) let use_response _ { t_assign; t_state; t_state_fb; t_kill } = function | RespBuiltSubProof o -> t_assign (`Val o); `Stay | RespError msg -> - let e = Stateid.add ~valid:t_state (RemoteException msg) t_state_fb in + let info = Stateid.add ~valid:t_state Exninfo.null t_state_fb in + let e = (RemoteException msg, info) in t_assign (`Exn e); t_kill (); `Stay @@ -1710,8 +1715,9 @@ let known_state ?(redefine_qed=false) ~cache id = reach view.next; (try vernac_interp id x; with e when Errors.noncritical e -> - let e = Errors.push e in - raise (Stateid.add e ~valid:prev id)); + let (e, info) = Errors.push e in + let info = Stateid.add info ~valid:prev id in + iraise (e, info)); wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> @@ -1832,7 +1838,7 @@ let observe id = let e = Errors.push e in VCS.print (); VCS.restore vcs; - raise e + iraise e let finish ?(print_goals=false) () = observe (VCS.get_branch_pos (VCS.current_branch ())); @@ -1877,7 +1883,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = (u,a,true), p with e -> let e = Errors.push e in - Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e); + Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 let merge_proof_branch ?id qast keep brname = @@ -1903,13 +1909,13 @@ let merge_proof_branch ?id qast keep brname = VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> - raise (State.exn_on Stateid.dummy Proof_global.NoCurrentProof) + iraise (State.exn_on Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) -let handle_failure e vcs tty = - if e = Errors.Drop then raise e else - match Stateid.get e with +let handle_failure (e, info) vcs tty = + if e = Errors.Drop then iraise (e, info) else + match Stateid.get info with | None -> VCS.restore vcs; VCS.print (); @@ -1931,7 +1937,7 @@ let handle_failure e vcs tty = Reach.known_state ~cache:(interactive ()) safe_id; end; VCS.print (); - raise e + iraise (e, info) let snapshot_vi ldir long_f_dot_v = finish (); @@ -2003,12 +2009,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = { verbose = true; loc; expr } with e when Errors.noncritical e -> let e = Errors.push e in - raise(State.exn_on report_id e)); `Ok + iraise (State.exn_on report_id e)); `Ok | VtQuery (false,(report_id,route)), VtNow -> (try vernac_interp report_id ~route x with e when Errors.noncritical e -> let e = Errors.push e in - raise(State.exn_on report_id e)); `Ok + iraise (State.exn_on report_id e)); `Ok | VtQuery (true,(report_id,_)), w -> assert(Stateid.equal report_id Stateid.dummy); let id = VCS.new_node ~id:newtip () in @@ -2298,8 +2304,8 @@ let edit_at id = VCS.print (); rc with e -> - let e = Errors.push e in - match Stateid.get e with + let (e, info) = Errors.push e in + match Stateid.get info with | None -> VCS.print (); anomaly (str ("edit_at "^Stateid.to_string id^": ") ++ @@ -2308,7 +2314,7 @@ let edit_at id = prerr_endline ("Failed at state " ^ Stateid.to_string id); VCS.restore vcs; VCS.print (); - raise e + iraise (e, info) (*********************** TTY API (PG, coqtop, coqc) ***************************) (******************************************************************************) diff --git a/stm/stm.mli b/stm/stm.mli index 475a367b3..b39fd5082 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -126,7 +126,7 @@ val get_current_proof_name : unit -> Id.t option val show_script : ?proof:Proof_global.closed_proof -> unit -> unit (** Reverse dependency hooks *) -val process_error_hook : (exn -> exn) Hook.t +val process_error_hook : Future.fix_exn Hook.t val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t diff --git a/tactics/auto.ml b/tactics/auto.ml index 43aa84e7a..ef6c38bf6 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -205,7 +205,7 @@ let tclLOG (dbg,depth,trace) pp tac = with reraise -> let reraise = Errors.push reraise in msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); - raise reraise + iraise reraise end | Info -> (* For "info (trivial/auto)", we store a log trace *) @@ -217,7 +217,7 @@ let tclLOG (dbg,depth,trace) pp tac = with reraise -> let reraise = Errors.push reraise in trace := (depth, None) :: !trace; - raise reraise + iraise reraise end (** For info, from the linear trace information, we reconstitute the part diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 9a241c7ef..13742f740 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -71,9 +71,9 @@ let contradiction_context = filter_hyp (fun typ -> is_conv_leq typ t) (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|]))) end) - begin function + begin function (e, info) -> match e with | Not_found -> seek_neg rest - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end) | _ -> seek_neg rest in @@ -108,9 +108,9 @@ let contradiction_term (c,lbind as cl) = else Proofview.tclZERO Not_found end - begin function + begin function (e, info) -> match e with | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction.")) - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end end diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 303c73d6b..ca1cc7506 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -228,6 +228,7 @@ module SearchProblem = struct (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) (lgls,pptac) :: aux tacl with e when Errors.noncritical e -> + let e = Errors.push e in Refiner.catch_failerror e; aux tacl in aux l diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index a43e99a7f..df8a018bb 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -157,9 +157,9 @@ let solveEqBranch rectype = (tclTHEN (choose_eq eqonleft) intros_reflexivity) end end - begin function + begin function (e, info) -> match e with | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!")) - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end (* The tactic Decide Equality *) @@ -184,10 +184,10 @@ let decideGralEquality = (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) end end - begin function + begin function (e, info) -> match e with | PatternMatchingFailure -> Proofview.tclZERO (UserError ("", Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.")) - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end let decideEqualityGoal = tclTHEN intros decideGralEquality diff --git a/tactics/equality.ml b/tactics/equality.ml index 536112553..9740f6c1f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -223,10 +223,10 @@ let general_elim_clause with_evars frzevars cls rew elim = tclNOTSAMEGOAL (rewrite_elim with_evars frzevars cls rew elim) | Some _ -> rewrite_elim with_evars frzevars cls rew elim end - begin function + begin function (e, info) -> match e with | PretypeError (env, evd, NoOccurrenceFound (c', _)) -> Proofview.tclZERO (PretypeError (env, evd, NoOccurrenceFound (c', cls))) - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end let general_elim_clause with_evars frzevars tac cls c t l l2r elim = @@ -394,7 +394,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac lft2rgt occs (c,l) ~new_goals:[]) tac end begin function - | e -> + | (e, info) -> let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) match match_with_equality_type t' with @@ -402,7 +402,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl - | None -> Proofview.tclZERO e + | None -> Proofview.tclZERO ~info e (* error "The provided term does not end with an equality or a declared rewrite relation." *) end end @@ -1507,7 +1507,7 @@ let cutSubstInHyp l2r eqn id = end let try_rewrite tac = - Proofview.tclORELSE tac begin function + Proofview.tclORELSE tac begin function (e, info) -> match e with | ConstrMatching.PatternMatchingFailure -> tclZEROMSG (str "Not a primitive equality here.") | e when catchable_exception e -> @@ -1516,7 +1516,7 @@ let try_rewrite tac = | NothingToRewrite -> tclZEROMSG (strbrk "Nothing to rewrite.") - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end let cutSubstClause l2r eqn cls = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 289014a58..436a66ad2 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -627,7 +627,8 @@ let hResolve id c occ t = Pretyping.understand env sigma t_hole with | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> - let loc = match Loc.get_loc e with None -> Loc.ghost | Some loc -> loc in + let (e, info) = Errors.push e in + let loc = match Loc.get_loc info with None -> Loc.ghost | Some loc -> loc in resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole) in let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in diff --git a/tactics/inv.ml b/tactics/inv.ml index d0de08c27..39310798d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -472,7 +472,7 @@ let raw_inversion inv_kind id status names = end (* Error messages of the inversion tactics *) -let wrap_inv_error id = function +let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> Proofview.tclENV >>= fun env -> @@ -481,7 +481,7 @@ let wrap_inv_error id = function pr_sort k ++ strbrk " which is not allowed for inductive definition " ++ pr_inductive env (fst i) ++ str ".")) - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e (* The most general inversion tactic *) let inversion inv_kind status names id = diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 1245e7c29..9d9847ea5 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -2011,15 +2011,15 @@ let setoid_proof ty fn fallback = | e -> Proofview.tclORELSE fallback - begin function + begin function (e', info) -> match e' with | Hipattern.NoEquationFound -> begin match e with - | Not_found -> + | (Not_found, _) -> let rel, _, _ = decompose_app_rel env sigma concl in not_declared env ty rel - | _ -> Proofview.tclZERO e + | (e, info) -> Proofview.tclZERO ~info e end - | e' -> Proofview.tclZERO e' + | e' -> Proofview.tclZERO ~info e' end end end diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index fc31c3a99..dd937cf6a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -128,15 +128,15 @@ end let dloc = Loc.ghost -let catching_error call_trace fail e = +let catching_error call_trace fail (e, info) = let inner_trace = - Option.default [] (Exninfo.get e ltac_trace_info) + Option.default [] (Exninfo.get info ltac_trace_info) in - if List.is_empty call_trace && List.is_empty inner_trace then fail e + if List.is_empty call_trace && List.is_empty inner_trace then fail (e, info) else begin assert (Errors.noncritical e); (* preserved invariant *) let new_trace = inner_trace @ call_trace in - let located_exc = Exninfo.add e ltac_trace_info new_trace in + let located_exc = (e, Exninfo.add info ltac_trace_info new_trace) in fail located_exc end @@ -144,12 +144,12 @@ let catch_error call_trace f x = try f x with e when Errors.noncritical e -> let e = Errors.push e in - catching_error call_trace raise e + catching_error call_trace iraise e let catch_error_tac call_trace tac = Proofview.tclORELSE tac - (catching_error call_trace Proofview.tclZERO) + (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e)) let curr_debug ist = match TacStore.get ist.extra f_debug with | None -> DebugOff @@ -747,9 +747,9 @@ let interp_may_eval f ist env sigma = function (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) - Proofview.NonLogical.run (debugging_exception_step ist false reraise (fun () -> + Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"interpretation of term " ++ pr_glob_constr_env env (fst c))); - raise reraise + iraise reraise (* Interprets a constr expression possibly to first evaluate *) let interp_constr_may_eval ist env sigma c = @@ -761,8 +761,8 @@ let interp_constr_may_eval ist env sigma c = (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) - Proofview.NonLogical.run (debugging_exception_step ist false reraise (fun () -> str"evaluation of term")); - raise reraise + Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"evaluation of term")); + iraise reraise in begin (* spiwack: to avoid unnecessary modifications of tacinterp, as this @@ -1462,9 +1462,9 @@ and interp_app loc ist fv largs : typed_generic_argument Ftactic.t = catch_error_tac trace (val_interp ist body) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end - begin fun e -> + begin fun (e, info) -> Proofview.tclLIFT (debugging_exception_step ist false e (fun () -> str "evaluation")) <*> - Proofview.tclZERO e + Proofview.tclZERO ~info e end end >>= fun v -> (* No errors happened, we propagate the trace *) @@ -1553,9 +1553,9 @@ and interp_match_successes lz ist tac = let tac = Proofview.tclONCE tac in tac >>= fun ans -> interp_match_success ist ans else - let break e = match e with + let break (e, info) = match e with | FailError (0, _) -> None - | FailError (n, s) -> Some (FailError (pred n, s)) + | FailError (n, s) -> Some (FailError (pred n, s), info) | _ -> None in let tac = Proofview.tclBREAK break tac >>= fun ans -> interp_match_success ist ans in @@ -1568,10 +1568,10 @@ and interp_match ist lz constr lmr = begin Proofview.tclORELSE (interp_ltac_constr ist constr) begin function - | e -> + | (e, info) -> Proofview.tclLIFT (debugging_exception_step ist true e (fun () -> str "evaluation of the matched expression")) <*> - Proofview.tclZERO e + Proofview.tclZERO ~info e end end >>= fun constr -> Ftactic.enter begin fun gl -> @@ -1715,7 +1715,7 @@ and interp_ltac_constr ist e : constr Ftactic.t = let (>>=) = Ftactic.bind in begin Proofview.tclORELSE (val_interp ist e) - begin function + begin function (err, info) -> match err with | Not_found -> Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1726,7 +1726,7 @@ and interp_ltac_constr ist e : constr Ftactic.t = end <*> Proofview.tclZERO Not_found end - | e -> Proofview.tclZERO e + | err -> Proofview.tclZERO ~info err end end >>= fun result -> Ftactic.enter begin fun gl -> @@ -2348,9 +2348,8 @@ let _ = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> (** Catch the inner error of the monad tactic *) - let src = Errors.push src in - let e = Backtrace.app_backtrace ~src ~dst:e in - raise e + let (_, info) = Errors.push src in + iraise (e, info) in (** Plug back the retrieved sigma *) let sigma = Proof.in_proof prf (fun sigma -> sigma) in diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml index c662fad0b..52fa2e4a2 100644 --- a/tactics/tacticMatching.ml +++ b/tactics/tacticMatching.ml @@ -104,6 +104,8 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) = let matching_error = Errors.UserError ("tactic matching" , Pp.str "No matching clauses for match.") +let imatching_error = (matching_error, Exninfo.null) + (** A functor is introduced to share the environment and the evar_map. They do not change and it would be a pity to introduce closures everywhere just for the occasional calls to @@ -191,12 +193,12 @@ module PatternMatching (E:StaticEnvironment) = struct m.stream eval ctx (** Chooses in a list, in the same order as the list *) - let rec pick (l:'a list) e : 'a m = match l with - | [] -> { stream = fun _ _ -> Proofview.tclZERO e } + let rec pick (l:'a list) (e, info) : 'a m = match l with + | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e } | x :: l -> { stream = fun k ctx -> Proofview.tclOR (k x ctx) (fun e -> (pick l e).stream k ctx) } - let pick l = pick l matching_error + let pick l = pick l imatching_error (** Declares a subsitution, a context substitution and a term substitution. *) let put subst context terms : unit m = @@ -234,20 +236,20 @@ module PatternMatching (E:StaticEnvironment) = struct end | Subterm (with_app_context,id_ctxt,p) -> - let rec map s e = + let rec map s (e, info) = { stream = fun k ctx -> match IStream.peek s with - | IStream.Nil -> Proofview.tclZERO e + | IStream.Nil -> Proofview.tclZERO ~info e | IStream.Cons ({ ConstrMatching.m_sub ; m_ctx }, s) -> let subst = adjust m_sub in let context = id_map_try_add id_ctxt m_ctx Id.Map.empty in let terms = empty_term_subst in let nctx = { subst ; context ; terms ; lhs = () } in match merge ctx nctx with - | None -> (map s e).stream k ctx + | None -> (map s (e, info)).stream k ctx | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx) } in - map (ConstrMatching.match_subterm_gen E.env E.sigma with_app_context p term) matching_error + map (ConstrMatching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error (** [rule_match_term term rule] matches the term [term] with the @@ -261,8 +263,8 @@ module PatternMatching (E:StaticEnvironment) = struct (** [match_term term rules] matches the term [term] with the set of matching rules [rules].*) - let rec match_term e term rules = match rules with - | [] -> { stream = fun _ _ -> Proofview.tclZERO e } + let rec match_term (e, info) term rules = match rules with + | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e } | r :: rules -> { stream = fun k ctx -> let head = rule_match_term term r in @@ -333,8 +335,8 @@ module PatternMatching (E:StaticEnvironment) = struct (** [match_goal hyps concl rules] matches the goal [hyps|-concl] with the set of matching rules [rules]. *) - let rec match_goal e hyps concl rules = match rules with - | [] -> { stream = fun _ _ -> Proofview.tclZERO e } + let rec match_goal (e, info) hyps concl rules = match rules with + | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e } | r :: rules -> { stream = fun k ctx -> let head = rule_match_goal hyps concl r in @@ -354,7 +356,7 @@ let match_term env sigma term rules = let sigma = sigma end in let module M = PatternMatching(E) in - M.run (M.match_term matching_error term rules) + M.run (M.match_term imatching_error term rules) (** [match_goal env sigma hyps concl rules] matches the goal @@ -368,4 +370,4 @@ let match_goal env sigma hyps concl rules = let sigma = sigma end in let module M = PatternMatching(E) in - M.run (M.match_goal matching_error hyps concl rules) + M.run (M.match_goal imatching_error hyps concl rules) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 82ec15559..5c899aefc 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -300,11 +300,11 @@ module New = struct let tclZEROMSG ?loc msg = let err = UserError ("", msg) in - let err = match loc with - | None -> err - | Some loc -> Loc.add_loc err loc + let info = match loc with + | None -> Exninfo.null + | Some loc -> Loc.add_loc Exninfo.null loc in - tclZERO err + tclZERO ~info err let catch_failerror e = try @@ -362,14 +362,14 @@ module New = struct t1 <*> Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *) begin tclEXTEND (Array.to_list l1) repeat (Array.to_list l2) end - begin function + begin function (e, info) -> match e with | SizeMismatch (i,_)-> let errmsg = str"Incorrect number of goals" ++ spc() ++ str"(expected "++int i++str(String.plural i " tactic") ++ str")" in tclFAIL 0 errmsg - | reraise -> tclZERO reraise + | reraise -> tclZERO ~info reraise end end let tclTHENSFIRSTn t1 l repeat = @@ -385,14 +385,14 @@ module New = struct tclINDEPENDENT begin t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *) begin tclDISPATCH l end - begin function + begin function (e, info) -> match e with | SizeMismatch (i,_)-> let errmsg = str"Incorrect number of goals" ++ spc() ++ str"(expected "++int i++str(String.plural i " tactic") ++ str")" in tclFAIL 0 errmsg - | reraise -> tclZERO reraise + | reraise -> tclZERO ~info reraise end end let tclTHENLIST l = @@ -410,7 +410,7 @@ module New = struct tclINDEPENDENT begin Proofview.tclIFCATCH t1 (fun () -> t2) - (fun e -> Proofview.tclORELSE t3 (fun e' -> tclZERO e)) + (fun (e, info) -> Proofview.tclORELSE t3 (fun e' -> tclZERO ~info e)) end let tclIFTHENSVELSE t1 a t3 = Proofview.tclIFCATCH t1 @@ -519,9 +519,9 @@ module New = struct let tclTIMEOUT n t = Proofview.tclOR (Proofview.tclTIMEOUT n t) - begin function + begin function (e, info) -> match e with | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e))) - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end let tclTIME s t = diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index fbdc6d94e..49cae37a7 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -156,7 +156,7 @@ module New : sig (** [catch_failerror e] fails and decreases the level if [e] is an Ltac error with level more than 0. Otherwise succeeds. *) - val catch_failerror : exn -> unit tactic + val catch_failerror : Util.iexn -> unit tactic val tclIDTAC : unit tactic val tclTHEN : unit tactic -> unit tactic -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 40228c4df..26fd77323 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -763,11 +763,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = Proofview.tclORELSE (Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl) (intro_then_gen name_flag move_flag false dep_flag tac)) - begin function + begin function (e, info) -> match e with | RefinerError IntroNeedsProduct -> Proofview.tclZERO (Errors.UserError("Intro",str "No product even after head-reduction.")) - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end end @@ -805,10 +805,10 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = intro_then_gen name_flag move_flag false dep_flag (fun id -> aux (n+1) (id::ids)) end - begin function + begin function (e, info) -> match e with | RefinerError IntroNeedsProduct -> tac ids - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end else tac ids @@ -1246,12 +1246,12 @@ let default_elim with_evars clear_flag (c,_ as cx) = Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) (general_elim with_evars clear_flag cx elim) end) - begin function + begin function (e, info) -> match e with | IsNonrec -> (* For records, induction principles aren't there by default anymore. Instead, we do a case analysis instead. *) general_case_analysis with_evars clear_flag cx - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end let elim_in_context with_evars clear_flag c = function @@ -1452,16 +1452,18 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) in Proofview.tclORELSE (try_apply thm_ty0 concl_nprod) - (function PretypeError _|RefinerError _|UserError _|Failure _ as exn0 -> + (function (e, info) -> match e with + | PretypeError _|RefinerError _|UserError _|Failure _ as exn0 -> let rec try_red_apply thm_ty = try (* Try to head-reduce the conclusion of the theorem *) let red_thm = try_red_product env sigma thm_ty in Proofview.tclORELSE (try_apply red_thm concl_nprod) - (function PretypeError _|RefinerError _|UserError _|Failure _ -> + (function (e, info) -> match e with + | PretypeError _|RefinerError _|UserError _|Failure _ -> try_red_apply red_thm - | exn -> raise exn) + | exn -> iraise (exn, info)) with Redelimination -> (* Last chance: if the head is a variable, apply may try second order unification *) @@ -1472,22 +1474,26 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) Tacticals.New.tclTHEN (try_main_apply b (mkVar id)) (Proofview.V82.tactic (thin [id]))) - (fun _ -> Proofview.tclZERO (Loc.add_loc exn0 loc)) c + (fun _ -> + let info = Loc.add_loc info loc in + Proofview.tclZERO ~info exn0) c else - Proofview.tclZERO (Loc.add_loc exn0 loc) in + let info = Loc.add_loc info loc in + Proofview.tclZERO ~info exn0 in if not (Int.equal concl_nprod 0) then try Proofview.tclORELSE (try_apply thm_ty 0) - (function PretypeError _|RefinerError _|UserError _|Failure _-> + (function (e, info) -> match e with + | PretypeError _|RefinerError _|UserError _|Failure _-> tac - | exn -> raise exn) + | exn -> iraise (exn, info)) with UserError _ | Exit -> tac else tac in try_red_apply thm_ty0 - | exn -> raise exn) + | exn -> iraise (exn, info)) end in Tacticals.New.tclTHENLIST [ @@ -1570,7 +1576,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) = with e when Errors.noncritical e -> let e = Errors.push e in try aux (clenv_push_prod clause) - with NotExtensibleClause -> raise e + with NotExtensibleClause -> iraise e in aux (make_clenv_binding env sigma (d,thm) lbind) @@ -1601,7 +1607,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming let e = Errors.push e in (descend_in_conjunctions [targetid] (fun b id -> aux (id::idstoclear) b (mkVar id)) - (fun _ -> raise e) c) + (fun _ -> iraise e) c) end in aux [] with_destruct d @@ -2652,14 +2658,14 @@ let dest_intro_patterns avoid thin dest pat tac = let safe_dest_intro_patterns avoid thin dest pat tac = Proofview.tclORELSE (dest_intro_patterns avoid thin dest pat tac) - begin function + begin function (e, info) -> match e with | UserError ("move_hyp",_) -> (* May happen e.g. with "destruct x using s" with an hypothesis which is morally an induction hypothesis to be "MoveLast" if known as such but which is considered instead as a subterm of a constructor to be move at the place of x. *) dest_intro_patterns avoid thin MoveLast pat tac - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end type elim_arg_kind = RecArg | IndArg | OtherArg @@ -4155,9 +4161,9 @@ let reflexivity_red allowred = let reflexivity = Proofview.tclORELSE (reflexivity_red false) - begin function + begin function (e, info) -> match e with | NoEquationFound -> Hook.get forward_setoid_reflexivity - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end let intros_reflexivity = (Tacticals.New.tclTHEN intros reflexivity) @@ -4209,9 +4215,9 @@ let symmetry_red allowred = let symmetry = Proofview.tclORELSE (symmetry_red false) - begin function + begin function (e, info) -> match e with | NoEquationFound -> Hook.get forward_setoid_symmetry - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () @@ -4232,9 +4238,9 @@ let symmetry_in id = [ intro_replacing id; Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] end - begin function + begin function (e, info) -> match e with | NoEquationFound -> Hook.get forward_setoid_symmetry_in id - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end end @@ -4306,9 +4312,9 @@ let transitivity_red allowred t = let transitivity_gen t = Proofview.tclORELSE (transitivity_red false t) - begin function + begin function (e, info) -> match e with | NoEquationFound -> Hook.get forward_setoid_transitivity t - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end let etransitivity = transitivity_gen None @@ -4365,9 +4371,8 @@ let abstract_subproof id gk tac = which is an error irrelevant to the proof system (in fact it means that [e] comes from [tac] failing to yield enough success). Hence it reraises [e]. *) - let src = Errors.push src in - let e = Backtrace.app_backtrace ~src ~dst:e in - raise e + let (_, info) = Errors.push src in + iraise (e, info) in let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 346f560f8..075f66751 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -314,10 +314,10 @@ let intuition_gen ist flags tac = let tauto_intuitionistic flags = Proofview.tclORELSE (intuition_gen (default_ist ()) flags <:tactic<fail>>) - begin function + begin function (e, info) -> match e with | Refiner.FailError _ | UserError _ -> Proofview.tclZERO (UserError ("tauto" , str "tauto failed.")) - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end let coq_nnpp_path = @@ -327,9 +327,9 @@ let coq_nnpp_path = let tauto_classical flags nnpp = Proofview.tclORELSE (Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags)) - begin function + begin function (e, info) -> match e with | UserError _ -> Proofview.tclZERO (UserError ("tauto" , str "Classical tauto failed.")) - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end let tauto_gen flags = diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 8c98c813a..03c9afbf7 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -53,12 +53,12 @@ let _ = Errors.register_handler explain_exn_default (** Pre-explain a vernac interpretation error *) -let wrap_vernac_error exn strm = +let wrap_vernac_error (exn, info) strm = 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 - Exninfo.copy exn e + (e, info) -let process_vernac_interp_error exn = match exn with +let process_vernac_interp_error exn = match fst exn with | Univ.UniverseInconsistency i -> let msg = if !Constrextern.print_universes then @@ -99,29 +99,30 @@ let process_vernac_interp_error exn = match exn with if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").") | AlreadyDeclared msg -> wrap_vernac_error exn (msg ++ str ".") - | exc -> - exc + | _ -> + exn let rec strip_wrapping_exceptions = function - | Logic_monad.TacticFailure e as src -> - let e = Backtrace.app_backtrace ~src ~dst:e in + | Logic_monad.TacticFailure e -> strip_wrapping_exceptions e | exc -> exc -let process_vernac_interp_error exc = +let process_vernac_interp_error (exc, info) = let exc = strip_wrapping_exceptions exc in - let e = process_vernac_interp_error exc in - let ltac_trace = Exninfo.get exc Proof_type.ltac_trace_info in - let loc = Option.default Loc.ghost (Loc.get_loc e) in + let e = process_vernac_interp_error (exc, info) in + let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in + let loc = Option.default Loc.ghost (Loc.get_loc info) in match ltac_trace with | None -> e | Some trace -> + let (e, info) = e in match Himsg.extract_ltac_trace trace loc with - | None, loc -> Loc.add_loc e loc - | Some msg, loc -> Loc.add_loc (EvaluatedError (msg, Some e)) loc + | None, loc -> (e, Loc.add_loc info loc) + | Some msg, loc -> + (EvaluatedError (msg, Some e), Loc.add_loc info loc) let _ = Tactic_debug.explain_logic_error := - (fun e -> Errors.print (process_vernac_interp_error e)) + (fun e -> Errors.print (fst (process_vernac_interp_error (e, Exninfo.null)))) let _ = Tactic_debug.explain_logic_error_no_anomaly := - (fun e -> Errors.print_no_report (process_vernac_interp_error e)) + (fun e -> Errors.print_no_report (fst (process_vernac_interp_error (e, Exninfo.null)))) diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 2079de8b1..f027f8c75 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds (** Pre-explain a vernac interpretation error *) -val process_vernac_interp_error : exn -> exn +val process_vernac_interp_error : Util.iexn -> Util.iexn (** General explain function. Should not be used directly now, see instead function [Errors.print] and variants *) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 0e52fe6ab..9d4a74b75 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -53,7 +53,7 @@ let load_rcfile() = with reraise -> let reraise = Errors.push reraise in let () = msg_info (str"Load of rcfile failed.") in - raise reraise + iraise reraise else Flags.if_verbose msg_info (str"Skipping rcfile loading.") diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index c29b52cec..05bf3dc98 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -260,16 +260,16 @@ let locate_exn = function (* Toplevel error explanation. *) -let print_toplevel_error e = - let loc = Option.default Loc.ghost (Loc.get_loc e) in - let locmsg = match Vernac.get_exn_files e with +let print_toplevel_error (e, info) = + let loc = Option.default Loc.ghost (Loc.get_loc info) in + let locmsg = match Vernac.get_exn_files info with | Some files -> print_location_in_file files loc | None -> if locate_exn e && valid_buffer_loc top_buffer loc then print_highlight_location top_buffer loc else mt () in - locmsg ++ Errors.print e + locmsg ++ Errors.iprint (e, info) (* Read the input stream until a dot is encountered *) let parse_to_dot = @@ -297,7 +297,7 @@ let read_sentence () = with reraise -> let reraise = Errors.push reraise in discard_to_dot (); - raise reraise + iraise reraise (** [do_vernac] reads and executes a toplevel phrase, and print error messages when an exception is raised, except for the following: @@ -322,6 +322,7 @@ let do_vernac () = if Mltop.is_ocaml_top() then raise Errors.Drop else ppnl (str"Error: There is no ML toplevel." ++ fnl ()) | any -> + let any = Errors.push any in Format.set_formatter_out_channel stdout; let msg = print_toplevel_error any ++ fnl () in pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg; diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 4aedaa035..3011471f2 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -30,7 +30,7 @@ val set_prompt : (unit -> string) -> unit May raise only the following exceptions: [Drop] and [End_of_input], meaning we get out of the Coq loop. *) -val print_toplevel_error : exn -> std_ppcmds +val print_toplevel_error : Exninfo.iexn -> std_ppcmds (** Parse and execute one vernac command. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5bf8cfb3b..83d693644 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -581,12 +581,13 @@ let init arglist = check_vi_tasks (); outputstate () with any -> + let any = Errors.push any in flush_all(); let msg = if !batch_mode then mt () else str "Error during initialization:" ++ fnl () in - fatal_error (msg ++ Coqloop.print_toplevel_error any) (Errors.is_anomaly any) + fatal_error (msg ++ Coqloop.print_toplevel_error any) (Errors.is_anomaly (fst any)) end; if !batch_mode then begin flush_all(); diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 6e63c4e13..85f8f61a8 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -310,8 +310,9 @@ let parse_format ((loc, str) : lstring) = else error "Empty format." with reraise -> - let e = Errors.push reraise in - Loc.raise loc e + let (e, info) = Errors.push reraise in + let info = Loc.add_loc info loc in + iraise (e, info) (***********************) (* Analyzing notations *) @@ -1136,7 +1137,7 @@ let with_lib_stk_protection f x = with reraise -> let reraise = Errors.push reraise in let () = Lib.unfreeze fs in - raise reraise + iraise reraise let with_syntax_protection f x = with_lib_stk_protection diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index d9b739354..9b040d70b 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -120,8 +120,8 @@ let ml_load s = with | e when Errors.noncritical e -> let e = Errors.push e in - match e with - | (UserError _ | Failure _ | Not_found as u) -> raise u + match fst e with + | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e) | exc -> let msg = report_on_load_obj_error exc in errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index d5073802d..aa0685861 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -839,7 +839,8 @@ let rec solve_obligation prg num tac = obls (pred rem) with e when Errors.noncritical e -> - pperror (Errors.print (Cerrors.process_vernac_interp_error e)) + let e = Errors.push e in + pperror (Errors.iprint (Cerrors.process_vernac_interp_error e)) in match res with | Remain n when n > 0 -> @@ -892,7 +893,7 @@ and solve_obligation_by_tac prg obls i tac = true else false with e when Errors.noncritical e -> - let e = Errors.push e in + let (e, _) = Errors.push e in match e with | Refiner.FailError (_, s) -> user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 98a3d7496..e5c9849a9 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -78,9 +78,9 @@ let get_exn_files e = Exninfo.get e files_of_exn let add_exn_files e f = Exninfo.add e files_of_exn f -let raise_with_file f e = - let inner_f = match get_exn_files e with None -> f | Some ff -> ff.inner in - raise (add_exn_files e { outer = f; inner = inner_f }) +let raise_with_file f (e, info) = + let inner_f = match get_exn_files info with None -> f | Some ff -> ff.inner in + iraise (e, add_exn_files info { outer = f; inner = inner_f }) let disable_drop = function | Drop -> Errors.error "Drop is forbidden." @@ -232,7 +232,7 @@ let rec vernac_com verbosely checknav (loc,com) = with reraise -> let reraise = Errors.push reraise in restore_translator_coqdoc st; - raise reraise + iraise reraise end | v when !just_parsing -> () @@ -246,11 +246,11 @@ let rec vernac_com verbosely checknav (loc,com) = let com = if !Flags.time then VernacTime [loc,com] else com in interp com with reraise -> - let reraise = Errors.push reraise in + let (reraise, info) = Errors.push reraise in Format.set_formatter_out_channel stdout; - let loc' = Option.default Loc.ghost (Loc.get_loc reraise) in - if Loc.is_ghost loc' then Loc.raise loc reraise - else raise reraise + let loc' = Option.default Loc.ghost (Loc.get_loc info) in + if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc) + else iraise (reraise, info) and read_vernac_file verbosely s = Flags.make_warn verbosely; @@ -269,14 +269,14 @@ and read_vernac_file verbosely s = pp_flush () done with any -> (* whatever the exception *) - let e = Errors.push any in + let (e, info) = Errors.push any in Format.set_formatter_out_channel stdout; close_input in_chan input; (* we must close the file first *) match e with | End_of_input -> if do_beautify () then pr_new_syntax (Loc.make_loc (max_int,max_int)) None - | _ -> raise_with_file fname (disable_drop e) + | _ -> raise_with_file fname (disable_drop e, info) (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit] It executes one vernacular command. By default the command is @@ -299,9 +299,9 @@ let load_vernac verb file = read_vernac_file verb file; if !Flags.beautify_file then close_out !chan_beautify; with any -> - let e = Errors.push any in + let (e, info) = Errors.push any in if !Flags.beautify_file then close_out !chan_beautify; - raise_with_file file (disable_drop e) + raise_with_file file (disable_drop e, info) (* Compile a vernac file (f is assumed without .v suffix) *) let compile verbosely f = diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index d46622a02..42353c31a 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -39,4 +39,4 @@ val is_navigation_vernac : Vernacexpr.vernac_expr -> bool type location_files = { outer : string; inner : string } -val get_exn_files : exn -> location_files option +val get_exn_files : Exninfo.info -> location_files option diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 287bf2304..4a4c5a433 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -355,7 +355,7 @@ let dump_universes_gen g s = with reraise -> let reraise = Errors.push reraise in close (); - raise reraise + iraise reraise let dump_universes sorted s = let g = Global.universes () in @@ -2037,10 +2037,10 @@ let vernac_timeout f = let restore_timeout () = current_timeout := None -let locate_if_not_already loc exn = - match Loc.get_loc exn with - | None -> Loc.add_loc exn loc - | Some l -> if Loc.is_ghost l then Loc.add_loc exn loc else exn +let locate_if_not_already loc (e, info) = + match Loc.get_loc info with + | None -> (e, Loc.add_loc info loc) + | Some l -> if Loc.is_ghost l then (e, Loc.add_loc info loc) else (e, info) exception HasNotFailed exception HasFailed of string @@ -2056,11 +2056,13 @@ let with_fail b f = try f v; raise HasNotFailed with | HasNotFailed as e -> raise e - | e -> raise (HasFailed (Pp.string_of_ppcmds - (Errors.print (Cerrors.process_vernac_interp_error e))))) + | e -> + let e = Errors.push e in + raise (HasFailed (Pp.string_of_ppcmds + (Errors.iprint (Cerrors.process_vernac_interp_error e))))) () with e when Errors.noncritical e -> - let e = Errors.push e in + let (e, _) = Errors.push e in match e with | HasNotFailed -> errorlabstrm "Fail" (str "The command has not failed!") @@ -2116,7 +2118,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = let e = locate_if_not_already loc e in let () = restore_timeout () in Flags.program_mode := orig_program_mode; - raise e + iraise e and aux_list ?locality ?polymorphism isprogcmd l = List.iter (aux false) (List.map snd l) in diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 31d1c641c..863a923da 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Pp open Errors @@ -56,4 +57,4 @@ let call ?locality (opn,converted_args) = let reraise = Errors.push reraise in if !Flags.debug then msg_debug (str"Vernac Interpreter " ++ str !loc); - raise reraise + iraise reraise |