@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.
This avoids the temporary files workaround on macOS and Windows, and makes sure
we can process a `#eval` command and write messages to stdout at the same time.
Consider the following example
```lean
def div!: Nat → Nat → Nat
| x, 0 => panic! "division by zero"
| x, y => x/y
def weird (x : Nat) : MetaM Nat :=
unless (x > 0) (throwOther "x == 0") *>
let y := div! 10 x;
pure y
```
If we execute `weird 0`, it produces a "division by zero" panic
message.
This is a simple version of a much bigger function in the new
frontend.
This is not due to a bug in the compiler.
It produces the panic message because of the `do`-encoding
refactoring. Recall that, a few months ago,
we started to compile `do a; b` as `a *> b` (i.e., `seqRight a b`).
Thus, the example above is
`seqRight action1 (let y := div! 10 x; pure y)`
where `action1` is the `unless ...`.
In A-normal form, this is equivalent to
```lean
let y:= div! 10 x;
let action2 := pure y;
seqRight action1 action2
```
Thus, we execute `div! 10 x` before we even execute the `seqRight`.
This is counterintuitive and demonstrates once again how impure
features such as `panic!` are dangerous.
This commit reverts the `do`-encoding refactoring, and encodes
`do a; b` as `a >>= fun _ b` as we did in Lean3.
cc @Kha
Before this commit
```lean
pattern <- action
```
was being translated by the old frontend into
```lean
pattern <- action | matchFailed
```
This produced counterintuitive behavior, and performance problems when
tryin to synthesize `MonadFail` instances.
BTW, the new frontend does not implement this feature. I didn't even
remember the old frontend did this.
I will also remove the class `MonadFail` from stdlib.
cc @Kha @dselsam
@cipher1024 I modified your fix. It would produce memory leaks if the
code executed by #eval modifies the stdout.
Here is the problem.
- Your replaces the handler with some new handler `H` and stores the
old handler `O` in a `flet`.
- Code is executed and replaces the stdout handler with `H'`. The `H`s RC is
decremented and `H'`s RC is incremeneted. So far, so good.
- Now, the destructor of your `flet` is executed, and it replaces `H'`
with `O`, but `H'` RC is not decremented.
