aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/logic_monad.ml36
-rw-r--r--proofs/logic_monad.mli16
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/proof_global.mli2
-rw-r--r--proofs/proofview.ml55
-rw-r--r--proofs/proofview.mli15
-rw-r--r--proofs/refiner.ml19
-rw-r--r--proofs/refiner.mli2
-rw-r--r--proofs/tactic_debug.ml12
9 files changed, 85 insertions, 74 deletions
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index 55eb434d38..5bad5f0f52 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 46cab18d25..0d05a2181e 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 8e0f3accb2..f4747c0d01 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 8dd7396868..1a13edf17e 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 01bb41ad35..f1d10bbe55 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 eb54ba3ae5..25f4547a91 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 391a78b34a..e443ce0772 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 ea1677f069..744843fc94 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 80aaf9f2a9..b25f37b369 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 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 03:32:18 +0000