`derive` attribute parsing · Elpi users & devs

Stream: Elpi users & devs

Topic: `derive` attribute parsing

Gordon Stewart (Jun 26 2023 at 16:18):

The code here (https://github.com/LPCIC/coq-elpi/blob/aeb4caed4a2f86f5885bd8d7d1968d05cdfed18f/apps/derive/theories/derive.v#L68):

% runs P in a context where Coq #[attributes] are parsed
pred with-attributes i:prop.
with-attributes P :-
  attributes A,
  coq.parse-attributes A [
    att "verbose" bool,
    att "only" attmap,
    att "recursive" bool,
  ] Opts, !,
  Opts => P.

main [str I] :- !,
  coq.locate I GR,
  with-attributes (derive.main GR tt _).

main [indt-decl D] :- !,
  with-attributes (derive.decl+main D).

seems to make it difficult to pass additional attributes to derive extensions, e.g.,

#[only(my_extension), my_extension_attr(X,Y,Z)] derive T.

Is there an easy workaround that doesn't change the above code? If not, is there interest in an MR that generalizes derive attribute parsing?

Possible generalizations:

Option 1: send the entire attribute map to each extension so the extension can re-parse it
Option 2: have extensions declare their attribute grammar when they are registered with derive
Option 3: ?

Enrico Tassi (Jun 26 2023 at 21:07):

I'm OK accepting changes to that piece of code.

I'm a bit rusty so I don't know if it is easy to do, but I can imagine that each derivation foo (for which we support only(foo)) can be assumed to parse all attributes of the form foo(...).

I think parse-attributes already has an option to accept unknown attributes. Maybe that option should be refined so that one can accept all attributes from known "name spaces".

Similarly with-attributes could take an extra argument (or have a twin function) that takes a name space and parses only the attributes which belong to that name space. IIRC foo(bar) becomes "foo.bar" in the parsing code, when we append the two strings we could also filter I guess. We would then call each derivation under with-attributes-for NameSpace P.

And a derivation could specify a list of accepted attributes in its declaration clause, or in a companion one, like the one for dependencies.

Enrico Tassi (Jun 26 2023 at 21:07):

I hope this makes sense to you

Enrico Tassi (Jun 26 2023 at 21:12):

Your example would become

#[only(my_extension), my_extension(attr(X,Y,Z))] derive T.

Gordon Stewart (Jun 26 2023 at 21:15):

Yes, that makes sense. Thanks! I'll look into it, time permitting.

Enrico Tassi (Jun 26 2023 at 21:18):

The rule of thumb is that:

a misspelled attribute is not silently ignored
there is no risk of collision between attributes of different derivations.

Other than that, I'm OK with anything really.

Last updated: Oct 13 2024 at 01:02 UTC