Merge PR coq#19584: Provide source location for declared objects

Reviewed-by: gares
Ack-by: ejgallego
Co-authored-by: gares <[email protected]>

dev/ci/user-overlays/19584-SkySkimmer-jump-to-def.sh

@@ -0,0 +1 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi jump-to-def 19584

interp/abbreviation.ml

@@ -24,6 +24,7 @@ type abbreviation =
     abbrev_onlyparsing : bool;
     abbrev_user_warns : Globnames.extended_global_reference UserWarn.with_qf option;
     abbrev_activated : bool; (* Not really necessary in practice *)
+    abbrev_src : Loc.t option;
   }
 
 let abbrev_table =
@@ -60,7 +61,8 @@ let load_abbreviation i ((sp,kn),(_local,abbrev)) =
     user_err
       (Id.print (basename sp) ++ str " already exists.");
   add_abbreviation kn sp abbrev;
-  Nametab.push_abbreviation ?user_warns:abbrev.abbrev_user_warns (Nametab.Until i) sp kn
+  Nametab.push_abbreviation ?user_warns:abbrev.abbrev_user_warns (Nametab.Until i) sp kn;
+  abbrev.abbrev_src |> Option.iter (fun loc -> Nametab.set_cci_src_loc (Abbrev kn) loc)
 
 let is_alias_of_already_visible_name sp = function
   | _,NRef (ref,None) ->
@@ -108,6 +110,7 @@ let declare_abbreviation ~local user_warns id ~onlyparsing pat =
       abbrev_onlyparsing = onlyparsing;
       abbrev_user_warns = user_warns;
       abbrev_activated = true;
+      abbrev_src = Loc.get_current_command_loc();
     }
   in
   add_leaf (inAbbreviation id (local,abbrev))

lib/loc.ml

@@ -114,3 +114,9 @@ let pr loc =
     (str"File " ++ str "\"" ++ str file ++ str "\"" ++
      str", line " ++ int loc.line_nb ++ str", characters " ++
      int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos))
+
+let current_command_loc = ref None
+
+let get_current_command_loc () = !current_command_loc
+
+let set_current_command_loc v = current_command_loc := v

lib/loc.mli

@@ -86,3 +86,9 @@ val map : ('a -> 'b) -> 'a located -> 'b located
 
 val pr : t -> Pp.t
 (** Print for user consumption. *)
+
+(** {5 Location of the current command (if any) } *)
+
+val get_current_command_loc : unit -> t option
+
+val set_current_command_loc : t option -> unit

library/nametab.ml

@@ -10,6 +10,7 @@
 
 open Names
 open Libnames
+open Globnames
 
 type object_prefix = {
   obj_dir : DirPath.t;
@@ -400,7 +401,7 @@ struct
       id, (DirPath.repr dir)
 end
 
-module ExtRefEqual = Globnames.ExtRefOrdered
+module ExtRefEqual = ExtRefOrdered
 module MPEqual = Names.ModPath
 
 module ExtRefTab = Make(FullPath)(ExtRefEqual)
@@ -427,11 +428,11 @@ let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)
 (* Reversed name tables ***************************************************)
 
 (* This table translates extended_global_references back to section paths *)
-type globrevtab = full_path Globnames.ExtRefMap.t
+type globrevtab = full_path ExtRefMap.t
 let the_globrevtab =
-  Summary.ref ~name:"globrevtab" (Globnames.ExtRefMap.empty : globrevtab)
+  Summary.ref ~name:"globrevtab" (ExtRefMap.empty : globrevtab)
 
-let the_globwarntab = Summary.ref ~name:"globwarntag" Globnames.ExtRefMap.empty
+let the_globwarntab = Summary.ref ~name:"globwarntag" ExtRefMap.empty
 
 type mprevtab = DirPath.t MPmap.t
 
@@ -479,9 +480,9 @@ let push_xref ?user_warns visibility sp xref =
   match visibility with
     | Until _ ->
         the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
-        the_globrevtab := Globnames.ExtRefMap.add xref sp !the_globrevtab;
+        the_globrevtab := ExtRefMap.add xref sp !the_globrevtab;
         user_warns |> Option.iter (fun warn ->
-            the_globwarntab := Globnames.ExtRefMap.add xref warn !the_globwarntab)
+            the_globwarntab := ExtRefMap.add xref warn !the_globwarntab)
     | Exactly _ ->
       begin
         assert (Option.is_empty user_warns);
