Author: | Enrico Tassi |
---|
This tutorial focuses on the integration of Elpi within Coq, in particular it describes how Coq terms are exposed to Elpi programs and how Coq APIs can be called.
This tutorial assumes the reader is familiar with Elpi and HOAS; if it is not the case, please take a look at the Elpi tutorial first.
Contents
The full syntax of Coq terms can be found in coq-builtin.elpi together with a detailed documentation of the encoding of contexts and the APIs one can use to interact with Coq. This tutorial, and the two more that focus on commands and tactics, are a gentle introduction to all that.
We defer to later quotations and antiquotations: syntactic features that let one write terms in Coq's native syntax. Here we focus on the abstract syntax tree of Coq terms.
global
Let's start with the gref data type (for global rerence).
type const constant -> gref. type indt inductive -> gref. type indc constructor -> gref.
constant, inductive and constructor are Coq specific data types that are opaque to Elpi. Still the gref data type lets you see what these names point to (a constant, and inductive type or a constructor).
The coq.locate API resolves a string to a gref.
The coq.env.*
family of APIs lets one access the
environment of well typed Coq terms that have a global name.
Definition x := 2.
An expression like indt «nat»
is not a Coq term (or better a type) yet.
The global term constructor turns a gref into an actual term.
type global gref -> term.
app
and fun
The app term constructor takes a list of terms and builds the (n-ary) application. The first term is the head, while the others are the arguments.
For example app [global (indc «S»), global (indc «O»)]
is
the representation of 1
.
type app list term -> term.
Let's move to binders!
Definition f := fun x : nat => x.
The fun constructor carries a pretty printing hint `x`,
the type of the bound variable nat
and a function describing the body:
type fun name -> term -> (term -> term) -> term.
Note
name is just for pretty printing: in spite of carrying a value in the Coq world, it has no content in Elpi (like the unit type)
Elpi terms of type name are just identifiers written between ` (backticks).
API such as coq.name-suffix lets one craft a family of
names starting from one, eg coq.name-suffix `H` 1 N sets N
to `H1`.
fix
and match
The other binders prod (Coq's forall
, AKA Π
) and let are similar,
so let's rather focus on fix here.
The fix constructor carries a pretty printing hint,
the number of the recursive argument (starting at 0
), the type
of the recursive function and finally the body where the recursive
call is represented via a bound variable
type fix name -> int -> term -> (term -> term) -> term.
A match constructor carries the term being inspected, the return clause and a list of branches. Each branch is a Coq function expecting in input the arguments of the corresponding constructor. The order follows the order of the constructors in the inductive type declaration.
type match term -> term -> list term -> term.
The return clause is represented as a Coq function expecting in input the indexes of the inductive type, the inspected term and generating the type of the branches.
Definition m (h : 0 = 1 ) P : P 0 -> P 1 := match h as e in eq _ x return P 0 -> P x with eq_refl => fun (p : P 0) => p end.
sort
The last term constructor worth discussing is sort.
type sort universe -> term. type prop universe. type typ univ -> universe.
The opaque type univ is a universe level variable. Elpi holds a store of
constraints among these variables and provides APIs named coq.univ.*
to
impose constraints.
Note
the user is not expected to declare universe constraints by hand
The type checking primitives update the store of constraints
automatically and put Coq universe variables in place of Elpi's unification
variables (U
and V
below).
Let's play a bit more with universe constraints using the coq.typecheck API:
The diagnostic data type is used by coq.typecheck to
tell if the term is well typed. The constructor ok
signals success, while
error
carries an error message. In case of success universe constraints
are added to the store.
Writing Gallina terms as we did so far is surely possible but very verbose and unhandy. Elpi provides a system of quotations and antiquotations to let one take advantage of the Coq parser to write terms.
The antiquotation, from Coq to Elpi, is written lp:{{ ... }}
and we have
been using it since the beginning of the tutorial. The quotation from
Elpi to Coq is written {{:coq ... }}
or also just {{ ... }}
since
the :coq
is the default quotation (Coq has no default quotation, hence you always need
to write lp:
there).
Of course quotations can nest.
One rule governs bound variables:
Important
if a variable is bound in a language, Coq or Elpi, then the variable is only visible in that language (not in the other one).
The following example is horrible but proves this point. In real code you are encouraged to pick appropriate names for your variables, avoiding gratuitous (visual) clashes.
A commodity quotation without parentheses let's one quote identifiers
omitting the curly braces.
That is lp:{{ ident }}
can be written just lp:ident
.
It is quite frequent to put Coq variables in the scope of an Elpi
unification variable, and this can be done by simply writing
lp:(X a b)
which is a shorhand for lp:{{ X {{ a }} {{ b }} }}
.
Warning
writing lp:X a b
(without parentheses) would result in a
Coq application, not an Elpi one
Let's play a bit with these shorthands:
Another commodity quotation lets one access the coqlib feature introduced in Coq 8.10.
Coqlib gives you an indirection between your code and the actual name of constants.
Register Coq.Init.Datatypes.nat as my.N. Register Coq.Init.Logic.eq as my.eq.
Note
The (optional) @
in lib:@some.name
disables implicit arguments.
The {{:gref .. }}
quotation lets one build the gref data type, instead of the
term one. It supports lib:
as well.
The last thing to keep in mind when using quotations is that implicit
arguments are inserted (according to the Arguments
setting in Coq)
but not synthesized automatically.
It is the job of the type checker or elaborator to synthesize them. We shall see more on this in the section on holes.
The context of Elpi (the hypothetical program made of rules loaded
via =>
) is taken into account by the Coq APIs. In particular every time
a bound variable is crossed, the programmer must load in the context a
rule attaching to that variable a type. There are a few facilities to
do that, but let's first see what happens if one forgets it.
This fatal error says that x
in (Bo x)
is unknown to Coq.
It is
a variable postulated in Elpi, but it's type, nat
, was lost. There
is nothing wrong per se in using pi x\
as we did if we don't call Coq
APIs under it. But if we do, we have to record the type of x
somewhere.
In some sense Elpi's way of traversing a binder is similar to a Zipper. The context of Elpi must record the part of the Zipper context that is relevant for binders.
The two predicates decl and def are used for that purpose:
pred decl i:term, o:name, o:term. % Var Name Ty pred def i:term, o:name, o:term, o:term. % Var Name Ty Bo
where def
is used to cross a let
.
In order to ease this task, Coq-Elpi provides a few commodity macros such as
@pi-decl
:
macro @pi-decl N T F :- pi x\ decl x N T => F x.
Note
the precedence of lambda abstraction x\
lets you write the
following code without parentheses for F
.
An "Evar" (Coq slang for existentially quantified meta variable) is represented as a Elpi unification variable and a typing constraint.
Before the call to coq.typecheck, coq.sigma.print prints nothing interesting, while after the call it also prints the following syntactic constraint:
evar (X1) (global (indt «nat»)) (X1) /* suspended on X1 */
which indicates that the hole X1
is linked to a Coq evar
and is expected to have type nat
.
Now the bijective mapping from Coq evars to Elpi's unification variables is not empty anymore:
Coq-Elpi mapping: RAW: ?X11 <-> X1 ELAB: ?X11 <-> X1
Note that Coq's evar identifiers are of the form ?X<n>
, while the Elpi ones
have no leading ?
. The Coq Evar map says that ?X11
has type nat
:
EVARS: ?X11==[ |- nat] (internal placeholder) {?e0} ?X10==[ |- => nat] (internal placeholder) SHELF: FUTURE GOALS STACK: ?X11
The intuition is that Coq's Evar map (AKA sigma or evd), which assigns typing judgement to evars, is represented with Elpi constraints which carry the same piece of info.
Naked Elpi unification variables, when passed to Coq's API, are
automatically linked to a Coq evar. We postpone the explanation of the
difference "raw" and "elab" unification variables to the chapter about
tactics, here the second copy of X1
in the evar constraint plays
no role.
Now, what about the typing context?
In the value of raw T
we can see that the hole in x + _
, which occurs under the
binder c0\
, is represented by an Elpi unification variable X1 c0
, that
means that X1
sees c0
(c0
is in the scope of X1
).
The constraint is this time a bit more complex. Let's dissect it:
{c0 c1} : decl c1 `x` (global (indt «nat»)) ?- evar (X1 c1) (global (indt «nat»)) (X1 c1) /* suspended on X1 */
Here {...}
is the set of names (not necessarily minimized) used in the
constraint, while ?-
separates the assumptions (the context) from the
conclusion (the suspended goal).
The mapping between Coq and Elpi is:
Coq-Elpi mapping: RAW: ?X13 <-> c0 \ X1 c0 ELAB: ?X13 <-> X1
where ?X13
can be found in Coq's sigma:
EVARS: ?X13==[x |- nat] (internal placeholder) {?e0} ?X12==[x |- => nat] (internal placeholder) SHELF: FUTURE GOALS STACK: ?X13
As expected both Elpi's constraint and Coq's evar map record a context
with a variable x
(of type nat
) which is in the scope of the hole.
Unless one is writing a tactic, Elpi's constraints are just used to represent the evar map. When a term is assigned to a variable the corresponding constraint is dropped. When one is writing a tactic, things are wired up so that assigning a term to an Elpi variable representing an evar resumes a type checking goal to ensure the term has the expected type. We will explain this in detail in the tutorial about tactics.
This encoding of evars is such that the programmer does not need to care much about them: no need to carry around an assignment/typing map like the Evar map, no need to declared new variables there, etc. The programmer can freely call Coq API passing an Elpi term containing holes.
There is one limitation, though. The rest of this tutorial describes it and introduces a few APIs and options to deal with it.
The limitation is that the automatic declaration and mapping does not work in all situations. In particular it only works for Elpi unification variables which are in the pattern fragment, which mean that they are applied only to distinct names (bound variables).
This is the case for all the {{ _ }}
one writes inside quotations, for
example, but it is not hard to craft a term outside this fragment.
In particular we can use Elpi's substitution (function application) to
put an arbitrary term in place of a bound variable.
This snippet fails hard, with the following message:
Flexible term outside pattern fragment: X0 (app [global (indc «S»), global (indc «O»)])
Indeed Bo1
contains a term outside the pattern fragment,
the second argument of plus
, which is obtained by replacing
c0
with {{ 1 }}
in X0 c0
.
While programming Coq extensions in Elpi, it may happen that we want to
use a Coq term as a syntax tree (with holes) and we need to apply
substitutions to it but we don't really care about the scope of holes.
We would like these holes to stay {{ _ }}
(a fresh hole which sees the
entire context of bound variables). In some sense, we would like {{ _ }}
to be a special dummy constant, to be turned into an actual hole on the
fly when needed.
This use case is perfectly legitimate and is supported by all APIs taking terms in input thanks to the @holes! option.
Note that after the call to coq.typecheck, X0
is assigned the
term _\ X1
, that means that the offending argument has been pruned
(discarded).
Note
All APIs taking a term support the @holes! option.
In addition to the @holes! option, there is a class of APIs which can deal with terms outside the pattern fragment. These APIs take in input a term skeleton. A skeleton is not modified in place, as coq.typecheck does with its first argument, but is rather elaborated to a term related to it.
In some sense APIs taking a skeleton are more powerful, because they can modify the structure of the term, eg. insert a coercions, but are less precise, in the sense that the relation between the input and the output terms is not straightforward (it's not unification).
Coercion nat2bool n := match n with O => false | _ => true end. Open Scope bool_scope.
Here Bo2
is obtained by taking Bo1
, considering all
unification variables as holes and all {{ Type }}
levels as fresh
(the are none in this example), and running Coq's elaborator on it.
The result is a term with a similar structure (skeleton), but a coercion
is inserted to make x
fit as a boolean value, and a fresh hole X1
is
put in place of the term X0 (app [global (indc «S»), global (indc «O»)])
which is left untouched.
Skeletons and their APIs are described in more details in the tutorial on commands.
That is all for this tutorial. You can continue by reading the tutorial about commands or the one about tactics.