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.
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
under (app _ as T) :- coq.say T. under (prod _ _ F) :- pi x\ under (F x).
x is fresh, no program clause (static clause) can mention it, so you can attach some knowledge to
=>. 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).
This is so common that there is a macro
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
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
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.
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"
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.
But all in all the tutorial is very good, understandable and to the point.
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?
Btw.: In Ltac2 the bound term is pretty printed as follows:
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 = ()
I guess it's because Elpi cannot know what will be done on the Coq side, so it gives the full context, right?
Exactly. Also if you have a hole, then it is likely to see the whole context, including the variables which you did not type.
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
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)
Last updated: Jun 06 2023 at 23:01 UTC