Fix file resolution.

This includes: - Duplicating [elpi2html.elpi] and [elpi-quoted_syntax.elpi] form elpi. - Always resolving file paths by treating the first component as a Coq directory path, and the rest as a relative path from its mapping. - Require a file path argument in the [Elpi Print] command, resolved in the same way.
LPCIC · Sep 24, 2024 · e7eabff · e7eabff
1 parent 4a6e479
commit e7eabff
Show file tree

Hide file tree

Showing 30 changed files with 578 additions and 123 deletions.
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/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, ...