@Kha We currently have a few macros that create binder names
such as `x`. These macros rely on the hygienic framework. This part is
great. Before this commit we were simply erasing the macro
scopes when creating the actual binders at `Expr.lean`.
The result produced expressions that were hard to debug.
For example, consider the following scenario
1- Macro creates a few binder names using ``x <- `(x)``
2- We create a lambda expression `t` with these binder names.
3- Then, we use `lambdaTelescope t fun xs body => ...`
Now, if we trace `xs` and `body`, we get `#[x, x, ... x]` and
we can't distinguish the different `x`s in `body`.
So, it is really hard to debug anything using the traces.
This commit adds `Name.simpMacroScopes` for simplying "macro scoped"
names. Example: given `x._@.Init.Data.List.Basic._hyg.2.5`, it
produces `x.2.5`. I exported this function, and used it in the old
pretty printer.
I have considered modifying `lambdaTelescope` to make sure it creates
unused names. I think this option is bad because it introduces
overhead, and in a few places we want to preserve the binder names.
I have also considered replacing the `let x := x.eraseMacroScopes` at
`Expr.lean` with `let x := x.simpMacroScopes`. I think this option is
bad since we are destroying scoping information and will not be able
to distiguish which variables have macro scopes when processing
tactics.
Anyway, the solution in this commit is good for this week, but we
should discuss a more permanent solution next week.
@Kha I am reverting this change for now.
I understand that the "default-value" approach is bad for debugging,
and it does not produce good error messages, but at least the frontend
will not "panic" when users add a bad macro.
After we switch to the new frontend, we can have a monadic `getArg`
and `getArgs` in the Elab and Macro monads which produces an
"unexpected syntax" error message. I say we wait for the new frontend
because we will be able to write `(<- s.getArg)` inside of
expressions.
@Kha I had to do this because of the `ident` vs `Term.id` recurrent
issue. `match_syntax` fails if a `Term.id` is used at `Term.letIdDecl`
where an `ident` is expected.
We should try to remove `Term.id` in the future.
@Kha The `Name` (tactic name) approach used in Lean3 is not suitable
for Lean4. The issue is that we define tactics using macros, and in
most cases, the user doesn't even know the node id.
@Kha Patterns with nested "choice" nodes produce counterintuitive
behavior, and hard to understand errors. They only work when we have
the exact same overloads at macro definition and application time.
Here is a funky example
```
syntax [myAdd] term "++":65 term:65 : term -- overloads "++"
/- The following `macro_rules` manages to eliminate "choice" node by using the
explicitly provided node kind. -/
macro_rules [myAdd] `($a ++ $b) => `($a + $b)
check (1:Nat) ++ 2 -- works as expected
syntax "FOO!" term : term
/- Before this commit, the following pattern was accepted,
and it contained a "choice" node for `++`. It is a `myAdd` or
`HasAppend.append`.
Now, this kind of pattern is rejected since it contains a nested
"choice" -/
macro_rules `(FOO! $a ++ $b) => `($a ++ $b)
/- Before this commit, the following command worked because
it contained a "choice" node similar to the one at macro definition
time. -/
check FOO! [1, 2] ++ [2, 3]
-- Now, we have 3 overloads for "++".
syntax [myAppend] term "++":65 term:65 : term
-- The `macro_rules` fails here.
```
This commit fixes this weird behavior by disallowing "choice" nodes in
patterns.
@Kha I am adding this kind of feature to improve the user experience.
For example, the macro
```
syntax "[" ident "↦" term "]" : term
macro_rules
| `([$x ↦ $v]) => `(fun $x => $v)
```
is accepted and looks perfectly reasonable.
However, before this commit, we would get a nasty error when
elaborating
```lean
check [x ↦ x + 1]
```
