Elpi provides an easy-to-embed implementation of a dialect of λProlog, a programming language well suited to manipulate abstract syntax trees containing binders and unification variables.
Coq-Elpi provides a Coq plugin that lets one define new commands and tactics in
Elpi. For that purpose it provides an embedding of Coq's terms into λProlog
using the Higher-Order Abstract Syntax approach
(HOAS). It also
exports to Elpi a comprehensive set of Coq's primitives, so that one can
print a message, access the environment of theorems and data types, define a
new constant, declare implicit arguments, type classes instances, and so on.
For convenience it also provides a quotation and anti-quotation for Coq's
syntax, so that one can write {{ nat -> lp:X }}
in the middle of a λProlog
program instead of the equivalent AST
prod `_` (global (indt «Coq.Init.Datatypes.nat»)) X
.
In the short term, provide an extension language for Coq well suited to manipulate terms containing binders. One can already use Elpi to implement commands and tactics.
In addition to that Elpi extends λProlog with higher order constraints, a language feature that helps to manipulate terms containing not only binders, but also unification variables (evars, in Coq's slang). As ongoing research we are looking forward to express algorithms like higher order unification and type inference for Coq.
The simplest way is to use OPAM and type
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-elpi
The recommended user interface is VSCoq. We provide an extension for vscode in the market place, just look for Coq Elpi. The extension provides syntax hilighting for both languages even when they are nested via quotations and antiquotations.
Other editors (click to expand)
At the time of writing Proof General does not handle quotations correctly, see ProofGeneral/PG#437.
In particular Elpi Accumulate lp:{{ .... }}.
is used in tutorials to mix Coq and Elpi code
without escaping. Coq-Elpi also accepts Elpi Accumulate " .... ".
but strings part of the
Elpi code needs to be escaped. Finally, for non-tutorial material, one can always put
the code in an external file and use Elpi Accumulate File "filename".
instead.
CoqIDE does not handle quotations correctly. The installation process puts
coq-elpi.lang
in a place where CoqIDE can find it. Then you can select coq-elpi
from the menu Edit -> Preferences -> Colors
.
If you use Vim, we recommend to add the following lines to ~/.vimrc
(in addition to the ones
for elpi)
(click to expand)
"coq-elpi
autocmd FileType lprolog syn keyword coqElpiSpecial fun prod sort let match fix axiom indc indt const prop app
autocmd FileType lprolog syn cluster elpiAntiQuotation contains=elpiAntiQuotationVar,elpiAntiQuotationBound,elpiAntiQuotationTerm
autocmd FileType lprolog syn region elpiAntiQuotationTerm start=+lp:"+ end=+"+ contains=elpiQuotation,lprologVariable,coqElpiSpecial,elpiMacro,lprologSpecial
autocmd FileType lprolog syn match elpiAntiQuotationVar "lp:[A-Z_-]\+"ms=s+3
autocmd FileType lprolog syn match elpiAntiQuotationBound "lp:[a-z_-]\+"
autocmd FileType lprolog hi def link elpiAntiQuotationVar Keyword
autocmd FileType lprolog hi def link elpiAntiQuotationBound Normal
autocmd FileType lprolog hi def link coqElpiSpecial Special
Development version (click to expand)
To install the development version one can type
opam pin add coq-elpi https://github.com/LPCIC/coq-elpi.git
One can also clone this repository and type make
, but check you have
all the dependencies installed first (see coq-elpi.opam).
- The Elpi programming language is an Elpi tutorial, there is nothing Coq specific in there even if the tutorial uses Coq to step trough the various examples. If you never heard of λProlog or HOAS based languages (like Twelf or Beluga) then you are strongly encouraged to read this tutorial and have a look at λProlog's home page for additional documentation. Even if you are familiar with λProlog or HOAS it may be worth reading the last sections since they focus on Elpi specific features. Last but not least it covers common pitfalls for people with a background in functional programming and the tracing mechanisms (useful for debugging).
- Elpi's HOAS of Coq terms focuses on how Coq terms are represented in Elpi, how to inspect them and call Coq APIs under a context of binders, and finally how holes ("evars" in Coq slang) are represented. It assumes the reader is familiar with Elpi.
- Writing commands focuses on how to write commands, in particular how to store a state across calls via so called DBs and how to handled command arguments. It assumes the reader is familiar with Elpi and the HOAS of Coq terms.
- Writing tactics describes how goals and tactics are represented, how to handle tactic arguments and finally how to define tactic notations. It assumes the reader is familiar with Elpi and the HOAS of Coq terms.
- Coq-Elpi in 20 minutes video recording of a talk given at the Coq Users and Developers Workshop 2020.
- reification is the typical use case for meta programs: reading the syntax of terms into an inductive representing a sub language on which some decision procedure can be implemented
- data bases shows how Elpi programs can store data and reuse it across multiple runs
- record expansion sketches a program to unpack records in a definition: it replaces and abstraction over a records with abstractions over all of its components
- record to sigma sketches a program that de-sugars a record type to iterated sigma types
- fuzzer sketches a program to alter an inductive type while preserving its well typedness. It makes nothing useful per se, but shows how to map a term and call the type checker deep inside it.
- tactics show how to create simple tactics by using (proof) terms and the elaborator of Coq
- generalize show how to abstract subterms out (one way to skin the cat, there are many)
- record import gives short names to record projections applied to the given record instance.
- Derive shows how to obtain proved equality tests and a few extra gadgets out of inductive type declarations. See the README for the list of derivations. It comes bundled with Coq-Elpi.
- Hierarchy Builder is a Coq extension to declare hierarchies of algebraic structures.
- Namespace Emulation System implements most of the features of namespaces (on top of Coq's modules).
In order to load Coq-Elpi use From elpi Require Import elpi
.
(click to expand)
-
Elpi Command <qname>
creates command named<qname>
containing the preamble elpi-command. -
Elpi Tactic <qname>
creates a tactic<qname>
containing the preamble elpi-tactic. -
Elpi Db <dbname> <code>
creates a Db (a program that is accumulated into other programs).<code>
is the initial contents of the Db, including the type declaration of its constituting predicates. -
Elpi Program <qname> <code>
lower level primitive letting one crate a command/tactic with a custom preamble<code>
. -
Elpi Accumulate [<qname>] [<code>|File <filename>|Db <dbname>]
adds code to the current program (or<qname>
if specified). The code can be verbatim, from a file or a Db. It understands the#[skip="rex"]
and#[only="rex"]
which make the command a no op if the Coq version is matched (or not) by the given regular expression. -
Elpi Typecheck [<qname>]
typechecks the current program (or<qname>
if specified). -
Elpi Debug <string>
sets the variable<string>
, relevant for conditional clause compilation (the:if VARIABLE
clause attribute). -
Elpi Trace [[<start> <stop>] <predicate-filter>*|Off]
enable/disable tracing, eventually limiting it to a specific range of execution steps or predicate names. -
Elpi Bound Steps <number>
limits the number of steps an Elpi program can make. -
Elpi Print <qname> [<string> <filter>*]
prints the program<qname>
to an HTML file named<qname>.html
(or<string>
if provided filtering out clauses whose file/clause name matches<filter>
.
where:
<qname>
is a qualified Coq name, e.g.derive.eq
ormy_program
.<dbname>
is like<qname>
but lives in a different namespace. By convention<dbname>
ends in.db
, e.g.derive.eq.db
.<code>
is verbatim Elpi code, eitherlp:{{ ... }}
or" ... "
(in the latter case, strings delimiters need to be escaped following Coq rules, e.g.lp:{{ coq.say "hello!" }}
becomes" coq.say ""hello!"" "
).<filename>
is a string containing the path of an external file, e.g."this_file.elpi"
.<start>
and<stop>
are numbers, e.g.17 24
.<predicate-filter>
is a regexp against which the predicate name is matched, e.g."derive.*"
.
(click to expand)
-
Elpi <qname> <argument>*.
invokes themain
predicate of the<qname>
program passing a possible empty list of arguments. This is how you invoke a command. -
elpi <qname> <argument>*.
invokes thesolve
predicate of the<qname>
program passing a possible empty list of arguments and the current goal. This is how you invoke a tactic. -
Elpi Export <qname>
makes it possible to invoke command<qname>
without theElpi
prefix or invoke tactic<qname>
in the middle of a term just writing<qname> args
instead ofltac:(elpi <qname> args)
. Note that in the case of tactics, all arguments are considered to be terms. Moreover, remember that one can useTactic Notation
to give the tactic a better syntax and a shorter name when used in the middle of a proof script.
where <argument>
can be:
- a number, e.g.
3
, represented in Elpi as(int 3)
- a string, e.g.
"foo"
orbar.baz
, represented in Elpi as(str "foo")
and(str "bar.baz")
. Coq keywords and symbols are recognized as strings, eg=>
requires no quotes. Quotes are necessary if the string contains a space or a character that is not accepted for qualified identifiers or if the string isDefinition
,Axiom
,Record
,Structure
,Inductive
,CoInductive
,Variant
orContext
. - a term, e.g.
(3)
or(f x)
, represented in Elpi as(trm ...)
. Note that terms always require parentheses, that is3
is a number while(3)
is a Coq term and depending on the context could be a natural number (i.e.S (S (S O))
) or aZ
or ... See also the section Terms as arguments down below, and the syntax for Ltac variables down below.
Commands also accept the following arguments (the syntax is as close as possible
to the Coq one: [...] means optional, * means 0 or more). See the argument
data type in coq-builtin.elpi
for their HOAS encoding. See also the section
Terms as arguments down below.
Definition
name binder* [:
term]:=
termAxiom
name:
term- [
Record
|Structure
] name binder* [:
sort]:=
[name]{
name:
term;
*}
- [
Inductive
|CoInductive
|Variant
] name binder* [|
binder] [:
term]:=
|
name binder:
term * Context
binder*
Tactics also accept Ltac variables as follows:
ltac_string:(v)
(forv
of typestring
orident
)ltac_int:(v)
(forv
of typeint
orinteger
)ltac_term:(v)
(forv
of typeconstr
oropen_constr
oruconstr
orhyp
)ltac_(string|int|term)_list:(v)
(forv
of typelist
of ...)ltac_attributes:(v)
(forv
of typeattributes
) For example:
Tactic Notation "tac" string(X) ident(Y) int(Z) hyp(T) constr_list(L) :=
elpi tac ltac_string:(X) ltac_string:(Y) ltac_int:(Z) ltac_term:(T) ltac_term_list:(L).
lets one write tac "a" b 3 H t1 t2 t3
in any Ltac context.
Arguments are first interpreted by Ltac according to the types declared
in the tactic notation and then injected in the corresponding Elpi argument.
For example H
must be an existing hypothesis, since it is typed with
the hyp
Ltac type, but in Elpi it will appear as a term, eg trm c0
.
Similarly t1
, t2
and t3
are checked to be well typed and to contain no
unresolved implicit arguments, since this is what the constr
Ltac type means
If they were typed as open_constr
or uconstr
, the last or both checks would
be respectively skipped. In any case they are passed to the Elpi code as trm ...
.
Both "a"
and b
are passed to Elpi as str ...
.
Finally, ltac_term:(T)
and (T)
are synonyms, but the former is preferred
when defining tactic notations.
Attributes are supported in both commands and tactics. Examples:
#[ att ] Elpi cmd
#[ att ] cmd
for a commandcmd
exported viaElpi Export cmd
#[ att ] elpi tac
Tactic Notation ... attributes(A) ... := ltac_attributes:(A) elpi tac
. Due to a parsing conflict in Coq grammar, at the time of writing this code:has the following limitation:Tactic Notation "#[" attributes(A) "]" "tac" := ltac_attributes:(A) elpi tac.
#[ att ] tac.
does not parse(#[ att ] tac).
worksidtac; #[ att ] tac.
works
Terms passed to Elpi commands code via (term)
or via a declaration (like Record
,
Inductive
...) are in raw format. Notations are unfolded, implicit arguments are
expanded (holes _
are added) and lexical analysis is performed (global names and
bound names are identified, holes are applied to bound names in scope).
Type checking/inference is not performed: the coq.typecheck
or coq.elaborate-skeleton
APIs can be used to fill in implicit arguments and
insert coercions.
Terms passed to Elpi tactics via tactic notations can be forced to be elaborated
beforehand by declaring the parameters to be of type constr
or open_constr
.
Arguments of type uconstr
are passed raw.
Elpi Query [<qname>] <code>
runs<code>
in the current program (or in<qname>
if specified).elpi query [<qname>] <string> <argument>*
runs the<string>
predicate (that must have the same signature of the default predicatesolve
).
- coq-builtin documents the HOAS encoding of Coq terms and the API to access Coq
- elpi-buitin documents Elpi's standard library, you may look here for list processing code
- coq-lib provides some utilities to manipulate Coq terms; it is an addendum to coq-builtin
- elpi-command-template provides the pre-loaded code for
Elpi Command
- elpi-tactic-template provides the pre-loaded code for
Elpi Tactic
The code of the Coq plugin is at the root of the repository in the src, elpi and theories directories.
The apps directory contains client applications written in Coq-Elpi.