Fix resolver + duplicate [elpi2html.elpi].

LPCIC · Sep 6, 2024 · 81805a2 · 81805a2
1 parent e3e2180
commit 81805a2
Show file tree

Hide file tree

Showing 8 changed files with 501 additions and 71 deletions.
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, ...