api: coq.mod[ty]path->library

Author: gares

Changelog.md

@@ -1,5 +1,11 @@
 # Changelog
 
+## UNRELEASED
+
+### API
+- New `coq.modpath->library`
+- New `coq.modtypath->library`
+
 ## [1.16.0] - 10/11/2022
 
 Requires Elpi 1.16.5 and Coq 8.16.

coq-builtin.elpi

@@ -1594,6 +1594,14 @@ external pred coq.modpath->path i:modpath, o:list string.
 % component is a separate list item
 external pred coq.modtypath->path i:modtypath, o:list string.
 
+% [coq.modpath->library MP LibraryPath] extract the enclosing module which
+% can be Required
+external pred coq.modpath->library i:modpath, o:modpath.
+
+% [coq.modtypath->library MTP LibraryPath] extract the enclosing module
+% which can be Required
+external pred coq.modtypath->library i:modtypath, o:modpath.
+
 % [coq.term->string T S] prints a term T to a string S using Coq's pretty
 % printer
 % Supported attributes:

src/coq_elpi_builtins.ml

@@ -3586,6 +3586,20 @@ coq.id->name S N :- coq.string->name S N.
   (fun mtyp _ ~depth h c state -> !: (mp2path mtyp))),
   DocAbove);
 
+  MLCode(Pred("coq.modpath->library",
+    In(modpath, "MP",
+    Out(modpath, "LibraryPath",
+    Read(unit_ctx, "extract the enclosing module which can be Required"))),
+  (fun mp _ ~depth h c state -> !: ModPath.(MPfile (dp mp)))),
+  DocAbove);
+
+  MLCode(Pred("coq.modtypath->library",
+    In(modtypath, "MTP",
+    Out(modpath, "LibraryPath",
+    Read(unit_ctx, "extract the enclosing module which can be Required"))),
+  (fun mtyp _ ~depth h c state -> !: ModPath.(MPfile (dp mtyp)))),
+  DocAbove);
+
   MLCode(Pred("coq.term->string",
     CIn(failsafe_term,"T",
     Out(B.string, "S",

tests/test_API_env.v

@@ -369,3 +369,11 @@ Elpi Query lp:{{
 
 Set Printing Universes. Print Module Test.
 Check Test.f.
+
+From Coq Require Import ZArith.
+
+Elpi Query lp:{{
+  coq.locate-module "N2Z" MP,
+  coq.locate-module "Znat" LP,
+  coq.modpath->library MP LP
+}}.