Merge PR #1114: Generic handling of nameable objects for plugins

12 files changed, 101 insertions, 21 deletions

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 86c983bdd..d639dd0e1 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -482,6 +482,11 @@ VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
   [ Feedback.msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
 END
 
+VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
+| [ "Locate" "Ltac" reference(r) ] ->
+  [ Tacentries.print_located_tactic r ]
+END
+
 let pr_ltac_ref = Libnames.pr_reference
 
 let pr_tacdef_body tacdef_body =
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index 12b4c81fc..3972b7aac 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -1,9 +1,9 @@
 Tacarg
+Tacsubst
+Tacenv
 Pptactic
 Pltac
 Taccoerce
-Tacsubst
-Tacenv
 Tactic_debug
 Tacintern
 Tacentries
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index d8bd16620..d588c888c 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -336,7 +336,7 @@ type 'a extra_genarg_printer =
   let pr_ltac_constant kn =
     if !Flags.in_debugger then KerName.print kn
     else try
-           pr_qualid (Nametab.shortest_qualid_of_tactic kn)
+           pr_qualid (Tacenv.shortest_qualid_of_tactic kn)
       with Not_found -> (* local tactic not accessible anymore *)
         str "<" ++ KerName.print kn ++ str ">"
 
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index c79d5b389..d9da954fe 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -93,7 +93,7 @@ val pr_alias_key : Names.KerName.t -> Pp.t
 val pr_alias : (Val.t -> Pp.t) ->
   int -> Names.KerName.t -> Val.t list -> Pp.t
 
-val pr_ltac_constant : Nametab.ltac_constant -> Pp.t
+val pr_ltac_constant : ltac_constant -> Pp.t
 
 val pr_raw_tactic : raw_tactic_expr -> Pp.t
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index a8d518fbd..bcd5b388a 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -409,7 +409,7 @@ let create_ltac_quotation name cast (e, l) =
 
 type tacdef_kind =
   | NewTac of Id.t
-  | UpdateTac of Nametab.ltac_constant
+  | UpdateTac of Tacexpr.ltac_constant
 
 let is_defined_tac kn =
   try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
@@ -441,7 +441,7 @@ let register_ltac local tacl =
     | Tacexpr.TacticRedefinition (ident, body) ->
         let loc = loc_of_reference ident in
         let kn =
-          try Nametab.locate_tactic (snd (qualid_of_reference ident))
+          try Tacenv.locate_tactic (snd (qualid_of_reference ident))
           with Not_found ->
             CErrors.user_err ?loc 
                        (str "There is no Ltac named " ++ pr_reference ident ++ str ".")
@@ -464,7 +464,7 @@ let register_ltac local tacl =
   let defs () =
     (** Register locally the tactic to handle recursivity. This function affects
         the whole environment, so that we transactify it afterwards. *)
-    let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in
+    let iter_rec (sp, kn) = Tacenv.push_tactic (Nametab.Until 1) sp kn in
     let () = List.iter iter_rec recvars in
     List.map map rfun
   in
@@ -475,7 +475,7 @@ let register_ltac local tacl =
     Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
   | UpdateTac kn ->
     Tacenv.redefine_ltac local kn tac;
-    let name = Nametab.shortest_qualid_of_tactic kn in
+    let name = Tacenv.shortest_qualid_of_tactic kn in
     Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
   in
   List.iter iter defs
@@ -488,7 +488,7 @@ let print_ltacs () =
   let entries = List.sort sort entries in
   let map (kn, entry) =
     let qid =
-      try Some (Nametab.shortest_qualid_of_tactic kn)
+      try Some (Tacenv.shortest_qualid_of_tactic kn)
       with Not_found -> None
     in
     match qid with
@@ -506,6 +506,31 @@ let print_ltacs () =
   in
   Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
 
+let locatable_ltac = "Ltac"
+
+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 about = name in
+  register_locatable locatable_ltac {
+    locate;
+    locate_all;
+    shortest_qualid;
+    name;
+    print;
+    about;
+  }
+
+let print_located_tactic qid =
+  Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid)
+
 (** Grammar *)
 
 let () =
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index aa8f4efe6..ab2c6b307 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -62,3 +62,6 @@ val create_ltac_quotation : string ->
 
 val print_ltacs : unit -> unit
 (** Display the list of ltac definitions currently available. *)
+
+val print_located_tactic : Libnames.reference -> unit
+(** Display the absolute name of a tactic. *)
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 13b44f0e2..8c59a36fa 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -11,6 +11,42 @@ open Pp
 open Names
 open Tacexpr
 
