In the definition of copy here:
namein the first rule?
!in the first rule?
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)
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).
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
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
Y, and finally take the first solution of the assignment.
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
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: Feb 04 2023 at 02:03 UTC