aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/tacinterp.ml70
1 files changed, 44 insertions, 26 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fdebe14a23..2ca9a0e69d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -161,27 +161,45 @@ let catching_error call_trace fail (e, info) =
fail located_exc
end
-let update_loc ?loc (e, info) =
- (e, Option.cata (Loc.add_loc info) info loc)
+let update_loc loc use_finer (e, info as e') =
+ match loc with
+ | Some loc ->
+ if use_finer then
+ (* ensure loc if there is none *)
+ match Loc.get_loc info with
+ | None -> (e, Loc.add_loc info loc)
+ | _ -> (e, info)
+ else
+ (* override loc (because loc refers to inside of Ltac functions) *)
+ (e, Loc.add_loc info loc)
+ | None -> e'
-let catch_error ?loc call_trace f x =
+let catch_error_with_trace_loc loc use_finer call_trace f x =
try f x
with e when CErrors.noncritical e ->
let e = Exninfo.capture e in
- let e = update_loc ?loc e in
+ let e = update_loc loc use_finer e in
catching_error call_trace Exninfo.iraise e
-let catch_error_loc ?loc tac =
- Proofview.tclOR tac (fun exn ->
- let (e, info) = update_loc ?loc exn in
+let catch_error_loc loc use_finer tac =
+ Proofview.tclORELSE tac (fun exn ->
+ let (e, info) = update_loc loc use_finer exn in
Proofview.tclZERO ~info e)
-let wrap_error ?loc tac k =
+let wrap_error tac k =
+ if is_traced () then Proofview.tclORELSE tac k else tac
+
+let wrap_error_loc loc use_finer tac k =
if is_traced () then Proofview.tclORELSE tac k
- else catch_error_loc ?loc tac
+ else catch_error_loc loc use_finer tac
+
+let catch_error_tac call_trace tac =
+ wrap_error
+ tac
+ (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
-let catch_error_tac ?loc call_trace tac =
- wrap_error ?loc
+let catch_error_tac_loc loc use_finer call_trace tac =
+ wrap_error_loc loc use_finer
tac
(catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
@@ -553,7 +571,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
let loc = loc_of_glob_constr term in
let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in
let (evd,c) =
- catch_error ?loc trace (understand_ltac flags env sigma vars kind) term
+ catch_error_with_trace_loc loc true trace (understand_ltac flags env sigma vars kind) term
in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
@@ -1066,12 +1084,12 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
| _ -> value_interp ist >>= fun v -> return (name_vfun appl v)
-and eval_tactic ist tac : unit Proofview.tactic = match tac with
+and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
| TacAtom {loc;v=t} ->
let call = LtacAtomCall t in
let trace = push_trace(loc,call) ist in
Profile_ltac.do_profile "eval_tactic:2" trace
- (catch_error_tac ?loc trace (interp_atomic ist t))
+ (catch_error_tac_loc loc true trace (interp_atomic ist t))
| TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac
| TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) [])
| TacId s ->
@@ -1145,7 +1163,7 @@ and eval_tactic 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 -> interp_tactic ist (TacArg a)
+ | TacArg a -> Ftactic.run (val_interp ist tac) (fun v -> catch_error_loc a.CAst.loc false (tactic_of_value ist v))
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias {loc; v=(s,l)} ->
@@ -1162,7 +1180,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
; poly
; extra = TacStore.set ist.extra f_trace trace } in
val_interp ist alias.Tacenv.alias_body >>= fun v ->
- Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v))
+ Ftactic.lift (catch_error_loc loc false (tactic_of_value ist v))
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
@@ -1191,7 +1209,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
let tac args =
let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
- Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist))
+ Proofview.Trace.name_tactic name (catch_error_tac_loc loc false trace (tac args ist))
in
Ftactic.run args tac
@@ -1225,7 +1243,7 @@ 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
- (val_interp ~appl ist (Tacenv.interp_ltac r))
+ (catch_error_tac_loc loc false trace (val_interp ~appl ist (Tacenv.interp_ltac r)))
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
@@ -1294,7 +1312,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 trace (val_interp ist body)) >>= fun v ->
+ (catch_error_tac_loc loc false trace (val_interp ist body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
@@ -1341,7 +1359,7 @@ and tactic_of_value ist vle =
lfun = lfun;
poly;
extra = TacStore.set ist.extra f_trace []; } in
- let tac = name_if_glob appl (eval_tactic ist t) 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,_) ->
let tactic_nm =
@@ -1428,7 +1446,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
; poly
; extra = TacStore.set ist.extra f_trace trace
} in
- let tac = eval_tactic ist t in
+ let tac = eval_tactic_ist ist t in
let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in
catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy))
| _ -> Ftactic.return v
@@ -1909,11 +1927,11 @@ let default_ist () =
let eval_tactic t =
Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *)
Proofview.tclLIFT db_initialize <*>
- interp_tactic (default_ist ()) t
+ eval_tactic_ist (default_ist ()) t
let eval_tactic_ist ist t =
Proofview.tclLIFT db_initialize <*>
- interp_tactic ist t
+ eval_tactic_ist ist t
(** FFI *)
@@ -1959,7 +1977,7 @@ let interp_tac_gen lfun avoid_ids debug t =
let extra = TacStore.set extra f_avoid_ids avoid_ids in
let ist = { lfun; poly; extra } in
let ltacvars = Id.Map.domain lfun in
- interp_tactic ist
+ eval_tactic_ist ist
(intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
end
@@ -2076,7 +2094,7 @@ let () =
register_interp0 wit_tactic interp
let () =
- let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in
+ let interp ist tac = eval_tactic_ist ist tac >>= fun () -> Ftactic.return () in
register_interp0 wit_ltac interp
let () =
@@ -2103,7 +2121,7 @@ let _ =
let eval lfun poly env sigma ty tac =
let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
let ist = { lfun; poly; extra; } in
- let tac = interp_tactic ist tac in
+ let tac = eval_tactic_ist ist tac in
(* EJGA: We should also pass the proof name if desired, for now
poly seems like enough to get reasonable behavior in practice
*)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 14:29:14 +0000