From 424772b48affc68514cd44bb968209089904cb70 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 13 Apr 2021 23:26:19 +0200
Subject: [PATCH] [serapi] New query `(Query () (LogicalPath file))`

Coq's library handling code contains an API to map "logical" paths to
"physical" paths and vice-versa, we provide a helper query

```lisp
(Query () (LogicalPath file))
```

which exposes this resolution for users, as requested in
https://github.com/cpitclaudel/alectryon/pull/25

Note that the plan for 8.14 is to expose the fully principled API that
will be introduced at https://github.com/coq/coq/pull/14059.
---
 CHANGES.md                 | 7 +++++++
 serapi/serapi_protocol.ml  | 5 +++++
 serapi/serapi_protocol.mli | 4 ++++
 3 files changed, 16 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 534f5a1f..532871b3 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,10 @@
+## Version 0.13.1:
+
+ - [serapi] New query `(Query () (LogicalPath file))` which will
+            return the logical path for a particular `.v` file
+            (@ejgallego, see also
+            https://github.com/cpitclaudel/alectryon/pull/25)
+
 ## Version 0.13.0:
 
  - [serapi] (!) support for Coq 8.13, see upstream changes; in
diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml
index c86a3e09..af78e927 100644
--- a/serapi/serapi_protocol.ml
+++ b/serapi/serapi_protocol.ml
@@ -113,6 +113,7 @@ type coq_object =
   (* | CoqRichpp    of Richpp.richpp *)
   | CoqLoc       of Loc.t
   | CoqTok       of Tok.t CAst.t list
+  | CoqDP        of Names.DirPath.t
   | CoqAst       of Vernacexpr.vernac_control
   | CoqOption    of Goptions.option_name * Goptions.option_state
   | CoqConstr    of Constr.constr
@@ -199,6 +200,7 @@ let gen_pp_obj env sigma (obj : coq_object) : Pp.t =
   (* | CoqRichpp  s    -> Pp.str (pp_richpp s) *)
   | CoqLoc    _loc  -> Pp.mt ()
   | CoqTok    toks  -> Pp.pr_sequence (fun {CAst.v = tok;_} -> Pp.str (Tok.(extract_string false tok))) toks
+  | CoqDP dp        -> Names.DirPath.print dp
   | CoqAst v        -> Ppvernac.pr_vernac v
   | CoqMInd(m,mind) -> Printmod.pr_mutual_inductive_body env m mind None
   | CoqOption (n,s) -> pp_opt n s
@@ -359,6 +361,7 @@ let prefix_pred (prefix : string) (obj : coq_object) : bool =
   | CoqPp      _    -> true
   (* | CoqRichpp  _    -> true *)
   | CoqAst     _    -> true
+  | CoqDP     _     -> true
   | CoqOption (n,_) -> Extra.is_prefix (String.concat "." n) ~prefix
   | CoqConstr _     -> true
   | CoqExpr _       -> true
@@ -407,6 +410,7 @@ type query_cmd =
   | Implicits  of string           (* XXX Print LTAC signatures (with prefix) *)
   | Unparsing  of string           (* XXX  *)
   | Definition of string
+  | LogicalPath of string
   | PNotations                     (* XXX  *)
   | ProfileData
   | Proof                          (* Return the proof object *)
@@ -589,6 +593,7 @@ let obj_query ~doc ~pstate ~env (opt : query_opt) (cmd : query_cmd) : coq_object
                                 [CoqUnparsing(up,upe,gr)]
                       with _exn -> []
                       end
+  | LogicalPath f  -> [CoqDP (Serapi_paths.dirpath_of_file f)]
   | PNotations     -> List.map (fun s -> CoqNotation s) @@ QueryUtil.query_pnotations ()
   | Definition id  -> fst (QueryUtil.info_of_id env id)
   | TypeOf id      -> snd (QueryUtil.info_of_id env id)
diff --git a/serapi/serapi_protocol.mli b/serapi/serapi_protocol.mli
index d52e488a..2a47bda1 100644
--- a/serapi/serapi_protocol.mli
+++ b/serapi/serapi_protocol.mli
@@ -183,6 +183,8 @@ type coq_object =
   (** A Coq Location object, used for positions inside the document. *)
   | CoqTok       of Tok.t CAst.t list
   (** Coq Tokens, as produced by the lexer  *)
+  | CoqDP        of Names.DirPath.t
+  (** Coq "Logical" Paths, used for module and section names *)
   | CoqAst       of Vernacexpr.vernac_control
   (** Coq Abstract Syntax tress, as produced by the parser *)
   | CoqOption    of Goptions.option_name * Goptions.option_state
@@ -340,6 +342,8 @@ type query_cmd =
   (** Return internal information for a given notation *)
   | Definition of string
   (** Return the definition for a given global *)
+  | LogicalPath of string
+  (** Returns Coq's "logical path" for a given file *)
   | PNotations                     (* XXX  *)
   (** Return a list of notations *)
   | ProfileData