From e8bde450d05908f70ab2c82d9d24f0807c56a94a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 4 Mar 2020 21:39:42 -0500
Subject: [exn] [tactics] improve backtraces on monadic errors

Current backtraces for tactics leave a bit to desire, for example
given the program:

```coq
Lemma u n : n + 0 = n.
rewrite plus_O_n.
```

the backtrace stops at:

```
Found no subterm matching "0 + ?M160" in the current goal.
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```

Backtrace information `?info` is as of today optional in some tactics,
such as `tclZERO`, it doesn't cost a lot  however to reify backtrace
information indeed in `tclZERO` and provide backtraces for all tactic
errors. The cost should be small if we are not in debug mode.

The backtrace for the failed rewrite is now:

```
Found no subterm matching "0 + ?M160" in the current goal.
Raised at file "pretyping/unification.ml", line 1827, characters 14-73
Called from file "pretyping/unification.ml", line 1929, characters 17-53
Called from file "pretyping/unification.ml", line 1948, characters 22-72
Called from file "pretyping/unification.ml", line 2020, characters 14-56
Re-raised at file "pretyping/unification.ml", line 2021, characters 66-73
Called from file "proofs/clenv.ml", line 254, characters 12-58
Called from file "proofs/clenvtac.ml", line 95, characters 16-53
Called from file "engine/proofview.ml", line 1110, characters 40-46
Called from file "engine/proofview.ml", line 1115, characters 10-34
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```

which IMO is much better.
---
 engine/proofview.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2e036be9e3..de38104ecd 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -261,13 +261,9 @@ module Monad = Proof
 
 
 (** [tclZERO e] fails with exception [e]. It has no success. *)
-let tclZERO ?info e =
+let tclZERO ?(info=Exninfo.null) e =
   if not (CErrors.noncritical e) then
     CErrors.anomaly (Pp.str "tclZERO receiving critical error: " ++ CErrors.print 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
@@ -323,9 +319,10 @@ let tclEXACTLY_ONCE e t =
   split t >>= function
     | Nil (e, info) -> tclZERO ~info e
     | Cons (x,k) ->
-        Proof.split (k (e, Exninfo.null)) >>= function
-          | Nil _ -> tclUNIT x
-          | _ -> tclZERO MoreThanOneSuccess
+      let info = Exninfo.null in
+      Proof.split (k (e, Exninfo.null)) >>= function
+      | Nil _ -> tclUNIT x
+      | _ -> tclZERO ~info MoreThanOneSuccess
 
 
 (** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
@@ -359,7 +356,7 @@ end
     is restored at the end of the tactic). If the range [i]-[j] is not
     valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *)
 let tclFOCUS ?nosuchgoal i j t =
-  let nosuchgoal = Option.default (tclZERO (NoSuchGoals (j+1-i))) nosuchgoal in
+  let nosuchgoal ~info = Option.default (tclZERO ~info (NoSuchGoals (j+1-i))) nosuchgoal in
   let open Proof in
   Pv.get >>= fun initial ->
   try
@@ -368,7 +365,9 @@ let tclFOCUS ?nosuchgoal i j t =
     t >>= fun result ->
     Pv.modify (fun next -> unfocus context next) >>
     return result
-  with CList.IndexOutOfRange -> nosuchgoal
+  with CList.IndexOutOfRange as exn ->
+    let _, info = Exninfo.capture exn in
+    nosuchgoal ~info
 
 let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
 
@@ -907,7 +906,8 @@ let tclPROGRESS t =
   if not test then
     tclUNIT res
   else
-    tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
+    let info = Exninfo.reify () in
+    tclZERO ~info (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
 
 let _ = CErrors.register_handler begin function
   | Logic_monad.Tac_Timeout ->
-- 
cgit v1.2.3