@@ -490,8 +491,8 @@ let push_xref ?user_warns visibility sp xref =
 
 let remove_xref sp xref =
   the_ccitab := ExtRefTab.remove sp !the_ccitab;
-  the_globrevtab := Globnames.ExtRefMap.remove xref !the_globrevtab;
-  the_globwarntab := Globnames.ExtRefMap.remove xref !the_globwarntab
+  the_globrevtab := ExtRefMap.remove xref !the_globrevtab;
+  the_globwarntab := ExtRefMap.remove xref !the_globwarntab
 
 let push_cci ?user_warns visibility sp ref =
   push_xref ?user_warns visibility sp (TrueGlobal ref)
@@ -538,7 +539,7 @@ let path_of_global ref =
   let open GlobRef in
   match ref with
     | VarRef id -> make_path DirPath.empty id
-    | _ -> Globnames.ExtRefMap.find (TrueGlobal ref) !the_globrevtab
+    | _ -> ExtRefMap.find (TrueGlobal ref) !the_globrevtab
 
 let dirpath_of_global ref =
   fst (repr_path (path_of_global ref))
@@ -547,7 +548,7 @@ let basename_of_global ref =
   snd (repr_path (path_of_global ref))
 
 let path_of_abbreviation kn =
-  Globnames.ExtRefMap.find (Abbrev kn) !the_globrevtab
+  ExtRefMap.find (Abbrev kn) !the_globrevtab
 
 let dirpath_of_module mp =
   MPmap.find mp Modules.(!nametab.modrevtab)
@@ -565,7 +566,7 @@ let shortest_qualid_of_global ?loc ctx ref =
   match ref with
     | VarRef id -> make_qualid ?loc DirPath.empty id
     | _ ->
-        let sp =  Globnames.ExtRefMap.find (TrueGlobal ref) !the_globrevtab in
+        let sp =  ExtRefMap.find (TrueGlobal ref) !the_globrevtab in
         ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
 let shortest_qualid_of_abbreviation ?loc ctx kn =
@@ -599,7 +600,7 @@ let pr_global_env env ref =
 (* Locate functions *******************************************************)
 
 let pr_depr_xref xref =
-  let sp = Globnames.ExtRefMap.get xref !the_globrevtab in
+  let sp = ExtRefMap.get xref !the_globrevtab in
   pr_qualid (ExtRefTab.shortest_qualid Id.Set.empty sp !the_ccitab)
 
 let pr_depr_ref ref = pr_depr_xref (TrueGlobal ref)
@@ -615,13 +616,13 @@ let warn_deprecated_abbreviation =
   ~pp_qf:pr_depr_xref pr_depr_abbrev
 
 let warn_deprecated_xref ?loc depr = function
-  | Globnames.TrueGlobal ref -> warn_deprecated_ref ?loc (ref, depr)
+  | TrueGlobal ref -> warn_deprecated_ref ?loc (ref, depr)
   | Abbrev a -> warn_deprecated_abbreviation ?loc (a, depr)
 
 let warn_user_warn =
   UserWarn.create_warning ~warning_name_if_no_cats:"warn-reference" ()
 
-let is_warned_xref xref : Globnames.extended_global_reference UserWarn.with_qf option = Globnames.ExtRefMap.find_opt xref !the_globwarntab
+let is_warned_xref xref : extended_global_reference UserWarn.with_qf option = ExtRefMap.find_opt xref !the_globwarntab
 
 let warn_user_warn_xref ?loc user_warns xref =
   user_warns.UserWarn.depr_qf
@@ -669,7 +670,7 @@ let locate_section qid =
 let locate_all qid =
   List.fold_right (fun a l ->
     match a with
-    | Globnames.TrueGlobal a -> a::l
+    | TrueGlobal a -> a::l
     | _ -> l)
     (ExtRefTab.find_prefixes qid !the_ccitab) []
 
@@ -730,3 +731,13 @@ let exists_module dir = MPDTab.exists dir Modules.(!nametab.modtab)
 let exists_modtype sp = MPTab.exists sp Modules.(!nametab.modtypetab)
 
 let exists_universe kn = UnivTab.exists kn !the_univtab
