It is still broken since we apply attributes before we compile code.
Recall that attributes such as `@[export]` and `@[extern]` must be applied before we
compile code.
On the other hand, any attribute `attrName`
```
@[attrName] def foo := ...
```
which creates auxiliary definitions that depend on `foo` must be applied
AFTER we generate code for `foo`. Otherwise, we will fail to compile the
auxiliary definition since we don't have code for `foo` yet.
I will fix the issue above by allowing attributes to specify when they
should be applied. I will start with only two options: before and after
code compilation. In the future, we may need more options (e.g., before
elaboration), but I don't see the need yet.
cc @kha
Main differences with respect to `tests/playground/parser`
1- There is a single (parametric) parser type: `Parser k`, where `k` is
used to identify whether it is a `nud` or `led` parser.
2- It assumes parsing tables are stored in the `Environment`.
3- We check precedence mismatch, and use the value `none` to represent
"use existing precedence".
4- We have support for silent (aka epsilon) parsing actions.
Remark: the experiments at `tests/playground/parser` demonstrated that the new
parsing infrastructure is at least 10x faster than the one based on the
`Parsec` monad.
The implementation is good enough for implementing extensible parsers,
elaborators and tactics, but there are a few TODOs
1- We should have a better story for standalone applications.
Most of them don't need `evalConst`, and the global table is
just initialization overhead.
2- The global table introduces a dependency on the `Lean.Name`
implementation. So, all standalone applications will depend on it.
3- We are not storing arity 0 constants in the table.
This one should be easy to fix in the future.
`TagAttribute`s are implemented on top of the low level Attribute API,
and `PersistentEnvExtension`.
This is just the first attribute on a series of attributes we are
going to implement using Lean itself.
We are going to start making drastic changes in the parser,
elaborator, attributes, etc. Examples:
- No View objects. I am going to implement match_syntax.
- No RecT in the parser. I am going to implement parser extensions
using an approach similar to the one I used to implement environment
extensions.
- No Parsec. I will use an approach similar to the one used in the
experiment https://github.com/leanprover/lean4/tree/master/tests/playground/parser
It is easier to perform these changes with the new frontend disabled.
I will slowly re-active it as I apply the changes.
cc @kha
