Merge pull request #525 from phikal/query-extra-dep

Add "coq.extra-dep" external predicate

Changelog.md

@@ -15,6 +15,7 @@ Requires Elpi 1.16.5 and Coq 8.18.
 - Change `coq.ltac.call-ltac1` now accepts either a string (tactic name) or
   a tactic expression (of type `ltac1-tactic`)
 - New `ltac_tactic:(...)` syntax to pass tactic expressions to Elpi tactics
+- New `coq.extra-dep` predicate
 
 ## [1.19.1] - 30/08/2023
 

_CoqProject.test

@@ -52,3 +52,4 @@ tests/test_link_order_import0.v
 tests/test_link_order_import1.v
 tests/test_link_order_import2.v
 tests/test_link_order_import3.v
+tests/test_query_extra_dep.v

coq-builtin.elpi

@@ -1666,6 +1666,12 @@ external pred coq.term->string i:term, o:string.
 % - @holes! (default: false, prints evars as _)
 external pred coq.term->pp i:term, o:coq.pp.
 
+% -- Extra Dependencies -----------------------------------------------
+
+% [coq.extra-dep Identifier FileName] Resolve the file name of an extra
+% dependency. See also Coq's From xxx Extra Dependency yyy as zzz.
+external pred coq.extra-dep i:id, o:option id.
+
 % -- Access to Elpi's data --------------------------------------------
 
 % clauses

src/coq_elpi_builtins.ml

@@ -3884,6 +3884,17 @@ Supported attributes:
      state, !: s, [])),
   DocAbove);
 
+  LPDoc "-- Extra Dependencies -----------------------------------------------";
+
+  MLCode(Pred("coq.extra-dep",
+    In(id, "Identifier",
+    Out(option id, "FileName",
+    Easy "Resolve the file name of an extra dependency. See also Coq's From xxx Extra Dependency yyy as zzz.")),
+  (fun id _ ~depth ->
+    !: (try Some (ComExtraDeps.query_extra_dep (Names.Id.of_string id))
+        with Not_found -> None))),
+  DocAbove);
+
   LPDoc "-- Access to Elpi's data --------------------------------------------";
 
    (* Self modification *)

tests/test_query_extra_dep.v

@@ -0,0 +1,9 @@
+From elpi Require Import elpi.
+
+From unreleased Extra Dependency "elpi_elaborator.elpi" as elab.
+
+Elpi Command test.
+
+Elpi Query lp:{{ coq.extra-dep "elab" (some P) }}.
+
+Elpi Query lp:{{ coq.extra-dep "foo" none }}.