+
+(* Source locations *)
+
+open Globnames
+
+let cci_loc_table : Loc.t ExtRefMap.t ref = Summary.ref ~name:"constant-loc-table" ExtRefMap.empty
+
+let set_cci_src_loc kn loc = cci_loc_table := ExtRefMap.add kn loc !cci_loc_table
+
+let cci_src_loc kn = ExtRefMap.find_opt kn !cci_loc_table

library/nametab.mli

@@ -174,6 +174,11 @@ val exists_module : DirPath.t -> bool
 val exists_dir : DirPath.t -> bool
 val exists_universe : full_path -> bool
 
+(** {6 These functions declare (resp. return) the source location of the object if known } *)
+
+val set_cci_src_loc : Globnames.extended_global_reference -> Loc.t -> unit
+val cci_src_loc : Globnames.extended_global_reference -> Loc.t option
+
 (** {6 These functions locate qualids into full user names } *)
 
 val full_name_modtype : qualid -> full_path

test-suite/output/Arguments.out

@@ -5,6 +5,7 @@ Arguments Nat.sub (n m)%nat_scope : simpl nomatch
 The reduction tactics unfold Nat.sub but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Stdlib.Init.Nat.sub
+Declared in library Stdlib.Init.Nat, line 71, characters 0-120
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
@@ -13,6 +14,7 @@ The reduction tactics unfold Nat.sub when applied to 1 argument
   but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Stdlib.Init.Nat.sub
+Declared in library Stdlib.Init.Nat, line 71, characters 0-120
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
@@ -22,6 +24,7 @@ The reduction tactics unfold Nat.sub
   when applied to 1 argument but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Stdlib.Init.Nat.sub
+Declared in library Stdlib.Init.Nat, line 71, characters 0-120
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
@@ -30,6 +33,7 @@ The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments
 Nat.sub is transparent
 Expands to: Constant Stdlib.Init.Nat.sub
+Declared in library Stdlib.Init.Nat, line 71, characters 0-120
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
@@ -38,6 +42,7 @@ The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor
 Nat.sub is transparent
 Expands to: Constant Stdlib.Init.Nat.sub
+Declared in library Stdlib.Init.Nat, line 71, characters 0-120
 pf :
 forall {D1 C1 : Type},
 (D1 -> C1) -> forall [D2 C2 : Type], (D2 -> C2) -> D1 * D2 -> C1 * C2
@@ -47,27 +52,31 @@ Arguments pf {D1}%foo_scope {C1}%type_scope f [D2 C2] g x : simpl never
 The reduction tactics never unfold pf
 pf is transparent
 Expands to: Constant Arguments.pf
+Declared in library Arguments, line 12, characters 11-13
 fcomp : forall {A B C : Type}, (B -> C) -> (A -> B) -> A -> C
 
 fcomp is not universe polymorphic
 Arguments fcomp {A B C}%type_scope f g x /
 The reduction tactics unfold fcomp when applied to 6 arguments
 fcomp is transparent
 Expands to: Constant Arguments.fcomp
+Declared in library Arguments, line 19, characters 11-16
 volatile : nat -> nat
 
 volatile is not universe polymorphic
 Arguments volatile / x%nat_scope
 The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Arguments.volatile
+Declared in library Arguments, line 22, characters 11-19
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
 Arguments f x y n%nat_scope v m%nat_scope
 f uses section variables T1 T2.
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
+Declared in library Arguments, line 30, characters 0-147
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
@@ -77,6 +86,7 @@ The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
+Declared in library Arguments, line 30, characters 0-147
 f : forall [T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
@@ -86,6 +96,7 @@ The reduction tactics unfold f when the 4th, 5th and
   6th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.S1.f
+Declared in library Arguments, line 30, characters 0-147
 f : forall [T1 T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
@@ -94,6 +105,7 @@ The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.f
+Declared in library Arguments, line 30, characters 0-147
      = forall v : unit, f 0 0 5 v 3 = 2
      : Prop
      = 2 = 2
@@ -106,6 +118,7 @@ The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor
 f is transparent
 Expands to: Constant Arguments.f
+Declared in library Arguments, line 30, characters 0-147
 forall w : r, w 3 true = tt
      : Prop
 File "./output/Arguments.v", line 52, characters 28-29:
@@ -124,6 +137,7 @@ The reduction tactics always unfold volatilematch
   but avoid exposing match constructs
 volatilematch is transparent
 Expands to: Constant Arguments.volatilematch
+Declared in library Arguments, line 58, characters 11-24
      = fun n : nat => volatilematch n
      : nat -> nat
 *** [ f :