Merge pull request #684 from rlepigre/resolver

Always resolve files using Coq
LPCIC · Sep 24, 2024 · 62407f0 · 62407f0
2 parents 3564cc9 + a591517
commit 62407f0
Show file tree

Hide file tree

Showing 33 changed files with 590 additions and 124 deletions.
diff --git a/Changelog.md b/Changelog.md
@@ -1,3 +1,14 @@
+# Development version
+
+### Build system
+- Support dune workspace build with `elpi`
+
+### Misc
+- Resolve `.elpi` files based on Coq's resolver. Paths are now expected to be
+  of the form `<coq_dir_path>/<rel_path>`, where `<coq_dir_path>` part is a
+  logical Coq directory (as mapped with `-Q` or `-R`), and `<rel_path>` is a
+  relative path from the corresponding directory.
+
 # [2.2.3] - 30/07/2024
 
 Requires Elpi 1.19.2 and Coq 8.19 or Coq 8.20.

diff --git a/Makefile b/Makefile
@@ -44,7 +44,7 @@ doc: build
 			-R $(shell pwd)/_build/install/default/lib/coq/user-contrib/elpi_elpi elpi_elpi \
 			-R $(shell pwd)/_build/install/default/lib/coq/user-contrib/elpi elpi \
 			$(tut) &&) true
-	@cp stlc.html doc/
+	@cp _build/default/examples/stlc.html doc/
 	@cp etc/tracer.png doc/
 
 clean:

diff --git a/apps/derive/tests/test_derive.v b/apps/derive/tests/test_derive.v
@@ -68,7 +68,7 @@ Redirect "tmp" Check list_eqb_refl.
 (* ---------------------------------------------------- *)
 
 Require Vector.
-Elpi Print derive.
+Elpi Print derive "elpi.apps.derive.tests/derive".
 #[only(eqOK), verbose] derive nat.
 Module Vector.
 derive Vector.t.

diff --git a/apps/derive/tests/test_param1.v b/apps/derive/tests/test_param1.v
@@ -172,7 +172,7 @@ Definition upair : Set := unit * unit.
 Elpi derive.param1 upair.
 Definition uplist := list upair.
 Elpi derive.param1 uplist.
-Elpi Print derive.param1.
+Elpi Print derive.param1 "elpi.apps.derive.tests/derive.param1".
 #[warning="-non-recursive"]
 Fixpoint bar (pl : uplist) (id : unit) : option unit := None unit.
 Elpi derive.param1 bar.

diff --git a/apps/tc/examples/tutorial.v b/apps/tc/examples/tutorial.v
@@ -55,7 +55,7 @@ Section Foo.
           context
   *)
 
-  Elpi Print TC.Solver.
+  Elpi Print TC.Solver "elpi.apps.tc.examples/TC.Solver".
 End Foo.
 
 (* 
@@ -89,7 +89,7 @@ Module Backtrack.
 
   Goal A 3. Fail apply _. Abort.
 
-  Elpi Print TC.Solver.
+  Elpi Print TC.Solver "elpi.apps.tc.examples/TC.Solver".
 End Backtrack.
 
 TC.Print_instances.

diff --git a/apps/tc/tests/WIP/premisesSort/sort2.v b/apps/tc/tests/WIP/premisesSort/sort2.v
@@ -26,7 +26,7 @@ Elpi AddAllInstances.
 
 Elpi TC Solver Override TC.Solver All.
 
-Elpi Print TC.Solver.
+Elpi Print TC.Solver "elpi.apps.tc.tests/TC.Solver".
 Goal C bool.
   apply _.
-Qed.
+Qed.
diff --git a/dune-workspace b/dune-workspace
diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi
@@ -6,7 +6,7 @@ shorten std.{fatal-error, fatal-error-w-data, debug-print, unsafe-cast}.
 shorten std.{rev, map, append, appendR, map2, forall-ok, take, do-ok!, lift-ok}.
 shorten std.{ omap, take-last, intersperse, map-ok, string.concat }.
 
-accumulate elpi/coq-lib-common.
+accumulate elpi_elpi/coq-lib-common.
 
 :before "stop:begin"
 stop S :- get-option "ltac:fail" N, !, coq.ltac.fail N S.

diff --git a/elpi/elpi-command-template-synterp.elpi b/elpi/elpi-command-template-synterp.elpi
@@ -2,4 +2,4 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
-accumulate elpi/coq-lib-common.
+accumulate elpi_elpi/coq-lib-common.
diff --git a/elpi/elpi-command-template.elpi b/elpi/elpi-command-template.elpi
@@ -2,7 +2,7 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
-accumulate elpi/coq-lib.  % basic term manipulation routines
-accumulate elpi/elpi-reduction.    % whd, hd-beta, ...
-accumulate elpi/elpi-ltac.         % refine, or, thenl, ...
+accumulate elpi_elpi/coq-lib.  % basic term manipulation routines
+accumulate elpi_elpi/elpi-reduction.    % whd, hd-beta, ...
+accumulate elpi_elpi/elpi-ltac.         % refine, or, thenl, ...
 
diff --git a/elpi/elpi-quoted_syntax.elpi b/elpi/elpi-quoted_syntax.elpi
@@ -0,0 +1,26 @@
+/* elpi: embedded lambda prolog interpreter                                  */
+/* license: GNU Lesser General Public License Version 2.1 or later           */
+/* ------------------------------------------------------------------------- */
+
+% HOAS for elpi programs
+
+kind term type.
+
+type app list term -> term.
+type lam (term -> term) -> term.
+type const string -> term.
+
+type cdata ctype "cdata" -> term. % int, string, float.. see also $is_cdata
+
+type arg (term -> term) -> term.  % only to bind the args of a clause
+
+kind clause type.
+type clause (ctype "Loc.t") -> list string -> term -> clause.
+
+% a program is then a list of clause while
+% the query is just one item of the same kind.
+
+% see elpi-checker.elpi for an example
+
+% vim: set ft=lprolog:
+
diff --git a/elpi/elpi-tactic-template.elpi b/elpi/elpi-tactic-template.elpi
@@ -2,11 +2,11 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
-accumulate elpi/coq-lib.  % basic term manipulation routines
-accumulate elpi/elpi-reduction.    % whd, hd-beta, ...
+accumulate elpi_elpi/coq-lib.  % basic term manipulation routines
+accumulate elpi_elpi/elpi-reduction.    % whd, hd-beta, ...
 
 % Since the elaborator written in Elpi is not ready, we fallback to the Coq one
 % accumulate engine/elaborator.   % of, unify
-accumulate elpi/coq-elaborator.
+accumulate elpi_elpi/coq-elaborator.
 
-accumulate elpi/elpi-ltac.           % refine, or, thenl, ...
+accumulate elpi_elpi/elpi-ltac.           % refine, or, thenl, ...