More improvements in locating tactic errors.

We finally pass the location in the "ist", and keep it in the "VFun"
which is associated to expanded Ltac constants.

11 files changed, 64 insertions, 25 deletions

diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 91d26519b8..f7037176d2 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -394,7 +394,7 @@ type appl =
 
 (* Values for interpretation *)
 type tacvalue =
-  | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+  | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t *
       Name.t list * Tacexpr.glob_tactic_expr
   | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
 
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 3afbb56b23..b8592c5c76 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -104,7 +104,7 @@ type appl =
        (** For calls to global constants, some may alias other. *)
 
 type tacvalue =
-  | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+  | VFun of appl *Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t *
       Name.t list * Tacexpr.glob_tactic_expr
   | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 2258201c22..2da3d1261b 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -124,7 +124,7 @@ let is_traced () =
 let name_vfun appl vle =
   if is_traced () && has_type vle (topwit wit_tacvalue) then
     match to_tacvalue vle with
-    | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t))
+    | VFun (appl0,trace,loc,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,loc,lfun,vars,t))
     | _ -> vle
   else vle
 
@@ -134,6 +134,7 @@ let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field ()
 (* ids inherited from the call context (needed to get fresh ids) *)
 let f_debug : debug_info TacStore.field = TacStore.field ()
 let f_trace : ltac_trace TacStore.field = TacStore.field ()
+let f_loc : Loc.t TacStore.field = TacStore.field ()
 
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign = Geninterp.interp_sign =
@@ -141,12 +142,23 @@ type interp_sign = Geninterp.interp_sign =
   ; poly : bool
   ; extra : TacStore.t }
 
+let add_extra_trace trace extra = TacStore.set extra f_trace trace
 let extract_trace ist =
   if is_traced () then match TacStore.get ist.extra f_trace with
   | None -> []
   | Some l -> l
   else []
 
+let add_extra_loc loc extra =
+  match loc with
+  | None -> extra
+  | Some loc -> TacStore.set extra f_loc loc
+let add_loc loc ist =
+  match loc with
+  | None -> ist
+  | Some loc -> { ist with extra = TacStore.set ist.extra f_loc loc }
+let extract_loc ist = TacStore.get ist.extra f_loc
+
 let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
 
 let catching_error call_trace fail (e, info) =
@@ -222,7 +234,7 @@ let pr_inspect env expr result =
   let pp_result =
     if has_type result (topwit wit_tacvalue) then
     match to_tacvalue result with
-    | VFun (_,_, ist, ul, b) ->
+    | VFun (_, _, _, ist, ul, b) ->
       let body = if List.is_empty ul then b else (TacFun (ul, b)) in
       str "a closure with body " ++ fnl() ++ pr_closure env ist body
     | VRec (ist, body) ->
@@ -249,10 +261,10 @@ let propagate_trace ist loc id v =
   if has_type v (topwit wit_tacvalue) then
     let tacv = to_tacvalue v in
     match tacv with
-    | VFun (appl,_,lfun,it,b) ->
+    | VFun (appl,_,_,lfun,it,b) ->
         let t = if List.is_empty it then b else TacFun (it,b) in
         let trace = push_trace(loc,LtacVarCall (id,t)) ist in
-        let ans = VFun (appl,trace,lfun,it,b) in
+        let ans = VFun (appl,trace,loc,lfun,it,b) in
         Proofview.tclUNIT (of_tacvalue ans)
     | _ ->  Proofview.tclUNIT v
   else Proofview.tclUNIT v
@@ -260,7 +272,7 @@ let propagate_trace ist loc id v =
 let append_trace trace v =
   if has_type v (topwit wit_tacvalue) then
     match to_tacvalue v with
-    | VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b))
+    | VFun (appl,trace',loc,lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,loc,lfun,it,b))
     | _ -> v
   else v
 
@@ -272,7 +284,7 @@ let coerce_to_tactic loc id v =
   if has_type v (topwit wit_tacvalue) then
     let tacv = to_tacvalue v in
     match tacv with
-    | VFun _ -> v
+    | VFun (appl,trace,_,lfun,it,b) -> of_tacvalue (VFun (appl,trace,loc,lfun,it,b))
     | _ -> fail ()
   else fail ()
 
@@ -1062,7 +1074,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
      function.  *)
   let value_interp ist = match tac with
   | TacFun (it, body) ->
