HOAS for Rocq terms 

HOAS for Gallina 

Set Warnings "-elpi.linear-variable".
From elpi Require Import elpi.
[Loading ML file ppx_deriving.runtime (implicit dependency) ... done]
[Loading ML file re (implicit dependency) ... done]
[Loading ML file re.str (implicit dependency) ... done]
[Loading ML file elpi.util (implicit dependency) ... done]
[Loading ML file elpi.lexer_config (implicit dependency) ... done]
[Loading ML file menhirLib (implicit dependency) ... done]
[Loading ML file stdlib-shims (implicit dependency) ... done]
[Loading ML file elpi.parser (implicit dependency) ... done]
[Loading ML file camlp-streams (implicit dependency) ... done]
[Loading ML file easy-format (implicit dependency) ... done]
[Loading ML file biniou (implicit dependency) ... done]
[Loading ML file yojson (implicit dependency) ... done]
[Loading ML file atdgen-runtime (implicit dependency) ... done]
[Loading ML file elpi.trace.atd (implicit dependency) ... done]
[Loading ML file elpi.trace.runtime (implicit dependency) ... done]
[Loading ML file elpi.runtime (implicit dependency) ... done]
[Loading ML file elpi.compiler (implicit dependency) ... done]
[Loading ML file elpi (implicit dependency) ... done]
[Loading ML file rocq-elpi.elpi ... done]

Elpi Command tutorial_HOAS.

The full syntax of Rocq 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 Rocq. 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 Rocq's native syntax. Here we focus on the abstract syntax tree of Rocq terms.

Constructor `global`

Let's start with the gref data type (for global reference).

symb const : constant -> gref.
symb indt : inductive -> gref.
symb indc : constructor -> gref.

constant, inductive and constructor are Rocq 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).

Note

keyword builtin symbol

Starting with Elpi 3.0 symbols like const, indt and indc are declared using the keyword builtin symbol, rather than type, since they are coming from Rocq.

The coq.locate API resolves a string to a gref.

Elpi Query lp:{{

  coq.locate "nat" GRnat,
  coq.locate "S" GRs,
  coq.locate "plus" GRplus

}}.
Query assignments:
  GRnat = indt «nat»
  GRplus = const «Nat.add»
  GRs = indc «S»

The coq.env.* family of APIs lets one access the environment of well typed Rocq terms that have a global name.

Definition x := 2.
x is defined

Elpi Query lp:{{

  coq.locate "x" GR,

  % all global references have a type
  coq.env.typeof GR Ty,

  % destruct GR to obtain its constant part C
  GR = const C,

  % constants may have a body, do have a type
  coq.env.const C (some Bo) TyC

}}.
Query assignments:
  Bo = app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]
  C = «x»
  GR = const «x»
  Ty = global (indt «nat»)
  TyC = global (indt «nat»)

An expression like indt «nat» is not a Rocq term (or better a type) yet.

The global term constructor turns a gref into an actual term.

symb global : gref -> term.

Constructors `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.

symb app   : list term -> term.

Let's move to binders!

Definition f := fun x : nat => x.
f is defined

Elpi Query lp:{{

  coq.locate "f" (const C),
  coq.env.const C (some Bo) _

}}.
Query assignments:
  Bo = fun `x:r` (global (indt «nat»)) c0 \ c0
  C = «f»

The fun constructor carries a pretty printing hint `x`, the type of the bound variable nat and a function describing the body:

symb fun  : name -> term -> (term -> term) -> term.

Note

name is just for pretty printing: in spite of carrying a value in the Rocq world, it has no content in Elpi (like the unit type)

Elpi terms of type name are just identifiers written between ` (backticks).

