aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/logic.ml2
-rw-r--r--proofs/proof_type.ml2
-rw-r--r--proofs/proof_type.mli2
-rw-r--r--proofs/proofs.mllib2
-rw-r--r--proofs/proofview.ml1
-rw-r--r--proofs/refiner.ml7
-rw-r--r--tactics/class_tactics.ml41
-rw-r--r--tactics/tacinterp.ml45
-rw-r--r--test-suite/output/Errors.out5
-rw-r--r--test-suite/output/Errors.v9
-rw-r--r--toplevel/cerrors.ml12
-rw-r--r--toplevel/himsg.ml30
-rw-r--r--toplevel/himsg.mli5
-rw-r--r--toplevel/obligations.ml10
14 files changed, 92 insertions, 41 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2f88c79a7..267e9d5bf 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -42,7 +42,7 @@ open Pretype_errors
let rec catchable_exception = function
| Loc.Exc_located(_,e) -> catchable_exception e
- | LtacLocated(_,e) -> catchable_exception e
+ | LtacLocated(_,_,e) -> catchable_exception e
| Errors.UserError _ | TypeError _ | PretypeError (_,_,TypingError _)
| RefinerError _ | Indrec.RecursionSchemeError _
| Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index eadf870fb..af50059b8 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -57,5 +57,5 @@ type ltac_call_kind =
type ltac_trace = (int * Loc.t * ltac_call_kind) list
-exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn
+exception LtacLocated of ltac_trace * Loc.t * exn
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 37d5c4544..7ff1afc22 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -82,4 +82,4 @@ type ltac_call_kind =
type ltac_trace = (int * Loc.t * ltac_call_kind) list
-exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn
+exception LtacLocated of ltac_trace * Loc.t * exn
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 96af73b71..19f289316 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,10 +1,10 @@
Goal
Evar_refiner
Monads
+Proof_type
Proofview
Proof
Proof_global
-Proof_type
Redexpr
Logic
Refiner
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bcd51fe2b..c18c48744 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -335,6 +335,7 @@ let tclEXTEND tacs1 rtac tacs2 env =
open Pretype_errors
let rec catchable_exception = function
| Loc.Exc_located(_,e) -> catchable_exception e
+ | Proof_type.LtacLocated(_,_,e) -> catchable_exception e
| Errors.UserError _
| Type_errors.TypeError _ | PretypeError (_,_,TypingError _)
| Indrec.RecursionSchemeError _
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index c83d5ca7a..332f255b2 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -217,14 +217,13 @@ let catch_failerror e =
if catchable_exception e then check_for_interrupt ()
else match e with
| FailError (0,_) | Loc.Exc_located(_, FailError (0,_))
- | Loc.Exc_located(_, LtacLocated (_,FailError (0,_))) ->
+ | LtacLocated (_,_,FailError (0,_)) ->
check_for_interrupt ()
| FailError (lvl,s) -> raise (FailError (lvl - 1, s))
| Loc.Exc_located(s,FailError (lvl,s')) ->
raise (Loc.Exc_located(s,FailError (lvl - 1, s')))
- | Loc.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
- raise
- (Loc.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s'))))
+ | LtacLocated (s'',loc,FailError (lvl,s')) ->
+ raise (LtacLocated (s'',loc,FailError (lvl - 1,s')))
| e -> raise e
(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 53a284fa8..c70351caa 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -196,6 +196,7 @@ let e_possible_resolve db_list local_db gl =
let rec catchable = function
| Refiner.FailError _ -> true
| Loc.Exc_located (_, e) -> catchable e
+ | Proof_type.LtacLocated (_, _, e) -> catchable e
| e -> Logic.catchable_exception e
let nb_empty_evars s =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f780ca79f..530f15f34 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -69,19 +69,15 @@ type value =
let dloc = Loc.ghost
let catch_error call_trace tac g =
- if List.is_empty call_trace then tac g else try tac g with
- | LtacLocated _ as e -> let e = Errors.push e in raise e
- | Loc.Exc_located (_,LtacLocated _) as e ->
- let e = Errors.push e in raise e
- | e ->
- let e = Errors.push e in
- let (nrep,loc',c),tail = List.sep_last call_trace in
- let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
- if List.is_empty tail then
- let loc = if Loc.is_ghost loc then loc' else loc in
- raise (Loc.Exc_located(loc,e'))
- else
- raise (Loc.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
+ try tac g with e ->
+ let e = Errors.push e in
+ let inner_trace,loc,e = match e with
+ | LtacLocated (inner_trace,loc,e) -> inner_trace,loc,e
+ | Loc.Exc_located (loc,e) -> [],loc,e
+ | e -> [],Loc.ghost,e in
+ if List.is_empty call_trace & List.is_empty inner_trace then raise e
+ else
+ raise (LtacLocated(inner_trace@call_trace,loc,e))
(* Signature for interpretation: val_interp and interpretation functions *)
type interp_sign =
@@ -161,6 +157,10 @@ let propagate_trace ist loc id = function
VFun (push_trace(loc,LtacVarCall (id,t)) ist.trace,lfun,it,b)
| x -> x
+let append_trace trace = function
+ | VFun (trace',lfun,it,b) -> VFun (trace'@trace,lfun,it,b)
+ | x -> x
+
(* Dynamically check that an argument is a tactic *)
let coerce_to_tactic loc id = function
| VFun _ | VRTactic _ as a -> a
@@ -469,7 +469,8 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma
let ltacdata = (List.map fst ltacvars,unbndltacvars) in
intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c
in
- let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
+ let trace =
+ push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist.trace in
let evdc =
catch_error trace
(understand_ltac ~resolve_classes:use_classes expand_evar sigma env vars kind) c
@@ -1139,14 +1140,18 @@ and interp_app loc ist gl fv largs =
(TacFun _|TacLetIn _|TacMatchGoal _|TacMatch _| TacArg _ as body))) ->
let (newlfun,lvar,lval)=head_with_value (var,largs) in
if List.is_empty lvar then
+ (* Check evaluation and report problems with current trace *)
let (sigma,v) =
try
- catch_error trace
- (val_interp {ist with lfun=newlfun@olfun; trace=trace} gl) body
+ catch_error trace
+ (val_interp {ist with lfun=newlfun@olfun; trace=[]} gl) body
with e ->
let e = Errors.push e in
debugging_exception_step ist false e (fun () -> str "evaluation");
raise e in
+ (* No errors happened, we propagate the trace *)
+ let v = append_trace trace v in
+
let gl = { gl with sigma=sigma } in
debugging_step ist
(fun () ->
@@ -1163,7 +1168,7 @@ and tactic_of_value ist vle g =
match vle with
| VRTactic res -> res
| VFun (trace,lfun,[],t) ->
- let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in
+ let tac = eval_tactic {ist with lfun=lfun; trace=[]} t in
catch_error trace tac g
| (VFun _|VRec _) -> error "A fully applied tactic is expected."
| VConstr _ -> errorlabstrm "" (str"Value is a term. Expected a tactic.")
@@ -1185,13 +1190,13 @@ and eval_with_fail ist is_lazy goal tac =
| a -> a)
with
| FailError (0,s) | Loc.Exc_located(_, FailError (0,s))
- | Loc.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
+ | LtacLocated (_,_,FailError (0,s)) ->
raise (Eval_fail (Lazy.force s))
| FailError (lvl,s) -> raise (FailError (lvl - 1, s))
| Loc.Exc_located(s,FailError (lvl,s')) ->
raise (Loc.Exc_located(s,FailError (lvl - 1, s')))
- | Loc.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
- raise (Loc.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
+ | LtacLocated (s'',loc,FailError (lvl,s')) ->
+ raise (LtacLocated (s'',loc,FailError (lvl - 1, s')))
(* Interprets the clauses of a recursive LetIn *)
and interp_letrec ist gl llc u =
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index f61b7ecf3..839611b65 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -1,2 +1,7 @@
The command has indeed failed with message:
=> Error: The field t is missing in Top.M.
+The command has indeed failed with message:
+=> Error: Unable to unify "nat" with "True".
+The command has indeed failed with message:
+=> In nested Ltac calls to "f" and "apply x", last call failed.
+ Error: Unable to unify "nat" with "True".
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index 75763f3b4..352c87385 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -7,3 +7,12 @@ Parameter t:Type.
End S.
Module M : S.
Fail End M.
+
+(* A simple check of how Ltac trace are used or not *)
+(* Unfortunately, cannot test error location... *)
+
+Ltac f x := apply x.
+Goal True.
+Fail simpl; apply 0.
+Fail simpl; f 0.
+Abort.
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 3739b0e4d..790520e97 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -117,11 +117,15 @@ let rec process_vernac_interp_error = function
if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
| AlreadyDeclared msg ->
wrap_vernac_error (msg ++ str ".")
- | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when not (is_mt s) ->
+ | Proof_type.LtacLocated (_,_,(Refiner.FailError (i,s) as exc)) when not (is_mt s) ->
+ (* Ltac error is intended, trace is irrelevant *)
process_vernac_interp_error exc
- | Proof_type.LtacLocated (s,exc) ->
- EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()),
- Some (process_vernac_interp_error exc))
+ | Proof_type.LtacLocated (s,loc,exc) ->
+ (match
+ Himsg.extract_ltac_trace s loc (process_vernac_interp_error exc)
+ with
+ | None,loc,e -> Loc.Exc_located (loc,e)
+ | Some msg, loc, e -> Loc.Exc_located (loc,EvaluatedError (msg,Some e)))
| Loc.Exc_located (loc,exc) ->
Loc.Exc_located (loc,process_vernac_interp_error exc)
| exc ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8e6ff1eb7..93c3a3b1a 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -795,7 +795,7 @@ let explain_refiner_error = function
(* Inductive errors *)
-let error_non_strictly_positive env c v =
+let error_non_strictly_positive env c v =
let pc = pr_lconstr_env env c in
let pv = pr_lconstr_env env v in
str "Non strictly positive occurrence of " ++ pv ++ str " in" ++
@@ -994,6 +994,14 @@ let explain_reduction_tactic_error = function
spc () ++ str "is not well typed." ++ fnl () ++
explain_type_error env' Evd.empty e
+let is_defined_ltac trace =
+ let rec aux = function
+ | (_,_,Proof_type.LtacNameCall _) :: tail -> true
+ | (_,_,Proof_type.LtacAtomCall _) :: tail -> false
+ | _ :: tail -> aux tail
+ | [] -> false in
+ aux (List.rev trace)
+
let explain_ltac_call_trace (nrep,last,trace,loc) =
let calls =
(nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace)
@@ -1031,3 +1039,23 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
pr_enum pr_call calls ++ strbrk kind_of_last_call)
else
mt ()
+
+let extract_ltac_trace trace eloc e =
+ let (nrep,loc,c),tail = List.sep_last trace in
+ if is_defined_ltac trace then
+ (* We entered a user-defined tactic,
+ we display the trace with location of the call *)
+ let msg = hov 0 (explain_ltac_call_trace (nrep,c,tail,eloc) ++ fnl()) in
+ Some msg, loc, e
+ else
+ (* We entered a primitive tactic, we don't display trace but
+ report on the finest location *)
+ let best_loc =
+ if not (Loc.is_ghost eloc) then eloc else
+ (* trace is with innermost call coming first *)
+ let rec aux = function
+ | (_,loc,_)::tail when not (Loc.is_ghost loc) -> loc
+ | _::tail -> aux tail
+ | [] -> Loc.ghost in
+ aux trace in
+ None, best_loc, e
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 028c33bd2..bd7fb8973 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -37,9 +37,8 @@ val explain_pattern_matching_error :
val explain_reduction_tactic_error :
Tacred.reduction_tactic_error -> std_ppcmds
-val explain_ltac_call_trace :
- int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Loc.t ->
- std_ppcmds
+val extract_ltac_trace :
+ Proof_type.ltac_trace -> Loc.t -> exn -> std_ppcmds option * Loc.t * exn
val explain_module_error : Modops.module_typing_error -> std_ppcmds
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 6ec01f547..7211417a6 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -822,11 +822,11 @@ and solve_obligation_by_tac prg obls i tac =
with e ->
let e = Errors.push e in
match e with
- | Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
- | Loc.Exc_located(_, Refiner.FailError (_, s))
- | Refiner.FailError (_, s) ->
- user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
- | e when is_anomaly e -> raise e
+ | Proof_type.LtacLocated (_, _, Refiner.FailError (_, s))
+ | Loc.Exc_located(_, Refiner.FailError (_, s))
+ | Refiner.FailError (_, s) ->
+ user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
+ | e when Errors.is_anomaly e -> raise e
| e -> false
and solve_prg_obligations prg ?oblset tac =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 03:48:37 +0000