-    Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, it, body)))
+    Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, it, body)))
   | TacLetIn (true,l,u) -> interp_letrec ist l u
   | TacLetIn (false,l,u) -> interp_letin ist l u
   | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr
@@ -1070,7 +1082,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
   | TacArg {loc;v} -> interp_tacarg ist v
   | t ->
     (* Delayed evaluation *)
-    Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t)))
+    Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, [], t)))
   in
   let open Ftactic in
   Control.check_for_interrupt ();
@@ -1163,7 +1175,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
   | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l)
   | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
   | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
-  | TacArg a -> Ftactic.run (val_interp ist tac) (fun v -> catch_error_loc a.CAst.loc false (tactic_of_value ist v))
+  | TacArg {CAst.loc} -> Ftactic.run (val_interp (add_loc loc ist) tac) (fun v -> tactic_of_value ist v)
   | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
   | TacAlias {loc; v=(s,l)} ->
@@ -1178,9 +1190,9 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
         let ist = {
           lfun
         ; poly
-        ; extra = TacStore.set ist.extra f_trace trace } in
+        ; extra = add_extra_loc loc (add_extra_trace trace ist.extra) } in
         val_interp ist alias.Tacenv.alias_body >>= fun v ->
-        Ftactic.lift (catch_error_loc loc false (tactic_of_value ist v))
+        Ftactic.lift (tactic_of_value ist v)
       in
       let tac =
         Ftactic.with_env interp_vars >>= fun (env, lr) ->
@@ -1243,7 +1255,8 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
       let ist = { lfun = Id.Map.empty; poly; extra } in
       let appl = GlbAppl[r,[]] in
       Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
-        (catch_error_tac_loc loc false trace (val_interp ~appl ist (Tacenv.interp_ltac r)))
+        (catch_error_tac_loc (* interp *) loc false trace
+           (val_interp ~appl (add_loc (* exec *) loc ist) (Tacenv.interp_ltac r)))
 
 and interp_tacarg ist arg : Val.t Ftactic.t =
   match arg with
@@ -1297,8 +1310,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
          is not a tactic that expects arguments.
          Otherwise Ltac goes into an infinite loop (val_interp puts
          a VFun back on body, and then interp_app is called again...) *)
-    | (VFun(appl,trace,olfun,(_::_ as var),body)
-      |VFun(appl,trace,olfun,([] as var),
+    | (VFun(appl,trace,_,olfun,(_::_ as var),body)
+      |VFun(appl,trace,_,olfun,([] as var),
          (TacFun _|TacLetIn _|TacMatchGoal _|TacMatch _| TacArg _ as body))) ->
         let (extfun,lvar,lval)=head_with_value (var,largs) in
         let fold accu (id, v) = Id.Map.add id v accu in
@@ -1312,7 +1325,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
                 ; extra = TacStore.set ist.extra f_trace []
                 } in
               Profile_ltac.do_profile "interp_app" trace ~count_call:false
-                (catch_error_tac_loc loc false trace (val_interp ist body)) >>= fun v ->
+                (catch_error_tac_loc loc false trace (val_interp (add_loc loc ist) body)) >>= fun v ->
               Ftactic.return (name_vfun (push_appl appl largs) v)
             end
             begin fun (e, info) ->
@@ -1333,8 +1346,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
         end <*>
         if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval
       else
-        Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body)))
-    | (VFun(appl,trace,olfun,[],body)) ->
+        Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,loc,newlfun,lvar,body)))
+    | (VFun(appl,trace,_,olfun,[],body)) ->
       let extra_args = List.length largs in
       let info = Exninfo.reify () in
       Tacticals.New.tclZEROMSG ~info
@@ -1353,15 +1366,15 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
 and tactic_of_value ist vle =
   if has_type vle (topwit wit_tacvalue) then
   match to_tacvalue vle with
-  | VFun (appl,trace,lfun,[],t) ->
+  | VFun (appl,trace,loc,lfun,[],t) ->
     Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
       let ist = {
         lfun = lfun;
         poly;
         extra = TacStore.set ist.extra f_trace []; } in
       let tac = name_if_glob appl (eval_tactic_ist ist t) in
-      Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
-  | VFun (appl,_,vmap,vars,_) ->
+      Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac_loc loc false trace tac)
+  | VFun (appl,_,loc,vmap,vars,_) ->
      let tactic_nm =
        match appl with
          UnnamedAppl -> "An unnamed user-defined tactic"