+(** Nametab for tactics *)
+
+(** TODO: Share me somewhere *)
+module FullPath =
+struct
+  open Libnames
+  type t = full_path
+  let equal = eq_full_path
+  let to_string = string_of_path
+  let repr sp =
+    let dir,id = repr_path sp in
+      id, (DirPath.repr dir)
+end
+
+module KnTab = Nametab.Make(FullPath)(KerName)
+
+let tactic_tab = Summary.ref ~name:"LTAC-NAMETAB" (KnTab.empty, KNmap.empty)
+
+let push_tactic vis sp kn =
+  let (tab, revtab) = !tactic_tab in
+  let tab = KnTab.push vis sp kn tab in
+  let revtab = KNmap.add kn sp revtab in
+  tactic_tab := (tab, revtab)
+
+let locate_tactic qid = KnTab.locate qid (fst !tactic_tab)
+
+let locate_extended_all_tactic qid = KnTab.find_prefixes qid (fst !tactic_tab)
+
+let exists_tactic kn = KnTab.exists kn (fst !tactic_tab)
+
+let path_of_tactic kn = KNmap.find kn (snd !tactic_tab)
+
+let shortest_qualid_of_tactic kn =
+  let sp = KNmap.find kn (snd !tactic_tab) in
+  KnTab.shortest_qualid Id.Set.empty sp (fst !tactic_tab)
+
 (** Tactic notations (TacAlias) *)
 
 type alias = KerName.t
@@ -103,19 +139,19 @@ let replace kn path t =
 
 let load_md i ((sp, kn), (local, id, b, t)) = match id with
 | None ->
-  let () = if not local then Nametab.push_tactic (Until i) sp kn in
+  let () = if not local then push_tactic (Until i) sp kn in
   add kn b t
 | Some kn0 -> replace kn0 kn t
 
 let open_md i ((sp, kn), (local, id, b, t)) = match id with
 | None ->
-  let () = if not local then Nametab.push_tactic (Exactly i) sp kn in
+  let () = if not local then push_tactic (Exactly i) sp kn in
   add kn b t
 | Some kn0 -> replace kn0 kn t
 
 let cache_md ((sp, kn), (local, id ,b, t)) = match id with
 | None ->
-  let () = Nametab.push_tactic (Until 1) sp kn in
+  let () = push_tactic (Until 1) sp kn in
   add kn b t
 | Some kn0 -> replace kn0 kn t
 
@@ -128,7 +164,7 @@ let subst_md (subst, (local, id, b, t)) =
 
 let classify_md (local, _, _, _ as o) = Substitute o
 
-let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj =
+let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 958109e5a..4ecc978fe 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -7,11 +7,21 @@
 (************************************************************************)
 
 open Names
+open Libnames
 open Tacexpr
 open Geninterp
 
 (** This module centralizes the various ways of registering tactics. *)
 
+(** {5 Tactic naming} *)
+
+val push_tactic : Nametab.visibility -> full_path -> ltac_constant -> unit
+val locate_tactic : qualid -> ltac_constant
+val locate_extended_all_tactic : qualid -> ltac_constant list
+val exists_tactic : full_path -> bool
+val path_of_tactic : ltac_constant -> full_path
+val shortest_qualid_of_tactic : ltac_constant -> qualid
+
 (** {5 Tactic notations} *)
 
 type alias = KerName.t
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 64da097de..2c36faeff 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -10,13 +10,14 @@ open Loc
 open Names
 open Constrexpr
 open Libnames
-open Nametab
 open Genredexpr
 open Genarg
 open Pattern
 open Misctypes
 open Locus
 
+type ltac_constant = KerName.t
+
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag =
   | General (* returns all possible successes *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index fc6ee6aab..99d7684d3 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -118,7 +118,7 @@ let intern_constr_reference strict ist = function
 
 let intern_isolated_global_tactic_reference r =
   let (loc,qid) = qualid_of_reference r in
-  TacCall (Loc.tag ?loc (ArgArg (loc,locate_tactic qid),[]))
+  TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
 
 let intern_isolated_tactic_reference strict ist r =
   (* An ltac reference *)
@@ -137,7 +137,7 @@ let intern_isolated_tactic_reference strict ist r =
 
 let intern_applied_global_tactic_reference r =
   let (loc,qid) = qualid_of_reference r in
-  ArgArg (loc,locate_tactic qid)
+  ArgArg (loc,Tacenv.locate_tactic qid)
 
 let intern_applied_tactic_reference ist r =
   (* An ltac reference *)
@@ -722,7 +722,7 @@ let pr_ltac_fun_arg n = spc () ++ Name.print n
 
 let print_ltac id =
  try
-  let kn = Nametab.locate_tactic id in
+  let kn = Tacenv.locate_tactic id in
   let entries = Tacenv.ltac_entries () in
   let tac = KNmap.find kn entries in
   let filter mp =
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index cf5fdf318..d37c676e3 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -814,8 +814,8 @@ let ssr_n_tac seed n gl =
   let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in
   let fail msg = CErrors.user_err (Pp.str msg) in
   let tacname = 
-    try Nametab.locate_tactic (Libnames.qualid_of_ident (Id.of_string name))
-    with Not_found -> try Nametab.locate_tactic (ssrqid name)
+    try Tacenv.locate_tactic (Libnames.qualid_of_ident (Id.of_string name))
+    with Not_found -> try Tacenv.locate_tactic (ssrqid name)
     with Not_found ->
       if n = -1 then fail "The ssreflect library was not loaded"
       else fail ("The tactic "^name^" was not found") in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 1e1a986da..7b591fead 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1554,8 +1554,8 @@ END
 let ssrautoprop gl =
   try 
     let tacname = 
-      try Nametab.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
-      with Not_found -> Nametab.locate_tactic (ssrqid "ssrautoprop") in
+      try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
+      with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in
     let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
     Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
   with Not_found -> Proofview.V82.of_tactic (Auto.full_trivial []) gl