diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-03 20:34:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-16 13:15:12 +0100 |
| commit | bff51607cfdda137d7bc55d802895d7f794d5768 (patch) | |
| tree | 1a159136a88ddc6561b814fb4ecbacdf9de0dd70 | |
| parent | 37ed28dfe253615729763b5d81a533094fb5425e (diff) | |
Getting rid of Exninfo hacks.
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
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 |