Janno (Feb 21 2024 at 13:49): Janno (Feb 21 2024 at 13:49):It would be very useful if derive extensions could accept extra attributes. AFAICT the current code turns #[only(foo(custom_attr=value))] into get-option foo.custom_attr value and looks for a derive extensions of the name foo.custom_attr. I am not sure what the best way would be to fix that. Ideally extensions could register their own attribute parsing but even a stupid post-processing step to gather a.X and a.Y into a single a with a map value and keys X, Y would already enable this to work I think.
Gordon Stewart (Feb 21 2024 at 14:10):Agreed here. Supporting derivation-specific extra attributes would be very useful.
Enrico Tassi (Feb 21 2024 at 16:53):Here your new attribute modifier: https://github.com/LPCIC/coq-elpi/pull/601 (not battle tested). This lets one declare "only" as an attlabel, that is only(x(bla..)) is parsed as only(x), x.bla..`. It should be backward compatible with attmap for what derive does.
In addition to that you need to replace the code that hardcodes a list of attributes with something like std.findall (att-declaration _) L0, std.map L0 (x\r\x = att-declaration r) L, attributes A, coq.parse-attributes A L and have plugins accumulate add-declaration (att "finite.my_option" string).
Last updated: Oct 13 2024 at 01:02 UTC