aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/taccoerce.ml2
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/ltac/tacinterp.ml59
-rw-r--r--test-suite/output/ErrorLocation_ltac_1.out3
-rw-r--r--test-suite/output/ErrorLocation_ltac_1.v3
-rw-r--r--test-suite/output/ErrorLocation_ltac_2.out3
-rw-r--r--test-suite/output/ErrorLocation_ltac_2.v4
-rw-r--r--test-suite/output/ErrorLocation_ltac_3.out3
-rw-r--r--test-suite/output/ErrorLocation_ltac_3.v4
-rw-r--r--test-suite/output/ErrorLocation_ltac_4.out3
-rw-r--r--test-suite/output/ErrorLocation_ltac_4.v3
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:48:55 +0000