Implementing a generic mechanism for locating named objects from Coq side.

3 files changed, 81 insertions, 12 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 10dd42ea9..a1cdfdbaa 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1156,7 +1156,7 @@ open Decl_kinds
           | LocateFile f -> keyword "File" ++ spc() ++ qs f
           | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid
           | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid
-          | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid
+          | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid
         in
         return (keyword "Locate" ++ spc() ++ pr_locate loc)
       | VernacRegister (id, RegisterInline) ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b2e7fe447..2077526db 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -304,13 +304,33 @@ let print_inductive_argument_scopes =
 (*********************)
 (* "Locate" commands *)
 
+type 'a locatable_info = {
+  locate : qualid -> 'a option;
+  locate_all : qualid -> 'a list;
+  shortest_qualid : 'a -> qualid;
+  name : 'a -> Pp.t;
+  print : 'a -> Pp.t;
+  about : 'a -> Pp.t;
+}
+
+type locatable = Locatable : 'a locatable_info -> locatable
+
 type logical_name =
   | Term of global_reference
   | Dir of global_dir_reference
   | Syntactic of kernel_name
   | ModuleType of module_path
+  | Other : 'a * 'a locatable_info -> logical_name
   | Undefined of qualid
 
+(** Generic table for objects that are accessible through a name. *)
+let locatable_map : locatable String.Map.t ref = ref String.Map.empty
+
+let register_locatable name f =
+  locatable_map := String.Map.add name (Locatable f) !locatable_map
+
+exception ObjFound of logical_name
+
 let locate_any_name ref =
   let (loc,qid) = qualid_of_reference ref in
   try Term (Nametab.locate qid)
@@ -320,7 +340,13 @@ let locate_any_name ref =
   try Dir (Nametab.locate_dir qid)
   with Not_found ->
   try ModuleType (Nametab.locate_modtype qid)
-  with Not_found -> Undefined qid
+  with Not_found ->
+    let iter _ (Locatable info) = match info.locate qid with
+    | None -> ()
+    | Some ans -> raise (ObjFound (Other (ans, info)))
+    in
+    try String.Map.iter iter !locatable_map; Undefined qid
+    with ObjFound obj -> obj
 
 let pr_located_qualid = function
   | Term ref ->
@@ -343,6 +369,7 @@ let pr_located_qualid = function
       str s ++ spc () ++ pr_dirpath dir
   | ModuleType mp ->
       str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp)
+  | Other (obj, info) -> info.name obj
   | Undefined qid ->
       pr_qualid qid ++ spc () ++ str "not a defined object."
 
@@ -401,12 +428,30 @@ let locate_modtype qid =
   in
   modtypes @ List.map_filter map all
 
+let locate_other s qid =
+  let Locatable info = String.Map.find s !locatable_map in
+  let ans = info.locate_all qid in
+  let map obj = (Other (obj, info), info.shortest_qualid obj) in
+  List.map map ans
+
+type locatable_kind =
+| LocTerm
+| LocModule
+| LocOther of string
+| LocAny
+
 let print_located_qualid name flags ref =
   let (loc,qid) = qualid_of_reference ref in
-  let located = [] in
-  let located = if List.mem `MODTYPE flags then locate_modtype qid @ located else located in
-  let located = if List.mem `MODULE flags then locate_module qid @ located else located in
-  let located = if List.mem `TERM flags then locate_term qid @ located else located in
+  let located = match flags with
+  | LocTerm -> locate_term qid
+  | LocModule -> locate_modtype qid @ locate_module qid
+  | LocOther s -> locate_other s qid
+  | LocAny ->
+    locate_term qid @
+    locate_modtype qid @
+    locate_module qid @
+    String.Map.fold (fun s _ accu -> locate_other s qid @ accu) !locatable_map []
+  in
   match located with
     | [] ->
 	let (dir,id) = repr_qualid qid in
@@ -424,10 +469,10 @@ let print_located_qualid name flags ref =
 	   else mt ()) ++
           display_alias o)) l
 
-let print_located_term ref = print_located_qualid "term" [`TERM] ref
-let print_located_tactic ref = print_located_qualid "tactic" [`LTAC] ref
-let print_located_module ref = print_located_qualid "module" [`MODULE; `MODTYPE] ref
-let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MODULE; `MODTYPE] ref
+let print_located_term ref = print_located_qualid "term" LocTerm ref
+let print_located_other s ref = print_located_qualid s (LocOther s) ref
+let print_located_module ref = print_located_qualid "module" LocModule ref
+let print_located_qualid ref = print_located_qualid "object" LocAny ref
 
 (******************************************)
 (**** Printing declarations and judgments *)
@@ -757,6 +802,7 @@ let print_any_name = function
   | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
   | Dir _ -> mt ()
   | ModuleType mp -> print_modtype mp
+  | Other (obj, info) -> info.print obj
   | Undefined qid ->
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in
@@ -815,6 +861,7 @@ let print_about_any ?loc k =
       hov 0 (str "Expands to: " ++ pr_located_qualid k))
   | Dir _ | ModuleType _ | Undefined _ ->
       hov 0 (pr_located_qualid k)
+  | Other (obj, info) -> hov 0 (info.about obj)
 
 let print_about = function
   | ByNotation (loc,(ntn,sc)) ->
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index f4277b6c5..dbd101159 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -50,12 +50,34 @@ val print_all_instances : unit -> Pp.t
 
 val inspect : int -> Pp.t
 
-(** Locate *)
+(** {5 Locate} *)
+
+type 'a locatable_info = {
+  locate : qualid -> 'a option;
+  (** Locate the most precise object with the provided name if any. *)
+  locate_all : qualid -> 'a list;
+  (** Locate all objects whose name is a suffix of the provided name *)
+  shortest_qualid : 'a -> qualid;
+  (** Return the shortest name in the current context *)
+  name : 'a -> Pp.t;
+  (** Data as printed by the Locate command *)
+  print : 'a -> Pp.t;
+  (** Data as printed by the Print command *)
+  about : 'a -> Pp.t;
+  (** Data as printed by the About command *)
+}
+(** Generic data structure representing locatable objects. *)
+
+val register_locatable : string -> 'a locatable_info -> unit
+(** Define a new type of locatable objects that can be reached via the
+    corresponding generic vernacular commands. The string should be a unique
+    name describing the kind of objects considered and that is added as a
+    grammar command prefix for vernacular commands Locate. *)
 
 val print_located_qualid : reference -> Pp.t
 val print_located_term : reference -> Pp.t
-val print_located_tactic : reference -> Pp.t
 val print_located_module : reference -> Pp.t
+val print_located_other : string -> reference -> Pp.t
 
 type object_pr = {
   print_inductive           : mutual_inductive -> Pp.t;