@@ -1440,14 +1453,14 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
   let ist = { ist with lfun } in
   val_interp ist lhs >>= fun v ->
   if has_type v (topwit wit_tacvalue) then match to_tacvalue v with
-  | VFun (appl,trace,lfun,[],t) ->
+  | VFun (appl,trace,loc,lfun,[],t) ->
       let ist =
         { lfun = lfun
         ; poly
         ; extra = TacStore.set ist.extra f_trace trace
         } in
       let tac = eval_tactic_ist ist t in
-      let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in
+      let dummy = VFun (appl, extract_trace ist, loc, Id.Map.empty, [], TacId []) in
       catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy))
   | _ -> Ftactic.return v
   else Ftactic.return v
@@ -1940,7 +1953,7 @@ module Value = struct
   include Taccoerce.Value
 
   let of_closure ist tac =
-    let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
+    let closure = VFun (UnnamedAppl, extract_trace ist, None, ist.lfun, [], tac) in
     of_tacvalue closure
 
   let apply_expr f args =
diff --git a/test-suite/output/ErrorLocation_ltac_1.out b/test-suite/output/ErrorLocation_ltac_1.out
new file mode 100644
index 0000000000..a9014c4b46
--- /dev/null
+++ b/test-suite/output/ErrorLocation_ltac_1.out
@@ -0,0 +1,3 @@
+File "stdin", line 2, characters 7-11:
+Error: Tactic failure: Cannot solve this goal.
+
diff --git a/test-suite/output/ErrorLocation_ltac_1.v b/test-suite/output/ErrorLocation_ltac_1.v
new file mode 100644
index 0000000000..368a4592f2
--- /dev/null
+++ b/test-suite/output/ErrorLocation_ltac_1.v
@@ -0,0 +1,3 @@
+Goal False.
+idtac; easy.
+Abort.
diff --git a/test-suite/output/ErrorLocation_ltac_2.out b/test-suite/output/ErrorLocation_ltac_2.out
new file mode 100644
index 0000000000..d38727ffa4
--- /dev/null
+++ b/test-suite/output/ErrorLocation_ltac_2.out
@@ -0,0 +1,3 @@
+File "stdin", line 3, characters 7-8:
+Error: Tactic failure.
+
diff --git a/test-suite/output/ErrorLocation_ltac_2.v b/test-suite/output/ErrorLocation_ltac_2.v
new file mode 100644
index 0000000000..c3a9bd626a
--- /dev/null
+++ b/test-suite/output/ErrorLocation_ltac_2.v
@@ -0,0 +1,4 @@
+Ltac f := fail.
+Goal False.
+idtac; f.
+Abort.
diff --git a/test-suite/output/ErrorLocation_ltac_3.out b/test-suite/output/ErrorLocation_ltac_3.out
new file mode 100644
index 0000000000..409b72bba8
--- /dev/null
+++ b/test-suite/output/ErrorLocation_ltac_3.out
@@ -0,0 +1,3 @@
+File "stdin", line 3, characters 7-10:
+Error: Not a negated primitive equality.
+
diff --git a/test-suite/output/ErrorLocation_ltac_3.v b/test-suite/output/ErrorLocation_ltac_3.v
new file mode 100644
index 0000000000..43ce1fc6e2
--- /dev/null
+++ b/test-suite/output/ErrorLocation_ltac_3.v
@@ -0,0 +1,4 @@
+Ltac inj := injection.
+Goal False.
+idtac; inj.
+Abort.
diff --git a/test-suite/output/ErrorLocation_ltac_4.out b/test-suite/output/ErrorLocation_ltac_4.out
new file mode 100644
index 0000000000..f9107cdc3f
--- /dev/null
+++ b/test-suite/output/ErrorLocation_ltac_4.out
@@ -0,0 +1,3 @@
+File "stdin", line 2, characters 22-23:
+Error: Tactic failure.
+
diff --git a/test-suite/output/ErrorLocation_ltac_4.v b/test-suite/output/ErrorLocation_ltac_4.v
new file mode 100644
index 0000000000..58c370c31b
--- /dev/null
+++ b/test-suite/output/ErrorLocation_ltac_4.v
@@ -0,0 +1,3 @@
+Goal False.
+let x := fail in x || x.
+Abort.