From 7e432c4e68b9df96803db5bc0536a8d63aff9a1c Mon Sep 17 00:00:00 2001 From: Philip Kaludercic Date: Sat, 21 Oct 2023 15:26:54 +0200 Subject: [PATCH 1/4] Add "coq.extra-dep" external predicate --- Changelog.md | 1 + coq-builtin.elpi | 4 ++++ src/coq_elpi_builtins.ml | 11 +++++++++++ 3 files changed, 16 insertions(+) diff --git a/Changelog.md b/Changelog.md index 39ce8a438..98d9ecfc4 100644 --- a/Changelog.md +++ b/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 diff --git a/coq-builtin.elpi b/coq-builtin.elpi index fa4f798d4..dcf503a30 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -1666,6 +1666,10 @@ 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. +% [coq.extra-dep Identifier File Name] Resolve the file name of an Extra +% Dependency +external pred coq.extra-dep i:id, o:option id. + % -- Access to Elpi's data -------------------------------------------- % clauses diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index ebb75198c..fc747d1c3 100644 --- a/src/coq_elpi_builtins.ml +++ b/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, "File Name", + Easy "Resolve the file name of an Extra Dependency")), + (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 *) From 995505a2710fe9877555a468855c25da7b1105a4 Mon Sep 17 00:00:00 2001 From: Philip Kaludercic Date: Sat, 21 Oct 2023 15:31:57 +0200 Subject: [PATCH 2/4] Implement basic tests for "coq.extra-dep" --- _CoqProject.test | 1 + tests/test_query_extra_dep.v | 7 +++++++ 2 files changed, 8 insertions(+) create mode 100644 tests/test_query_extra_dep.v diff --git a/_CoqProject.test b/_CoqProject.test index c6fa00829..ccbfd241e 100644 --- a/_CoqProject.test +++ b/_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 diff --git a/tests/test_query_extra_dep.v b/tests/test_query_extra_dep.v new file mode 100644 index 000000000..c10dded36 --- /dev/null +++ b/tests/test_query_extra_dep.v @@ -0,0 +1,7 @@ +From elpi Require Import elpi. + +From unreleased Extra Dependency "elpi_elaborator.elpi" as elab. + +Elpi Query lp:{{ coq.extra-dep "elab" _ }}. + +Fail Elpi Query lp:{{ coq.extra-dep "foo" (some _) }}. From f2038ac86d63611bfb86c1bd9906a9a8485b977a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 21 Oct 2023 23:05:19 +0100 Subject: [PATCH 3/4] improve doc --- coq-builtin.elpi | 6 ++++-- src/coq_elpi_builtins.ml | 4 ++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index dcf503a30..f0fd40a23 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -1666,8 +1666,10 @@ 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. -% [coq.extra-dep Identifier File Name] Resolve the file name of an Extra -% Dependency +% -- 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 -------------------------------------------- diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index fc747d1c3..28a45a10b 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -3888,8 +3888,8 @@ Supported attributes: MLCode(Pred("coq.extra-dep", In(id, "Identifier", - Out(option id, "File Name", - Easy "Resolve the file name of an Extra Dependency")), + 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))), From c269f48e3253026e2eac61d64a45790dc8719589 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 22 Oct 2023 14:38:49 +0100 Subject: [PATCH 4/4] fix test --- tests/test_query_extra_dep.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tests/test_query_extra_dep.v b/tests/test_query_extra_dep.v index c10dded36..32020f17c 100644 --- a/tests/test_query_extra_dep.v +++ b/tests/test_query_extra_dep.v @@ -2,6 +2,8 @@ From elpi Require Import elpi. From unreleased Extra Dependency "elpi_elaborator.elpi" as elab. -Elpi Query lp:{{ coq.extra-dep "elab" _ }}. +Elpi Command test. -Fail Elpi Query lp:{{ coq.extra-dep "foo" (some _) }}. +Elpi Query lp:{{ coq.extra-dep "elab" (some P) }}. + +Elpi Query lp:{{ coq.extra-dep "foo" none }}.