How inspect terms under binders in Elpi · Elpi users & devs

I guess this is a silly beginner question, but I don't quite understand how I would write a function which inspects the term under a binder. The Elpi term constructor for a product term is:

type prod name -> term -> (term -> term) -> term.         % forall x : t,

I don't understand how I can use the 3rd argument of type term -> term in e.g. a recursive call of a fold term function without something like a quod libet sandbox. Say I have a Coq term forall (x:False), some_term how can I look into some_term without providing a term of type False as argument to the term -> term thing?

In Ltac2 this is quite obvious. The kind constructor for a product is Prod (binder, constr) where binder is an opaque type with some functions to access the variable name and type. For the body I get a constr and I can look at it without providing an argument.

What I want to do is collect all arguments of a specific constructor in a term as list.

Enrico Tassi (Oct 26 2022 at 12:30):

There are some hints in this tutorial: https://lpcic.github.io/coq-elpi/tutorial_elpi_lang.html#higher-order-features, in particular the language gives you pi x\ and =>. The idea is that pi postulates a fresh name x, and you can pass that to the term of type term -> term in order to get the body where the bound variable was replaced a by a fresh name x.

under (app _ as T) :- coq.say T.
under (prod _ _ F) :- pi x\ under (F x).

Since x is fresh, no program clause (static clause) can mention it, so you can attach some knowledge to x via =>. Typically you would attach to x its type.

under (app _ as T) :- coq.say T.
under (prod N S F) :- pi x\ decl x N S => under (F x).

under (app _ as T) :- coq.say T.
under (prod N S F) :- @pi-decl N S x\ under (F x).

It is important to attach decl to x, since it is part of the encoding of coq terms. If you call deep under the binder the coq type checker or even the pretty printer, it would use these clauses to know how to type/print x.

Enrico Tassi (Oct 26 2022 at 12:32):

This is a really good beginner question, I hope it is somehow covered by the first tutorial. Are you following them in linear order of you started from the Coq ones? If so, I may need to add backporinters, since this way of traversing terms is really of paramount importance.

Michael Soegtrop (Oct 26 2022 at 12:52):

Thanks for the details! I followed the tutorials in linear order, but i must admit I saved the section "higher-order-features" for later and then didn't come back to it after I went through the other tutorials. So I missed the "quod libet sandbox operator" pi.

Here and there some application examples would help. E.g. the HOAS tutorial doesn't define a single predicate (afair). Also I don't think I found non trivial examples for matching on Coq terms.

Enzo Crance (Oct 26 2022 at 13:08):

I will ask a related question. Do all the local variables introduced with pi have to be given a type if the typechecker is called somewhere below?

I am usually giving a type to things that are likely to be involved in typechecking later, but I also have to quantify over some temporary variables that I eventually remove by substitution with copy. Surprisingly, when typechecking a term that has nothing to do with these temporary variables, I get a message like Bound variable c8 not found in the Coq context, suggesting that the whole Elpi context is given to Coq, and thus must be typed, even the terms that won't be used by the typechecker. Am I right? I guess it's because Elpi cannot know what will be done on the Coq side, so it gives the full context, right?

Michael Soegtrop (Oct 26 2022 at 13:09):

Require Import Ltac2.Ltac2.
Require Import Ltac2.Printf.

Ltac2 Eval match (Constr.Unsafe.kind '(fun x => S x)) with
| Constr.Unsafe.Lambda b c => printf "%t" c
| _ => printf "other"
end.

(S _UNBOUND_REL_1)
- : unit = ()

Enrico Tassi (Oct 26 2022 at 13:15):

Exactly. Also if you have a hole, then it is likely to see the whole context, including the variables which you did not type.

Enrico Tassi (Oct 26 2022 at 13:16):

it is a trade off, either the context is manually managed... or it is implicit, but in that case Elpi can't second guess you

Enzo Crance (Oct 26 2022 at 13:17):

It's ok there is still the workaround @pi-decl N (sort prop) x\ if I know variable x will not appear in typechecked terms, and has a type that is complex and that I don't want to generate
(should probably create a predicate called dummy-type or something that makes it explicit it does not matter what is put here as long as it has a valid type for Coq)

Stream: Elpi users & devs

Topic: How inspect terms under binders in Elpi

Michael Soegtrop (Oct 26 2022 at 12:13):