Stream: Elpi users & devs

Topic: Question on occurs

Louise Dubois de Prisque (Apr 07 2022 at 09:13):

Hello!

I don't understand the use of the external function occurs, as I tried it on a simple example.
The documentation says that the first argument should be a constant (so I guess either a global reference or a variable) and the error message says that the second argument should be a constant.

My code is:

Definition foo := nat -> nat.

Elpi Query lp:{{

  occurs {{nat}} {{foo}}.

}}.

and the message is : The second argument of occurs must be a constant, but foo is a constant and I don't understand why the documentation mentions the first and not the second argument.

Thanks in advance for your help

Enrico Tassi (Apr 07 2022 at 09:21):

Sorry the doc is written in the context of elpi alone, without Coq. An elpi contant is a symbol like foo while {{ nat }}, which is a Coq constant in some sense, unravels to global (indt "Coq.Init.Datatypes...") which is not a constant in the first sense.

Enrico Tassi (Apr 07 2022 at 09:23):

a not very efficient way to test what you want is

(pi x\ copy {{ nat }} x => copy T T1)

since T1 does not see x the goal fails if T did contain {{nat}}, since it was replaced by x, and hence the copied term cannot be assigned to T1.

Enrico Tassi (Apr 07 2022 at 09:26):

That can be made more efficient by writing a predicate similar to copy which does not really copy the term, but just fail if a predicate holds on any subterm, eg

pred anywhere i:(term -> prop), i:term.
anywhere P T :- P T, !, fail.
anywhere P (app L) :- forall L (anywhere P).
...

Enrico Tassi (Apr 07 2022 at 09:27):

and pass t\ t = {{ nat }} as P.

Louise Dubois de Prisque (Apr 07 2022 at 11:37):

Thank you, so I have another question. occurs is used there : https://github.com/LPCIC/coq-elpi/blob/fe9cdf7ae78f56980266cde47bae5f757c1a1739/apps/derive/elpi/projK.elpi#L47 and I don't understand exactly how this works because it seems to deal with Coq constants and not elpi ones.

And if I understood you well, occurs cannot be used to check if a specific reified Coq term occurs in another?

Enrico Tassi (Apr 07 2022 at 11:41):

This is just "an illusion" because the types are not helping. There is an invariant that the term is an elpi constant, a name in particular. See
how I fill the list in here: https://github.com/LPCIC/coq-elpi/blob/fe9cdf7ae78f56980266cde47bae5f757c1a1739/apps/derive/elpi/projK.elpi#L79

Enrico Tassi (Apr 07 2022 at 11:43):

x is an elpi constant (of type term), which one can use with occur.
Maybe my terminology in the doc of elpi is not clear, occurs works for "names", like the "x" in pi x\, sometimes these things are called eigenvariables, or nominal constants.

Enrico Tassi (Apr 07 2022 at 11:45):

The valid argument of occur is not determined by its type, but rather by its value. If the value is a constant (an atom), then it is ok. If it is a compound syntax tree, then it is not. The type of the value can by arbitrary.

Enrico Tassi (Apr 07 2022 at 11:45):

Sorry for the confusion, I'd be happy to apply any suggestion to the doc of occurs.

Louise Dubois de Prisque (Apr 07 2022 at 14:36):

Okay I understand better now! I think that the error message was confusing for me because it mentions the second argument of occurs while the doc mentions the first one, so my suggestion would be to clarify a bit this point if you can
Otherwise your documentation was clear and I just missed the meaning of eigenvariable, thank you very much !

Last updated: Oct 13 2024 at 01:02 UTC