Add a table of strings/warnings associated to a module or declaration.

vernac/docstring.ml

@@ -0,0 +1,120 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(*i*)
+open Names
+open Globnames
+open Libobject
+(*i*)
+
+type docstring_key =
+  | ModPathDocstring of ModPath.t
+  | GlobRefDocstring of GlobRef.t
+
+let subst_docstring_key subst = function
+  | ModPathDocstring mp -> ModPathDocstring (Mod_subst.subst_mp subst mp)
+  | GlobRefDocstring gr -> GlobRefDocstring (fst (subst_global subst gr))
+
+let _eq_docstring_key k1 k2 =
+  match k1, k2 with
+  | ModPathDocstring mp1, ModPathDocstring mp2 -> ModPath.equal mp1 mp2
+  | GlobRefDocstring gr1, GlobRefDocstring gr2 -> Environ.QGlobRef.equal (Global.env ()) gr1 gr2
+  | (ModPathDocstring _ | GlobRefDocstring _), _ -> false
+
+let string_of_docstring_key = function
+  | ModPathDocstring mp -> DirPath.to_string (Nametab.dirpath_of_module mp)
+  | GlobRefDocstring gr -> Libnames.string_of_path (Nametab.path_of_global gr)
+
+module DocstringKind =
+  struct
+    type t = docstring_key
+    let compare = Stdlib.compare
+  end
+
+type docstring_kind = Warning | Deprecation of string option | Comment
+
+type docstring_info = {
+  comment : string;
+  kind : docstring_kind;
+}
+
+module DocstringMap = Map.Make(DocstringKind)
+
+let docstring_table =
+  Summary.ref (DocstringMap.empty : docstring_info list DocstringMap.t) ~name:"docstring-table"
+
+let cache_docstring (_, k, m) =
+  let l = try DocstringMap.find k !docstring_table with Not_found -> [] in
+  docstring_table := DocstringMap.add k (m::l) !docstring_table
+
+let load_docstring _ x =
+  cache_docstring x
+
+let open_docstring _ _ = ()
+
+let subst_docstring (subst, (local, k, m)) =
+  (local, subst_docstring_key subst k, m)
+
+let discharge_docstring (local, k, m as x) =
+  if local then None else Some x
+
+let classify_docstring (local, _, _) =
+  if local then Dispose else Substitute
+
+type docstring = bool * docstring_key * docstring_info
+
+let inDocstring : docstring -> obj =
+  declare_object
+    { (default_object "DOC-STRINGS") with
+      cache_function = cache_docstring;
+      load_function = load_docstring;
+      open_function = simple_open ~cat:Hints.hint_cat open_docstring;
+      classify_function = classify_docstring;
+      discharge_function = discharge_docstring;
+      subst_function = subst_docstring }
+
+let declare_docstring_modpath mp info =
+  Lib.add_leaf (inDocstring (false,ModPathDocstring mp,info))
+
+let declare_docstring gr info =
+  let local = isVarRef gr && Lib.is_in_section gr in
+  Lib.add_leaf (inDocstring (local,GlobRefDocstring gr,info))
+
+let warn_docstring_info =
+  let warnings = ref CString.Map.empty in
+  let pp s = Pp.str s in
+  let info_cat = CWarnings.create_category ~name:"info" () in
+  fun ?loc (k,s) ->
+    let name = string_of_docstring_key k in
+    let w =
+      match CString.Map.find_opt name !warnings with
+      | Some w -> w
+      | None ->
+        let w = CWarnings.create ~category:info_cat ~name:("info-" ^ name) pp in
+        warnings := CString.Map.add name w !warnings;
+        w
+    in
+    w ?loc s
+
+let warn_docstring_deprecated =
+  (* TODO: create a warning specifically for this library?? *)
+  Deprecation.create_warning ~object_name:"Library" ~warning_name_if_no_since:"deprecated-libraries"
+    (fun k -> Pp.str (string_of_docstring_key k))
+
+let get_warnings_modpath mp =
+  try DocstringMap.find (ModPathDocstring mp) !docstring_table
+  with Not_found -> []
+
+let output_warnings_modpath mp =
+  let l = get_warnings_modpath mp in
+  List.iter (function
+      | {kind=Warning; comment} -> warn_docstring_info (ModPathDocstring mp, comment)
+      | {kind=Deprecation since; comment} -> warn_docstring_deprecated (ModPathDocstring mp, { since ; note = Some comment })
+      | {kind=Comment; comment} -> ()) l

vernac/docstring.mli

@@ -0,0 +1,23 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+type docstring_kind = Warning | Deprecation of string option | Comment
+
+type docstring_info = {
+  comment : string;
+  kind : docstring_kind;
+}
+
+val declare_docstring_modpath : ModPath.t -> docstring_info -> unit
+val declare_docstring : GlobRef.t -> docstring_info -> unit
+
+val output_warnings_modpath : ModPath.t -> unit