@kha, the implementation is a little bit hackish. It is whitespace
sensitive to avoid `f @g`, an application with argument `@g` to be
parsed as a named pattern.
Here are other approaches I have considered:
1- In the `namedPattern`, we add a guard that ensures the pattern
is *not* an identifier. Thus, `f @g` would not be considered a valid
`namedPattern`. Drawback: we would always try to parse it as a
namedPattern first, fail, and then try as an application.
2- Enforce whitespace before application arguments. Drawback: `f(a+b)`
would not be a valid application anymore.
We are going to use a simpler approach to help users writing hygienic
macros. Suppose we have a syntax quotation such as
```
`(let x := %%a;
ite x x %%b)
```
We will parse this quotation, and during elaboration, we must create
code (i.e., an `Expr`) such that given `a` and `b`, it constructs
a (new) syntax object, and we want to guarantee that there is no accidental name capture.
So, given the syntax object `S` representing the quotation above, we
first pre-resolve the identifiers in `S`. In this step, we annotate the
identifier `ite` with the global declaration `_root_.ite`.
Then, we create a fresh identifier for each identifier, but we would
preserve the pre-resolved information.
Assume the monadic action `mkFresh <id>` creates a fresh identifier with
prefix `<id>`, and `mkFreshWithPreresolved <id> <pre-list>` creates a
fresh identifier with prefix <id> and pre-resolved list `<pre-list>`.
Then, the quotation above would be transformed into:
```
let x := mkFresh `x;
let ite := mkFreshWith `ite [`_root_.ite];
`(let %%x := %%a;
%%ite %%x %%x %%b)
```
Here, the new quotation is just syntax sugar for a sequence of `Syntax`
constructor applications. Now, whenever we want to create a syntax
object using the quotation above, we guarantee there is no accidental
name capture because we are creating a fresh identifier for all
identifiers in the quotation. Global references are preserved using the
field preresolved that we already have.
It is straightforward to implement the transformation above using a
mapping. Note that if we use the same mapping to elaborate two different
quotations, we are essentially saying they share the same scope.
For example, suppose we have
```
let c := `(ite x x %%b);
`(let x := %%a; %%c)
```
If we use the same mapping, we produce
```
let x := mkFresh `x;
let ite := mkFreshWith `ite [`_root_.ite];
let c := `(%%ite %%x %%x %%b);
`(let %%x := %%a; %%c)
```
If we create a new mapping when compiling each quotation, we get
```
let x := mkFresh `x;
let ite := mkFreshWith `ite [`_root_.ite];
let c := `(%%ite %%x %%x %%b);
let x1 := mkFresh `x;
`(let %%x1 := %%a; %%c)
```
which is probably not what the user wants.
We can provide a simple notation for users specifying which behavior
they want. The default may be super simple. Example: we have a new mapping (aka scope) per declaration.
The approach above is simple and efficient. It is also great for
users that want to create syntax objects during the elaboration phase
and want to avoid name capture.
In Lean 4, we will support the more general
`a + ·` ==> `fun x, a + x`
`· + b` ==> `fun x, x + b`
`· + ·` ==> `fun x y, x + y`
`f · y` ==> `fun x, f a y`
`g · · b` ==> `fun x y, g x y b`
It ignores error only if `p` does not consume any input. This change
improves the quality of the error messages. The previous behavior can be
obtained by using `optional (try p)`.
