aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/taccoerce.ml9
-rw-r--r--plugins/ltac/tacentries.ml51
-rw-r--r--plugins/ltac/tacentries.mli3
-rw-r--r--plugins/ltac/tacintern.ml32
-rw-r--r--plugins/ltac/tacintern.mli3
-rw-r--r--plugins/ltac/tacinterp.ml21
7 files changed, 68 insertions, 53 deletions
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c38a4dcd90..c54f8ffa78 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -466,7 +466,7 @@ END
VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
| [ "Print" "Ltac" reference(r) ] ->
- { Feedback.msg_notice (Tacintern.print_ltac r) }
+ { Feedback.msg_notice (Tacentries.print_ltac r) }
END
VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index ee28229cb7..4c1fe6417e 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -394,8 +394,13 @@ type appl =
(* Values for interpretation *)
type tacvalue =
- | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t *
- Name.t list * Tacexpr.glob_tactic_expr
+ | VFun of
+ appl *
+ Tacexpr.ltac_trace *
+ Loc.t option * (* when executing a global Ltac function: the location where this function was called *)
+ Val.t Id.Map.t * (* closure *)
+ Name.t list * (* binders *)
+ Tacexpr.glob_tactic_expr (* body *)
| VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index a05b36c1b4..29e29044f1 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -528,16 +528,40 @@ let print_ltacs () =
let locatable_ltac = "Ltac"
+let split_ltac_fun = function
+ | Tacexpr.TacFun (l,t) -> (l,t)
+ | t -> ([],t)
+
+let pr_ltac_fun_arg n = spc () ++ Name.print n
+
+let print_ltac_body qid tac =
+ let filter mp =
+ try Some (Nametab.shortest_qualid_of_module mp)
+ with Not_found -> None
+ in
+ let mods = List.map_filter filter tac.Tacenv.tac_redef in
+ let redefined = match mods with
+ | [] -> mt ()
+ | mods ->
+ let redef = prlist_with_sep fnl pr_qualid mods in
+ fnl () ++ str "Redefined by:" ++ fnl () ++ redef
+ in
+ let l,t = split_ltac_fun tac.Tacenv.tac_body in
+ hv 2 (
+ hov 2 (str "Ltac" ++ spc() ++ pr_qualid qid ++
+ prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
+ ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
+
let () =
let open Prettyp in
- let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in
- let locate_all = Tacenv.locate_extended_all_tactic in
- let shortest_qualid = Tacenv.shortest_qualid_of_tactic in
- let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
- let print kn =
- let qid = qualid_of_path (Tacenv.path_of_tactic kn) in
- Tacintern.print_ltac qid
- in
+ let locate qid = try Some (qid, Tacenv.locate_tactic qid) with Not_found -> None in
+ let locate_all qid = List.map (fun kn -> (qid,kn)) (Tacenv.locate_extended_all_tactic qid) in
+ let shortest_qualid (qid,kn) = Tacenv.shortest_qualid_of_tactic kn in
+ let name (qid,kn) = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
+ let print (qid,kn) =
+ let entries = Tacenv.ltac_entries () in
+ let tac = KNmap.find kn entries in
+ print_ltac_body qid tac in
let about = name in
register_locatable locatable_ltac {
locate;
@@ -551,6 +575,17 @@ let () =
let print_located_tactic qid =
Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid)
+let print_ltac id =
+ try
+ let kn = Tacenv.locate_tactic id in
+ let entries = Tacenv.ltac_entries () in
+ let tac = KNmap.find kn entries in
+ print_ltac_body id tac
+ with
+ Not_found ->
+ user_err ~hdr:"print_ltac"
+ (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
+
(** Grammar *)
let () =
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 6ee3ce091b..fc9ab54eba 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -69,6 +69,9 @@ val print_ltacs : unit -> unit
val print_located_tactic : Libnames.qualid -> unit
(** Display the absolute name of a tactic. *)
+val print_ltac : Libnames.qualid -> Pp.t
+(** Display the definition of a tactic. *)
+
(** {5 Low-level registering of tactics} *)
type (_, 'a) ml_ty_sig =
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 9c3b05fdf1..47f1d3bf66 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -769,38 +769,6 @@ let glob_tactic_env l env x =
(intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars })
x
-let split_ltac_fun = function
- | TacFun (l,t) -> (l,t)
- | t -> ([],t)
-
-let pr_ltac_fun_arg n = spc () ++ Name.print n
-
-let print_ltac id =
- try
- let kn = Tacenv.locate_tactic id in
- let entries = Tacenv.ltac_entries () in
- let tac = KNmap.find kn entries in
- let filter mp =
- try Some (Nametab.shortest_qualid_of_module mp)
- with Not_found -> None
- in
- let mods = List.map_filter filter tac.Tacenv.tac_redef in
- let redefined = match mods with
- | [] -> mt ()
- | mods ->
- let redef = prlist_with_sep fnl pr_qualid mods in
- fnl () ++ str "Redefined by:" ++ fnl () ++ redef
- in
- let l,t = split_ltac_fun tac.Tacenv.tac_body in
- hv 2 (
- hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++
- prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
- ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
- with
- Not_found ->
- user_err ~hdr:"print_ltac"
- (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
-
(** Registering *)
let lift intern = (); fun ist x -> (ist, intern ist x)
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 22ec15566b..f779aa470c 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -55,9 +55,6 @@ val intern_hyp : glob_sign -> lident -> lident
val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument
-(** printing *)
-val print_ltac : Libnames.qualid -> Pp.t
-
(** Reduction expressions *)
val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 7728415ddd..3d734d3a66 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -153,11 +153,15 @@ let add_extra_loc loc extra =
match loc with
| None -> extra
| Some loc -> TacStore.set extra f_loc loc
-let add_loc loc ist =
+let extract_loc ist = TacStore.get ist.extra f_loc
+
+let ensure_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
+ | Some loc ->
+ match extract_loc ist with
+ | None -> { ist with extra = TacStore.set ist.extra f_loc loc }
+ | Some _ -> ist
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
@@ -1175,7 +1179,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 {CAst.loc} -> Ftactic.run (val_interp (add_loc loc ist) tac) (fun v -> tactic_of_value ist v)
+ | TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_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)} ->
@@ -1254,9 +1258,12 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
let extra = TacStore.set extra f_trace trace in
let ist = { lfun = Id.Map.empty; poly; extra } in
let appl = GlbAppl[r,[]] in
+ (* We call a global ltac reference: add a loc on its executation only if not
+ already in another global reference *)
+ let ist = ensure_loc loc ist in
Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
- (catch_error_tac_loc (* interp *) loc false trace
- (val_interp ~appl (add_loc (* exec *) loc ist) (Tacenv.interp_ltac r)))
+ (catch_error_tac_loc (* loc for interpretation *) loc false trace
+ (val_interp ~appl ist (Tacenv.interp_ltac r)))
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
@@ -1325,7 +1332,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 (add_loc loc ist) body)) >>= fun v ->
+ (catch_error_tac_loc loc false trace (val_interp (ensure_loc loc ist) body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 12:37:26 +0000