Stream: Elpi users & devs

Topic: Definition of copy

Chantal Keller (Apr 11 2022 at 15:31):

Hi
In the definition of copy here:

• what is the predicate name in the first rule?
• what is the interest of having two ! in the first rule?
  (Just a remark: there is a typo in the initial comment l.106, a " is missing.)

Enrico Tassi (Apr 11 2022 at 18:11):

name is an Elpi builtin (not specific to Coq) so it is documented briefly here: https://github.com/LPCIC/coq-elpi/blob/master/elpi-builtin.elpi#L347 . The basic usage is to test if a term (of any type) is an eigenvariable, a name, aka a pi quantified constant.

Now that I have to explain it, I regret I wrote copy this way, but anyway, here it is.

The nicest version of copy is, for the lambda case, something like:

copy (fun N T B) (fun N T1 B1) :- copy T T1, pi x\ copy x x => copy (B x) (B1 x)

since x is a fresh constant it is introduced with a specific rule, to say to copy it to itself.

As a speedup, I did add a

copy X X.

clause, and omit the copy x x => part when I cross a binder (that is the speedup).

Unfortunately copy X X is too rough, it also applies to non atomic terms for example, so I refined it to copy X X :- name X to ensure it is only used for names like x.

Now, the last detail is that I wrote it like

copy X Y :- name X, !, X = Y, !.

this rule is operationally a bit more precise: first tests if X is a name, then commit to this rule with !, then say that X is Y, and finally take the first solution of the assignment.

About using X = Y, I think I wanted to be super sure that in case where the the input term is flexible but the user also gave an explicit second term, the behavior was OK. Imagine calling copy (A x) x, I'd like the rule for variables ("documentation" of uvar) of copy to apply (and fail), not this one. copy X X would work, set A = y\y and succeed, while I did not want this behavior (after all the first argument is an input, I should not touch it). Non linear heads, and input mode, is not exactly what one thinks.

About the last ! I don't think it is really needed now that = is a builtin (hence the user cannot add clauses for =). But in the past = was, by chance/mistake/lazyness, a regular predicate and the user was able to write more rules for it (I'm afraid not intentionally).

Well, that was a bit of a mouthful ;-)

Thanks for the typo.

Last updated: Oct 13 2024 at 01:02 UTC