Elpi Query lp:{{

  fun `foo` T B = fun `bar` T B    % names don't matter

}}.
Query assignments:
  B = X0
  T = X1

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`.

Constructors `fix` and `match`

The other binders prod (Rocq's forall, AKA Π) and let are similar, so let's rather focus on fix here.

Elpi Query lp:{{

  coq.locate "plus" (const C),
  coq.env.const C (some Bo) _

}}.
Query assignments:
  Bo = fix `add:r` 0 
 (prod `n:r` (global (indt «nat»)) c0 \
   prod `m:r` (global (indt «nat»)) c1 \ global (indt «nat»)) c0 \
 fun `n:r` (global (indt «nat»)) c1 \
  fun `m:r` (global (indt «nat»)) c2 \
   match c1 (fun `n:r` (global (indt «nat»)) c3 \ global (indt «nat»)) 
    [c2, 
     fun `p:r` (global (indt «nat»)) c3 \
      app [global (indc «S»), app [c0, c3, c2]]]
  C = «Nat.add»

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

symb 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 Rocq function expecting in input the arguments of the corresponding constructor. The order follows the order of the constructors in the inductive type declaration.

symb match : term -> term -> list term -> term.

The return clause is represented as a Rocq 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.
m is defined

Elpi Query lp:{{

coq.locate "m" (const C),
coq.env.const C (some (fun _ _ h\ fun _ _ p\ match _ (RT h p) _)) _,
coq.say "The return type of m is:" RT

}}.
The return type of m is: c0 \ c1 \
fun `x:r` (global (indt «nat»)) c2 \
 fun `e:r` 
  (app [global (indt «eq»), global (indt «nat»), global (indc «O»), c2]) 
  c3 \ prod `_:r` (app [c1, global (indc «O»)]) c4 \ app [c1, c2]
Query assignments:
  C = «m»
  RT = c0 \ c1 \
fun `x:r` (global (indt «nat»)) c2 \
 fun `e:r` 
  (app [global (indt «eq»), global (indt «nat»), global (indc «O»), c2]) 
  c3 \ prod `_:r` (app [c1, global (indc «O»)]) c4 \ app [c1, c2]

Constructor `sort`

The last term constructor worth discussing is sort.

symb sort  : universe -> term.
symb prop : universe.
symb 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.

Elpi Query lp:{{

  coq.sort.sup U U1,
  coq.say U "<" U1,
  % This constraint can't be allowed in the store!
  not(coq.sort.leq U1 U)

}}.
X0 < X1
Debug: Cannot enforce Top.29 <= Top.28 because Top.28 < Top.29
Query assignments:
  U = X0
  U1 = X1
Universe constraints:
UNIVERSES:
 {Top.29 Top.28} |= Top.28 < Top.29
ALGEBRAIC UNIVERSES:
 {}
FLEXIBLE UNIVERSES:
 
SORTS:
  |= Prop -> SProp
     Type -> Prop
          -> SProp
     
WEAK 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 Rocq 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:

Elpi Query lp:{{

  ID = (fun `x` (sort (typ U)) x\ x),
  A = (sort (typ U)), % the same U as before
  B = (sort (typ V)),
  coq.say "(id b) is:" (app [ID, B]),

  % error, since U : U is not valid
  coq.typecheck (app [ID, A]) T (error ErrMsg),
  coq.say "(id a) is illtyped:" ErrMsg,

  % ok, since V : U is possible
  coq.typecheck (app [ID, B]) T ok,

  % remark: U and V are now Rocq's univ with constraints
  coq.say "after typing (id b) is:" (app [ID, B]) ":" T,
  coq.univ.print

}}.
(id b) is: app [fun `x:r` (sort (typ X0)) c0 \ c0, sort (typ X1)]
(id a) is illtyped: 
Illegal application: 
The term "fun x : Type => x" of type "Type -> Type"
cannot be applied to the term
 "Type" : "Type"
This term has type "Type@{Top.30+1}" which should be a subtype of
 "Type@{Top.30}".
(universe inconsistency: Cannot enforce Top.30 < Top.30 because Top.30
= Top.30)
after typing (id b) is: 
app [fun `x:r` (sort (typ «Top.30»)) c0 \ c0, sort (typ «Top.31»)] : 
sort (typ «Top.30»)
Universe constraints: UNIVERSES:
                       {Top.31 Top.30} |= Top.31 < Top.30
                      ALGEBRAIC UNIVERSES:
                       {Top.31 Top.30}
                      FLEXIBLE UNIVERSES:
                       Top.31
                       Top.30
                      SORTS:
                        |= Prop -> SProp
                           Type -> Prop
                                -> SProp
                           
                      WEAK CONSTRAINTS:
                       
                      
Query assignments:
  A = sort (typ «Top.30»)
  B = sort (typ «Top.31»)
  ErrMsg = Illegal application: 
The term "fun x : Type => x" of type "Type -> Type"
cannot be applied to the term
 "Type" : "Type"
This term has type "Type@{Top.30+1}" which should be a subtype of
 "Type@{Top.30}".
(universe inconsistency: Cannot enforce Top.30 < Top.30 because Top.30
= Top.30)
  ID = fun `x:r` (sort (typ «Top.30»)) c0 \ c0
  T = sort (typ «Top.30»)
  U = «Top.30»
  V = «Top.31»
Universe constraints:
UNIVERSES:
 {Top.31 Top.30} |= Top.31 < Top.30
ALGEBRAIC UNIVERSES:
 {Top.31 Top.30}
FLEXIBLE UNIVERSES:
 Top.31
 Top.30
SORTS:
  |= Prop -> SProp
     Type -> Prop
          -> SProp
     
WEAK CONSTRAINTS:
 

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.

Quotations and Antiquotations 

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 Rocq parser to write terms.

The antiquotation, from Rocq to Elpi, is written lp:{{ ... }} and we have been using it since the beginning of the tutorial. The quotation from Elpi to Rocq is written {{:coq ... }} or also just {{ ... }} since the :coq is the default quotation (Rocq has no default quotation, hence you always need to write lp: there).

Elpi Query lp:{{

  % the ":coq" flag is optional
  coq.say {{:coq 1 + 2 }} "=" {{ 1 + 2 }}

}}.
app
 [global (const «Nat.add»), 
  app [global (indc «S»), global (indc «O»)], 
  app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]] 
= 
app
 [global (const «Nat.add»), 
  app [global (indc «S»), global (indc «O»)], 
  app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]]

Of course quotations can nest.

Elpi Query lp:{{

  coq.locate "S" S,
  coq.say {{ 1 + lp:{{ app[global S, {{ 0 }} ]  }}   }}
% elpi....  coq..     elpi...........  coq  elpi  coq

}}.
app
 [global (const «Nat.add»), 
  app [global (indc «S»), global (indc «O»)], 
  app [global (indc «S»), global (indc «O»)]]
Query assignments:
  S = indc «S»

One rule governs bound variables:

Important

if a variable is bound in a language, Rocq 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.

Elpi Query lp:{{

  coq.say (fun `x` {{nat}} x\ {{ fun x : nat => x + lp:{{ x }} }})
%                          e         c          c         e
}}.
fun `x:r` (global (indt «nat»)) c0 \
 fun `x:r` (global (indt «nat»)) c1 \
  app [global (const «Nat.add»), c1, c0]

A commodity quotation without parentheses let's one quote identifiers omitting the curly braces. That is lp:{{ ident }} can be written just lp:ident.

Elpi Query lp:{{

  coq.say (fun `x` {{nat}} x\ {{ fun x : nat => x + lp:x }})
%                          e         c          c      e
}}.
fun `x:r` (global (indt «nat»)) c0 \
 fun `x:r` (global (indt «nat»)) c1 \
  app [global (const «Nat.add»), c1, c0]

It is quite frequent to put Rocq variables in the scope of an Elpi unification variable, and this can be done by simply writing lp:(X a b) which is a shorthand for lp:{{ X {{ a }} {{ b }} }}.

Warning

writing lp:X a b (without parentheses) would result in a Rocq application, not an Elpi one

Let's play a bit with these shorthands:

Elpi Query lp:{{

  X = (x\y\ {{ lp:y + lp:x }}), % x and y live in Elpi

  coq.say {{ fun a b : nat => lp:(X a b) }} % a and b live in Rocq

}}.
fun `a:r` (global (indt «nat»)) c0 \
 fun `b:r` (global (indt «nat»)) c1 \
  app [global (const «Nat.add»), c1, c0]
Query assignments:
  X = c0 \ c1 \
app [global (const «Nat.add»), c1, c0]

Another commodity quotation lets one access the coqlib feature introduced in Rocq 8.10.

Rocqlib gives you an indirection between your code and the actual name of constants.

Register Corelib.Init.Datatypes.nat as my.N.
Register Corelib.Init.Logic.eq as my.eq.
Elpi Query lp:{{

  coq.say {{ fun a b : lib:my.N => lib:@my.eq lib:my.N a b }}

}}.
fun `a:r` (global (indt «nat»)) c0 \
 fun `b:r` (global (indt «nat»)) c1 \
  app [global (indt «eq»), global (indt «nat»), c0, c1]

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.

Elpi Query lp:{{

  coq.say {{:gref  nat  }},
  coq.say {{:gref  lib:my.N  }}.

}}.
indt «nat»
indt «nat»

The last thing to keep in mind when using quotations is that implicit arguments are inserted (according to the Arguments setting in Rocq) 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 (implicit arguments).

Elpi Query lp:{{

  T = (fun `ax` {{nat}} a\ {{ fun b : nat => lp:a = b }}),
  coq.say "before:" T,
  coq.typecheck T _ ok,
  coq.say "after:" T

}}.
before: 
fun `ax:r` (global (indt «nat»)) c0 \
 fun `b:r` (global (indt «nat»)) c1 \
  app [global (indt «eq»), X0 c1, c0, c1]
after: 
fun `ax:r` (global (indt «nat»)) c0 \
 fun `b:r` (global (indt «nat»)) c1 \
  app [global (indt «eq»), global (indt «nat»), c0, c1]
Query assignments:
  T = fun `ax:r` (global (indt «nat»)) c0 \
 fun `b:r` (global (indt «nat»)) c1 \
  app [global (indt «eq»), global (indt «nat»), c0, c1]
  X1_ = c0 \
global (indt «nat»)
Universe constraints:
UNIVERSES:
 {Top.33 Top.32} |= Top.33 < Top.32
                    Set <= Top.33
ALGEBRAIC UNIVERSES:
 {}
FLEXIBLE UNIVERSES:
 Top.33
SORTS:
 α6 := Type
 α7 |= α6 <-> Type
       Prop -> SProp
       Type -> α7
            -> Prop
            -> SProp
       
WEAK CONSTRAINTS:
 

The context 

The context of Elpi (the hypothetical program made of rules loaded via =>) is taken into account by the Rocq 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.

Fail Elpi Query lp:{{

  T = {{ fun x : nat => x + 1 }},
  coq.typecheck T _ ok,
  T = fun _ _ Bo,
  pi x\
    coq.typecheck (Bo x) _ _

}}.
The command has indeed failed with message:
Bound variable c0 not found in the Coq context:
Mapping from DBL:
  

Named:
  
Rel:
  
Did you forget to load some hypotheses with => ?

This fatal error says that x in (Bo x) is unknown to Rocq. 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 Rocq 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:

func decl term -> name, term.       % Var Name Ty
func def  term -> name, term, term. % Var Name Ty Bo

where def is used to cross a let.

Elpi Query lp:{{

  T = {{ fun x : nat => x + 1 }},
  coq.typecheck T _ ok,
  T = fun N Ty Bo,
  pi x\
    decl x N Ty ==>
      coq.typecheck (Bo x) _ ok

}}.
Query assignments:
  Bo = c0 \
app
 [global (const «Nat.add»), c0, 
  app [global (indc «S»), global (indc «O»)]]
  N = `x:r`
  T = fun `x:r` (global (indt «nat»)) c0 \
 app
  [global (const «Nat.add»), c0, 
   app [global (indc «S»), global (indc «O»)]]
  Ty = global (indt «nat»)

In order to ease this task, Rocq-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.

Elpi Query lp:{{

  T = {{ fun x : nat => x + 1 }},
  coq.typecheck T _ ok,
  T =  fun N Ty Bo,
  @pi-decl N Ty x\
      coq.typecheck (Bo x) _ ok

}}.
Query assignments:
  Bo = c0 \
app
 [global (const «Nat.add»), c0, 
  app [global (indc «S»), global (indc «O»)]]
  N = `x:r`
  T = fun `x:r` (global (indt «nat»)) c0 \
 app
  [global (const «Nat.add»), c0, 
   app [global (indc «S»), global (indc «O»)]]
  Ty = global (indt «nat»)

Tip

@pi-decl N Ty x\ takes arguments in the same order of fun and prod, while @pi-def N Ty Bo x\ takes arguments in the same order of let.

Holes (implicit arguments)

An "Evar" (Rocq slang for existentially quantified meta variable) is represented as a Elpi unification variable and a typing constraint.

Elpi Query lp:{{

    T = {{ _ }},
    coq.say "raw T =" T,
    coq.sigma.print,
    coq.say "--------------------------------",
    coq.typecheck T {{ nat }} ok,
    coq.sigma.print

}}.
raw T = X0

SHELF:
FUTURE GOALS STACK:
 

Rocq-Elpi mapping:
RAW:
ELAB:

--------------------------------
 evar X0 (global (indt «nat»)) X0  /* suspended on X0 */
EVARS:
 ?X11==[ |- nat] (internal placeholder) {?e0}
 ?X10==[ |- => nat] (internal placeholder)

SHELF:
FUTURE GOALS STACK:
 ?X11

Rocq-Elpi mapping:
RAW:
?X11 <-> X0 ELAB:
?X11 <-> X0 
Query assignments:
  T = X0
  X2_ = X0
Syntactic constraints:
 evar X0 (global (indt «nat»)) X0  /* suspended on X0 */
Universe constraints:
UNIVERSES:
 {Top.34} |= Set <= Top.34
ALGEBRAIC UNIVERSES:
 {}
FLEXIBLE UNIVERSES:
 
SORTS:
 α8 := Type |= α8 <-> Type
               Prop -> SProp
               Type -> Prop
                    -> SProp
               
WEAK CONSTRAINTS:
 

Before the call to coq.typecheck, coq.sigma.print prints nothing interesting, while after the call (see the output above) it also prints a syntactic constraint stating that a hole is linked to a Rocq evar and is expected to have type nat.

Now the bijective mapping from Rocq evars to Elpi's unification variables is not empty anymore, as the Rocq-Elpi mapping: line above shows.

Note that Rocq's evar identifiers are of the form ?X<n>, while the Elpi ones have no leading ?. The EVARS: line of the output above shows that Rocq's Evar map assigns that evar the type nat.

The intuition is that Rocq'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 Rocq's API, are automatically linked to a Rocq evar. We postpone the explanation of the difference "raw" and "elab" unification variables to the chapter about tactics, here the second copy of the hole variable in the evar constraint plays no role.

Now, what about the typing context?

Elpi Query lp:{{

  T = {{ fun x : nat => x + _ }},
  coq.say "raw T =" T,
  T = fun N Ty Bo,
  @pi-decl N Ty x\
      coq.typecheck (Bo x) {{ nat }} ok,
      coq.sigma.print.

}}.
raw T = 
fun `x:r` (global (indt «nat»)) c0 \
 app [global (const «Nat.add»), c0, X0 c0]
 {c0 c1} : decl c1 `x:r` (global (indt «nat»))
   ?- evar (X0 c1) (global (indt «nat»)) (X0 c1)  /* suspended on X0 */
EVARS:
 ?X13==[x |- nat] (internal placeholder) {?e0}
 ?X12==[x |- => nat] (internal placeholder)

SHELF:
FUTURE GOALS STACK:
 ?X13

Rocq-Elpi mapping:
RAW:
?X13 <-> X0 ELAB:
?X13 <-> X0 
Query assignments:
  Bo = c0 \
app [global (const «Nat.add»), c0, X0 c0]
  N = `x:r`
  T = fun `x:r` (global (indt «nat»)) c0 \
 app [global (const «Nat.add»), c0, X0 c0]
  Ty = global (indt «nat»)
  X3_ = X0
Syntactic constraints:
 {c0 c1} : decl c1 `x:r` (global (indt «nat»))
   ?- evar (X0 c1) (global (indt «nat»)) (X0 c1)  /* suspended on X0 */
Universe constraints:
UNIVERSES:
 {Top.35} |= Set <= Top.35
ALGEBRAIC UNIVERSES:
 {}
FLEXIBLE UNIVERSES:
 
SORTS:
 α9 := Type |= α9 <-> Type
               Prop -> SProp
               Type -> Prop
                    -> SProp
               
WEAK CONSTRAINTS:
 

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 X0 c0, that means that X0 sees c0 (c0 is in the scope of X0).

The constraint is this time a bit more complex: as shown above, {...} is the set of names (not necessarily minimized) used in the constraint, while ?- separates the assumptions (the context) from the conclusion (the suspended goal).

As shown by the mapping and evar-map lines of the output above, both Elpi's constraint and Rocq'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.

Outside the pattern fragment 

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 declare new variables there, etc. The programmer can freely call Rocq 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.

Fail Elpi Query lp:{{

  T = {{ fun x : nat => x + _ }},
  % remark the hole sees x
  T = fun N Ty Bo,
  % 1 is the offending term we put in place of x
  Bo1 = Bo {{ 1 }},
  % Bo1 is outside the pattern fragment
  coq.say "Bo1 (not in pattern fragment) =" Bo1,
  % boom
  coq.typecheck Bo1 {{ nat }} ok.

}}.
Bo1 (not in pattern fragment) = 
app
 [global (const «Nat.add»), 
  app [global (indc «S»), global (indc «O»)], 
  X0 (app [global (indc «S»), global (indc «O»)])]
The command has indeed failed with message:
Flexible term outside pattern fragment:
X0 (app [global (indc «S»), global (indc «O»)])

This snippet fails hard, as shown above: the term 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 Rocq extensions in Elpi, it may happen that we want to use a Rocq 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.

Elpi Query lp:{{

  T = {{ fun x : nat => x + _ }},
  T = fun N Ty Bo,
  Bo1 = Bo {{ 1 }},
  coq.say "Bo1 before =" Bo1,
  % by loading this rule in the context, we set
  % the option for the APIs called under it
  (@holes! ==> coq.typecheck Bo1 {{ nat }} ok),
  coq.say "Bo1 after =" Bo1.

}}.
Bo1 before = 
app
 [global (const «Nat.add»), 
  app [global (indc «S»), global (indc «O»)], 
  X0 (app [global (indc «S»), global (indc «O»)])]
Bo1 after = 
app
 [global (const «Nat.add»), 
  app [global (indc «S»), global (indc «O»)], X1]
Query assignments:
  Bo = c0 \
app [global (const «Nat.add»), c0, X1]
  Bo1 = app
 [global (const «Nat.add»), 
  app [global (indc «S»), global (indc «O»)], X1]
  N = `x:r`
  T = fun `x:r` (global (indt «nat»)) c0 \
 app [global (const «Nat.add»), c0, X1]
  Ty = global (indt «nat»)
  X5_ = c0 \
X1
Syntactic constraints:
 evar X1 (global (indt «nat»)) X1  /* suspended on X1 */
Universe constraints:
UNIVERSES:
 {Top.36} |= Set <= Top.36
ALGEBRAIC UNIVERSES:
 {}
FLEXIBLE UNIVERSES:
 
SORTS:
 α10 := Type |= α10 <-> Type
                Prop -> SProp
                Type -> Prop
                     -> SProp
                
WEAK CONSTRAINTS:
 

Note that after the call to coq.typecheck, the hole variable is assigned a term where the offending argument has been pruned (discarded), as shown by the Bo1 after line above.

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.
nat2bool is defined
nat2bool is now a coercion

Open Scope bool_scope.
Elpi Query lp:{{

  T = {{ fun x : nat => x && _ }},
  T = fun N Ty Bo,
  Bo1 = Bo {{ 1 }},
  coq.elaborate-skeleton Bo1 {{ bool }} Bo2 ok

}}.
Query assignments:
  Bo = c0 \
app [global (const «andb»), c0, X0 c0]
  Bo1 = app
 [global (const «andb»), app [global (indc «S»), global (indc «O»)], 
  X0 (app [global (indc «S»), global (indc «O»)])]
  Bo2 = app
 [global (const «andb»), 
  app
   [global (const «nat2bool»), 
    app [global (indc «S»), global (indc «O»)]], X1]
  N = `x:r`
  T = fun `x:r` (global (indt «nat»)) c0 \
 app [global (const «andb»), c0, X0 c0]
  Ty = global (indt «nat»)
  X6_ = X0
Syntactic constraints:
 evar X2 (global (indt «bool»)) X1  /* suspended on X2, X1 */

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 Rocq'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 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 Writing commands in Elpi or the one about Writing tactics in Elpi.